packages feed

cflp 0.2.2 → 0.2.5

raw patch · 15 files changed

+327/−360 lines, 15 filesdep +containersdep +value-supplydep −ghc

Dependencies added: containers, value-supply

Dependencies removed: ghc

Files

cflp.cabal view
@@ -1,6 +1,6 @@ Name:          cflp-Version:       0.2.2-Cabal-Version: >= 1.2+Version:       0.2.5+Cabal-Version: >= 1.6 Synopsis:      Constraint Functional-Logic Programming in Haskell Description:   This package provides combinators for constraint                functional-logic programming ((C)FLP) in Haskell. The @@ -13,6 +13,7 @@ License-File:  LICENSE Author:        Sebastian Fischer Maintainer:    sebf@informatik.uni-kiel.de+Bug-Reports:   mailto:sebf@informatik.uni-kiel.de Homepage:      http://www-ps.informatik.uni-kiel.de/~sebf/projects/cflp.html Build-Type:    Custom Stability:     alpha@@ -20,10 +21,15 @@ Extra-Source-Files: README, INSTALL, Makefile, configure, Test.lhs  Library-  Build-Depends:    base >= 4, ghc, mtl, syb, HUnit+  Build-Depends:    base >= 4, +                    containers, +                    value-supply >= 0.3, +                    mtl, +                    syb, +                    HUnit   Exposed-Modules:  Control.CFLP-  Other-Modules:    Control.Monad.Constraint,-                    Control.Monad.Constraint.Choice,+  Other-Modules:    Control.Monad.Update,+                    Control.Constraint.Choice,                     Data.LazyNondet,                     Data.LazyNondet.Types,                     Data.LazyNondet.Types.Bool,@@ -35,7 +41,7 @@                     Control.CFLP.Tests,                     Control.CFLP.Tests.CallTimeChoice   Hs-Source-Dirs:   src-  Extensions:       ExistentialQuantification,+  Extensions:       FunctionalDependencies,                     MultiParamTypeClasses,                     FlexibleInstances,                     FlexibleContexts,
src/Control/CFLP.lhs view
@@ -24,36 +24,32 @@ > ) where > > import Data.LazyNondet-> import Data.LazyNondet.Primitive > import Data.LazyNondet.Types.Bool > import Data.LazyNondet.Types.List > > import Control.Monad.State-> import Control.Monad.Constraint-> import Control.Monad.Constraint.Choice+> import Control.Monad.Update >-> class (MonadConstr Choice m,->        ConstraintStore Choice cs,->        ChoiceStore cs,->        MonadSolve cs m m)->  => CFLP cs m+> import Control.Constraint.Choice+>+> class (MonadUpdate s m, Update s m m, ChoiceStore s) => CFLP s m  The type class `CFLP` is a shortcut for the type-class constraints on constraint functional-logic computations that are parameterized over a constraint store and a constraint monad. Hence, such computations can be executed with different constraint stores and search strategies. -> instance CFLP ChoiceStoreUnique (ConstrT ChoiceStoreUnique [])+> instance CFLP ChoiceStoreIM (UpdateT ChoiceStoreIM [])  We declare instances for every combination of monad and constraint store that we intend to use. -> type CS = ChoiceStoreUnique+> type CS = ChoiceStoreIM > > noConstraints :: CS > noConstraints = noChoices >-> type Computation m a = CS -> ID -> Nondet CS (ConstrT CS m) a+> type Computation m a = CS -> ID -> Nondet CS (UpdateT CS m) a  Currently, the constraint store used to evaluate constraint functional-logic programs is simply a `ChoiceStore`. It will be a@@ -70,7 +66,7 @@  The strategy of the list monad is depth-first search. -> evaluate :: (CFLP CS m, MonadSolve CS m m')+> evaluate :: (CFLP CS m, Update CS m m') >          => (Nondet CS m a -> CS -> m' b) >          -> Strategy m' -> (CS -> ID -> Nondet CS m a) >          -> IO [b]@@ -81,17 +77,16 @@ The `evaluate` function enumerates the non-deterministic solutions of a constraint functional-logic computation according to a given strategy. -> eval, evalPartial :: (CFLP CS m, MonadSolve CS m m', Data a)+> eval, evalPartial :: (CFLP CS m, Update CS m m', Data a) >                   => Strategy m' -> (CS -> ID -> Nondet CS m a) >                   -> IO [a] > eval        s = liftM (map prim) . evaluate groundNormalForm  s > evalPartial s = liftM (map prim) . evaluate partialNormalForm s >-> evalPrint :: (CFLP CS m, MonadSolve CS m m', Data a, Show a)+> evalPrint :: (CFLP CS m, Update CS m m', Data a, Show a) >           => Strategy m' -> (CS -> ID -> Nondet CS m a) >           -> IO ()-> evalPrint s op = eval s op >>= printSols->  -- evaluate partialNormalForm s op >>= printSols+> evalPrint s op = evaluate partialNormalForm s op >>= printSols > > printSols :: Show a => [a] -> IO () > printSols []     = putStrLn "No more solutions."
src/Control/CFLP/Tests/CallTimeChoice.lhs view
@@ -34,7 +34,7 @@ > > ignot :: CFLP cs m >       => Nondet cs m a -> Nondet cs m Bool -> cs -> Nondet cs m Bool-> ignot _ x = not x+> ignot _ = not  This test checks a function with two arguments, where the first must be ignored. Any changes in the translation scheme must not lead to@@ -45,7 +45,7 @@ > sharedVarsAreEqual :: Assertion > sharedVarsAreEqual = assertResults comp [[False,False],[True,True]] >  where->   comp _ u = two (unknown u)+>   comp _ = two . unknown > > two :: Monad m => Nondet cs m a -> Nondet cs m [a] > two x = x ^: x ^: nil
+ src/Control/Constraint/Choice.lhs view
@@ -0,0 +1,78 @@+% Sharing Choices with Constraints+% Sebastian Fischer (sebf@informatik.uni-kiel.de)++We define a constraint store that stores choice constraints which+ensure that shared non-deterministic choices evaluate to the same+values when translating lazy functional logic programs.++Based on this constraint store, we provide a function `choice` that+can be used to generate choices that are constrained to evaluate to+the same value if they are shared.++> {-# LANGUAGE+>       MultiParamTypeClasses,+>       FlexibleInstances,+>       FlexibleContexts+>   #-}+>+> module Control.Constraint.Choice (+>+>   ChoiceStore(..), ChoiceStoreIM, noChoices, choice+>+> ) where+>+> import Control.Monad.State+> import Control.Monad.Update+>+> import qualified Data.IntMap as IM+>+> class ChoiceStore s+>  where+>   lookupChoice :: Int -> s -> Maybe Int+>   assertChoice :: MonadPlus m => s -> Int -> Int -> s -> m s++We define an interface for choice stores that provide an operation to+lookup a previously made choice. The first argument of `assertChoice`+is a dummy argument to fix the type of the store in partial+applications.+++> newtype ChoiceStoreIM = ChoiceStoreIM (IM.IntMap Int) deriving Show+>+> noChoices :: ChoiceStoreIM+> noChoices = ChoiceStoreIM IM.empty+>+> instance ChoiceStore ChoiceStoreIM+>  where+>   lookupChoice u (ChoiceStoreIM cs) = IM.lookup u cs+>+>   assertChoice _ u x (ChoiceStoreIM cs) = do+>     maybe (return (ChoiceStoreIM (IM.insert u x cs)))+>           (\y -> do guard (x==y); return (ChoiceStoreIM cs))+>           (IM.lookup u cs)++A finite map mapping unique identifiers to integers is a+`ChoiceStore`. The `assertChoice` operations fails to insert+conflicting choices.++> choice :: (MonadUpdate s m, ChoiceStore s) => s -> Int -> [m a] -> m a+> choice cs u xs =+>   maybe (foldr1 mplus . (mzero:) . zipWith constrain [(0::Int)..] $ xs)+>         (xs!!)+>         (lookupChoice u cs)+>  where constrain n = (update (assertChoice cs u n)>>)++The operation `choice` takes a unique label and a list of monadic+values that can be constrained with choice constraints. The result is+a single monadic action combining the alternatives with `mplus`. If it+occurs more than once in a bigger monadic action, the result is+constrained to take the same alternative everywhere when collecting+constraints.++If a choice with the same label has been created previously and the+label is already constrained to an alternative, then this alternative+is returned directly and no choice is created.++This situation occurs when a shared logic variable is renarrowed when+it is demanded again during a computation.+
− src/Control/Monad/Constraint.lhs 
@@ -1,170 +0,0 @@-% Constraint Collecting Monads-% Sebastian Fischer (sebf@informatik.uni-kiel.de)--We define type classes and instances for monads that can collect-constraints. The challenge is to define the interface such that-instances can implement it without threading a store through monadic-computations and shared monadic computations are evaluated only once.--> {-# LANGUAGE ->       MultiParamTypeClasses,->       FlexibleInstances,->       ExistentialQuantification->   #-}->-> module Control.Monad.Constraint (->->   -- type classes->   ConstraintStore(..), MonadConstr(..), MonadSolve(..),->->   -- monad transformer->   ConstrT->-> ) where-> -> import Control.Monad.State-> import Control.Monad.Trans->-> class ConstraintStore c cs->  where->   assert :: (MonadState cs m, MonadPlus m) => c -> m ()--Constraint Stores provide an operation to assert a constraint into a-store. The constraint store is manipulated in an instance of-`MonadState`. The `assert` operation may fail or branch depending on-the given constraint or the current store and is, hence, performed in-an instance of `MonadPlus`.--A constraint store may support different types of constraints and a-constraint may be supported by different constraint stores.--> class MonadPlus m => MonadConstr c m->  where->   constr :: c -> m ()--A monad that supports collecting constraints is an instance of the-class `MonadConstr` that provides an operation to associate a-constraint of type `c` to monadic computations. One monad may support-different types of constraints and the same constraint type may be-supported by different monads.--> instance (MonadPlus m, ConstraintStore c cs) => MonadConstr c (StateT cs m)->  where->   constr = assert--An instance of `MonadPlus` that threads a constraint store can be-constrained with constraints that are supported by the threaded store.--> class (MonadPlus m, MonadPlus m') => MonadSolve cs m m'->  where->   solve :: m a -> StateT cs m' a--We also define an interface for monads that can solve associated-constraints by threading a constraint store through a (possibly, but-not necessarily different) monad.--We use the state monad transformer `StateT` to thread the constraint-store through the monad that returns the results.--> instance MonadPlus m => MonadSolve cs (StateT cs m) m->  where->   solve = id--Again, a state threading monad gives rise to a natural instance, where-results are returned in the base monad.--State monads are a natural choice for a constraint monad, but they-have a drawback: monadic values are functions that are reexecuted for-each shared occurrence of a monadic sub computation.--Shared Monadic Values------------------------We define a monad transformer `ConstrT` that adds the capability of-collecting and solving constraints to arbitrary instances of-`MonadPlus`. Monadic actions in the resulting monads are data terms if-monadic actions are data terms in the base monad. As a consequence,-they are evaluated only once if they are shared.--> newtype ConstrT cs m a = ConstrT { unConstrT :: m (WithConstr cs m a) }-> data WithConstr cs m a->   = Return a->   | forall c . ConstraintStore c cs => Constr c (ConstrT cs m a)--The type `c` of collected constraints is existentially quantified in-order to allow different types of constraints in the same monadic-action. All types of constraints that are collected in a monadic-action need to be supported by the constraint store of type `cs`.--> instance (MonadPlus m, ConstraintStore c cs) => MonadConstr c (ConstrT cs m)->  where->   constr c = ConstrT (return (Constr c (return ())))--A transformed instance of `MonadPlus` is an instance of `MonadConstr`.--> instance MonadPlus m => MonadSolve cs (ConstrT cs m) m->  where->   solve = run->    where->     run :: MonadPlus m => ConstrT cs m a -> StateT cs m a->     run x = lift (unConstrT x) >>= constrain->->     constrain (Return a)   = return a->     constrain (Constr c y) = do constr c; run y--It is also an instance of `MonadSolve` where results are returned in-the base monad. In order to eliminate stored constraints, we thread a-constraint store through the monadic value and assert the associated-constraints into the store.--> instance MonadPlus m => MonadSolve cs (ConstrT cs m) (ConstrT cs m)->  where->   solve = run->    where->     run :: MonadPlus m => ConstrT cs m a -> StateT cs (ConstrT cs m) a->     run x = lift (lift (unConstrT x)) >>= constrain->->     constrain (Return a)   = return a->     constrain (Constr c y) = do lift (constr c); constr c; run y--We define another instance of `MonadSolve` where results are not-returned in the base monad but in the transformed base monad. This-instance is useful to support computations that may or may not-consider the threaded constraint store. All constraints are kept in-the monadic values and threaded additionally.--> instance Monad m => Monad (ConstrT cs m)->  where->   return = ConstrT . return . Return->->   x >>= f = ConstrT (unConstrT x >>= g)->    where g (Return a)   = unConstrT (f a)->          g (Constr c y) = return (Constr c (y >>= f))->-> instance MonadPlus m => MonadPlus (ConstrT cs m)->  where->   mzero       = ConstrT mzero->   x `mplus` y = ConstrT (unConstrT x `mplus` unConstrT y)->-> instance MonadTrans (ConstrT cs)->  where->   lift x = ConstrT (x >>= return . Return)--We specify that a transformed monad is indeed a monad, that it is an-instance of `MonadPlus` if the base monad is, and that, `ConstrT`-(with an arbitrary constraint store `cs`) is a monad transformer.--> instance Show a => Show (ConstrT cs [] a)->  where->   show (ConstrT x) = show x->-> instance Show a => Show (WithConstr cs [] a)->  where->   show (Return x) = "(Return "++show x++")"->   show (Constr _ (ConstrT x)) = "(Constr _ "++show x++")"--To simplify debugging, we define `Show` instances for transformed list-monads. Unfortunately, I don't know an easy way to show collected-constraints, because their type is not determined by the constraint-store and not mentioned in the signature of the instances.-
− src/Control/Monad/Constraint/Choice.lhs 
@@ -1,87 +0,0 @@-% Sharing Choices with Constraints-% Sebastian Fischer (sebf@informatik.uni-kiel.de)--We define a constraint store that stores choice constraints which-ensure that shared non-deterministic choices evaluate to the same-values when translating lazy functional logic programs.--Based on this constraint store, we provide a function `choice` that-can be used to generate choices that are constrained to evaluate to-the same value if they are shared.--> {-# LANGUAGE->       MultiParamTypeClasses,->       FlexibleInstances,->       FlexibleContexts->   #-}->-> module Control.Monad.Constraint.Choice (->->   Choice, ChoiceStore(..), ChoiceStoreUnique, noChoices, choice->-> ) where->-> import Control.Monad.State-> import Control.Monad.Constraint->-> import Unique-> import UniqFM--We borrow unique identifiers from the package `ghc` which is hidden by-default.--> class ChoiceStore cs->  where->   lookupChoice :: Unique -> cs -> Maybe Int--We define an interface for choice stores that provide an operation to-lookup a previously made choice.--> newtype Choice = Choice (Unique,Int)-> newtype ChoiceStoreUnique = ChoiceStore (UniqFM Int)->-> noChoices :: ChoiceStoreUnique-> noChoices = ChoiceStore emptyUFM->-> instance ChoiceStore ChoiceStoreUnique->  where->   lookupChoice u (ChoiceStore cs) = lookupUFM_Directly cs u--A finite map mapping `Unique`s to integers is a `ChoiceStore`.--> instance ConstraintStore Choice ChoiceStoreUnique->  where->   assert (Choice (u,x)) = do->     ChoiceStore cs <- get->     maybe (put (ChoiceStore (addToUFM_Directly cs u x)))->           (guard . (x==))->           (lookupUFM_Directly cs u)--Choices are labeled with a `Unique`, so we can store them in a-`UniqFM` making it an instance of `ConstraintStore`.--The `assert` operations fails to insert conflicting choices.--> choice :: (MonadConstr Choice m, ChoiceStore cs)->        => cs -> Unique -> [m a] -> m a-> choice cs u xs =->   maybe (foldr1 mplus . (mzero:) . zipWith constrain [(0::Int)..] $ xs)->         (xs!!)->         (lookupChoice u cs)->  where constrain n = (constr (Choice (u,n))>>)--The operation `choice` takes a unique label and a list of monadic-values that can be constrained with choice constraints. The result is-a single monadic action combining the alternatives with `mplus`. If it-occurs more than once in a bigger monadic action, the result is-constrained to take the same alternative everywhere when collecting-constraints.--If a choice with the same label has been created previously and the-label is already constrained to an alternative, then this alternative-is returned directly and no choice is created.--This situation may occur if a shared logic variable is renarrowed-whenever it is demanded rather than shared and only narrowed on-creation.-
+ src/Control/Monad/Update.lhs view
@@ -0,0 +1,153 @@+% Monads with Non-Deterministically Updateable State+% Sebastian Fischer (sebf@informatik.uni-kiel.de)++We define type classes and instances for monads that+non-deterministically update state. The challenge is to define the+interface such that instances can implement it without threading a+store through monadic computations and shared monadic computations are+evaluated only once.++> {-# LANGUAGE +>       MultiParamTypeClasses,+>       FlexibleInstances,+>       FlexibleContexts,+>       RankNTypes+>   #-}+>+> module Control.Monad.Update (+>+>   -- type classes+>   MonadUpdate(..), Update(..),+>+>   -- monad transformer+>   UpdateT+>+> ) where+> +> import Control.Monad.State+> import Control.Monad.Trans+>+> class MonadPlus m => MonadUpdate s m+>  where+>   update :: (forall m' . MonadPlus m' => s -> m' s) -> m ()++A monad that supports non-deterministic state updates is an instance+of the class `MonadUpdate` that provides an operation to incorporate a+monadic update-action into monadic computations.++> instance MonadPlus m => MonadUpdate s (StateT s m)+>  where+>   update upd = get >>= upd >>= put++An instance of `MonadPlus` that threads a state can update that state+non-deterministically.++> class (MonadPlus m, MonadPlus m') => Update s m m'+>  where+>   updateState :: m a -> StateT s m' a++We also define an interface for monads that perform associated updates+in a state that is threaded through a (possibly, but not necessarily+different) monad.++We use the state monad transformer `StateT` to thread the constraint+store through the monad that returns the results.++> instance MonadPlus m => Update s (StateT s m) m+>  where+>   updateState = id++Again, a state threading monad gives rise to a natural instance, where+results are returned in the base monad.++State monads are a natural choice for a monad that updates state, but+they have a drawback: monadic values are functions that are reexecuted+for each shared occurrence of a monadic sub computation.++Shared Monadic Values+---------------------++We define a monad transformer `UpdateT` that adds the capability of+non-deterministic state updates to arbitrary instances of+`MonadPlus`. Monadic actions in the resulting monads are data terms if+monadic actions are data terms in the base monad. As a consequence,+they are evaluated only once if they are shared.++> newtype UpdateT s m a = UpdateT { unUpdateT :: m (WithUpdate s m a) }+> data WithUpdate s m a+>   = Return a+>   | Update (forall m' . MonadPlus m' => s -> m' s)+>            (UpdateT s m a)++The updating monadic action must be polymorphic in the used monad+`m'`.++> instance MonadPlus m => MonadUpdate s (UpdateT s m)+>  where+>   update upd = UpdateT (return (Update upd (return ())))++A transformed instance of `MonadPlus` is an instance of `MonadUpdate`.++> instance MonadPlus m => Update s (UpdateT s m) m+>  where+>   updateState = run+>    where+>     run :: MonadPlus m => UpdateT s m a -> StateT s m a+>     run x = lift (unUpdateT x) >>= doUpdate+>+>     doUpdate (Return a)     = return a+>     doUpdate (Update upd y) = do update upd; run y++It is also an instance of `Update` where results are returned in the+base monad. In order to perform stored updates, we thread a state+through the monadic computation.++> instance MonadPlus m => Update s (UpdateT s m) (UpdateT s m)+>  where+>   updateState = run+>    where+>     run :: MonadPlus m => UpdateT s m a -> StateT s (UpdateT s m) a+>     run x = lift (lift (unUpdateT x)) >>= doUpdate+>+>     doUpdate (Return a)     = return a+>     doUpdate (Update upd y) = do lift (update upd); update upd; run y++We define another instance of `Update` where results are not returned+in the base monad but in the transformed base monad. This instance is+useful to support computations that may or may not consider the+threaded store. All upcate actions are kept in the monadic values and+threaded additionally.++> instance Monad m => Monad (UpdateT s m)+>  where+>   return = UpdateT . return . Return+>+>   x >>= f = UpdateT (unUpdateT x >>= g)+>    where g (Return a)     = unUpdateT (f a)+>          g (Update upd y) = return (Update upd (y >>= f))+>+> instance MonadPlus m => MonadPlus (UpdateT s m)+>  where+>   mzero       = UpdateT mzero+>   x `mplus` y = UpdateT (unUpdateT x `mplus` unUpdateT y)+>+> instance MonadTrans (UpdateT s)+>  where+>   lift = UpdateT . liftM Return++We specify that a transformed monad is indeed a monad, that it is an+instance of `MonadPlus` if the base monad is, and that, `UpdateT`+(with an arbitrary store `s`) is a monad transformer.++> instance Show a => Show (UpdateT s [] a)+>  where+>   show (UpdateT x) = show x+>+> instance Show a => Show (WithUpdate cs [] a)+>  where+>   show (Return x) = "(Return "++show x++")"+>   show (Update _ (UpdateT x)) = "(Update _ "++show x++")"++To simplify debugging, we define `Show` instances for transformed list+monads.+
src/Data/LazyNondet.lhs view
@@ -16,7 +16,7 @@ > >   withHNF, caseOf, caseOf_, Match, >->   Data, nondet, groundNormalForm, partialNormalForm,+>   Data, nondet, prim, groundNormalForm, partialNormalForm, > >   ConsRep(..), cons, match, >
src/Data/LazyNondet/Matching.lhs view
@@ -7,8 +7,7 @@ >       FlexibleContexts, >       FlexibleInstances, >       MultiParamTypeClasses,->       FunctionalDependencies,->       ExistentialQuantification+>       FunctionalDependencies >   #-} > > module Data.LazyNondet.Matching (@@ -23,23 +22,22 @@ > import Data.LazyNondet.Types > > import Control.Monad.State-> import Control.Monad.Constraint-> import Control.Monad.Constraint.Choice+> import Control.Monad.Update >-> withHNF :: (Monad m, MonadSolve cs m m)+> withHNF :: (Monad m, Update cs m m) >         => Nondet cs m a >         -> (HeadNormalForm cs m -> cs -> Nondet cs m b) >         -> cs -> Nondet cs m b > withHNF x b cs = Typed (do->   (hnf,cs') <- runStateT (solve (untyped x)) cs+>   (hnf,cs') <- runStateT (updateState (untyped x)) cs >   untyped (b hnf cs'))  The `withHNF` operation can be used for pattern matching and solves constraints associated to the head constructor of a non-deterministic value. An updated constraint store is passed to the computation of the branch function. Collected constraints are kept attached to the-computed value by using an appropriate instance of `MonadSolve` that-does not eliminate them.+computed value by using an appropriate instance of `Update` that does+not eliminate them.  > class WithUntyped a >  where@@ -99,12 +97,11 @@ function to typed versions of these values.  > newtype Match a cs m b = Match { unMatch :: (ConIndex, cs -> Branch cs m b) }-> data Branch cs m a =->   forall t . (WithUntyped t, cs ~ C t, m ~ M t, a ~ T t) => Branch t+> type Branch cs m a = [Untyped cs m] -> Nondet cs m a > > match :: (ConsRep a, WithUntyped b) >       => a -> (C b -> b) -> Match t (C b) (M b) (T b)-> match c alt = Match (constrIndex (consRep c), Branch . alt)+> match c alt = Match (constrIndex (consRep c), withUntyped . alt)  The operation `match` is used to build destructor functions for non-deterministic values that can be used with `caseOf`.@@ -114,11 +111,11 @@  Failure is just a type version of `mzero`. -> caseOf :: (MonadSolve cs m m, MonadConstr Choice m)+> caseOf :: Update cs m m >        => Nondet cs m a -> [Match a cs m b] -> cs -> Nondet cs m b > caseOf x bs = caseOf_ x bs failure >-> caseOf_ :: (MonadSolve cs m m, MonadConstr Choice m)+> caseOf_ :: Update cs m m >         => Nondet cs m a -> [Match a cs m b] -> Nondet cs m b >         -> cs -> Nondet cs m b > caseOf_ x bs def =@@ -129,10 +126,7 @@ >       | p cs      -> delayed p (\cs -> caseOf_ (Typed (res cs)) bs def cs) >       | otherwise -> caseOf_ (Typed (res cs)) bs def cs >     Cons _ idx args ->->       maybe def (\b -> branch (b cs) args) (lookup idx (map unMatch bs))->-> branch :: Branch cs m a -> [Untyped cs m] -> Nondet cs m a-> branch (Branch alt) = withUntyped alt+>       maybe def (\b -> b cs args) (lookup idx (map unMatch bs))  We provide operations `caseOf_` and `caseOf` (with and without a default alternative) for more convenient pattern matching. The untyped@@ -148,7 +142,7 @@ > > instance (Monad m, Data a) => MkCons cs m a (Nondet cs m t) >  where->   mkCons c args = Typed (return (mkHNF (toConstr c) (reverse args)))+>   mkCons c = Typed . return . mkHNF (toConstr c) . reverse > > instance MkCons cs m b c => MkCons cs m (a -> b) (Nondet cs m t -> c) >  where
src/Data/LazyNondet/Narrowing.lhs view
@@ -15,23 +15,24 @@ > import Data.Maybe > import Data.LazyNondet.Types >-> import Control.Monad.Constraint-> import Control.Monad.Constraint.Choice+> import Control.Monad.Update >-> import UniqSupply+> import Control.Constraint.Choice >-> unknown :: (MonadConstr Choice m, Narrow cs a) => ID -> Nondet cs m a+> import Data.Supply+>+> unknown :: (MonadUpdate cs m, Narrow cs a) => ID -> Nondet cs m a > unknown u = freeVar u (delayed (redelay u) (\cs -> narrow cs u)) > > redelay :: ChoiceStore cs => ID -> cs -> Bool-> redelay (ID us) = isNothing . lookupChoice (uniqFromSupply us)+> redelay (ID us) = isNothing . lookupChoice (supplyValue us)  The application of `unknown` to a constraint store and a unique identifier represents a logic variable of an arbitrary type.   > class ChoiceStore cs => Narrow cs a >  where->   narrow :: MonadConstr Choice m => cs -> ID -> Nondet cs m a+>   narrow :: MonadUpdate cs m => cs -> ID -> Nondet cs m a  Logic variables of type `a` can be narrowed to head-normal form if there is an instance of the type class `Narrow`. A constraint store@@ -40,7 +41,7 @@ non-deterministic generator using `oneOf`, but for specific types different strategies may be implemented. -> (?) :: (MonadConstr Choice m, ChoiceStore cs)+> (?) :: (MonadUpdate cs m, ChoiceStore cs) >     => Nondet cs m a -> Nondet cs m a -> ID -> Nondet cs m a > (x ? y) u = delayed (redelay u) (\cs -> oneOf [x,y] cs u) @@ -50,9 +51,9 @@ current constraint store, the arguments of `(?)` are shared among all executions and *not* reexecuted. -> oneOf :: (MonadConstr Choice m, ChoiceStore cs)+> oneOf :: (MonadUpdate cs m, ChoiceStore cs) >       => [Nondet cs m a] -> cs -> ID -> Nondet cs m a-> oneOf xs cs (ID us) = Typed (choice cs (uniqFromSupply us) (map untyped xs))+> oneOf xs cs (ID us) = Typed (choice cs (supplyValue us) (map untyped xs))  The operation `oneOf` takes a list of non-deterministic values and returns a non-deterministic value that yields one of the elements in
src/Data/LazyNondet/Primitive.lhs view
@@ -18,12 +18,12 @@ > import Data.LazyNondet.Types > > import Control.Monad.State-> import Control.Monad.Constraint-> import Control.Monad.Constraint.Choice+> import Control.Monad.Update >-> import Unique-> import UniqSupply+> import Control.Constraint.Choice >+> import Data.Supply+> > prim :: Data a => NormalForm -> a > prim (Var u) = error $ "demand on logic variable " ++ show u > prim (NormalForm con args) =@@ -49,10 +49,10 @@ We also provide a generic operation `nondet` to translate instances of the `Data` class into non-deterministic data. -> groundNormalForm :: MonadSolve cs m m' => Nondet cs m a -> cs -> m' NormalForm-> groundNormalForm  = evalStateT . gnf . untyped+> groundNormalForm :: Update cs m m' => Nondet cs m a -> cs -> m' NormalForm+> groundNormalForm = evalStateT . gnf . untyped >-> partialNormalForm :: (MonadSolve cs m m', ChoiceStore cs)+> partialNormalForm :: (Update cs m m', ChoiceStore cs) >                   => Nondet cs m a -> cs -> m' NormalForm > partialNormalForm = evalStateT . pnf . untyped @@ -62,13 +62,13 @@ representation. Partial normal forms may contain unbound logic variables while ground normal forms are data terms. -> gnf :: MonadSolve cs m m' => Untyped cs m -> StateT cs m' NormalForm+> gnf :: Update cs m m' => Untyped cs m -> StateT cs m' NormalForm > gnf = nf (\_ _ -> Just ()) NormalForm mkVar > > mkVar :: ID -> a -> NormalForm-> mkVar (ID us) _ = Var (uniqFromSupply us)+> mkVar (ID us) _ = Var (supplyValue us) >-> pnf :: (MonadSolve cs m m', ChoiceStore cs)+> pnf :: (Update cs m m', ChoiceStore cs) >     => Untyped cs m -> StateT cs m' NormalForm > pnf x = nf lookupChoice ((return.).mkHNF) ((return.).FreeVar) x >     >>= nf lookupChoice NormalForm mkVar@@ -81,17 +81,17 @@ that `x` will be bound in the result when we encounter it for the first time. -> nf :: MonadSolve cs m m'->    => (Unique -> cs -> Maybe a)+> nf :: Update cs m m'+>    => (Int -> cs -> Maybe a) >    -> (Constr -> [nf] -> nf) >    -> (ID -> Untyped cs m -> nf) >    -> Untyped cs m -> StateT cs m' nf > nf lkp cns fv x = do->   hnf <- solve x+>   hnf <- updateState x >   case hnf of >     FreeVar u@(ID us) y -> >       get >>= maybe (return (fv u y)) (const (nf lkp cns fv y))->             . lkp (uniqFromSupply us)+>             . lkp (supplyValue us) >     Delayed _ resume -> get >>= nf lkp cns fv . resume >     Cons typ idx args -> do >       nfs <- mapM (nf lkp cns fv) args@@ -100,7 +100,7 @@ The `nf` function is used by all normal-form functions and performs all the work. -> prim_eq :: MonadSolve cs m m+> prim_eq :: Update cs m m >         => Untyped cs m -> Untyped cs m -> StateT cs m Bool > prim_eq x y = do >   Cons _ ix xs <- solveCons x@@ -117,10 +117,10 @@ data that is used to define a typed equality test in the `Data.LazyNondet.Types.Bool` module. -> solveCons :: MonadSolve cs m m+> solveCons :: Update cs m m >           => Untyped cs m -> StateT cs m (HeadNormalForm cs m) > solveCons x = do->   hnf <- solve x+>   hnf <- updateState x >   case hnf of >     FreeVar _ y -> solveCons y >     Delayed _ res -> get >>= solveCons . res
src/Data/LazyNondet/Types.lhs view
@@ -19,14 +19,13 @@ > > import Data.Data >-> import Control.Monad.Constraint+> import Control.Monad.Update >-> import Unique-> import UniqSupply+> import Data.Supply >-> newtype ID = ID UniqSupply+> newtype ID = ID (Supply Int) >-> data NormalForm = NormalForm Constr [NormalForm] | Var Unique+> data NormalForm = NormalForm Constr [NormalForm] | Var Int  The normal form of data is represented by the type `NormalForm` which defines a tree of constructors and logic variables. The type `Constr`@@ -53,7 +52,7 @@ data type that should be used for conversion into primitive data.  > mkHNF :: Constr -> [Untyped cs m] -> HeadNormalForm cs m-> mkHNF c args = Cons (constrType c) (constrIndex c) args+> mkHNF c = Cons (constrType c) (constrIndex c)  In head-normal forms we split the constructor representation into a representation of the data type and the index of the constructor, to@@ -87,24 +86,24 @@  > instance Show (HeadNormalForm cs []) >  where->   show (FreeVar (ID u) _) = show (uniqFromSupply u)+>   show (FreeVar (ID u) _) = '_':show (supplyValue u) >   show (Delayed _ _) = "<delayed>" >   show (Cons typ idx args)  >     | null args = show con->     | otherwise = unwords (("("++show con):map show args++[")"])+>     | otherwise = unwords (('(':show con):map show args++[")"]) >    where con = indexConstr typ idx > > instance Show (Nondet cs [] a) >  where >   show = show . untyped >-> instance Show (Nondet cs (ConstrT cs []) a)+> instance Show (Nondet cs (UpdateT cs []) a) >  where >   show = show . untyped >-> instance Show (HeadNormalForm cs (ConstrT cs []))+> instance Show (HeadNormalForm cs (UpdateT cs [])) >  where->   show (FreeVar (ID u) _)  = show (uniqFromSupply u)+>   show (FreeVar (ID u) _)  = '_':show (supplyValue u) >   show (Delayed _ _)         = "<delayed>" >   show (Cons typ idx [])   = show (indexConstr typ idx) >   show (Cons typ idx args) =@@ -115,11 +114,12 @@  > instance Show NormalForm >  where->   showsPrec _ (Var u) = shows u+>   showsPrec _ (Var u) = ('_':) . shows u >   showsPrec _ (NormalForm cons []) = shows cons >   showsPrec n x@(NormalForm cons args) >     | Just xs <- fromList x = shows xs->     | n == 0    = shows cons . foldr1 (\y z -> (' ':).y.z) (map shows args)+>     | n == 0 = shows cons . (' ':) . foldr1 (\y z -> y.(' ':).z)+>                 (map (showsPrec 1) args) >     | otherwise = ('(':) . shows x . (')':) > > fromList :: NormalForm -> Maybe [NormalForm]
src/Data/LazyNondet/Types/Bool.lhs view
@@ -17,9 +17,10 @@ > import Data.LazyNondet.Primitive > > import Control.Monad.State-> import Control.Monad.Constraint-> import Control.Monad.Constraint.Choice+> import Control.Monad.Update >+> import Control.Constraint.Choice+> > instance ConsRep Bool where consRep = toConstr > > true :: Monad m => Nondet cs m Bool@@ -43,11 +44,10 @@  Some operations with `Bool`s: -> not :: (MonadSolve cs m m, MonadConstr Choice m)->     => Nondet cs m Bool -> cs -> Nondet cs m Bool-> not x = caseOf_ x [pFalse (\_ -> true)] false+> not :: Update cs m m => Nondet cs m Bool -> cs -> Nondet cs m Bool+> not x = caseOf_ x [pFalse (const true)] false >-> (===) :: MonadSolve cs m m+> (===) :: Update cs m m >       => Nondet cs m a -> Nondet cs m a -> cs -> Nondet cs m Bool > (x === y) cs = Typed $ do >   eq <- evalStateT (prim_eq (untyped x) (untyped y)) cs
src/Data/LazyNondet/Types/List.lhs view
@@ -15,9 +15,10 @@ > import Data.LazyNondet > import Data.LazyNondet.Types.Bool >-> import Control.Monad.Constraint-> import Control.Monad.Constraint.Choice+> import Control.Monad.Update >+> import Control.Constraint.Choice+> > instance ConsRep [()] where consRep = toConstr > > nil :: Monad m => Nondet cs m [a]@@ -42,20 +43,17 @@  > instance (ChoiceStore cs, Narrow cs a) => Narrow cs [a] >  where->   narrow cs = withUnique $ \u1 u2 -> ->                 oneOf [nil, unknown u1 ^: unknown u2] cs+>   narrow cs u = withUnique (\u1 u2 -> +>                   (oneOf [nil, unknown u1 ^: unknown u2] cs u)) u  Some operations on lists: -> null :: (MonadSolve cs m m, MonadConstr Choice m)->      => Nondet cs m [a] -> cs -> Nondet cs m Bool-> null xs = caseOf_ xs [pNil (\_ -> true)] false+> null :: Update cs m m => Nondet cs m [a] -> cs -> Nondet cs m Bool+> null xs = caseOf_ xs [pNil (const true)] false >-> head :: (MonadSolve cs m m, MonadConstr Choice m)->      => Nondet cs m [a] -> cs -> Nondet cs m a+> head :: Update cs m m => Nondet cs m [a] -> cs -> Nondet cs m a > head l = caseOf l [pCons (\_ x _ -> x)] >-> tail :: (MonadSolve cs m m, MonadConstr Choice m)->      => Nondet cs m [a] -> cs -> Nondet cs m [a]+> tail :: Update cs m m => Nondet cs m [a] -> cs -> Nondet cs m [a] > tail l = caseOf l [pCons (\_ _ xs -> xs)]
src/Data/LazyNondet/UniqueID.lhs view
@@ -18,13 +18,13 @@ > > import Control.Monad >-> import UniqSupply+> import Data.Supply  Non-deterministic computations need a supply of unique identifiers in order to constrain shared choices.  > initID :: IO ID-> initID = liftM ID $ mkSplitUniqSupply 'x'+> initID = liftM ID newNumSupply > > class With x a >  where@@ -48,8 +48,7 @@ >   type M ID (ID -> a) = M ID a >   type T ID (ID -> a) = T ID a >->   with f (ID us) = withUnique (f (ID vs)) (ID ws)->    where (vs,ws) = splitUniqSupply us+>   with f (ID us) = with (f (ID (supplyLeft us))) (ID (supplyRight us)) > > withUnique :: With ID a => a -> ID -> Nondet (C ID a) (M ID a) (T ID a) > withUnique = with