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

Safe HaskellNone
LanguageHaskell98

Language.Fixpoint.Solver.Rewrite

Documentation

getRewrite :: RewriteArgs -> [(Expr, TermOrigin)] -> SubExpr -> AutoRewrite -> MaybeT IO (Expr, TermOrigin) Source #

subExprs :: Expr -> [SubExpr] Source #

unify :: [Symbol] -> Expr -> Expr -> Maybe Subst Source #

data RewriteArgs Source #

Constructors

RWArgs 

Fields

data RWTerminationOpts Source #

Constructors

RWTerminationCheckEnabled (Maybe Int) 
RWTerminationCheckDisabled 

type SubExpr = (Expr, Expr -> Expr) Source #

data TermOrigin Source #

Constructors

PLE 
RW OpOrdering 
Instances
Eq TermOrigin Source # 
Instance details

Defined in Language.Fixpoint.Solver.Rewrite

Methods

(==) :: TermOrigin -> TermOrigin -> Bool #

(/=) :: TermOrigin -> TermOrigin -> Bool #

Show TermOrigin Source # 
Instance details

Defined in Language.Fixpoint.Solver.Rewrite

Methods

showsPrec :: Int -> TermOrigin -> ShowS #

show :: TermOrigin -> String #

showList :: [TermOrigin] -> ShowS #