1 files changed, 58 insertions, 0 deletions
diff --git a/backend/Duplicatepasses.v b/backend/Duplicatepasses.v
new file mode 100644
index 00000000..7e58eedf
--- /dev/null
+++ b/backend/Duplicatepasses.v
@@ -0,0 +1,58 @@
+Require Import RTL.
+Require Import Maps.
+Require Import Duplicate.
+Require Import Duplicateproof.
+
+(** Static Prediction *)
+
+Module StaticPredictOracle <: DuplicateOracle.
+  Axiom duplicate_aux : function -> code * node * (PTree.t node).
+  Extract Constant duplicate_aux => "Duplicateaux.static_predict".
+End StaticPredictOracle.
+
+Module Staticpredictproof := DuplicateProof StaticPredictOracle.
+
+Module Staticpredict := Staticpredictproof.
+
+(** Unrolling one iteration out of the body *)
+
+Module UnrollSingleOracle <: DuplicateOracle.
+  Axiom duplicate_aux : function -> code * node * (PTree.t node).
+  Extract Constant duplicate_aux => "Duplicateaux.unroll_single".
+End UnrollSingleOracle.
+
+Module Unrollsingleproof := DuplicateProof UnrollSingleOracle.
+
+Module Unrollsingle := Unrollsingleproof.
+
+(** Unrolling the body of innermost loops *)
+
+Module UnrollBodyOracle <: DuplicateOracle.
+  Axiom duplicate_aux : function -> code * node * (PTree.t node).
+  Extract Constant duplicate_aux => "Duplicateaux.unroll_body".
+End UnrollBodyOracle.
+
+Module Unrollbodyproof := DuplicateProof UnrollBodyOracle.
+
+Module Unrollbody := Unrollbodyproof.
+
+(** Tail Duplication *)
+
+Module TailDuplicateOracle <: DuplicateOracle.
+ Axiom duplicate_aux : function -> code * node * (PTree.t node).
+ Extract Constant duplicate_aux =>  "Duplicateaux.tail_duplicate".
+End TailDuplicateOracle.
+
+Module Tailduplicateproof := DuplicateProof TailDuplicateOracle.
+
+Module Tailduplicate := Tailduplicateproof.
+
+(** Loop Rotate *)
+
+Module LoopRotateOracle <: DuplicateOracle.
+  Axiom duplicate_aux : function -> code * node * (PTree.t node).
+  Extract Constant duplicate_aux =>  "Duplicateaux.loop_rotate".
+End LoopRotateOracle.
+
+Module Looprotateproof := DuplicateProof LoopRotateOracle.
+Module Looprotate := Looprotateproof.