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

Safe HaskellNone
LanguageHaskell98

Language.Fixpoint.Visitor

Contents

Synopsis

Visitor

data Visitor acc ctx Source

Constructors

Visitor 

Fields

ctxExpr :: ctx -> Expr -> ctx

Context ctx is built up in a "top-down" fashion but not across siblings

ctxPred :: ctx -> Pred -> ctx
 
txExpr :: ctx -> Expr -> Expr

Transforms can access current ctx

txPred :: ctx -> Pred -> Pred
 
accExpr :: ctx -> Expr -> acc

Accumulations can access current ctx; acc value is monoidal

accPred :: ctx -> Pred -> acc
 

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