| Copyright | (c) Chris Penner 2019 |
|---|---|
| License | BSD3 |
| Safe Haskell | None |
| Language | Haskell2010 |
Props
Description
Synopsis
- type Prop a = PropT Identity a
- data PropT m a
- data PVar (f :: * -> *) a
- newPVar :: (Monad m, Foldable f, Typeable f, Typeable a) => f a -> PropT m (PVar f a)
- solveT :: forall m a r. Monad m => ((forall f x. PVar f x -> x) -> a -> r) -> PropT m a -> m (Maybe r)
- solveAllT :: forall m a r. Monad m => ((forall f x. PVar f x -> x) -> a -> r) -> PropT m a -> m [r]
- solve :: forall a r. ((forall f x. PVar f x -> x) -> a -> r) -> Prop a -> Maybe r
- solveAll :: forall a r. ((forall f x. PVar f x -> x) -> a -> r) -> Prop a -> [r]
- constrain :: Monad m => PVar f a -> PVar g b -> (a -> g b -> g b) -> PropT m ()
- disjoint :: forall a m. (Monad m, Ord a) => PVar Set a -> PVar Set a -> PropT m ()
- equal :: forall a m. (Monad m, Ord a) => PVar Set a -> PVar Set a -> PropT m ()
- require :: Monad m => (a -> b -> Bool) -> PVar Set a -> PVar Set b -> PropT m ()
Initializing problems
A monad transformer for setting up constraint problems.
data PVar (f :: * -> *) a Source #
A propagator variable where the possible values a are contained in the container f.
newPVar :: (Monad m, Foldable f, Typeable f, Typeable a) => f a -> PropT m (PVar f a) Source #
Used to create a new propagator variable within the setup for your problem.
f is any Foldable container which contains each of the possible states which the variable could take.
E.g. For a sudoku solver you would use newPVar to create a variable for each cell, passing a Set Int containing the numbers [1..9].
Finding Solutions
solveT :: forall m a r. Monad m => ((forall f x. PVar f x -> x) -> a -> r) -> PropT m a -> m (Maybe r) Source #
Provide an initialization action which constrains the problem, and a finalizer, and solveT will return a result if one exists.
The finalizer is an annoyance caused by the fact that GHC does not yet support Impredicative Types.
For example, if you wrote a solution to the nQueens problem, you might run it like so:
-- Set up the problem for 'n' queens and return their PVar's as a list. initNQueens :: Int -> Prop [PVar S.Set Coord] initNQueens = ... solution :: [Coord] solution = solve (\readPVar vars -> fmap readPVar vars) (initNQueens 8) -- or more simply: solution = solve fmap (initNQueens 8)
which converts PVars into a result.Given an action which initializes and constrains a problem solveT will and returns some container of PVars, solveT will attempt to find a solution which passes all valid constraints.
solveAllT :: forall m a r. Monad m => ((forall f x. PVar f x -> x) -> a -> r) -> PropT m a -> m [r] Source #
Like solveT, but finds ALL possible solutions. There will likely be duplicates.
solve :: forall a r. ((forall f x. PVar f x -> x) -> a -> r) -> Prop a -> Maybe r Source #
Pure version of solveT
solveAll :: forall a r. ((forall f x. PVar f x -> x) -> a -> r) -> Prop a -> [r] Source #
Pure version of solveAllT
Constraining variables
constrain :: Monad m => PVar f a -> PVar g b -> (a -> g b -> g b) -> PropT m () Source #
constrain the relationship between two PVars. Note that this is a ONE WAY relationship; e.g. constrain a b f will propagate constraints from a to b but not vice versa.
Given PVar f a and PVar g b as arguments, provide a function which will filter/alter the options in g according to the choice.
For a sudoku puzzle you'd have two Pvar Set Int's, each representing a cell on the board.
You can constrain b to be a different value than a with the following call:
constrain a b $ \elementA setB -> S.delete elementA setB)
Take a look at some linking functions which are already provided: disjoint, equal, require
disjoint :: forall a m. (Monad m, Ord a) => PVar Set a -> PVar Set a -> PropT m () Source #
Apply the constraint that two variables may NOT be set to the same value. This constraint is bidirectional.
E.g. you might apply this constraint to two cells in the same row of sudoku grid to assert they don't contain the same value.