% Constraints for Call-Time Choice
% Sebastian Fischer ([sebf])
% October, 2008

This module implements a choice construct in a constrained monad. This
construct allows to implement functional-logic programs lazily because
shared choices are constrained to take the same branch. Internally, we
use a constraint store that associates unique identifiers to integers.

This module is written in a way that supports the use of [Pandoc] for
rendering.

[sebf]:       mailto:sebf@informatik.uni-kiel.de
[Pandoc]:     http://johnmacfarlane.net/pandoc/


~~~ {.literatehaskell}

> {-# OPTIONS_GHC -XTypeFamilies #-}
>
> module Control.Monad.Constraint.Choice (
>
>   module Control.Monad.Constraint.Choice, UniqSupply
>
> ) where
>
> import Control.Monad
> import Control.Monad.State
> import Control.Monad.Constraint
> import Data.IDSupply

~~~

We borrow unique identifiers from the GHC sources. You need to include
the package ghc-6.8.3 or similar to be able to import the necessary
modules.

~~~ {.literatehaskell}

> import Unique
> import UniqSupply
> import UniqFM

~~~

The `choice` function takes a supply of unique identifiers and yields
a choice in a monad that is constrained by `Choice`s.

~~~ {.literatehaskell}

> choice :: ( IDSupply is, MonadC m, Constraint (Store m) ~ Choice is )
>        => is -> [m a] -> m a
> choice is xs = foldr1 mplus (mzero:zipWith ((&>).Choice i) [0..] xs)
>  where i = idFromSupply is

~~~

GHC's `UniqSupply` is an instance of IDSupply.

~~~ {.literatehaskell}

> instance IDSupply UniqSupply
>  where
>   type ID UniqSupply = Unique
>
>   initSupply   = mkSplitUniqSupply 'x'
>   splitSupply  = splitUniqSupply
>   idFromSupply = uniqFromSupply

~~~

The constraint store `Choices` is a `UniqFM` of choices. Constraints
are modeled as values of type `Choice`.

~~~ {.literatehaskell}

> newtype Choices (m :: * -> *) = CS (UniqFM Int)
>
> data Choice is = Choice (ID is) Int

~~~

The type `Choices` is an instance of the class `CStore`
and `Choice` is the associated type of constraints.

The function `assert` fails to insert a conflicting choice in the
store and possibly updates the store if the given choice constraint is
consistent.

The function `labeling` does not modify the store, as there are no
ambigous constraints in a store of choices.

~~~ {.literatehaskell}

> instance MonadPlus m => CStore (Choices m)
>  where
>   type Constraint (Choices m) = Choice UniqSupply
>   type     Solver (Choices m) = m
>
>   noConstraints = CS emptyUFM
>
>   assert (Choice u n) = do
>     CS cs <- get
>     case lookupUFM_Directly cs u of
>       Nothing -> put (CS (addToUFM_Directly cs u n))
>       Just n' -> guard (n==n')
>
>   labeling = return ()

~~~

~~~ {.literatehaskell}
~~~