Language.Fixpoint.Solver.Rewrite

Documentation

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

subExprs :: Expr -> [SubExpr]

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

data RewriteArgs

Constructors

RWArgs

Fields

• isRWValid :: Expr -> IO Bool
• rwTerminationOpts :: RWTerminationOpts

data RWTerminationOpts

Constructors

RWTerminationCheckEnabled (Maybe Int)

RWTerminationCheckDisabled

type SubExpr = (Expr, Expr -> Expr)

data TermOrigin

Constructors

PLE

RW OpOrdering

Instances

Eq TermOrigin

Defined in Language.Fixpoint.Solver.Rewrite

Methods

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

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

Show TermOrigin

Defined in Language.Fixpoint.Solver.Rewrite

Methods

showsPrec :: Int -> TermOrigin -> ShowS

show :: TermOrigin -> String

showList :: [TermOrigin] -> ShowS