packages feed

holmes 0.2.0.0 → 0.3.0.0

raw patch · 18 files changed

+367/−128 lines, 18 files

Files

README.lhs view
@@ -351,7 +351,7 @@  `Watson` knows `Holmes`' methods, and can apply them to compute results. Unlike `Holmes`, however, `Watson` is built on top of `ST` rather than `IO`, and is-thus is a much purer soul.+thus a much purer soul.  Users can import `Control.Monad.Watson` and use the equivalent `satisfying` and `whenever` functions to return results _without_ the `IO` wrapper, thus making
README.md view
@@ -351,7 +351,7 @@  `Watson` knows `Holmes`' methods, and can apply them to compute results. Unlike `Holmes`, however, `Watson` is built on top of `ST` rather than `IO`, and is-thus is a much purer soul.+thus a much purer soul.  Users can import `Control.Monad.Watson` and use the equivalent `satisfying` and `whenever` functions to return results _without_ the `IO` wrapper, thus making
examples/WaveFunctionCollapse.hs view
@@ -9,7 +9,7 @@ import Data.Function ((&)) import Data.Hashable (Hashable) import Data.Holmes-import Data.JoinSemilattice.Intersect (fromList, singleton, toList)+import Data.JoinSemilattice.Intersect (fromList, toList) import Data.List (transpose) import Data.List.Split (chunksOf) import Data.Maybe (isJust, mapMaybe)@@ -93,16 +93,16 @@     and'       [ -- As we're trying to draw an island, we'll surround the whole map with         -- water:-        all' (.== lift (singleton Water)) (head rows)-      , all' (.== lift (singleton Water)) (last rows)+        all' (.== lift Water) (head rows)+      , all' (.== lift Water) (last rows) -      , all' (.== lift (singleton Water)) (head columns)-      , all' (.== lift (singleton Water)) (last columns)+      , all' (.== lift Water) (head columns)+      , all' (.== lift Water) (last columns)          -- To generate more interesting maps, we'll require that every valid         -- map contains at least one tree (and thus has at least one 5 × 5         -- island).-      , any' (.== lift (singleton Tree)) board+      , any' (.== lift Tree) board          -- For each tile, find the valid surrounding tiles, then constraint its         -- neighbours to those possibilities.
holmes.cabal view
@@ -11,7 +11,7 @@ name:               holmes description:        A reference library for constraint-solving with propagators and CDCL. synopsis:           Tools and combinators for solving constraint problems.-version:            0.2.0.0+version:            0.3.0.0  library   exposed-modules: Control.Monad.Cell.Class@@ -30,6 +30,7 @@                , Data.JoinSemilattice.Class.FlatMapping                , Data.JoinSemilattice.Class.Fractional                , Data.JoinSemilattice.Class.Integral+               , Data.JoinSemilattice.Class.Lifting                , Data.JoinSemilattice.Class.Mapping                , Data.JoinSemilattice.Class.Merge                , Data.JoinSemilattice.Class.Ord
src/Control/Monad/Holmes.hs view
@@ -6,6 +6,7 @@ {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE CPP #-}  {-| Module      : Control.Monad.Holmes@@ -36,6 +37,9 @@   , whenever   ) where +#if __GLASGOW_HASKELL__ == 806+import Control.Monad.Fail (MonadFail, fail)+#endif import Control.Monad.Cell.Class (MonadCell (..)) import Control.Monad.IO.Class (MonadIO (..)) import qualified Control.Monad.Cell.Class as Cell@@ -43,7 +47,7 @@ import qualified Control.Monad.MoriarT as MoriarT import Data.Coerce (coerce) import Data.Input.Config (Config (..))-import Data.JoinSemilattice.Class.Eq (EqR)+import Data.JoinSemilattice.Class.Eq (EqR (..)) import Data.JoinSemilattice.Class.Merge (Merge) import Data.Kind (Type) import Data.Propagator (Prop)@@ -117,8 +121,16 @@  -- | Given an input configuration, and a predicate on those input variables, -- return the __first__ configuration that satisfies the predicate.-satisfying :: (EqR x b, Typeable x) => Config Holmes x -> (forall m. MonadCell m => [ Prop m x ] -> Prop m b) -> IO (Maybe [ x ])-satisfying (coerce -> config :: Config (MoriarT IO) x) f = MoriarT.runOne (MoriarT.solve config f)+satisfying+  :: ( EqC f x+     , EqR f+     , Typeable x+     )+  => Config Holmes (f x)+  -> (forall m. MonadCell m => [ Prop m (f x) ] -> Prop m (f Bool))+  -> IO (Maybe [ f x ])+satisfying (coerce -> config :: Config (MoriarT IO) x) f+  = MoriarT.runOne (MoriarT.solve config f)  -- | Shuffle the refinements in a configuration. If we make a configuration -- like @100 `from` [1 .. 10]@, the first configuration will be one hundred @1@@@ -137,5 +149,13 @@ -- return __all configurations__ that satisfy the predicate. It should be noted -- that there's nothing lazy about this; if your problem has a lot of -- solutions, or your search space is very big, you'll be waiting a long time!-whenever :: (EqR x b, Typeable x) => Config Holmes x -> (forall m. MonadCell m => [ Prop m x ] -> Prop m b) -> IO [[ x ]]-whenever (coerce -> config :: Config (MoriarT IO) x) f = MoriarT.runAll (MoriarT.solve config f)+whenever+  :: ( EqC f x+     , EqR f+     , Typeable x+     )+  => Config Holmes (f x)+  -> (forall m. MonadCell m => [ Prop m (f x) ] -> Prop m (f Bool))+  -> IO [[ f x ]]+whenever (coerce -> config :: Config (MoriarT IO) x) f+  = MoriarT.runAll (MoriarT.solve config f)
src/Control/Monad/MoriarT.hs view
@@ -186,7 +186,15 @@ -- | Given an input configuration, and a predicate on those input variables, -- compute the configurations that satisfy the predicate. This result (or these -- results) can be extracted using 'runOne' or 'runAll'.-solve :: (PrimMonad m, EqR x b, Merge x, Typeable x) => Config (MoriarT m) x -> (forall f. MonadCell f => [ Prop f x ] -> Prop f b) -> MoriarT m [ x ]+solve+  :: ( PrimMonad m+     , EqR f+     , Merge (f x)+     , Typeable x+     )+  => Config (MoriarT m) (f x)+  -> (forall m'. MonadCell m' => [ Prop m' (f x) ] -> Prop m' (f Bool))+  -> MoriarT m [ f x ] solve Config{..} predicate = do   inputs <- traverse Cell.fill initial   output <- Prop.down (predicate (map Prop.up inputs))
src/Control/Monad/Watson.hs view
@@ -4,6 +4,7 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE CPP #-}  {-| Module      : Control.Monad.Watson@@ -30,6 +31,9 @@   , whenever   ) where +#if __GLASGOW_HASKELL__ == 806+import Control.Monad.Fail (MonadFail, fail)+#endif import Control.Monad.ST (ST, runST) import Control.Monad.Cell.Class (MonadCell (..)) import qualified Control.Monad.Cell.Class as Cell@@ -37,7 +41,7 @@ import qualified Control.Monad.MoriarT as MoriarT import Data.Coerce (coerce) import Data.Input.Config (Config (..))-import Data.JoinSemilattice.Class.Eq (EqR)+import Data.JoinSemilattice.Class.Eq (EqR (..)) import Data.JoinSemilattice.Class.Merge (Merge) import Data.Kind (Type) import Data.Propagator (Prop)@@ -109,12 +113,28 @@  -- | Given an input configuration, and a predicate on those input variables, -- return the __first__ configuration that satisfies the predicate.-satisfying :: (EqR x b, Typeable x) => (forall h. Config (Watson h) x) -> (forall m. MonadCell m => [ Prop m x ] -> Prop m b) -> Maybe [ x ]-satisfying config f = runST (MoriarT.runOne (MoriarT.solve (coerce config) f))+satisfying+  :: ( EqC f x+     , EqR f+     , Typeable x+     )+  => (forall h. Config (Watson h) (f x))+  -> (forall m. MonadCell m => [ Prop m (f x) ] -> Prop m (f Bool))+  -> Maybe [ f x ]+satisfying config f+  = runST (MoriarT.runOne (MoriarT.solve (coerce config) f))  -- | Given an input configuration, and a predicate on those input variables, -- return __all configurations__ that satisfy the predicate. It should be noted -- that there's nothing lazy about this; if your problem has a lot of -- solutions, or your search space is very big, you'll be waiting a long time!-whenever :: (EqR x b, Typeable x) => (forall h. Config (Watson h) x) -> (forall m. MonadCell m => [ Prop m x ] -> Prop m b) -> [[ x ]]-whenever config f = runST (MoriarT.runAll (MoriarT.solve (coerce config) f))+whenever+  :: ( EqC f x+     , EqR f+     , Typeable x+     )+  => (forall h. Config (Watson h) (f x))+  -> (forall m. MonadCell m => [ Prop m (f x) ] -> Prop m (f Bool))+  -> [[ f x ]]+whenever config f+  = runST (MoriarT.runAll (MoriarT.solve (coerce config) f))
src/Data/JoinSemilattice/Class/Boolean.hs view
@@ -24,23 +24,24 @@ -- tell you that the /output/ of @x && y@ is 'True', you can tell me what the -- inputs are, even if your computer can't. The implementations of 'BooleanR' -- should be such that all directions of inference are considered.-class Merge x => BooleanR (x :: Type) where+class Merge (f Bool) => BooleanR (f :: Type -> Type) where+   -- | An overloaded 'False' value.-  falseR :: x+  falseR :: f Bool    -- | An overloaded 'True' value.-  trueR :: x+  trueR :: f Bool    -- | A relationship between a boolean value and its opposite.-  notR :: ( x, x ) -> ( x, x )+  notR :: ( f Bool, f Bool ) -> ( f Bool, f Bool )    -- | A relationship between two boolean values and their conjunction.-  andR :: ( x, x, x ) -> ( x, x, x )+  andR :: ( f Bool, f Bool, f Bool ) -> ( f Bool, f Bool, f Bool )    -- | A relationship between two boolean values and their disjunction.-  orR :: ( x, x, x ) -> ( x, x, x )+  orR :: ( f Bool, f Bool, f Bool ) -> ( f Bool, f Bool, f Bool ) -instance BooleanR (Defined Bool) where+instance BooleanR Defined where   falseR = Exactly False   trueR  = Exactly True @@ -70,7 +71,7 @@       , liftA2 (||) x y       ) -instance BooleanR (Intersect Bool) where+instance BooleanR Intersect where   falseR = Intersect.singleton False   trueR  = Intersect.singleton True
src/Data/JoinSemilattice/Class/Eq.hs view
@@ -2,6 +2,10 @@ {-# LANGUAGE KindSignatures #-} {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE MultiWayIf #-}+{-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE UndecidableSuperClasses #-}  {-| Module      : Data.JoinSemilattice.Class.Eq@@ -12,26 +16,48 @@ module Data.JoinSemilattice.Class.Eq where  import Control.Applicative (liftA2)-import Data.Hashable (Hashable) import Data.JoinSemilattice.Class.Boolean (BooleanR (..)) import Data.JoinSemilattice.Class.Merge (Merge) import Data.JoinSemilattice.Defined (Defined (..))-import Data.JoinSemilattice.Intersect (Intersect (..))+import Data.JoinSemilattice.Intersect (Intersect (..), Intersectable) import qualified Data.JoinSemilattice.Intersect as Intersect-import Data.Kind (Type)+import Data.Kind (Constraint, Type) +class EqC f x => EqC' f x+instance EqC f x => EqC' f x+ -- | Equality between two variables as a relationship between them and their -- result. The hope here is that, if we learn the output before the inputs, we -- can often "work backwards" to learn something about them. If we know the -- result is exactly /true/, for example, we can effectively then -- 'Control.Monad.Cell.Class.unify' the two input cells, as we know that their -- values will always be the same.-class (BooleanR b, Merge x) => EqR (x :: Type) (b :: Type) | x -> b where-  eqR :: ( x, x, b ) -> ( x, x, b )+--+-- The class constraints are a bit ugly here, and it's something I'm hoping I+-- can tidy up down the line. The idea is that, previously, our class was+-- defined as:+--+-- @+--   class EqR (x :: Type) (b :: Type) | x -> b where+--     eqR :: (x -> x -> b) -> (x -> x -> b)+-- @+--+-- The problem here was that, if we said @x .== x :: Prop m (Defined Bool)@, we+-- couldn't even infer that the type of @x@ was @Defined@-wrapped, which made+-- the overloaded literals, for example, largely pointless.+--+-- To fix it, the class was rewritten to parameterise the wrapper type, which+-- means we can always make this inference. However, the constraints got a bit+-- grizzly when I hacked it together.+class (forall x. EqC' f x => Merge (f x), BooleanR f)+    => EqR (f :: Type -> Type) where+  type EqC f :: Type -> Constraint +  eqR :: EqC' f x => ( f x, f x, f Bool ) -> ( f x, f x, f Bool )+ -- | A relationship between two variables and the result of a not-equals -- comparison between them.-neR :: EqR x b => ( x, x, b ) -> ( x, x, b )+neR :: (EqR f, EqC' f x) => ( f x, f x, f Bool ) -> ( f x, f x, f Bool ) neR ( x, y, z )   = let ( notZ', _ ) = notR ( mempty, z )         ( x', y', notZR ) = eqR ( x, y, notZ' )@@ -39,15 +65,18 @@      in ( x', y', z' ) -instance Eq x => EqR (Defined x) (Defined Bool) where+instance EqR Defined where+  type EqC Defined = Eq+   eqR ( x, y, z )     = ( if z == trueR then y else mempty       , if z == trueR then x else mempty       , liftA2 (==) x y       ) -instance (Bounded x, Enum x, Ord x, Hashable x)-    => EqR (Intersect x) (Intersect Bool) where+instance EqR Intersect where+  type EqC Intersect = Intersectable+   eqR ( x, y, z )     = ( if | z == trueR                           -> y            | z == falseR && Intersect.size y == 1 -> Intersect.except y
+ src/Data/JoinSemilattice/Class/Lifting.hs view
@@ -0,0 +1,31 @@+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE KindSignatures #-}++{-|+Module      : Data.JoinSemilattice.Class.Lifting+Description : Lifting values into parameter types.+Copyright   : (c) Tom Harding, 2020+License     : MIT+-}+module Data.JoinSemilattice.Class.Lifting where++import Data.Hashable (Hashable)+import Data.JoinSemilattice.Defined (Defined (..))+import Data.JoinSemilattice.Intersect (Intersect)+import qualified Data.JoinSemilattice.Intersect as Intersect+import Data.Kind (Constraint, Type)++-- | Embed a regular value inside a parameter type.+class Lifting (f :: Type -> Type) (c :: Type -> Constraint) | f -> c where+  lift' :: c x => x -> f x++class Trivial (x :: Type)+instance Trivial x++instance Lifting Defined Trivial where+  lift' = Exactly++instance Lifting Intersect Hashable where+  lift' = Intersect.singleton
src/Data/JoinSemilattice/Class/Ord.hs view
@@ -1,7 +1,8 @@ {-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE FunctionalDependencies #-}-{-# LANGUAGE KindSignatures #-} {-# LANGUAGE MultiWayIf #-}+{-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-}  {-| Module      : Data.JoinSemilattice.Class.Ord@@ -12,31 +13,34 @@ module Data.JoinSemilattice.Class.Ord where  import Control.Applicative (liftA2)-import Data.Hashable (Hashable) import Data.JoinSemilattice.Defined (Defined (..))-import Data.JoinSemilattice.Intersect (Intersect (..))+import Data.JoinSemilattice.Intersect (Intersect (..), Intersectable) import qualified Data.JoinSemilattice.Intersect as Intersect import Data.JoinSemilattice.Class.Boolean (BooleanR (..))-import Data.JoinSemilattice.Class.Eq (EqR)-import Data.Kind (Type)+import Data.JoinSemilattice.Class.Eq (EqR (..), EqC')+import Data.Kind (Constraint, Type)  -- | Comparison relationships between two values and their comparison result.-class EqR x b => OrdR (x :: Type) (b :: Type) | x -> b where+-- See 'Data.JoinSemilattice.Class.Eq.EqR' for more information on the design+-- of this class, and a full apology for the constraints involved.+class (EqR f, forall x. OrdC f x => EqC' f x) => OrdR (f :: Type -> Type) where+  type OrdC f :: Type -> Constraint+  type OrdC f = EqC f    -- | A relationship between two values and whether the left is less than or   -- equal to the right.-  lteR :: ( x, x, b ) -> ( x, x, b )+  lteR :: OrdC f x => ( f x, f x, f Bool ) -> ( f x, f x, f Bool )  -- | Comparison between two values and their '(>)' result.-gtR :: OrdR x b => ( x, x, b ) -> ( x, x, b )+gtR :: (OrdR f, OrdC f x) => ( f x, f x, f Bool ) -> ( f x, f x, f Bool ) gtR ( x, y, z ) = let ( y', x', z' ) = ltR ( y, x, z ) in ( x', y', z' )  -- | Comparison between two values and their '(>=)' result.-gteR :: OrdR x b => ( x, x, b ) -> ( x, x, b )+gteR :: (OrdR f, OrdC f x) => ( f x, f x, f Bool ) -> ( f x, f x, f Bool ) gteR ( x, y, z ) = let ( y', x', z' ) = lteR ( y, x, z ) in ( x', y', z' )  -- | Comparison between two values and their '(<)' result.-ltR :: OrdR x b => ( x, x, b ) -> ( x, x, b )+ltR :: (OrdR f, OrdC f x) => ( f x, f x, f Bool ) -> ( f x, f x, f Bool ) ltR ( x, y, z )   = let ( notZ', _ ) = notR ( mempty, z )         ( x', y', notZR ) = gteR ( x, y, notZ' )@@ -44,11 +48,17 @@      in ( x', y', z' ) -instance Ord x => OrdR (Defined x) (Defined Bool) where+instance OrdR Defined where+  type OrdC Defined = Ord+   lteR ( x, y, _ ) = ( mempty, mempty, liftA2 (<=) x y ) -instance (Bounded x, Enum x, Hashable x, Ord x)-    => OrdR (Intersect x) (Intersect Bool) where+class (Ord x, Intersectable x) => OrdIntersectable (x :: Type)+instance (Ord x, Intersectable x) => OrdIntersectable x++instance OrdR Intersect where+  type OrdC Intersect = OrdIntersectable+   lteR ( x, y, z )     = ( if | z == trueR  -> Intersect.filter (<= maximum y) x            | z == falseR -> Intersect.filter ( > minimum y) x
src/Data/Propagator.hs view
@@ -30,7 +30,7 @@    , (.&&), all', allWithIndex', and'   , (.||), any', anyWithIndex', or'-  , false, not', true+  , false, not', true, exactly, choose    , (.==), (./=), distinct @@ -54,6 +54,7 @@ import Data.JoinSemilattice.Class.FlatMapping (FlatMapping (..)) import Data.JoinSemilattice.Class.Fractional (FractionalR (..), divideR, multiplyR, recipR) import Data.JoinSemilattice.Class.Integral (IntegralR (..), divR, modR, timesR)+import Data.JoinSemilattice.Class.Lifting (Lifting (..)) import Data.JoinSemilattice.Class.Mapping (Mapping (..)) import Data.JoinSemilattice.Class.Merge (Merge) import Data.JoinSemilattice.Class.Ord (OrdR (..), gtR, gteR, ltR)@@ -132,10 +133,8 @@     f x y z     pure z --- | Lift a regular value into a propagator network. This is analogous to--- 'pure' for some 'Applicative' type.-lift :: MonadCell m => x -> Prop m x-lift = Nullary . Cell.fill+lift :: forall f m c x. (MonadCell m, c x) => Lifting f c => x -> Prop m (f x)+lift = Nullary . fill . lift'  -- | Lift a regular function into a propagator network. The function is lifted -- into a relationship with one-way information flow.@@ -164,7 +163,7 @@ -- values. -- -- It's a lot of words, but the intuition is, "'(&&)' over propagators".-(.&&) :: BooleanR b => Prop m b -> Prop m b -> Prop m b+(.&&) :: BooleanR f => Prop m (f Bool) -> Prop m (f Bool) -> Prop m (f Bool) (.&&) = Binary (Cell.binary andR)  infixr 3 .&&@@ -174,7 +173,7 @@ -- focus on the conjunction of all these values. -- -- In other words, "'all' over propagators".-all' :: (BooleanR b, MonadCell m) => (x -> Prop m b) -> [ x ] -> Prop m b+all' :: (BooleanR f, MonadCell m) => (x -> Prop m (f Bool)) -> [ x ] -> Prop m (f Bool) all' f = and' . map f  -- | The same as the 'all'' function, but with access to the index of the@@ -182,14 +181,14 @@ -- each element to /other/ elements within the array. -- -- /For example, cells "surrounding" the current cell in a conceptual "board"./-allWithIndex' :: (BooleanR b, MonadCell m) => (Int -> x -> Prop m b) -> [ x ] -> Prop m b+allWithIndex' :: (BooleanR f, MonadCell m) => (Int -> x -> Prop m (f Bool)) -> [ x ] -> Prop m (f Bool) allWithIndex' f = all' (uncurry f) . zip [0 ..]  -- | Given a list of propagator networks with a focus on boolean values, create -- a new network with a focus on the conjugation of all these values. -- -- In other words, "'and' over propagators".-and' :: (BooleanR b, MonadCell m) => [ Prop m b ] -> Prop m b+and' :: (BooleanR f, MonadCell m) => [ Prop m (f Bool) ] -> Prop m (f Bool) and' = foldr (.&&) true  -- | Run a predicate on all values in a list, producing a list of propagator@@ -197,7 +196,7 @@ -- focus on the disjunction of all these values. -- -- In other words, "'any' over propagators".-any' :: (BooleanR b, MonadCell m) => (x -> Prop m b) -> [ x ] -> Prop m b+any' :: (BooleanR f, MonadCell m) => (x -> Prop m (f Bool)) -> [ x ] -> Prop m (f Bool) any' f = or' . map f  -- | The same as the 'any'' function, but with access to the index of the@@ -205,37 +204,59 @@ -- each element to /other/ elements within the array. -- -- /For example, cells "surrounding" the current cell in a conceptual "board"./-anyWithIndex' :: (BooleanR b, MonadCell m) => (Int -> x -> Prop m b) -> [ x ] -> Prop m b+anyWithIndex' :: (BooleanR f, MonadCell m) => (Int -> x -> Prop m (f Bool)) -> [ x ] -> Prop m (f Bool) anyWithIndex' f = any' (uncurry f) . zip [0 ..] +-- | Asserts that exactly n of the elements must match the given predicate.+exactly :: (BooleanR f, MonadCell m) => Int -> (x -> Prop m (f Bool)) -> [x] -> Prop m (f Bool)+exactly n f xs = +    let l = length xs+        choices = choose l n+        applyChoice picks = zipWith (\pick x -> if pick then f x else not' (f x)) picks xs+    in or' (map (and'.applyChoice) choices)++-- | Utility function that calculates all possible ways to pick k values out of n.+-- It returns a list of picks, where each pick contains a boolean indicating whether+-- that value was picked+choose :: Int -> Int -> [[Bool]]+choose n k = +  if k<0 || k>n+    then []+    else+      if n==0+        then [[]]+        else+          map (False:) (choose (pred n) k) +++          map (True:)  (choose (pred n) (pred k))+ -- | Different parameter types come with different representations for 'Bool'. -- This value is a propagator network with a focus on a polymorphic "falsey" -- value.-false :: (BooleanR b, MonadCell m) => Prop m b+false :: (BooleanR f, MonadCell m) => Prop m (f Bool) false = Nullary (Cell.fill falseR)  -- | Given a propagator network with a focus on a boolean value, produce a -- network with a focus on its negation. -- -- ... It's "'not' over propagators".-not' :: (BooleanR b, MonadCell m) => Prop m b -> Prop m b +not' :: (BooleanR f, MonadCell m) => Prop m (f Bool) -> Prop m (f Bool)  not' = Unary (Cell.unary notR)  -- | Given a list of propagator networks with a focus on boolean values, create -- a new network with a focus on the disjunction of all these values. -- -- In other words, "'or' over propagators".-or' :: (BooleanR b, MonadCell m) => [ Prop m b ] -> Prop m b +or' :: (BooleanR f, MonadCell m) => [ Prop m (f Bool) ] -> Prop m (f Bool) or' = foldr (.||) false  -- | Different parameter types come with different representations for 'Bool'. -- This value is a propagator network with a focus on a polymorphic "truthy" -- value.-true :: (BooleanR b, MonadCell m) => Prop m b+true :: (BooleanR f, MonadCell m) => Prop m (f Bool) true = Nullary (Cell.fill trueR)  -- | Calculate the disjunction of two boolean propagator network values.-(.||) :: BooleanR b => Prop m b -> Prop m b -> Prop m b+(.||) :: BooleanR f => Prop m (f Bool) -> Prop m (f Bool) -> Prop m (f Bool) (.||) = Binary (Cell.binary orR)  infixr 2 .||@@ -244,7 +265,7 @@ -- result of testing the two for equality. -- -- In other words, "it's '(==)' for propagators".-(.==) :: (EqR x b, MonadCell m) => Prop m x -> Prop m x -> Prop m b+(.==) :: (EqR f, EqC f x, MonadCell m) => Prop m (f x) -> Prop m (f x) -> Prop m (f Bool) (.==) = Binary (Cell.binary eqR)  infix 4 .==@@ -253,7 +274,7 @@ -- result of testing the two for inequality. -- -- In other words, "it's '(/=)' for propagators".-(./=) :: (EqR x b, MonadCell m) => Prop m x -> Prop m x -> Prop m b+(./=) :: (EqR f, EqC f x, MonadCell m) => Prop m (f x) -> Prop m (f x) -> Prop m (f Bool) (./=) = Binary (Cell.binary neR)  infix 4 ./=@@ -263,7 +284,7 @@ -- every propagator network's focus is different to the others. -- -- /Are all the values in this list distinct?/-distinct :: (EqR x b, MonadCell m) => [ Prop m x ] -> Prop m b+distinct :: (EqR f, EqC f x, MonadCell m) => [ Prop m (f x) ] -> Prop m (f Bool) distinct = \case   x : xs -> all' (./= x) xs .&& distinct xs   [    ] -> Nullary (Cell.fill trueR)@@ -272,7 +293,7 @@ -- whether the first network's focus be greater than the second. -- -- In other words, "it's '(>)' for propagators".-(.>) :: (OrdR x b, MonadCell m) => Prop m x -> Prop m x -> Prop m b+(.>) :: (OrdR f, OrdC f x, MonadCell m) => Prop m (f x) -> Prop m (f x) -> Prop m (f Bool) (.>) = Binary (Cell.binary gtR)  infix 4 .>@@ -281,7 +302,7 @@ -- whether the first network's focus be greater than or equal to the second. -- -- In other words, "it's '(>=)' for propagators".-(.>=) :: (OrdR x b, MonadCell m) => Prop m x -> Prop m x -> Prop m b+(.>=) :: (OrdR f, OrdC f x, MonadCell m) => Prop m (f x) -> Prop m (f x) -> Prop m (f Bool) (.>=) = Binary (Cell.binary gteR)  infix 4 .>=@@ -290,7 +311,7 @@ -- whether the first network's focus be less than the second. -- -- In other words, "it's '(<)' for propagators".-(.<) :: (OrdR x b, MonadCell m) => Prop m x -> Prop m x -> Prop m b+(.<) :: (OrdR f, OrdC f x, MonadCell m) => Prop m (f x) -> Prop m (f x) -> Prop m (f Bool) (.<) = Binary (Cell.binary ltR)  infix 4 .<@@ -299,7 +320,7 @@ -- whether the first network's focus be less than or equal to the second. -- -- In other words, "it's '(<=)' for propagators".-(.<=) :: (OrdR x b, MonadCell m) => Prop m x -> Prop m x -> Prop m b+(.<=) :: (OrdR f, OrdC f x, MonadCell m) => Prop m (f x) -> Prop m (f x) -> Prop m (f Bool) (.<=) = Binary (Cell.binary lteR)  infix 4 .<=
test/Test/Data/JoinSemilattice/Class/Boolean.hs view
@@ -9,13 +9,13 @@ import Hedgehog import qualified Hedgehog.Gen as Gen -bool :: BooleanR x => Gen x+bool :: BooleanR f => Gen (f Bool) bool = Gen.element [ trueR, falseR ] -booleanR_andR :: forall x. (BooleanR x, Eq x, Show x) => Property+booleanR_andR :: forall f. (BooleanR f, Eq (f Bool), Show (f Bool)) => Property booleanR_andR = property do-  (a :: x) <- forAll bool-  (b :: x) <- forAll bool+  a :: f Bool <- forAll bool+  b :: f Bool <- forAll bool    let ( _, _, c ) = andR ( a, b, mempty )   annotateShow c@@ -28,10 +28,10 @@   annotateShow b'   b' <> b === b -booleanR_deMorgan_and :: forall x. (BooleanR x, Eq x, Show x) => Property+booleanR_deMorgan_and :: forall f. (BooleanR f, Eq (f Bool), Show (f Bool)) => Property booleanR_deMorgan_and = property do-  (a :: x) <- forAll bool-  (b :: x) <- forAll bool+  a :: f Bool <- forAll bool+  b :: f Bool <- forAll bool    let ( _, _, c ) = andR ( a, b, mempty )       ( _, a' ) = notR ( a, mempty )@@ -41,10 +41,10 @@    c === d -booleanR_deMorgan_or :: forall x. (BooleanR x, Eq x, Show x) => Property+booleanR_deMorgan_or :: forall f. (BooleanR f, Eq (f Bool), Show (f Bool)) => Property booleanR_deMorgan_or = property do-  (a :: x) <- forAll bool-  (b :: x) <- forAll bool+  a :: f Bool <- forAll bool+  b :: f Bool <- forAll bool    let ( _, _, c ) = orR ( a, b, mempty )       ( _, a' ) = notR ( a, mempty )@@ -54,10 +54,10 @@    c === d -booleanR_orR :: forall x. (BooleanR x, Eq x, Show x) => Property+booleanR_orR :: forall f. (BooleanR f, Eq (f Bool), Show (f Bool)) => Property booleanR_orR = property do-  (a :: x) <- forAll bool-  (b :: x) <- forAll bool+  a :: f Bool <- forAll bool+  b :: f Bool <- forAll bool    let ( _, _, c ) = orR ( a, b, mempty )   annotateShow c@@ -70,9 +70,9 @@   annotateShow b'   b' <> b === b -booleanR_notR :: forall x. (BooleanR x, Eq x, Show x) => Property+booleanR_notR :: forall f. (BooleanR f, Eq (f Bool), Show (f Bool)) => Property booleanR_notR = property do-  (a :: x) <- forAll bool+  a :: f Bool <- forAll bool    let ( _, b ) = notR ( a, mempty )   annotateShow b
test/Test/Data/JoinSemilattice/Class/Eq.hs view
@@ -8,7 +8,16 @@ import Data.Holmes (BooleanR (..), EqR (..), neR) import Hedgehog -eqR_eqR :: (EqR x b, Show b, Eq x, Show x) => Gen x -> Property+eqR_eqR+  :: ( EqC f x+     , EqR f+     , Eq (f x)+     , Eq (f Bool)+     , Show (f x)+     , Show (f Bool)+     )+  => Gen (f x)+  -> Property eqR_eqR gen = property do   a <- forAll gen   b <- forAll gen@@ -24,7 +33,16 @@   annotateShow b'   b' <> b === b -eqR_negation :: (EqR x b, Show b, Eq b, Eq x, Show x) => Gen x -> Property+eqR_negation+  :: ( EqC f x+     , EqR f+     , Eq (f x)+     , Eq (f Bool)+     , Show (f x)+     , Show (f Bool)+     )+  => Gen (f x)+  -> Property eqR_negation gen = property do   a <- forAll gen   b <- forAll gen@@ -38,14 +56,32 @@   let ( _, c' ) = notR ( c, mempty )   c' === d -eqR_reflexivity :: (EqR x b, Show b, Eq b, Show x) => Gen x -> Property+eqR_reflexivity+  :: ( EqC f x+     , EqR f+     , Eq (f x)+     , Eq (f Bool)+     , Show (f x)+     , Show (f Bool)+     )+  => Gen (f x)+  -> Property eqR_reflexivity gen = property do   a <- forAll gen    let ( _, _, c ) = eqR ( a, a, mempty )   c <> trueR === trueR -eqR_symmetry :: (EqR x b, Eq b, Show b, Show x) => Gen x -> Property+eqR_symmetry+  :: ( EqC f x+     , EqR f+     , Eq (f x)+     , Eq (f Bool)+     , Show (f x)+     , Show (f Bool)+     )+  => Gen (f x)+  -> Property eqR_symmetry gen = property do   a <- forAll gen   b <- forAll gen
test/Test/Data/JoinSemilattice/Class/Ord.hs view
@@ -8,7 +8,16 @@ import Data.Holmes (BooleanR (..), OrdR (..)) import Hedgehog -ordR_lteR :: (OrdR x b, Show b, Eq x, Show x) => Gen x -> Property+ordR_lteR+  :: ( OrdR f+     , OrdC f x+     , Eq (f x)+     , Eq (f Bool)+     , Show (f x)+     , Show (f Bool)+     )+  => Gen (f x)+  -> Property ordR_lteR gen = property do   a <- forAll gen   b <- forAll gen@@ -24,7 +33,15 @@   annotateShow b'   b' <> b === b -ordR_symmetry :: (OrdR x b, Eq b, Eq x, Show x) => Gen x -> Property+ordR_symmetry+  :: ( OrdR f+     , OrdC f x+     , Eq (f x)+     , Eq (f Bool)+     , Show (f x)+     )+  => Gen (f x)+  -> Property ordR_symmetry gen = property do   a <- forAll gen   b <- forAll gen
test/Test/Data/JoinSemilattice/Defined.hs view
@@ -78,19 +78,19 @@   z === Exactly (x && y)  hprop_booleanR_andR :: Property-hprop_booleanR_andR = BooleanR.booleanR_andR @(Defined Bool)+hprop_booleanR_andR = BooleanR.booleanR_andR @Defined  hprop_booleanR_deMorgan_and :: Property-hprop_booleanR_deMorgan_and = BooleanR.booleanR_deMorgan_and @(Defined Bool)+hprop_booleanR_deMorgan_and = BooleanR.booleanR_deMorgan_and @Defined  hprop_booleanR_deMorgan_or :: Property-hprop_booleanR_deMorgan_or = BooleanR.booleanR_deMorgan_or @(Defined Bool)+hprop_booleanR_deMorgan_or = BooleanR.booleanR_deMorgan_or @Defined  hprop_booleanR_notR :: Property-hprop_booleanR_notR = BooleanR.booleanR_notR @(Defined Bool)+hprop_booleanR_notR = BooleanR.booleanR_notR @Defined  hprop_booleanR_orR :: Property-hprop_booleanR_orR = BooleanR.booleanR_orR @(Defined Bool)+hprop_booleanR_orR = BooleanR.booleanR_orR @Defined  hprop_eqR_simple :: Property hprop_eqR_simple = property do
test/Test/Data/JoinSemilattice/Intersect.hs view
@@ -54,23 +54,23 @@   x <- forAll Gen.bool   y <- forAll Gen.bool -  let ( _, _, z ) = andR ( Exactly x, Exactly y, mempty )-  z === Exactly (x && y)+  let ( _, _, z ) = andR ( Intersect.singleton x, Intersect.singleton y, mempty )+  z === Intersect.singleton (x && y)  hprop_booleanR_andR :: Property-hprop_booleanR_andR = BooleanR.booleanR_andR @(Defined Bool)+hprop_booleanR_andR = BooleanR.booleanR_andR @Intersect  hprop_booleanR_deMorgan_and :: Property-hprop_booleanR_deMorgan_and = BooleanR.booleanR_deMorgan_and @(Defined Bool)+hprop_booleanR_deMorgan_and = BooleanR.booleanR_deMorgan_and @Intersect  hprop_booleanR_deMorgan_or :: Property-hprop_booleanR_deMorgan_or = BooleanR.booleanR_deMorgan_or @(Defined Bool)+hprop_booleanR_deMorgan_or = BooleanR.booleanR_deMorgan_or @Intersect  hprop_booleanR_notR :: Property-hprop_booleanR_notR = BooleanR.booleanR_notR @(Defined Bool)+hprop_booleanR_notR = BooleanR.booleanR_notR @Intersect  hprop_booleanR_orR :: Property-hprop_booleanR_orR = BooleanR.booleanR_orR @(Defined Bool)+hprop_booleanR_orR = BooleanR.booleanR_orR @Intersect  hprop_eqR_simple :: Property hprop_eqR_simple = property do
test/Test/Data/Propagator.hs view
@@ -8,39 +8,41 @@ import Hedgehog import qualified Hedgehog.Gen as Gen import qualified Hedgehog.Range as Range+import Data.List (nub) import Prelude hiding (read) import Test.Control.Monad.Cell.Class (Lestrade, read, scotlandYardSays)-import Test.Data.JoinSemilattice.Defined (defined_int)  hprop_eqR_reflexivity :: Property hprop_eqR_reflexivity = property do-  x <- forAll defined_int+  x <- forAll (Gen.int (Range.linear 0 10))    let program :: Lestrade h ()       program = Prop.down (Prop.lift x .== Prop.lift x)             >>= \o -> Cell.write o (Exactly True)    if scotlandYardSays program == Nothing-    then x === Conflict+    then failure     else success  hprop_eqR_negation :: Property hprop_eqR_negation = property do-  x <- forAll defined_int-  y <- forAll defined_int+  x <- forAll (Gen.int (Range.linear 0 10))+  y <- forAll (Gen.int (Range.linear 0 10))    let this :: Lestrade h ()-      this = Prop.down (Prop.lift x .== Prop.lift y) >>= \o -> Cell.write o (Exactly True)+      this = Prop.down (Prop.lift x .== Prop.lift y)+         >>= \o -> Cell.write o (Exactly True)        that :: Lestrade h ()-      that = Prop.down (Prop.lift x ./= Prop.lift y) >>= \o -> Cell.write o (Exactly False)+      that = Prop.down (Prop.lift x ./= Prop.lift y)+         >>= \o -> Cell.write o (Exactly False)    scotlandYardSays this === scotlandYardSays that  hprop_eqR_simple :: Property hprop_eqR_simple = property do-  (Exactly -> x) <- forAll (Gen.int (Range.linear 0 10))-  (Exactly -> y) <- forAll (Gen.int (Range.linear 0 10))+  x <- forAll (Gen.int (Range.linear 0 10))+  y <- forAll (Gen.int (Range.linear 0 10))    let program :: Lestrade h (Defined Bool)       program = Prop.down (Prop.lift x .== Prop.lift y) >>= read@@ -49,8 +51,8 @@  hprop_eqR_symmetry :: Property hprop_eqR_symmetry = property do-  x <- forAll defined_int-  y <- forAll defined_int+  x <- forAll (Gen.int (Range.linear 0 10))+  y <- forAll (Gen.int (Range.linear 0 10))    let this :: Lestrade h (Defined Bool)       this = Prop.down (Prop.lift x .== Prop.lift y) >>= read@@ -62,8 +64,8 @@  hprop_ordR_negation :: Property hprop_ordR_negation = property do-  x <- forAll defined_int-  y <- forAll defined_int+  x <- forAll (Gen.int (Range.linear 0 10))+  y <- forAll (Gen.int (Range.linear 0 10))    let this :: Lestrade h (Defined Bool)       this = Prop.down (Prop.lift x .<= Prop.lift y) >>= read@@ -75,8 +77,8 @@  hprop_ordR_lteR_symmetry :: Property hprop_ordR_lteR_symmetry = property do-  x <- forAll defined_int-  y <- forAll defined_int+  x <- forAll (Gen.int (Range.linear 0 10))+  y <- forAll (Gen.int (Range.linear 0 10))    let this :: Lestrade h (Defined Bool)       this = Prop.down (Prop.lift x .<= Prop.lift y) >>= read@@ -88,8 +90,8 @@  hprop_ordR_ltR_symmetry :: Property hprop_ordR_ltR_symmetry = property do-  x <- forAll defined_int-  y <- forAll defined_int+  x <- forAll (Gen.int (Range.linear 0 10))+  y <- forAll (Gen.int (Range.linear 0 10))    let this :: Lestrade h (Defined Bool)       this = Prop.down (Prop.lift x .< Prop.lift y) >>= read@@ -101,10 +103,53 @@  hprop_ordR_simple :: Property hprop_ordR_simple = property do-  (Exactly -> x) <- forAll (Gen.int (Range.linear 0 10))-  (Exactly -> y) <- forAll (Gen.int (Range.linear 0 10))+  x <- forAll (Gen.int (Range.linear 0 10))+  y <- forAll (Gen.int (Range.linear 0 10)) -  let program :: Lestrade h (Defined Bool)-      program = Prop.down (Prop.lift x .<= Prop.lift y) >>= read+  let x', y' :: MonadCell m => Prop m (Defined Int)+      x' = Prop.lift x+      y' = Prop.lift y +      program :: Lestrade h (Defined Bool)+      program = Prop.down (x' .<= y') >>= read+   scotlandYardSays program === Just (Exactly (x <= y))++hprop_choice_unique_choices :: Property+hprop_choice_unique_choices = property do+  n <- forAll $ Gen.int (Range.linear 0 6)+  k <- forAll $ Gen.int (Range.linear 0 n)++  let choices = Prop.choose n k++  nub choices === choices++hprop_choice_correct_number_of_choices :: Property+hprop_choice_correct_number_of_choices = property do+  n <- forAll $ Gen.int (Range.linear 0 6)+  k <- forAll $ Gen.int (Range.linear 0 n)++  let choices = Prop.choose n k+      factorial 0 = 1+      factorial n = n * factorial (pred n)++  length choices === factorial n `div` (factorial k * factorial (n-k))++hprop_exactly_simple :: Property+hprop_exactly_simple = property do+  xs <- forAll (Gen.list (Range.linear 0 10) (Gen.int (Range.linear 0 10)))+  k  <- forAll (Gen.int (Range.linear 0 (length xs)))+  x  <- forAll (Gen.int (Range.linear 0 10))++  let x' :: MonadCell m => Prop m (Defined Int)+      x' = Prop.lift x+      +      xs' :: MonadCell m => [Prop m (Defined Int)]+      xs' = map Prop.lift xs++      program :: Lestrade h (Defined Bool)+      program = Prop.down (Prop.exactly k (.== x') xs') >>= read++      expected = length (filter (==x) xs) == k++  scotlandYardSays program === Just (Exactly expected)