blob: de4c797384b5a2a02364273dd1c24c271b349583 (
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
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
|
Require Export String.
Require Export List.
Require Extraction.
Require Import Ascii.
Require Import BinNums.
Require Export ImpCore.
Require Export PArith.
Import Notations.
Local Open Scope impure.
(** Impure lazy andb of booleans *)
Definition iandb (k1 k2: ??bool): ?? bool :=
DO r1 <~ k1 ;;
if r1 then k2 else RET false.
Extraction Inline iandb. (* Juste pour l'efficacité à l'extraction ! *)
(** Strings for pretty-printing *)
Axiom caml_string: Type.
Extract Constant caml_string => "string".
(* New line *)
Definition nl: string := String (ascii_of_pos 10%positive) EmptyString.
Inductive pstring: Type :=
| Str: string -> pstring
| CamlStr: caml_string -> pstring
| Concat: pstring -> pstring -> pstring.
Coercion Str: string >-> pstring.
Bind Scope string_scope with pstring.
Notation "x +; y" := (Concat x y)
(at level 65, left associativity): string_scope.
(** Coq references *)
Record cref {A} := {
set: A -> ?? unit;
get: unit -> ?? A
}.
Arguments cref: clear implicits.
Axiom make_cref: forall {A}, A -> ?? cref A.
Extract Constant make_cref => "(fun x -> let r = ref x in { set = (fun y -> r:=y); get = (fun () -> !r) })".
(** Data-structure for a logger *)
Record logger {A:Type} := {
log_insert: A -> ?? unit;
log_info: unit -> ?? pstring;
}.
Arguments logger: clear implicits.
Axiom count_logger: unit -> ?? logger unit.
Extract Constant count_logger => "(fun () -> let count = ref 0 in { log_insert = (fun () -> count := !count + 1); log_info = (fun () -> (CamlStr (string_of_int !count))) })".
(** Axioms of Physical equality *)
Axiom phys_eq: forall {A}, A -> A -> ?? bool.
Axiom phys_eq_correct: forall A (x y:A), WHEN phys_eq x y ~> b THEN b=true -> x=y.
(* We only check here that above axioms are not trivially inconsistent...
(but this does not prove the correctness of the extraction directive below).
*)
Module PhysEqModel.
Definition phys_eq {A} (x y: A) := ret false.
Lemma phys_eq_correct: forall A (x y:A), WHEN phys_eq x y ~> b THEN b=true -> x=y.
Proof.
wlp_simplify. discriminate.
Qed.
End PhysEqModel.
Extract Inlined Constant phys_eq => "(==)".
Hint Resolve phys_eq_correct: wlp.
Axiom struct_eq: forall {A}, A -> A -> ?? bool.
Axiom struct_eq_correct: forall A (x y:A), WHEN struct_eq x y ~> b THEN if b then x=y else x<>y.
Extract Inlined Constant struct_eq => "(=)".
Hint Resolve struct_eq_correct: wlp.
(** Data-structure for generic hash-consing *)
Axiom hashcode: Type.
Extract Constant hashcode => "int".
(* NB: hashConsing is assumed to generate hash-code in ascending order.
This gives a way to check that a hash-consed value is older than an other one.
*)
Axiom hash_older: hashcode -> hashcode -> ?? bool.
Extract Inlined Constant hash_older => "(<)".
Module Dict.
Record hash_params {A:Type} := {
test_eq: A -> A -> ??bool;
test_eq_correct: forall x y, WHEN test_eq x y ~> r THEN r=true -> x=y;
hashing: A -> ??hashcode;
log: A -> ??unit (* for debugging only *)
}.
Arguments hash_params: clear implicits.
Record t {A B:Type} := {
set: A * B -> ?? unit;
get: A -> ?? option B
}.
Arguments t: clear implicits.
End Dict.
Module HConsingDefs.
Record hashinfo {A: Type} := {
hdata: A;
hcodes: list hashcode;
}.
Arguments hashinfo: clear implicits.
(* for inductive types with intrinsic hash-consing *)
Record hashP {A:Type}:= {
hash_eq: A -> A -> ?? bool;
get_hid: A -> hashcode;
set_hid: A -> hashcode -> A; (* WARNING: should only be used by hash-consing machinery *)
}.
Arguments hashP: clear implicits.
Axiom unknown_hid: hashcode.
Extract Constant unknown_hid => "-1".
Definition ignore_hid {A} (hp: hashP A) (hv:A) := set_hid hp hv unknown_hid.
Record hashExport {A:Type}:= {
get_info: hashcode -> ?? hashinfo A;
iterall: ((list pstring) -> hashcode -> hashinfo A -> ?? unit) -> ?? unit; (* iter on all elements in the hashtbl, by order of creation *)
}.
Arguments hashExport: clear implicits.
Record hashConsing {A:Type}:= {
hC: hashinfo A -> ?? A;
(**** below: debugging or internal functions ****)
next_hid: unit -> ?? hashcode; (* should be strictly less old than ignore_hid *)
remove: hashinfo A -> ??unit; (* SHOULD NOT BE USED ! *)
next_log: pstring -> ?? unit; (* insert a log info (for the next introduced element) -- regiven by [iterall export] below *)
export: unit -> ?? hashExport A ;
}.
Arguments hashConsing: clear implicits.
End HConsingDefs.
(** recMode: this is mainly for Tests ! *)
Inductive recMode:= StdRec | MemoRec | BareRec | BuggyRec.
(* This a copy-paste from definitions in CompCert/Lib/CoqLib.v *)
Lemma modusponens: forall (P Q: Prop), P -> (P -> Q) -> Q.
Proof. auto. Qed.
Ltac exploit x :=
refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _ _) _)
|| refine (modusponens _ _ (x _ _ _) _)
|| refine (modusponens _ _ (x _ _) _)
|| refine (modusponens _ _ (x _) _).
|
