Tip.Simplify

Documentation

data SimplifyOpts a

Options for the simplifier

Constructors

SimplifyOpts

Fields

touch_lets :: Bool

Allow simplifications on lets

should_inline :: Maybe (Scope a) -> Expr a -> Bool

Inlining predicate

inline_match :: Bool

Allow function inlining to introduce match

gently :: SimplifyOpts a

Gentle options: if there is risk for code duplication, only inline atomic expressions

aggressively :: Name a => SimplifyOpts a

Aggressive options: inline everything that might plausibly lead to simplification

simplifyTheory :: Name a => SimplifyOpts a -> Theory a -> Fresh (Theory a)

Simplify an entire theory

simplifyExpr :: forall f a. (TransformBiM (WriterT Any Fresh) (Expr a) (f a), Name a) => SimplifyOpts a -> f a -> Fresh (f a)

Simplify an expression, without knowing its theory

simplifyExprIn :: forall f a. (TransformBiM (WriterT Any Fresh) (Expr a) (f a), Name a) => Maybe (Theory a) -> SimplifyOpts a -> f a -> Fresh (f a)

Simplify an expression within a theory

isConstructor :: Name a => Maybe (Scope a) -> Head a -> Bool