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

class Visitable t where

Methods

visit :: Monoid a => Visitor a c -> c -> t -> VisitM a t

Instances

Visitable SortedReft

Defined in Language.Fixpoint.Types.Visitor

Methods

visit :: Monoid a => Visitor a c -> c -> SortedReft -> VisitM a SortedReft

Visitable Reft

Defined in Language.Fixpoint.Types.Visitor

Methods

visit :: Monoid a => Visitor a c -> c -> Reft -> VisitM a Reft

Visitable Expr

Defined in Language.Fixpoint.Types.Visitor

Methods

visit :: Monoid a => Visitor a c -> c -> Expr -> VisitM a Expr

Visitable BindEnv

Defined in Language.Fixpoint.Types.Visitor

Methods

visit :: Monoid a => Visitor a c -> c -> BindEnv -> VisitM a BindEnv

Visitable Rewrite

Defined in Language.Fixpoint.Types.Visitor

Methods

visit :: Monoid a => Visitor a c -> c -> Rewrite -> VisitM a Rewrite

Visitable Equation

Defined in Language.Fixpoint.Types.Visitor

Methods

visit :: Monoid a => Visitor a c -> c -> Equation -> VisitM a Equation

Visitable AxiomEnv

Defined in Language.Fixpoint.Types.Visitor

Methods

visit :: Monoid a => Visitor a c -> c -> AxiomEnv -> VisitM a AxiomEnv

Visitable Pred

Defined in Language.Fixpoint.Horn.Transformations

Methods

visit :: Monoid a => Visitor a c -> c -> Pred -> VisitM a Pred

Visitable (SimpC a)

Defined in Language.Fixpoint.Types.Visitor

Methods

visit :: Monoid a0 => Visitor a0 c -> c -> SimpC a -> VisitM a0 (SimpC a)

Visitable (SubC a)

Defined in Language.Fixpoint.Types.Visitor

Methods

visit :: Monoid a0 => Visitor a0 c -> c -> SubC a -> VisitM a0 (SubC a)

Visitable (Cstr a)

Defined in Language.Fixpoint.Horn.Transformations

Methods

visit :: Monoid a0 => Visitor a0 c -> c -> Cstr a -> VisitM a0 (Cstr a)

Visitable (Symbol, SortedReft)

Defined in Language.Fixpoint.Types.Visitor

Methods

visit :: Monoid a => Visitor a c -> c -> (Symbol, SortedReft) -> VisitM a (Symbol, SortedReft)

Visitable (c a) => Visitable (GInfo c a)

Defined in Language.Fixpoint.Types.Visitor

Methods

visit :: Monoid a0 => Visitor a0 c0 -> c0 -> GInfo c a -> VisitM a0 (GInfo c a)

Extracting Symbolic Constants (String Literals)

class SymConsts a where

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

Methods

symConsts :: a -> [SymConst]

Instances

SymConsts SortedReft

Defined in Language.Fixpoint.Types.Visitor

Methods

symConsts :: SortedReft -> [SymConst]

SymConsts Reft

Defined in Language.Fixpoint.Types.Visitor

Methods

symConsts :: Reft -> [SymConst]

SymConsts Expr

Defined in Language.Fixpoint.Types.Visitor

Methods

symConsts :: Expr -> [SymConst]

SymConsts BindEnv

Defined in Language.Fixpoint.Types.Visitor

Methods

symConsts :: BindEnv -> [SymConst]

SymConsts (SimpC a)

Defined in Language.Fixpoint.Types.Visitor

Methods

symConsts :: SimpC a -> [SymConst]

SymConsts (SubC a)

Defined in Language.Fixpoint.Types.Visitor

Methods

symConsts :: SubC a -> [SymConst]

SymConsts (c a) => SymConsts (GInfo c a)

Defined in Language.Fixpoint.Types.Visitor

Methods

symConsts :: GInfo c a -> [SymConst]

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

stripCasts :: Visitable t => t -> t

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

eapps :: Visitable t => t -> [Expr]

size :: Visitable t => t -> Integer

lamSize :: 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

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

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

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

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

Coercion Substitutions

type CoSub = HashMap Symbol Sort

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

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

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

(<$$>) :: Monad m => (a -> m b) -> [a] -> m [b]