% Primitive Generic Functions on Lazy Non-Deterministic Data
% Sebastian Fischer (sebf@informatik.uni-kiel.de)
> module Data.LazyNondet.Primitive (
>
> nondet, groundNormalForm, partialNormalForm,
>
> prim_eq
>
> ) where
>
> import Data.LazyNondet.Types
> import Data.LazyNondet.Generic
>
> import Control.Monad.State
> import Control.Monad.Update
>
> import Control.Constraint.Choice
>
> import Data.Supply
We provide a generic operation `nondet` to translate instances of
`Generic` into non-deterministic data.
> nondet :: (Update cs m m, Generic a) => a -> Nondet cs m a
> nondet = Typed . return . nf2hnf . generic
>
> nf2hnf :: Update cs m m => NormalForm -> HeadNormalForm cs m
> nf2hnf (Var _) = error "Primitive.nf2hnf: cannot convert logic variable"
> nf2hnf (Data label args) = Cons label (map (return . nf2hnf) args)
> nf2hnf (Fun f) = Lambda (\x _ _ -> liftM (nf2hnf . f) $ gnf x)
> where gnf x = groundNormalForm (Typed x) $
> error "Primitive.nf2hnf: primitive function uses context"
The `...NormalForm` functions evaluate a non-deterministic value and
lift all non-deterministic choices to the top level. The results are
deterministic values and can be converted into their Haskell
representation. Partial normal forms may contain unbound logic
variables while ground normal forms are data terms.
> groundNormalForm :: Update cs m m'
> => Nondet cs m a -> Context cs -> m' NormalForm
> groundNormalForm x (Context cs) = evalStateT (gnf (untyped x)) cs
>
> partialNormalForm :: (Update cs m m', ChoiceStore cs)
> => Nondet cs m a -> Context cs -> m' NormalForm
> partialNormalForm x (Context cs) = evalStateT (pnf (untyped x)) cs
To compute ground normal forms, we ignore free variables and narrow
them to ground terms. To compute partial normal forms, we do not
narrow unbound variables and in a second phase bind those variables
that were bound after we have visited them. For example, when
computing the normal form of `let x free in (x,not x)` we don't know
that `x` will be bound in the result when we encounter it for the
first time.
> gnf :: Update cs m m' => Untyped cs m -> StateT cs m' NormalForm
> gnf = nf (\_ _ -> Just ()) Data mkVar Fun
>
> mkVar :: ID -> a -> NormalForm
> mkVar (ID us) _ = Var (supplyValue us)
>
> pnf :: (Update cs m m', ChoiceStore cs)
> => Untyped cs m -> StateT cs m' NormalForm
> pnf x
> = nf lookupChoice ((return.).Cons) ((return.).FreeVar) (return.Lambda) x
> >>= nf lookupChoice Data mkVar Fun
The `nf` function is used by all normal-form functions and performs
all the work.
> nf :: Update cs m m'
> => (Int -> cs -> Maybe a)
> -> (ConsLabel -> [nf] -> nf)
> -> (ID -> Untyped cs m -> nf)
> -> (b -> nf)
> -> Untyped cs m -> StateT cs m' nf
> nf lkp cns fv fun x = do
> hnf <- updateState x
> case hnf of
> FreeVar u@(ID us) y ->
> get >>= maybe (return (fv u y)) (const (nf lkp cns fv fun y))
> . lkp (supplyValue us)
> Delayed _ resume -> get >>= nf lkp cns fv fun . resume . Context
> Cons label args -> do
> nfs <- mapM (nf lkp cns fv fun) args
> return (cns label nfs)
> Lambda _ -> return . fun $ error "Data.LazyNondet.Primitive.nf: function"
We provide a generic comparison function for untyped non-deterministic
data that is used to define a typed equality test in the
`Data.LazyNondet.Types.Bool` module.
> prim_eq :: Update cs m m
> => Untyped cs m -> Untyped cs m -> StateT cs m Bool
> prim_eq x y = do
> Cons lx xs <- solveCons x
> Cons ly ys <- solveCons y
> if index lx == index ly then all_eq xs ys else return False
> where
> all_eq [] [] = return True
> all_eq (v:vs) (w:ws) = do
> eq <- prim_eq v w
> if eq then all_eq vs ws else return False
> all_eq _ _ = return False
The function `solveCons` is like `solve` but always yields a
constructor-rooted term, i.e., no free variable or delayed
computation.
> solveCons :: Update cs m m
> => Untyped cs m -> StateT cs m (HeadNormalForm cs m)
> solveCons x = do
> hnf <- updateState x
> case hnf of
> FreeVar _ y -> solveCons y
> Delayed _ res -> get >>= solveCons . res . Context
> Lambda _ -> error "Data.LazyNondet.Primitive.solveCons: matched lambda"
> _ -> return hnf