diff options
Diffstat (limited to 'backend/Duplicatepasses.v')
| -rw-r--r-- | backend/Duplicatepasses.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/backend/Duplicatepasses.v b/backend/Duplicatepasses.v index 7e58eedf..ffab2f59 100644 --- a/backend/Duplicatepasses.v +++ b/backend/Duplicatepasses.v @@ -56,3 +56,13 @@ End LoopRotateOracle. Module Looprotateproof := DuplicateProof LoopRotateOracle. Module Looprotate := Looprotateproof. + +(** Lift If (TODO: this is a working title) *) + +Module LiftIfOracle <: DuplicateOracle. + Axiom duplicate_aux : function -> code * node * (PTree.t node). + Extract Constant duplicate_aux => "Duplicateaux.lift_if". +End LiftIfOracle. + +Module Liftifproof := DuplicateProof LiftIfOracle. +Module Liftif := Liftifproof. |