Safe Haskell	Safe-Inferred
Language	Haskell98

Language.Fixpoint.Types.Visitor

Contents

Visitor
Extracting Symbolic Constants (String Literals)
Default Visitor
Transformers
Accumulators
Clients
Coercion Substitutions
Predicates on Constraints
Sorts

Synopsis

data Folder acc ctx = Visitor {
- ctxExpr :: ctx -> Expr -> ctx
- txExpr :: ctx -> Expr -> Expr
- accExpr :: ctx -> Expr -> acc
}
class Foldable t where
- foldE :: Monoid a => Folder a c -> c -> t -> FoldM a t
class Visitable t where
- transE :: (Expr -> Expr) -> t -> t
class SymConsts a where
- symConsts :: a -> [SymConst]
defaultFolder :: Monoid acc => Folder acc ctx
trans :: Visitable t => (Expr -> Expr) -> t -> t
fold :: (Foldable t, Monoid a) => Folder a ctx -> ctx -> a -> t -> a
stripCasts :: Expr -> Expr
kvarsExpr :: ExprV v -> [KVar]
eapps :: Foldable t => t -> [Expr]
size :: Foldable t => t -> Integer
lamSize :: Foldable t => t -> Integer
envKVars :: TaggedC c a => BindEnv a -> c a -> [KVar]
envKVarsN :: TaggedC c a => BindEnv a -> c a -> [(KVar, Int)]
rhsKVars :: TaggedC c a => c a -> [KVar]
mapKVars :: Visitable t => (KVar -> Maybe Expr) -> t -> t
mapKVars' :: Visitable t => ((KVar, Subst) -> Maybe Expr) -> t -> t
mapGVars' :: Visitable t => ((KVar, Subst) -> Maybe Expr) -> t -> t
mapKVarSubsts :: Visitable t => (KVar -> Subst -> Subst) -> t -> t
mapExpr :: Visitable t => (Expr -> Expr) -> t -> t
mapExprOnExpr :: (Expr -> Expr) -> Expr -> Expr
mapMExpr :: Monad m => (Expr -> m Expr) -> Expr -> m Expr
type CoSub = HashMap Symbol Sort
applyCoSub :: CoSub -> Expr -> Expr
type CoSubV = HashMap Sort Sort
applyCoSubV :: CoSubV -> Expr -> Expr
isConcC :: TaggedC c a => c a -> Bool
isConc :: Expr -> Bool
isKvarC :: TaggedC c a => c a -> Bool
foldSort :: (a -> Sort -> a) -> a -> Sort -> a
mapSort :: (Sort -> Sort) -> Sort -> Sort
foldDataDecl :: (a -> Sort -> a) -> a -> DataDecl -> a

Visitor

data Folder acc ctx Source #

Constructors

Visitor
Fields ctxExpr :: ctx -> Expr -> ctx Context `ctx` is built in a "top-down" fashion; not "across" siblings txExpr :: ctx -> Expr -> Expr Transforms can access current `ctx` accExpr :: ctx -> Expr -> acc Accumulations can access current `ctx`; `acc` value is monoidal

class Foldable t where Source #

Methods

foldE :: Monoid a => Folder a c -> c -> t -> FoldM a t Source #

Instances

Instances details

Foldable Pred Source #
Instance details Defined in Language.Fixpoint.Horn.Transformations Methods foldE :: Monoid a => Folder a c -> c -> Pred -> FoldM a Pred Source #
Foldable AxiomEnv Source #
Instance details Defined in Language.Fixpoint.Types.Visitor Methods foldE :: Monoid a => Folder a c -> c -> AxiomEnv -> FoldM a AxiomEnv Source #
Foldable Equation Source #
Instance details Defined in Language.Fixpoint.Types.Visitor Methods foldE :: Monoid a => Folder a c -> c -> Equation -> FoldM a Equation Source #
Foldable Rewrite Source #
Instance details Defined in Language.Fixpoint.Types.Visitor Methods foldE :: Monoid a => Folder a c -> c -> Rewrite -> FoldM a Rewrite Source #
Foldable Expr Source #
Instance details Defined in Language.Fixpoint.Types.Visitor Methods foldE :: Monoid a => Folder a c -> c -> Expr -> FoldM a Expr Source #
Foldable Reft Source #
Instance details Defined in Language.Fixpoint.Types.Visitor Methods foldE :: Monoid a => Folder a c -> c -> Reft -> FoldM a Reft Source #
Foldable SortedReft Source #
Instance details Defined in Language.Fixpoint.Types.Visitor Methods foldE :: Monoid a => Folder a c -> c -> SortedReft -> FoldM a SortedReft Source #
Foldable (Cstr a) Source #
Instance details Defined in Language.Fixpoint.Horn.Transformations Methods foldE :: Monoid a0 => Folder a0 c -> c -> Cstr a -> FoldM a0 (Cstr a) Source #
Foldable (SimpC a) Source #
Instance details Defined in Language.Fixpoint.Types.Visitor Methods foldE :: Monoid a0 => Folder a0 c -> c -> SimpC a -> FoldM a0 (SimpC a) Source #
Foldable (SubC a) Source #
Instance details Defined in Language.Fixpoint.Types.Visitor Methods foldE :: Monoid a0 => Folder a0 c -> c -> SubC a -> FoldM a0 (SubC a) Source #
Foldable (BindEnv a) Source #
Instance details Defined in Language.Fixpoint.Types.Visitor Methods foldE :: Monoid a0 => Folder a0 c -> c -> BindEnv a -> FoldM a0 (BindEnv a) Source #
Foldable (c a) => Foldable (GInfo c a) Source #
Instance details Defined in Language.Fixpoint.Types.Visitor Methods foldE :: Monoid a0 => Folder a0 c0 -> c0 -> GInfo c a -> FoldM a0 (GInfo c a) Source #
Foldable (Symbol, SortedReft, a) Source #
Instance details Defined in Language.Fixpoint.Types.Visitor Methods foldE :: Monoid a0 => Folder a0 c -> c -> (Symbol, SortedReft, a) -> FoldM a0 (Symbol, SortedReft, a) Source #

class Visitable t where Source #

Methods

transE :: (Expr -> Expr) -> t -> t Source #

Instances

Instances details

Visitable AxiomEnv Source #
Instance details Defined in Language.Fixpoint.Types.Visitor Methods transE :: (Expr -> Expr) -> AxiomEnv -> AxiomEnv Source #
Visitable Equation Source #
Instance details Defined in Language.Fixpoint.Types.Visitor Methods transE :: (Expr -> Expr) -> Equation -> Equation Source #
Visitable Rewrite Source #
Instance details Defined in Language.Fixpoint.Types.Visitor Methods transE :: (Expr -> Expr) -> Rewrite -> Rewrite Source #
Visitable Expr Source #
Instance details Defined in Language.Fixpoint.Types.Visitor Methods transE :: (Expr -> Expr) -> Expr -> Expr Source #
Visitable Reft Source #
Instance details Defined in Language.Fixpoint.Types.Visitor Methods transE :: (Expr -> Expr) -> Reft -> Reft Source #
Visitable SortedReft Source #
Instance details Defined in Language.Fixpoint.Types.Visitor Methods transE :: (Expr -> Expr) -> SortedReft -> SortedReft Source #
Visitable (SimpC a) Source #
Instance details Defined in Language.Fixpoint.Types.Visitor Methods transE :: (Expr -> Expr) -> SimpC a -> SimpC a Source #
Visitable (SubC a) Source #
Instance details Defined in Language.Fixpoint.Types.Visitor Methods transE :: (Expr -> Expr) -> SubC a -> SubC a Source #
Visitable (BindEnv a) Source #
Instance details Defined in Language.Fixpoint.Types.Visitor Methods transE :: (Expr -> Expr) -> BindEnv a -> BindEnv a Source #
Visitable (c a) => Visitable (GInfo c a) Source #
Instance details Defined in Language.Fixpoint.Types.Visitor Methods transE :: (Expr -> Expr) -> GInfo c a -> GInfo c a Source #
Visitable (Symbol, SortedReft, a) Source #
Instance details Defined in Language.Fixpoint.Types.Visitor Methods transE :: (Expr -> Expr) -> (Symbol, SortedReft, a) -> (Symbol, SortedReft, a) Source #

Extracting Symbolic Constants (String Literals)

class SymConsts a where Source #

String Constants -----------------------------------------

Methods

symConsts :: a -> [SymConst] Source #

Instances

Instances details

SymConsts AxiomEnv Source #
Instance details Defined in Language.Fixpoint.Types.Visitor Methods symConsts :: AxiomEnv -> [SymConst] Source #
SymConsts Equation Source #
Instance details Defined in Language.Fixpoint.Types.Visitor Methods symConsts :: Equation -> [SymConst] Source #
SymConsts Rewrite Source #
Instance details Defined in Language.Fixpoint.Types.Visitor Methods symConsts :: Rewrite -> [SymConst] Source #
SymConsts Expr Source #
Instance details Defined in Language.Fixpoint.Types.Visitor Methods symConsts :: Expr -> [SymConst] Source #
SymConsts Reft Source #
Instance details Defined in Language.Fixpoint.Types.Visitor Methods symConsts :: Reft -> [SymConst] Source #
SymConsts SortedReft Source #
Instance details Defined in Language.Fixpoint.Types.Visitor Methods symConsts :: SortedReft -> [SymConst] Source #
SymConsts (SimpC a) Source #
Instance details Defined in Language.Fixpoint.Types.Visitor Methods symConsts :: SimpC a -> [SymConst] Source #
SymConsts (SubC a) Source #
Instance details Defined in Language.Fixpoint.Types.Visitor Methods symConsts :: SubC a -> [SymConst] Source #
SymConsts (BindEnv a) Source #
Instance details Defined in Language.Fixpoint.Types.Visitor Methods symConsts :: BindEnv a -> [SymConst] Source #
SymConsts a => SymConsts [a] Source #
Instance details Defined in Language.Fixpoint.Types.Visitor Methods symConsts :: [a] -> [SymConst] Source #
SymConsts (c a) => SymConsts (GInfo c a) Source #
Instance details Defined in Language.Fixpoint.Types.Visitor Methods symConsts :: GInfo c a -> [SymConst] Source #

Default Visitor

defaultFolder :: Monoid acc => Folder acc ctx Source #

Transformers

trans :: Visitable t => (Expr -> Expr) -> t -> t Source #

Accumulators

fold :: (Foldable t, Monoid a) => Folder a ctx -> ctx -> a -> t -> a Source #

Clients

stripCasts :: Expr -> Expr Source #

kvarsExpr :: ExprV v -> [KVar] Source #

eapps :: Foldable t => t -> [Expr] Source #

size :: Foldable t => t -> Integer Source #

lamSize :: Foldable t => t -> Integer Source #

envKVars :: TaggedC c a => BindEnv a -> c a -> [KVar] Source #

envKVarsN :: TaggedC c a => BindEnv a -> c a -> [(KVar, Int)] Source #

rhsKVars :: TaggedC c a => c a -> [KVar] Source #

mapKVars :: Visitable t => (KVar -> Maybe Expr) -> t -> t Source #

mapKVars' :: Visitable t => ((KVar, Subst) -> Maybe Expr) -> t -> t Source #

mapGVars' :: Visitable t => ((KVar, Subst) -> Maybe Expr) -> t -> t Source #

mapKVarSubsts :: Visitable t => (KVar -> Subst -> Subst) -> t -> t Source #

mapExpr :: Visitable t => (Expr -> Expr) -> t -> t Source #

mapExprOnExpr :: (Expr -> Expr) -> Expr -> Expr Source #

Specialized and faster version of mapExpr for expressions

mapMExpr :: Monad m => (Expr -> m Expr) -> Expr -> m Expr Source #

Coercion Substitutions

type CoSub = HashMap Symbol Sort Source #

CoSub is a map from (coercion) ty-vars represented as 'FObj s' to the ty-vars that they should be substituted with. Note the domain and range are both Symbol and not the Int used for real ty-vars.

applyCoSub :: CoSub -> Expr -> Expr Source #

type CoSubV = HashMap Sort Sort Source #

applyCoSubV :: CoSubV -> Expr -> Expr Source #

Predicates on Constraints

isConcC :: TaggedC c a => c a -> Bool Source #

isConc :: Expr -> Bool Source #

isKvarC :: TaggedC c a => c a -> Bool Source #

Sorts

foldSort :: (a -> Sort -> a) -> a -> Sort -> a Source #

Visitors over Sort

mapSort :: (Sort -> Sort) -> Sort -> Sort Source #

foldDataDecl :: (a -> Sort -> a) -> a -> DataDecl -> a Source #