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.