tip-lib-0.2.2: tons of inductive problems - support library and tools

Safe HaskellNone
LanguageHaskell2010

Tip.Simplify

Synopsis

Documentation

data SimplifyOpts a Source

Options for the simplifier

Constructors

SimplifyOpts 

Fields

touch_lets :: Bool

Allow simplifications on lets

remove_variable_scrutinee_in_branches :: Bool

transform (match x (case (K y) (e x y))) to (match x (case (K y) (e (K y) y)) This is useful for triggering other known-case simplifications, and is therefore on by default.

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

Inlining predicate

inline_match :: Bool

Allow function inlining to introduce match

newtype Occurrences Source

Constructors

Occurrences Int 

gentlyNoInline :: SimplifyOpts a Source

Gentle, but without inlining

gently :: SimplifyOpts a Source

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

aggressively :: Name a => SimplifyOpts a Source

Aggressive options: inline everything that might plausibly lead to simplification

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

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) Source

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) Source

Simplify an expression within a theory

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

missingCase :: Name a => Maybe (Scope a) -> a -> [Case a] -> Maybe (Datatype a, Constructor a) Source

tryMatch :: Name a => Maybe (Scope a) -> Expr a -> [Case a] -> Maybe (Expr a) Source