From f82bf792fdf0c03b5c76f4cef5c39d5f1fd32b81 Mon Sep 17 00:00:00 2001
From: Cyril SIX <cyril.six@kalray.eu>
Date: Tue, 27 Oct 2020 15:59:25 +0100
Subject: Oops forgot Duplicatepasses.v

---
 backend/Duplicatepasses.v | 64 +++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 64 insertions(+)
 create mode 100644 backend/Duplicatepasses.v

(limited to 'backend/Duplicatepasses.v')

diff --git a/backend/Duplicatepasses.v b/backend/Duplicatepasses.v
new file mode 100644
index 00000000..7f007251
--- /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 := static_predict_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 := static_predict_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 := static_predict_aux.
+End TailDuplicateParam.
+
+Module TailDuplicateDef := Duplicate TailDuplicateParam.
+
+Module Tailduplicateproof := DuplicateProof TailDuplicateDef.
+
+Module Tailduplicate := Tailduplicateproof.
\ No newline at end of file
-- 
cgit