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)

Methods

mempty :: Simplifier s a n

mappend :: Simplifier s a n -> Simplifier s a n -> Simplifier s a n

mconcat :: [Simplifier s a n] -> Simplifier s a n

Pretty (Simplifier s a n)

Associated Types

data PrettyMode (Simplifier s a n) :: *

Methods

pprDefaultMode :: PrettyMode (Simplifier s a n)

ppr :: Simplifier s a n -> Doc

pprPrec :: Int -> Simplifier s a n -> Doc

pprModePrec :: PrettyMode (Simplifier s a n) -> Int -> Simplifier s a n -> Doc

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.

Beta Config

Perform beta reduction when the argument is not a redex.

Bubble

Float casts outwards.

Elaborate

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

Eta Config

Perform eta expansion and reduction.

Flatten

Flatten nested let and case expressions.

Forward

Float single-use bindings forward into their use sites.

FoldCase Config

Fold case expressions.

Inline

Inline definitions into their use sites.

Fields

• transInlineDef :: InlinerTemplates a n

  Get the unfolding for a named variable.

Lambdas

Perform lambda lifting.

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.

Prune

Remove unused, pure let bindings.

Rewrite

Apply general rule-based rewrites.

Fields

• transRules :: NamedRewriteRules a n

  List of rewrite rules along with their names.

Snip Config

Introduce let-bindings for nested applications.

Instances

Pretty (Transform s a n)

Associated Types

data PrettyMode (Transform s a n) :: *

Methods

pprDefaultMode :: PrettyMode (Transform s a n)

ppr :: Transform s a n -> Doc

pprPrec :: Int -> Transform s a n -> Doc

pprModePrec :: PrettyMode (Transform s a n) -> Int -> Transform s a n -> Doc

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)

Associated Types

data PrettyMode (TransformResult r) :: *

Methods

pprDefaultMode :: PrettyMode (TransformResult r)

ppr :: TransformResult r -> Doc

pprPrec :: Int -> TransformResult r -> Doc

pprModePrec :: PrettyMode (TransformResult r) -> Int -> TransformResult r -> Doc

data TransformInfo

Existential package for a typeable thing, used in TransformResult.

Constructors

(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, Pretty a, Ord n, Show n, Pretty n, CompoundName 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, Pretty a, Show n, Ord n, Pretty n, CompoundName 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.