Language.Fixpoint.Solver.Rewrite

Documentation

getRewrite :: AbstractOC oc Expr IO -> RewriteArgs -> oc -> SubExpr -> AutoRewrite -> MaybeT IO (Expr, oc)

subExprs :: Expr -> [SubExpr]

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

ordConstraints :: (Handle, Handle) -> AbstractOC (ConstraintsADT Op) Expr IO

convert :: Expr -> RuntimeTerm

passesTerminationCheck :: AbstractOC oc a IO -> RewriteArgs -> oc -> IO Bool

data RewriteArgs

Constructors

RWArgs

Fields

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

data RWTerminationOpts

Constructors

RWTerminationCheckEnabled

RWTerminationCheckDisabled

type SubExpr = (Expr, Expr -> Expr)

data TermOrigin

Constructors

PLE

RW

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

PPrint TermOrigin

Defined in Language.Fixpoint.Solver.Rewrite

Methods

pprintTidy :: Tidy -> TermOrigin -> Doc

pprintPrec :: Int -> Tidy -> TermOrigin -> Doc