| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Language.Fixpoint.Types.Substitutions
Contents
Description
This module contains the various instances for Subable,
which (should) depend on the visitors, and hence cannot
be in the same place as the Term definitions.
Synopsis
- mkSubst :: [(Symbol, Expr)] -> Subst
- isEmptySubst :: Subst -> Bool
- substExcept :: Subst -> [Symbol] -> Subst
- substfExcept :: (Symbol -> Expr) -> [Symbol] -> Symbol -> Expr
- subst1Except :: Subable a => [Symbol] -> a -> (Symbol, Expr) -> a
- substSymbolsSet :: Subst -> HashSet Symbol
- rapierSubstExpr :: HashSet Symbol -> Subst -> Expr -> Expr
- targetSubstSyms :: Subst -> [Symbol]
- filterSubst :: (Symbol -> Expr -> Bool) -> Subst -> Subst
- catSubst :: Subst -> Subst -> Subst
- exprSymbolsSet :: Expr -> HashSet Symbol
- extendSubst :: Subst -> Symbol -> Expr -> Subst
- meetReft :: Reft -> Reft -> Reft
- pprReft :: Reft -> Doc -> Doc
Documentation
isEmptySubst :: Subst -> Bool Source #
rapierSubstExpr :: HashSet Symbol -> Subst -> Expr -> Expr Source #
Rapier style capture-avoiding substitution
The scope set parameter must contain any symbols that are expected to appear free in the result expression. Typically, this is the set of symbols that are free in the range of the substitution, plus any symbols that are already free in the input expression.
targetSubstSyms :: Subst -> [Symbol] Source #