liquid-fixpoint-0.8.0.2: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver

Safe HaskellNone
LanguageHaskell98

Language.Fixpoint.Types.Visitor

Contents

Synopsis

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
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
SymConsts SortedReft Source # 
Instance details

Defined in Language.Fixpoint.Types.Visitor

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

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

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 #

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.

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 #