E.Subst

Documentation

doSubst :: Bool -> Bool -> IdMap (Maybe E) -> E -> E

doSubst' :: Bool -> Bool -> IdMap E -> (Id -> Bool) -> E -> E

eAp :: E -> E -> E

litSMapM :: Monad m => (a -> m t) -> Lit a a -> m (Lit t t)

subst

Arguments

:: TVr

Variable to substitute

-> E

What to substitute with

-> E

input term

-> E

output term

Basic substitution routine

subst' :: TVr -> E -> E -> E

Identitcal to subst except that it substitutes inside the local types for variables in expressions. This should not be used because it breaks the sharing of types between a binding site of a variable and its uses and can lead to inconsistant terms. However, it is sometimes useful to create transient terms for typechecking.

substMap :: IdMap E -> E -> E

substMap' :: IdMap E -> E -> E

doesn't seed with free variables.

substMap'' :: IdMap (Maybe E) -> E -> E

doesn't seed with free variables.

typeSubst

Arguments

:: IdMap (Maybe E)

substitution to carry out at term level as well as a list of in-scope variables

-> IdMap E

substitution to carry out at type level

-> E -> E

the substitution function

substitution routine that can substitute different values at the term and type level. this is useful to enforce the invarient that let-bound variables must not occur at the type level, yet non-atomic values (even typelike ones) cannot appear in argument positions at the term level.

typeSubst' :: IdMap E -> IdMap E -> E -> E