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

(** Static Prediction *)

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.

(** Unrolling one iteration out of the body *)

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.

(** Unrolling the body of innermost loops *)

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.

(** Tail Duplication *)

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.

(** Loop Rotate *)

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.