Copyright | (C) 2015-2016, University of Twente |
---|---|
License | BSD2 (see the file LICENSE) |
Maintainer | Christiaan Baaij <christiaan.baaij@gmail.com> |
Safe Haskell | None |
Language | Haskell2010 |
Helper functions for the disjointExpressionConsolidation
transformation
The disjointExpressionConsolidation
transformation lifts applications of
global binders out of alternatives of case-statements.
e.g. It converts:
case x of A -> f 3 y B -> f x x C -> h x
into:
let f_arg0 = case x of {A -> 3; B -> x} f_arg1 = case x of {A -> y; B -> x} f_out = f f_arg0 f_arg1 in case x of A -> f_out B -> f_out C -> h x
- collectGlobals :: Set TmName -> [(Term, Term)] -> [Term] -> Term -> RewriteMonad NormalizeState (Term, [(Term, ([Term], CaseTree [Either Term Type]))])
- isDisjoint :: CaseTree [Either Term Type] -> Bool
- mkDisjointGroup :: Set TmName -> (Term, ([Term], CaseTree [Either Term Type])) -> RewriteMonad NormalizeState (Term, [Term])
Documentation
:: Set TmName | |
-> [(Term, Term)] | Substitution of (applications of) a global binder by a reference to a lifted term. |
-> [Term] | List of already seen global binders |
-> Term | The expression |
-> RewriteMonad NormalizeState (Term, [(Term, ([Term], CaseTree [Either Term Type]))]) |
Collect CaseTree
s for (potentially) disjoint applications of globals out
of an expression. Also substitute truly disjoint applications of globals by a
reference to a lifted out application.
isDisjoint :: CaseTree [Either Term Type] -> Bool Source #
Test if a CaseTree
collected from an expression indicates that
application of a global binder is disjoint: occur in separate branches of a
case-expression.
:: Set TmName | Current free variables. |
-> (Term, ([Term], CaseTree [Either Term Type])) | Case-tree of arguments belonging to the applied term. |
-> RewriteMonad NormalizeState (Term, [Term]) |
Given a case-tree corresponding to a disjoint interesting "term-in-a- function-position", return a let-expression: where the let-binding holds a case-expression selecting between the uncommon arguments of the case-tree, and the body is an application of the term applied to the common arguments of the case tree, and projections of let-binding corresponding to the uncommon argument positions.