DuplicateParam -> DuplicateOracle + simpler Duplicatepasses

1 files changed, 20 insertions, 36 deletions

diff --git a/backend/Duplicatepasses.v b/backend/Duplicatepasses.v
index f1770494..dc96f966 100644
--- a/backend/Duplicatepasses.v
+++ b/backend/Duplicatepasses.v
@@ -5,60 +5,44 @@ Require Import Duplicateproof.
 
 (** Static Prediction *)
 
-Axiom static_predict_aux : function -> code * node * (PTree.t node).
-Extract Constant static_predict_aux => "Duplicateaux.static_predict".
+Module StaticPredictOracle <: DuplicateOracle.
+  Axiom duplicate_aux : function -> code * node * (PTree.t node).
+  Extract Constant duplicate_aux => "Duplicateaux.static_predict".
+End StaticPredictOracle.
 
-Module StaticPredictParam <: DuplicateParam.
-  Definition duplicate_aux := static_predict_aux.
-End StaticPredictParam.
-
-Module StaticPredictDef := Duplicate StaticPredictParam.
-
-Module Staticpredictproof := DuplicateProof StaticPredictDef.
+Module Staticpredictproof := DuplicateProof StaticPredictOracle.
 
 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 UnrollSingleOracle <: DuplicateOracle.
+  Axiom duplicate_aux : function -> code * node * (PTree.t node).
+  Extract Constant duplicate_aux => "Duplicateaux.unroll_single".
+End UnrollSingleOracle.
 
-Module Unrollsingleproof := DuplicateProof UnrollSingleDef.
+Module Unrollsingleproof := DuplicateProof UnrollSingleOracle.
 
 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 UnrollBodyOracle <: DuplicateOracle.
+  Axiom duplicate_aux : function -> code * node * (PTree.t node).
+  Extract Constant duplicate_aux => "Duplicateaux.unroll_body".
+End UnrollBodyOracle.
 
-Module UnrollBodyParam <: DuplicateParam.
-  Definition duplicate_aux := unroll_body_aux.
-End UnrollBodyParam.
-
-Module UnrollBodyDef := Duplicate UnrollBodyParam.
-
-Module Unrollbodyproof := DuplicateProof UnrollBodyDef.
+Module Unrollbodyproof := DuplicateProof UnrollBodyOracle.
 
 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 TailDuplicateOracle <: DuplicateOracle.
+ Axiom duplicate_aux : function -> code * node * (PTree.t node).
+ Extract Constant duplicate_aux =>  "Duplicateaux.tail_duplicate".
+End TailDuplicateOracle.
 
-Module Tailduplicateproof := DuplicateProof TailDuplicateDef.
+Module Tailduplicateproof := DuplicateProof TailDuplicateOracle.
 
 Module Tailduplicate := Tailduplicateproof.
\ No newline at end of file