Safe Haskell | None |
---|
- 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 :: TVr -> E -> E -> E
- subst' :: TVr -> E -> E -> E
- substMap :: IdMap E -> E -> E
- substMap' :: IdMap E -> E -> E
- substMap'' :: IdMap (Maybe E) -> E -> E
- typeSubst :: IdMap (Maybe E) -> IdMap E -> E -> E
- typeSubst' :: IdMap E -> IdMap E -> E -> E
Documentation
Basic substitution routine
subst' :: TVr -> E -> E -> ESource
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.
:: 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.