Language.Hakaru.Evaluation.EvalMonad

Documentation

runPureEvaluate :: ABT Term abt => abt '[] a -> abt '[] a

Call evaluate on a term. This variant returns an abt expression itself so you needn't worry about the Eval monad. For the monadic-version, see pureEvaluate.

BUG: now that we've indexed ListContext by a Purity, does exposing the implementation details still enable clients to break our invariants?

pureEvaluate :: ABT Term abt => TermEvaluator abt (Eval abt)

Call evaluate on a term. This variant returns something in the Eval monad so you can string multiple evaluation calls together. For the non-monadic version, see runPureEvaluate.

The pure-evaluation monad

List-based version

data ListContext abt p

An ordered collection of statements representing the context surrounding the current focus of our program transformation. That is, since some transformations work from the bottom up, we need to keep track of the statements we passed along the way when reaching for the bottom.

The tail of the list takes scope over the head of the list. Thus, the back/end of the list is towards the top of the program, whereas the front of the list is towards the bottom.

This type was formerly called Heap (presumably due to the Statement type being called Binding) but that seems like a misnomer to me since this really has nothing to do with allocation. However, it is still like a heap inasmuch as it's a dependency graph and we may wish to change the topological sorting or remove "garbage" (subject to correctness criteria).

TODO: Figure out what to do with SWeight, SGuard, SStuff, etc, so that we can use an IntMap (Statement abt) in order to speed up the lookup times in select. (Assuming callers don't use unsafePush unsafely: we can recover the order things were inserted from their varID since we've freshened them all and therefore their IDs are monotonic in the insertion order.)

Constructors

ListContext

Fields

• nextFreshNat :: !Nat
• statements :: [Statement abt p]

type PureAns abt a = ListContext abt Pure -> abt '[] a

newtype Eval abt x

Constructors

Eval

Fields

• unEval :: forall a. (x -> PureAns abt a) -> PureAns abt a

Instances

ABT Hakaru Term abt => EvaluationMonad abt (Eval abt) Pure

Methods

freshNat :: Eval abt Nat

freshenStatement :: Statement abt Pure -> Eval abt (Statement abt Pure, Assocs Hakaru (Variable Hakaru))

getIndices :: Eval abt [Index (abt [Hakaru])]

unsafePush :: Statement abt Pure -> Eval abt ()

unsafePushes :: [Statement abt Pure] -> Eval abt ()

select :: Variable Hakaru a -> (Statement abt Pure -> Maybe (Eval abt r)) -> Eval abt (Maybe r)

Monad (Eval abt)

Methods

(>>=) :: Eval abt a -> (a -> Eval abt b) -> Eval abt b

(>>) :: Eval abt a -> Eval abt b -> Eval abt b

return :: a -> Eval abt a

fail :: String -> Eval abt a

Functor (Eval abt)

Methods

fmap :: (a -> b) -> Eval abt a -> Eval abt b

(<$) :: a -> Eval abt b -> Eval abt a

Applicative (Eval abt)

Methods

pure :: a -> Eval abt a

(<*>) :: Eval abt (a -> b) -> Eval abt a -> Eval abt b

(*>) :: Eval abt a -> Eval abt b -> Eval abt b

(<*) :: Eval abt a -> Eval abt b -> Eval abt a

runEval :: (ABT Term abt, Foldable f) => Eval abt (abt '[] a) -> f (Some2 abt) -> abt '[] a

Run a computation in the Eval monad, residualizing out all the statements in the final evaluation context. The second argument should include all the terms altered by the Eval expression; this is necessary to ensure proper hygiene; for example(s):

runEval (pureEvaluate e) [Some2 e]

We use Some2 on the inputs because it doesn't matter what their type or locally-bound variables are, so we want to allow f to contain terms with different indices.

residualizePureListContext :: forall abt a. ABT Term abt => abt '[] a -> ListContext abt Pure -> abt '[] a

TODO: IntMap-based version