Core Transform Specifications

This is the grammar for the transform specifications supplied to the -trans command of ddc, or set with the :set trans command of ddci-core.

TRANS   ::= 
 { TRANS }             Parenthesis.
 fix N TRANS           Transform to a fixpoint, or bail out after N iterations.
 TRANS; TRANS          Sequence two transforms.
 Id                    Return the original program unharmed.
 Anonymize             Anonymize names to deBruijn form.
 Namify                Introduce fresh names for deBruijn binders.
 Snip                  Introduce let-bindings for nested applications.
 SnipOver               ... and over-applications.
 Flatten               Flatten nested let-bindings.
 Beta                  Perform beta-reduction for value arguments.
 BetaLets               ... introducing new let-bindings for redex arguments.
 Bubble                Float casts outwards, and combine similar ones.
 Prune                 Erase unused, ineffectual let-bindings.
 Forward               Float let-bindings forward into their use sites.
 Rewrite               Perform rule based rewriting.
 Elaborate             Introduce default witnesses for unconstrained regions.
 Inline MODULE[NAME..] Perform inlining. Use '-with' to add source modules.
Last modified 7 years ago Last modified on Dec 19, 2012, 6:19:40 AM