blob: f1770494bc7dd34a3b3b645c5e5b01244225de37 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
|
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.
|
