Language.Fixpoint.Types.Visitor

Visitor

data Visitor acc ctx

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

Extracting Symbolic Constants (String Literals)

class SymConsts a where

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

Methods

symConsts :: a -> [SymConst]

Instances

SymConsts SortedReft

SymConsts Reft

SymConsts Expr

SymConsts BindEnv

SymConsts (FInfo a)

SymConsts (SubC a)

Default Visitor

defaultVisitor :: Monoid acc => Visitor acc ctx

Transformers

trans :: (Visitable t, Monoid a) => Visitor a ctx -> ctx -> a -> t -> t

Accumulators

fold :: (Visitable t, Monoid a) => Visitor a ctx -> ctx -> a -> t -> a

Clients

kvars :: Visitable t => t -> [KVar]

size :: Visitable t => t -> Integer

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

envKVarsN :: TaggedC c a => BindEnv -> 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

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

Predicates on Constraints

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

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

Sorts

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

Visitors over Sort

mapSort :: (Sort -> Sort) -> Sort -> Sort