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