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

## Synopsis

- collectGlobals :: Set TmOccName -> [(Term, Term)] -> [Term] -> Term -> RewriteMonad NormalizeState (Term, [(Term, ([Term], CaseTree [Either Term Type]))])
- isDisjoint :: CaseTree [Either Term Type] -> Bool
- mkDisjointGroup :: Set TmOccName -> (Term, ([Term], CaseTree [Either Term Type])) -> RewriteMonad NormalizeState (Term, [Term])

# Documentation

:: Set TmOccName | |

-> [(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 TmOccName | 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.