Module Duplicatepasses

Require Import RTL.
Require Import Maps.
Require Import Duplicate.
Require Import Duplicateproof.


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.


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.


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.


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.


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.