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
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* Certification of Imperative Programs / Jean-Christophe Filliâtre *)
(* $Id$ *)
open Names
open Term
open Termast
open Pattern
open Matching
open Pmisc
open Ptype
open Past
open Putil
open Prename
open Penv
open Peffect
open Ptyping
open Pmonad
let has_proof_part ren env c =
let sign = Pcicenv.trad_sign_of ren env in
let ty = Typing.type_of (Global.env_of_context sign) Evd.empty c in
Hipattern.is_matching_sigma (Reductionops.nf_betaiota ty)
(* main part: translation of imperative programs into functional ones.
*
* [env] is the environment
* [ren] is the current renamings of variables
* [t] is the imperative program to translate, annotated with type+effects
*
* we return the translated program in type cc_term
*)
let rec trad ren t =
let env = t.info.env in
trad_desc ren env t.info.kappa t.desc
and trad_desc ren env ct d =
let (_,tt),eft,pt,qt = ct in
match d with
| Expression c ->
let ids = get_reads eft in
let al = current_vars ren ids in
let c' = subst_in_constr al c in
if has_proof_part ren env c' then
CC_expr c'
else
let ty = trad_ml_type_v ren env tt in
make_tuple [ CC_expr c',ty ] qt ren env (current_date ren)
| Variable id ->
if is_mutable_in_env env id then
invalid_arg "Mlise.trad_desc"
else if is_local env id then
CC_var id
else
CC_expr (constant (string_of_id id))
| Acc _ ->
failwith "Mlise.trad: pure terms are supposed to be expressions"
| TabAcc (check, x, e1) ->
let _,ty_elem,_ = array_info ren env x in
let te1 = trad ren e1 in
let (_,ef1,p1,q1) = e1.info.kappa in
let w = get_writes ef1 in
let ren' = next ren w in
let id = id_of_string "index" in
let access =
make_raw_access ren' env (x,current_var ren' x) (mkVar id)
in
let t,ty = result_tuple ren' (current_date ren) env
(CC_expr access, ty_elem) (eft,qt) in
let t =
if check then
let h = make_pre_access ren env x (mkVar id) in
let_in_pre ty (anonymous_pre true h) t
else
t
in
make_let_in ren env te1 p1
(current_vars ren' w,q1) (id,constant "Z") (t,ty)
| Aff (x, e1) ->
let tx = trad_type_in_env ren env x in
let te1 = trad ren e1 in
let (_,ef1,p1,q1) = e1.info.kappa in
let w1 = get_writes ef1 in
let ren' = next ren (x::w1) in
let t_ty = result_tuple ren' (current_date ren) env
(CC_expr (constant "tt"), constant "unit") (eft,qt)
in
make_let_in ren env te1 p1
(current_vars ren' w1,q1) (current_var ren' x,tx) t_ty
| TabAff (check, x, e1, e2) ->
let _,ty_elem,ty_array = array_info ren env x in
let te1 = trad ren e1 in
let (_,ef1,p1,q1) = e1.info.kappa in
let w1 = get_writes ef1 in
let ren' = next ren w1 in
let te2 = trad ren' e2 in
let (_,ef2,p2,q2) = e2.info.kappa in
let w2 = get_writes ef2 in
let ren'' = next ren' w2 in
let id1 = id_of_string "index" in
let id2 = id_of_string "v" in
let ren''' = next ren'' [x] in
let t,ty = result_tuple ren''' (current_date ren) env
(CC_expr (constant "tt"), constant "unit") (eft,qt) in
let store = make_raw_store ren'' env (x,current_var ren'' x) (mkVar id1)
(mkVar id2) in
let t = make_let_in ren'' env (CC_expr store) [] ([],None)
(current_var ren''' x,ty_array) (t,ty) in
let t = make_let_in ren' env te2 p2
(current_vars ren'' w2,q2) (id2,ty_elem) (t,ty) in
let t =
if check then
let h = make_pre_access ren' env x (mkVar id1) in
let_in_pre ty (anonymous_pre true h) t
else
t
in
make_let_in ren env te1 p1
(current_vars ren' w1,q1) (id1,constant "Z") (t,ty)
| Seq bl ->
let before = current_date ren in
let finish ren = function
Some (id,ty) ->
result_tuple ren before env (CC_var id, ty) (eft,qt)
| None ->
failwith "a block should contain at least one statement"
in
let bl = trad_block ren env bl in
make_block ren env finish bl
| If (b, e1, e2) ->
let tb = trad ren b in
let _,efb,_,_ = b.info.kappa in
let ren' = next ren (get_writes efb) in
let te1 = trad ren' e1 in
let te2 = trad ren' e2 in
make_if ren env (tb,b.info.kappa) ren' (te1,e1.info.kappa)
(te2,e2.info.kappa) ct
(* Translation of the while. *)
| While (b, inv, var, bl) ->
let ren' = next ren (get_writes eft) in
let tb = trad ren' b in
let tbl = trad_block ren' env bl in
let var' = typed_var ren env var in
make_while ren env var' (tb,b.info.kappa) tbl (inv,ct)
| Lam (bl, e) ->
let bl' = trad_binders ren env bl in
let env' = traverse_binders env bl in
let ren' = initial_renaming env' in
let te = trans ren' e in
CC_lam (bl', te)
| SApp ([Variable id; Expression q1; Expression q2], [e1; e2])
when id = connective_and or id = connective_or ->
let c = constant (string_of_id id) in
let te1 = trad ren e1
and te2 = trad ren e2 in
let q1' = apply_post ren env (current_date ren) (anonymous q1)
and q2' = apply_post ren env (current_date ren) (anonymous q2) in
CC_app (CC_expr c, [CC_expr q1'.a_value; CC_expr q2'.a_value; te1; te2])
| SApp ([Variable id; Expression q], [e]) when id = connective_not ->
let c = constant (string_of_id id) in
let te = trad ren e in
let q' = apply_post ren env (current_date ren) (anonymous q) in
CC_app (CC_expr c, [CC_expr q'.a_value; te])
| SApp _ ->
invalid_arg "mlise.trad (SApp)"
| Apply (f, args) ->
let trad_arg (ren,args) = function
| Term a ->
let ((_,tya),efa,_,_) as ca = a.info.kappa in
let ta = trad ren a in
let w = get_writes efa in
let ren' = next ren w in
ren', ta::args
| Refarg _ ->
ren, args
| Type v ->
let c = trad_ml_type_v ren env v in
ren, (CC_expr c)::args
in
let ren',targs = List.fold_left trad_arg (ren,[]) args in
let tf = trad ren' f in
let cf = f.info.kappa in
let c,(s,_,_),capp = effect_app ren env f args in
let tc_args =
List.combine
(List.rev targs)
(Util.map_succeed
(function
| Term x -> x.info.kappa
| Refarg _ -> failwith "caught"
| Type _ ->
(result_id,TypePure mkSet),Peffect.bottom,[],None)
args)
in
make_app env ren tc_args ren' (tf,cf) (c,s,capp) ct
| LetRef (x, e1, e2) ->
let (_,v1),ef1,p1,q1 = e1.info.kappa in
let te1 = trad ren e1 in
let tv1 = trad_ml_type_v ren env v1 in
let env' = add (x,Ref v1) env in
let ren' = next ren [x] in
let (_,v2),ef2,p2,q2 = e2.info.kappa in
let tv2 = trad_ml_type_v ren' env' v2 in
let te2 = trad ren' e2 in
let ren'' = next ren' (get_writes ef2) in
let t,ty = result_tuple ren'' (current_date ren) env
(CC_var result_id, tv2) (eft,qt) in
let t = make_let_in ren' env' te2 p2
(current_vars ren'' (get_writes ef2),q2)
(result_id,tv2) (t,ty) in
let t = make_let_in ren env te1 p1
(current_vars ren' (get_writes ef1),q1) (x,tv1) (t,ty)
in
t
| Let (x, e1, e2) ->
let (_,v1),ef1,p1,q1 = e1.info.kappa in
let te1 = trad ren e1 in
let tv1 = trad_ml_type_v ren env v1 in
let env' = add (x,v1) env in
let ren' = next ren (get_writes ef1) in
let (_,v2),ef2,p2,q2 = e2.info.kappa in
let tv2 = trad_ml_type_v ren' env' v2 in
let te2 = trad ren' e2 in
let ren'' = next ren' (get_writes ef2) in
let t,ty = result_tuple ren'' (current_date ren) env
(CC_var result_id, tv2) (eft,qt) in
let t = make_let_in ren' env' te2 p2
(current_vars ren'' (get_writes ef2),q2)
(result_id,tv2) (t,ty) in
let t = make_let_in ren env te1 p1
(current_vars ren' (get_writes ef1),q1) (x,tv1) (t,ty)
in
t
| LetRec (f,bl,v,var,e) ->
let (_,ef,_,_) as c =
match tt with Arrow(_,c) -> c | _ -> assert false in
let bl' = trad_binders ren env bl in
let env' = traverse_binders env bl in
let ren' = initial_renaming env' in
let (phi0,var') = find_recursion f e.info.env in
let te = trad ren' e in
let t = make_letrec ren' env' (phi0,var') f bl' (te,e.info.kappa) c in
CC_lam (bl', t)
| PPoint (s,d) ->
let ren' = push_date ren s in
trad_desc ren' env ct d
| Debug _ -> failwith "Mlise.trad: Debug: not implemented"
and trad_binders ren env = function
| [] ->
[]
| (_,BindType (Ref _ | Array _))::bl ->
trad_binders ren env bl
| (id,BindType v)::bl ->
let tt = trad_ml_type_v ren env v in
(id, CC_typed_binder tt) :: (trad_binders ren env bl)
| (id,BindSet)::bl ->
(id, CC_typed_binder mkSet) :: (trad_binders ren env bl)
| (_,Untyped)::_ -> invalid_arg "trad_binders"
and trad_block ren env = function
| [] ->
[]
| (Assert c)::block ->
(Assert c)::(trad_block ren env block)
| (Label s)::block ->
let ren' = push_date ren s in
(Label s)::(trad_block ren' env block)
| (Statement e)::block ->
let te = trad ren e in
let _,efe,_,_ = e.info.kappa in
let w = get_writes efe in
let ren' = next ren w in
(Statement (te,e.info.kappa))::(trad_block ren' env block)
and trans ren e =
let env = e.info.env in
let _,ef,p,_ = e.info.kappa in
let ty = trad_ml_type_c ren env e.info.kappa in
let ids = get_reads ef in
let al = current_vars ren ids in
let c = trad ren e in
let c = abs_pre ren env (c,ty) p in
let bl = binding_of_alist ren env al in
make_abs (List.rev bl) c
|
