DDC.Core.Simplifier

Simplifier Specifications

data Simplifier s a n

Specification of how to simplify a core program.

Constructors

Trans (Transform s a n)

Apply a single transform.

Seq (Simplifier s a n) (Simplifier s a n)

Apply two simplifiers in sequence.

Fix Int (Simplifier s a n)

Keep applying a transform until it reports that further applications won't be helpful, bailing out after a maximum number of applications.

Instances

Monoid (Simplifier s a n)

Pretty (Simplifier s a n)

Transform Specifications

data Transform s a n

Individual transforms to apply during simplification.

Constructors

Id

The Identity transform returns the original program unharmed.

Anonymize

Rewrite named binders to anonymous deBruijn binders.

Snip Config

Introduce let-bindings for nested applications.

Flatten

Flatten nested let and case expressions.

Beta Config

Perform beta reduction when the argument is not a redex.

Eta Config

Perform eta expansion and reduction.

Prune

Remove unused, pure let bindings.

Forward

Float single-use bindings forward into their use sites.

Bubble

Float casts outwards.

Elaborate

Elaborate possible Const and Distinct witnesses that aren't otherwise in the program.

Inline

Inline definitions into their use sites.

Fields

transInlineDef :: InlinerTemplates a n

Get the unfolding for a named variable.

Rewrite

Apply general rule-based rewrites.

Fields

transRules :: NamedRewriteRules a n

List of rewrite rules along with their names.

Namify

Rewrite anonymous binders to fresh named binders.

Fields

transMkNamifierT :: Env n -> Namifier s n

Create a namifier to make fresh type (level-1) names that don't conflict with any already in this environment.

transMkNamifierX :: Env n -> Namifier s n

Create a namifier to make fresh value or witness (level-0) names that don't conflict with any already in this environment.

Instances

Pretty (Transform s a n)

type InlinerTemplates a n = n -> Maybe (Exp a n)

Function to get the inliner template (unfolding) for the given name.

type NamedRewriteRules a n = [(String, RewriteRule a n)]

Rewrite rules along with their names.

Transform Results

data TransformResult r

Package up the result of applying a single transform.

Constructors

TransformResult

Fields

result :: r

Transform result proper (eg the new module)

resultProgress :: Bool

Whether this transform made any progess.

If False then the result program must be the same as the input program, and a simplifer fixpoint won't apply this transform again to the result program.

resultAgain :: Bool

Whether it might help to run the same transform again.

If False then a simplifier fixpoint won't apply this transform again to the result program.

resultInfo :: TransformInfo

Transform specific log. This might contain a count of what rules fired, or information about what parts of the program couldn't be processed.

Instances

Pretty (TransformResult r)

data TransformInfo

Existential package for a typeable thing, used in TransformResult.

Constructors

forall i . (Typeable i, Pretty i) => TransformInfo i

resultDone :: String -> r -> TransformResult r

Create a default result with no transform again.

We'll say we made progress, but set resultAgain to False so to stop any simplifier fixpoints.

Application

applySimplifier

Arguments

:: (Show a, Ord n, Show n, Pretty n)

=> Profile n

Profile of language we're working in

-> KindEnv n

Kind environment

-> TypeEnv n

Type environment

-> Simplifier s a n

Simplifier to apply

-> Module a n

Module to simplify

-> State s (TransformResult (Module a n))

Apply a simplifier to a module.

The state monad can be used by Namifier functions to generate fresh names.

applySimplifierX

Arguments

:: (Show a, Show n, Ord n, Pretty n)

=> Profile n

Profile of language we're working in

-> KindEnv n

Kind environment

-> TypeEnv n

Type environment

-> Simplifier s a n

Simplifier to apply

-> Exp a n

Expression to simplify

-> State s (TransformResult (Exp a n))

Apply a simplifier to an expression.

The state monad can be used by Namifier functions to generate fresh names.