Safe Haskell | Safe-Inferred |
---|
- data RewriteEnv a n
- empty :: Ord n => RewriteEnv a n
- extend :: Ord n => Bind n -> RewriteEnv a n -> RewriteEnv a n
- extendLets :: Ord n => Lets a n -> RewriteEnv a n -> RewriteEnv a n
- containsRegion :: Ord n => Bound n -> RewriteEnv a n -> Bool
- containsWitness :: Ord n => Type n -> RewriteEnv a n -> Bool
- getWitnesses :: Ord n => RewriteEnv a n -> [Type n]
- insertDef :: Bind n -> Maybe (Exp a n) -> RewriteEnv a n -> RewriteEnv a n
- getDef :: (Ord n, MapBoundX (Exp a) n) => Bound n -> RewriteEnv a n -> Maybe (Exp a n)
- hasDef :: (Ord n, MapBoundX (Exp a) n) => Bound n -> RewriteEnv a n -> Bool
- lift :: Bind n -> RewriteEnv a n -> RewriteEnv a n
- liftValue :: Bind n -> RewriteEnv a n -> RewriteEnv a n
Documentation
data RewriteEnv a n Source
A summary of the environment that we perform a rewrite in.
As we decend into the program looking for expressions to rewrite,
we keep track of what information as been defined in the environment
in a RewriteEnv
.
When we go under an anonymous binder then we push a new outermost list instead of lifting every element on the environment eagerly.
(Eq a, Eq n) => Eq (RewriteEnv a n) | |
(Show a, Show n) => Show (RewriteEnv a n) |
empty :: Ord n => RewriteEnv a nSource
An empty environment.
extend :: Ord n => Bind n -> RewriteEnv a n -> RewriteEnv a nSource
Extend an environment with some lambda-bound binder (XLam) Might be a witness. Don't count if it's a region.
extendLets :: Ord n => Lets a n -> RewriteEnv a n -> RewriteEnv a nSource
Extend an environment with the variables bount by these let-bindings.
If it's a letregion, remember the region's name and any witnesses.
containsRegion :: Ord n => Bound n -> RewriteEnv a n -> BoolSource
Check whether an environment contains the given region, bound by a letregion.
containsWitness :: Ord n => Type n -> RewriteEnv a n -> BoolSource
Check if the witness map in the given environment.
getWitnesses :: Ord n => RewriteEnv a n -> [Type n]Source
Get a list of all the witness types in an environment, normalising their indices.
insertDef :: Bind n -> Maybe (Exp a n) -> RewriteEnv a n -> RewriteEnv a nSource
Insert a rewrite definition into the environment.
getDef :: (Ord n, MapBoundX (Exp a) n) => Bound n -> RewriteEnv a n -> Maybe (Exp a n)Source
Lookup the definition of some let-bound variable from the environment.
lift :: Bind n -> RewriteEnv a n -> RewriteEnv a nSource
Raise all elements in witness map if binder is anonymous. Only call with type binders: ie XLAM, not XLam
liftValue :: Bind n -> RewriteEnv a n -> RewriteEnv a nSource
Raise all elements in definitions map if binder is anonymous Use for *value* binders, not type binders.