Safe Haskell	None
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 Visitor acc ctx = Visitor {
- ctxExpr :: ctx -> Expr -> ctx
- txExpr :: ctx -> Expr -> Expr
- accExpr :: ctx -> Expr -> acc
}
class Visitable t where
- visit :: Monoid a => Visitor a c -> c -> t -> VisitM a t
class SymConsts a where
- symConsts :: a -> [SymConst]
defaultVisitor :: Monoid acc => Visitor acc ctx
trans :: (Visitable t, Monoid a) => Visitor a ctx -> ctx -> a -> t -> t
fold :: (Visitable t, Monoid a) => Visitor a ctx -> ctx -> a -> t -> a
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
type CoSub = HashMap Symbol Sort
applyCoSub :: CoSub -> Expr -> Expr
isConcC :: TaggedC c a => c a -> 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
(<$$>) :: Monad m => (a -> m b) -> [a] -> m [b]

Visitor

data Visitor 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 Visitable t where Source #

Methods

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

Instances

Instances details

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

Extracting Symbolic Constants (String Literals)

class SymConsts a where Source #

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

Methods

symConsts :: a -> [SymConst] Source #

Instances

Instances details

SymConsts SortedReft Source #
Instance details Defined in Language.Fixpoint.Types.Visitor Methods symConsts :: SortedReft -> [SymConst] Source #
SymConsts Reft Source #
Instance details Defined in Language.Fixpoint.Types.Visitor Methods symConsts :: Reft -> [SymConst] Source #
SymConsts Expr Source #
Instance details Defined in Language.Fixpoint.Types.Visitor Methods symConsts :: Expr -> [SymConst] Source #
SymConsts BindEnv Source #
Instance details Defined in Language.Fixpoint.Types.Visitor Methods symConsts :: BindEnv -> [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 (c a) => SymConsts (GInfo c a) Source #
Instance details Defined in Language.Fixpoint.Types.Visitor Methods symConsts :: GInfo c a -> [SymConst] Source #

Default Visitor

defaultVisitor :: Monoid acc => Visitor acc ctx Source #

Transformers

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

Accumulators

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

Clients

stripCasts :: Visitable t => t -> t Source #

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

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

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

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

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

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

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 #

Predicates on Constraints

isConcC :: TaggedC c a => c a -> 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 #

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