From 2488c0eb8471eb07249a8b770c30c5cae2d629cc Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Wed, 28 Oct 2020 11:34:12 +0100 Subject: DuplicateParam -> DuplicateOracle + simpler Duplicatepasses --- backend/Duplicatepasses.v | 56 +++++++++++++++++------------------------------ 1 file changed, 20 insertions(+), 36 deletions(-) (limited to 'backend/Duplicatepasses.v') 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 -- cgit