1 files changed, 64 insertions, 0 deletions
diff --git a/backend/Duplicatepasses.v b/backend/Duplicatepasses.v
new file mode 100644
index 00000000..f1770494
--- /dev/null
+++ b/backend/Duplicatepasses.v
@@ -0,0 +1,64 @@
+Require Import RTL.
+Require Import Maps.
+Require Import Duplicate.
+Require Import Duplicateproof.
+
+(** Static Prediction *)
+
+Axiom static_predict_aux : function -> code * node * (PTree.t node).
+Extract Constant static_predict_aux => "Duplicateaux.static_predict".
+
+Module StaticPredictParam <: DuplicateParam.
+  Definition duplicate_aux := static_predict_aux.
+End StaticPredictParam.
+
+Module StaticPredictDef := Duplicate StaticPredictParam.
+
+Module Staticpredictproof := DuplicateProof StaticPredictDef.
+
+Module Staticpredict := Staticpredictproof.
+
+(** Unrolling one iteration out of the body *)
+
+Axiom unroll_single_aux : function -> code * node * (PTree.t node).
+Extract Constant unroll_single_aux => "Duplicateaux.unroll_single".
+
+Module UnrollSingleParam <: DuplicateParam.
+  Definition duplicate_aux := unroll_single_aux.
+End UnrollSingleParam.
+
+Module UnrollSingleDef := Duplicate UnrollSingleParam.
+
+Module Unrollsingleproof := DuplicateProof UnrollSingleDef.
+
+Module Unrollsingle := Unrollsingleproof.
+
+(** Unrolling the body of innermost loops *)
+
+Axiom unroll_body_aux : function -> code * node * (PTree.t node).
+Extract Constant unroll_body_aux => "Duplicateaux.unroll_body".
+
+Module UnrollBodyParam <: DuplicateParam.
+  Definition duplicate_aux := unroll_body_aux.
+End UnrollBodyParam.
+
+Module UnrollBodyDef := Duplicate UnrollBodyParam.
+
+Module Unrollbodyproof := DuplicateProof UnrollBodyDef.
+
+Module Unrollbody := Unrollbodyproof.
+
+(** Tail Duplication *)
+
+Axiom tail_duplicate_aux : function -> code * node * (PTree.t node).
+Extract Constant tail_duplicate_aux => "Duplicateaux.tail_duplicate".
+
+Module TailDuplicateParam <: DuplicateParam.
+  Definition duplicate_aux := tail_duplicate_aux.
+End TailDuplicateParam.
+
+Module TailDuplicateDef := Duplicate TailDuplicateParam.
+
+Module Tailduplicateproof := DuplicateProof TailDuplicateDef.
+
+Module Tailduplicate := Tailduplicateproof.
+\ No newline at end of file