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 := unroll_single_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 := unroll_body_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 := tail_duplicate_aux.
End TailDuplicateParam.

Module TailDuplicateDef := Duplicate TailDuplicateParam.

Module Tailduplicateproof := DuplicateProof TailDuplicateDef.

Module Tailduplicate := Tailduplicateproof.