% 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.
>       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.