MAJ terminée. Nous sommes passés en version 14.6.2 . Pour consulter les "releases notes" associées c'est ici :

https://about.gitlab.com/releases/2022/01/11/security-release-gitlab-14-6-2-released/
https://about.gitlab.com/releases/2022/01/04/gitlab-14-6-1-released/

pgm_typing.ml 36.8 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
(*    Francois Bobot                                                      *)
(*    Jean-Christophe Filliatre                                           *)
(*    Johannes Kanig                                                      *)
(*    Andrei Paskevich                                                    *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)

20
open Format
21
open Why
22
open Util
23
open Ident
24
open Ty
25
open Term
26
open Theory
27
28
open Denv
open Ptree
29
open Pgm_effect
30
open Pgm_ttree
31
open Pgm_env
32
module E = Pgm_effect
33

34
35
let debug = ref false

36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
type error =
  | Message of string

exception Error of error

let error ?loc e = match loc with
  | None -> raise (Error e)
  | Some loc -> raise (Loc.Located (loc, Error e))

let errorm ?loc f =
  let buf = Buffer.create 512 in
  let fmt = Format.formatter_of_buffer buf in
  Format.kfprintf
    (fun _ ->
       Format.pp_print_flush fmt ();
       let s = Buffer.contents buf in
       Buffer.clear buf;
       error ?loc (Message s))
    fmt f

let report fmt = function
  | Message s ->
      fprintf fmt "%s" s

60
61
let id_result = "result"

62
63
64
65
66
67
68
69
70
71
72
(* parsing LOGIC strings using functions from src/parser/
   requires proper relocation *)

let reloc loc lb =
  lb.Lexing.lex_curr_p <- loc;
  lb.Lexing.lex_abs_pos <- loc.Lexing.pos_cnum
    
let parse_string f loc s =
  let lb = Lexing.from_string s in
  reloc loc lb;
  f lb
73

74
75
76
77
let logic_list0_decl (loc, s) = parse_string Lexer.parse_list0_decl loc s
  
let lexpr (loc, s) = parse_string Lexer.parse_lexpr loc s

78
(* phase 1: typing programs (using destructive type inference) **************)
79

80
81
82
83
84
let dty_app (ts, tyl) = assert (ts.ts_def = None); Tyapp (ts, tyl)

let dty_bool gl = dty_app (gl.ts_bool, [])
let dty_unit gl = dty_app (gl.ts_unit, [])
let dty_label gl = dty_app (gl.ts_label, [])
85

86
87
(* note: local variables are sqimultaneously in locals (to type programs)
   and in denv (to type logic elements) *)
88
89
90
91
type denv = {
  env   : env;
  locals: dtype_v Mstr.t;
  denv  : Typing.denv;
92
}
93

94
95
96
97
98
let create_denv gl = 
  { env = gl;
    locals = Mstr.empty;
    denv = Typing.create_denv gl.uc; }

99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
let specialize_effect e =
  let reference r acc = match r with
    | Rlocal v -> DRlocal v.vs_name.id_string :: acc
    | Rglobal l -> DRglobal l :: acc
  in
  { de_reads  = Sref.fold reference e.reads  [];
    de_writes = Sref.fold reference e.writes [];
    de_raises = Sls.elements e.raises; }

let specialize_post ~loc htv ((v, f), ql) =
  assert (v.vs_name.id_string = "result"); (* TODO *)
  let specialize_exn (l, (v, f)) =
    assert 
      (match v with Some v -> v.vs_name.id_string = "result" | None -> true);
    (l, specialize_fmla ~loc htv f)
  in
  specialize_fmla ~loc htv f, List.map specialize_exn ql

117
118
119
120
121
122
123
124
let loc_of_id id = match id.id_origin with
  | User loc -> loc
  | _ -> assert false

let loc_of_ls ls = match ls.ls_name.id_origin with
  | User loc -> Some loc
  | _ -> None (* FIXME: loc for recursive functions *)

125
126
127
128
129
130
131
132
133
134
135
136
137
138
let rec specialize_type_v ~loc htv = function
  | Tpure ty ->
      DTpure (Denv.specialize_ty ~loc htv ty)
  | Tarrow (bl, c) ->
      DTarrow (List.map (specialize_binder ~loc htv) bl, 
	       specialize_type_c ~loc htv c)

and specialize_type_c ~loc htv c =
  { dc_result_type = specialize_type_v ~loc htv c.c_result_type;
    dc_effect      = specialize_effect c.c_effect;
    dc_pre         = specialize_fmla ~loc htv c.c_pre;
    dc_post        = specialize_post ~loc htv c.c_post; }

and specialize_binder ~loc htv (vs, tyv) =
139
140
  let id = { id = vs.vs_name.id_string; id_loc = loc } in
  id, specialize_type_v ~loc htv tyv
141

142
let specialize_global loc x gl =
143
  let s, tyv = Mstr.find x gl.globals in
144
  s, specialize_type_v ~loc (Htv.create 17) tyv
145

146
147
148
let specialize_exception loc x gl =
  if not (Mstr.mem x gl.exceptions) then errorm ~loc "unbound exception %s" x;
  let s = Mstr.find x gl.exceptions in
149
150
151
152
  match Denv.specialize_lsymbol ~loc s with
    | tyl, Some ty -> s, tyl, ty
    | _, None -> assert false

153
154
155
156
let create_type_var loc =
  let tv = Ty.create_tvsymbol (id_user "a" loc) in
  Tyvar (create_ty_decl_var ~loc ~user:false tv)

157
let dcurrying gl tyl ty =
158
  let make_arrow_type ty1 ty2 = dty_app (gl.ts_arrow, [ty1; ty2]) in
159
  List.fold_right make_arrow_type tyl ty
160

161
let uncurrying gl ty =
162
  let rec uncurry acc ty = match ty.ty_node with
163
164
165
166
    | Ty.Tyapp (ts, [t1; t2]) when ts_equal ts gl.ts_arrow -> 
	uncurry (t1 :: acc) t2
    | _ -> 
	List.rev acc, ty
167
168
169
  in
  uncurry [] ty

170
let expected_type e ty =
171
172
  if not (Denv.unify e.dexpr_type ty) then
    errorm ~loc:e.dexpr_loc 
173
      "this expression has type %a, but is expected to have type %a"
174
      print_dty e.dexpr_type print_dty ty
175

176
177
let pure_type env = Typing.dty env.denv

178
179
180
181
let rec dpurify env = function
  | DTpure ty -> 
      ty
  | DTarrow (bl, c) -> 
182
      dcurrying env.env (List.map (fun (_,ty) -> dpurify env ty) bl)
183
	(dpurify env c.dc_result_type)
184

185
let check_reference_type gl loc ty =
186
  let ty_ref = dty_app (gl.ts_ref, [create_type_var loc]) in
187
188
189
  if not (Denv.unify ty ty_ref) then
    errorm ~loc "this expression has type %a, but is expected to be a reference"
      print_dty ty
190
191
192
193
194
  
let dreference env id =
  if Typing.mem_var id.id env.denv then
    (* local variable *)
    let ty = Typing.find_var id.id env.denv in
195
    check_reference_type env.env id.id_loc ty;
196
197
198
    DRlocal id.id
  else 
    let p = Qident id in
199
200
    let s, _, ty = Typing.specialize_fsymbol p env.env.uc in
    check_reference_type env.env id.id_loc ty;
201
202
    DRglobal s

203
let dexception env id =
204
  let _, _, ty as r = specialize_exception id.id_loc id.id env.env in
205
  let ty_exn = dty_app (env.env.ts_exn, []) in
206
207
208
209
210
  if not (Denv.unify ty ty_exn) then
    errorm ~loc:id.id_loc
      "this expression has type %a, but is expected to be an exception"
      print_dty ty;
  r
211
212
213
214

let deffect env e =
  { de_reads  = List.map (dreference env) e.Pgm_ptree.pe_reads;
    de_writes = List.map (dreference env) e.Pgm_ptree.pe_writes;
215
216
217
    de_raises = 
      List.map (fun id -> let ls,_,_ = dexception env id in ls) 
	e.Pgm_ptree.pe_raises; }
218

219
220
221
let dterm env l = Typing.dterm env (lexpr l)
let dfmla env l = Typing.dfmla env (lexpr l)

222
223
224
225
226
227
228
229
let dpost env ty (q, ql) =
  let dexn (id, l) =
    let s, tyl, _ = dexception env id in
    let denv = match tyl with
      | [] -> env.denv
      | [ty] -> Typing.add_var id_result ty env.denv
      | _ -> assert false
    in
230
    s, dfmla denv l
231
232
  in
  let denv = Typing.add_var id_result ty env.denv in
233
  dfmla denv q, List.map dexn ql
234

235
236
237
238
239
240
let add_local env x tyv = 
  let ty = dpurify env tyv in
  { env with 
      locals = Mstr.add x tyv env.locals;
      denv = Typing.add_var x ty env.denv } 

241
242
243
244
245
246
247
248
249
250
let rec dtype_v env = function
  | Pgm_ptree.Tpure pt -> 
      DTpure (pure_type env pt)
  | Pgm_ptree.Tarrow (bl, c) -> 
      let env, bl = map_fold_left dbinder env bl in
      let c = dtype_c env c in
      DTarrow (bl, c) 

and dtype_c env c = 
  let ty = dtype_v env c.Pgm_ptree.pc_result_type in
251
  { dc_result_type = ty;
252
    dc_effect      = deffect env c.Pgm_ptree.pc_effect;
253
    dc_pre         = dfmla env.denv c.Pgm_ptree.pc_pre;
254
    dc_post        = dpost env (dpurify env ty) c.Pgm_ptree.pc_post;
255
  }
256

257
and dbinder env ({id=x; id_loc=loc} as id, v) =
258
259
260
261
  let v = match v with
    | Some v -> dtype_v env v 
    | None -> DTpure (create_type_var loc)
  in
262
  add_local env x v, (id, v)
263

264
265
let dvariant env (l, p) =
  let s, _ = Typing.specialize_psymbol p env.env.uc in
266
267
268
269
270
271
272
273
  let loc = Typing.qloc p in
  begin match s.ls_args with
    | [t1; t2] when Ty.ty_equal t1 t2 -> 
	()
    | _ -> 
	errorm ~loc "predicate %s should be a binary relation" 
	  s.ls_name.id_string
  end;
274
  dterm env.denv l, s
275

276
277
278
let dloop_annotation env a =
  { dloop_invariant = option_map (dfmla env.denv) a.Pgm_ptree.loop_invariant;
    dloop_variant   = option_map (dvariant env) a.Pgm_ptree.loop_variant; }
279

280
281
(* [dexpr] translates ptree into dexpr *)

282
let rec dexpr env e = 
283
  let d, ty = dexpr_desc env e.Pgm_ptree.expr_loc e.Pgm_ptree.expr_desc in
284
  { dexpr_desc = d; dexpr_loc = e.Pgm_ptree.expr_loc;
285
    dexpr_denv = env.denv; dexpr_type = ty; }
286

287
and dexpr_desc env loc = function
288
  | Pgm_ptree.Econstant (ConstInt _ as c) ->
289
      DEconstant c, dty_app (Ty.ts_int, [])
290
  | Pgm_ptree.Econstant (ConstReal _ as c) ->
291
      DEconstant c, dty_app (Ty.ts_real, [])
292
  | Pgm_ptree.Eident (Qident {id=x}) when Mstr.mem x env.locals ->
293
      (* local variable *)
294
295
      let tyv = Mstr.find x env.locals in
      DElocal (x, tyv), dpurify env tyv
296
  | Pgm_ptree.Eident (Qident {id=x}) when Mstr.mem x env.env.globals ->
297
      (* global variable *)
298
      let s, tyv = specialize_global loc x env.env in
299
      DEglobal (s, tyv), dpurify env tyv
300
  | Pgm_ptree.Eident p ->
301
302
      let s, tyl, ty = Typing.specialize_fsymbol p env.env.uc in
      DElogic s, dcurrying env.env tyl ty
303
  | Pgm_ptree.Eapply (e1, e2) ->
304
305
      let e1 = dexpr env e1 in
      let e2 = dexpr env e2 in
306
      let ty2 = create_type_var loc and ty = create_type_var loc in
307
      if not (Denv.unify e1.dexpr_type (dty_app (env.env.ts_arrow, [ty2; ty]))) 
308
      then
309
310
311
	errorm ~loc:e1.dexpr_loc "this expression is not a function";
      expected_type e2 ty2;
      DEapply (e1, e2), ty
312
313
314
  | Pgm_ptree.Efun (bl, t) ->
      let env, bl = map_fold_left dbinder env bl in
      let (_,e,_) as t = dtriple env t in
315
      let tyl = List.map (fun (x,_) -> Typing.find_var x.id env.denv) bl in
316
      let ty = dcurrying env.env tyl e.dexpr_type in
317
      DEfun (bl, t), ty
318
  | Pgm_ptree.Elet (x, e1, e2) ->
319
320
      let e1 = dexpr env e1 in
      let ty1 = e1.dexpr_type in
321
      let env = add_local env x.id (DTpure ty1) in
322
323
      let e2 = dexpr env e2 in
      DElet (x, e1, e2), e2.dexpr_type
324
325
326
327
  | Pgm_ptree.Eletrec (dl, e1) ->
      let env, dl = dletrec env dl in
      let e1 = dexpr env e1 in
      DEletrec (dl, e1), e1.dexpr_type
328
329
330
331
  | Pgm_ptree.Etuple el ->
      let n = List.length el in
      let s = Typing.fs_tuple n in
      let tyl = List.map (fun _ -> create_type_var loc) el in
332
      let ty = dty_app (Typing.ts_tuple n, tyl) in
333
334
335
336
337
338
339
340
      let create d ty = 
	{ dexpr_desc = d; dexpr_denv = env.denv;
	  dexpr_type = ty; dexpr_loc = loc }
      in
      let apply e1 e2 ty2 = 
	let e2 = dexpr env e2 in
	assert (Denv.unify e2.dexpr_type ty2);
	let ty = create_type_var loc in
341
	assert (Denv.unify e1.dexpr_type 
342
		  (dty_app (env.env.ts_arrow, [ty2; ty])));
343
344
	create (DEapply (e1, e2)) ty
      in
345
      let e = create (DElogic s) (dcurrying env.env tyl ty) in
346
347
      let e = List.fold_left2 apply e el tyl in
      e.dexpr_desc, ty
348

349
  | Pgm_ptree.Esequence (e1, e2) ->
350
      let e1 = dexpr env e1 in
351
      expected_type e1 (dty_unit env.env);
352
353
      let e2 = dexpr env e2 in
      DEsequence (e1, e2), e2.dexpr_type
354
  | Pgm_ptree.Eif (e1, e2, e3) ->
355
      let e1 = dexpr env e1 in
356
      expected_type e1 (dty_bool env.env);
357
358
359
360
      let e2 = dexpr env e2 in
      let e3 = dexpr env e3 in
      expected_type e3 e2.dexpr_type;
      DEif (e1, e2, e3), e2.dexpr_type
361
  | Pgm_ptree.Eloop (a, e1) ->
362
      let e1 = dexpr env e1 in
363
364
      expected_type e1 (dty_unit env.env);
      DEloop (dloop_annotation env a, e1), (dty_unit env.env)
365
  | Pgm_ptree.Elazy (op, e1, e2) ->
366
      let e1 = dexpr env e1 in
367
      expected_type e1 (dty_bool env.env);
368
      let e2 = dexpr env e2 in
369
370
      expected_type e2 (dty_bool env.env);
      DElazy (op, e1, e2), (dty_bool env.env)
371
372
373
374
375
376
377
378
379
380
381
382
383
  | Pgm_ptree.Ematch (el, bl) ->
      let el = List.map (dexpr env) el in
      let tyl = List.map (fun e -> e.dexpr_type) el in
      let ty = create_type_var loc in (* the type of all branches *)
      let branch (pl, e) =
	let denv, pl = Typing.dpat_list env.denv tyl pl in
	let env = { env with denv = denv } in
	let e = dexpr env e in
	expected_type e ty;
	pl, e
      in
      let bl = List.map branch bl in
      DEmatch (el, bl), ty
384
  | Pgm_ptree.Eskip ->
385
      DEskip, (dty_unit env.env)
386
387
  | Pgm_ptree.Eabsurd ->
      DEabsurd, create_type_var loc
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
  | Pgm_ptree.Eraise (id, e) ->
      let ls, tyl, _ = dexception env id in
      let e = match e, tyl with
	| None, [] ->  
	    None
	| Some _, [] ->
	    errorm ~loc "expection %s has no argument" id.id
	| None, [ty] ->
	    errorm ~loc "exception %s is expecting an argument of type %a"
	      id.id print_dty ty;
	| Some e, [ty] -> 
	    let e = dexpr env e in
	    expected_type e ty;
	    Some e
	| _ -> 
	    assert false
      in
      DEraise (ls, e), create_type_var loc
406
407
408
409
410
411
412
413
414
415
416
417
418
  | Pgm_ptree.Etry (e1, hl) ->
      let e1 = dexpr env e1 in
      let handler (id, x, h) =
	let ls, tyl, _ = dexception env id in
	let x, env = match x, tyl with
	  | Some _, [] -> 
	      errorm ~loc "expection %s has no argument" id.id
	  | None, [] -> 
	      None, env
	  | None, [ty] ->
	      errorm ~loc "exception %s is expecting an argument of type %a"
		id.id print_dty ty;
	  | Some x, [ty] -> 
419
	      Some x.id, add_local env x.id (DTpure ty)
420
421
422
423
424
425
426
427
	  | _ ->
	      assert false
	in
	let h = dexpr env h in
	expected_type h e1.dexpr_type;
	(ls, x, h)
      in
      DEtry (e1, List.map handler hl), e1.dexpr_type
428
429

  | Pgm_ptree.Eassert (k, le) ->
430
      DEassert (k, dfmla env.denv le), dty_unit env.env
431
  | Pgm_ptree.Elabel ({id=s}, e1) ->
432
      if Typing.mem_var s env.denv then 
433
	errorm ~loc "clash with previous label %s" s;
434
      let ty = dty_label env.env in
435
      let env = { env with denv = Typing.add_var s ty env.denv } in
436
      let e1 = dexpr env e1 in
437
      DElabel (s, e1), e1.dexpr_type
438
439
440
441
442
  | Pgm_ptree.Ecast (e1, ty) ->
      let e1 = dexpr env e1 in
      let ty = pure_type env ty in
      expected_type e1 ty;
      e1.dexpr_desc, ty
443
444
445
  | Pgm_ptree.Eany c ->
      let c = dtype_c env c in
      DEany c, dpurify env c.dc_result_type
446

447
448
and dletrec env dl =
  (* add all functions into environment *)
449
  let add_one env (id, bl, var, t) = 
450
    let ty = create_type_var id.id_loc in
451
    let env = add_local env id.id (DTpure ty) in
452
    env, ((id, ty), bl, var, t)
453
  in
454
  let env, dl = map_fold_left add_one env dl in
455
  (* then type-check all of them and unify *)
456
  let type_one ((id, tyres), bl, v, t) = 
457
    let env, bl = map_fold_left dbinder env bl in
458
    let v = option_map (dvariant env) v in
459
    let (_,e,_) as t = dtriple env t in
460
    let tyl = List.map (fun (x,_) -> Typing.find_var x.id env.denv) bl in
461
    let ty = dcurrying env.env tyl e.dexpr_type in
462
463
464
465
    if not (Denv.unify ty tyres) then 
      errorm ~loc:id.id_loc
	"this expression has type %a, but is expected to have type %a"
	print_dty ty print_dty tyres;
466
    ((id, tyres), bl, v, t)
467
468
469
  in
  env, List.map type_one dl

470
and dtriple env (p, e, q) =     
471
  let p = dfmla env.denv p in
472
473
  let e = dexpr env e in
  let ty = e.dexpr_type in
474
  let q = dpost env ty q in
475
476
  (p, e, q)

477
(* phase 2: remove destructive types and type annotations *****************)
478

479
let reference env = function
480
481
482
  | DRlocal x -> Rlocal (Mstr.find x env)
  | DRglobal ls -> Rglobal ls

483
484
485
let effect env e =
  let reads ef r = add_read (reference env r) ef in
  let writes ef r = add_write (reference env r) ef in
486
487
488
489
  let raises ef l = add_raise l ef in
  let ef = List.fold_left reads Pgm_effect.empty e.de_reads in
  let ef = List.fold_left writes ef e.de_writes in
  List.fold_left raises ef e.de_raises
490

491
let pre = Denv.fmla
492

493
494
let post env ty (f, ql) =
  let exn (ls, f) =
495
    let v, env = match ls.ls_args with
496
      | [] -> 
497
	  None, env
498
499
      | [ty] -> 
	  let v_result = create_vsymbol (id_fresh id_result) ty in
500
	  Some v_result, Mstr.add id_result v_result env
501
502
503
      | _ -> 
	  assert false
    in
504
    (ls, (v, Denv.fmla env f))
505
506
507
  in
  let v_result = create_vsymbol (id_fresh id_result) ty in
  let env = Mstr.add id_result v_result env in
508
  (v_result, Denv.fmla env f), List.map exn ql
509

510
511
let variant loc env (t, ps) =
  let t = Denv.term env t in
512
513
514
515
  match ps.ls_args with
    | [t1; _] when Ty.ty_equal t1 t.t_ty -> 
	t, ps
    | [t1; _] -> 
516
	errorm ~loc "@[variant has type %a, but is expected to have type %a@]"
517
518
519
520
	  Pretty.print_ty t.t_ty Pretty.print_ty t1
    | _ -> 
	assert false

521
let rec type_v gl env = function
522
523
524
  | DTpure ty -> 
      Tpure (Denv.ty_of_dty ty)
  | DTarrow (bl, c) -> 
525
526
      let env, bl = map_fold_left (binder gl) env bl in
      Tarrow (bl, type_c gl env c)
527

528
529
530
and type_c gl env c = 
  let tyv = type_v gl env c.dc_result_type in
  let ty = purify gl tyv in
531
  { c_result_type = tyv;
532
    c_effect      = effect env c.dc_effect;
533
    c_pre         = pre env c.dc_pre;
534
535
    c_post        = post env ty c.dc_post; }

536
537
and binder gl env (x, tyv) = 
  let tyv = type_v gl env tyv in
538
539
  let v = create_vsymbol (id_user x.id x.id_loc) (purify gl tyv) in
  let env = Mstr.add x.id v env in
540
541
  env, (v, tyv)

542
let mk_iexpr loc ty d = { iexpr_desc = d; iexpr_loc = loc; iexpr_type = ty }
543
544
545
546
547
548
549
550
551
552
553
554
555
556

(* apply ls to a list of expressions, introducing let's if necessary

  ls [e1; e2; ...; en]
->
  let x1 = e1 in
  let x2 = e2 in
  ...
  let xn = en in
  ls(x1,x2,...,xn)
*)
let make_logic_app loc ty ls el =
  let rec make args = function
    | [] -> 
557
	IElogic (t_app ls (List.rev args) ty)
558
    | ({ iexpr_desc = IElogic t }, _) :: r ->
559
	make (t :: args) r
560
    | ({ iexpr_desc = IElocal (vs, _) }, _) :: r ->
561
	make (t_var vs :: args) r
562
    | ({ iexpr_desc = IEglobal (ls, _); iexpr_type = ty }, _) :: r ->
563
	make (t_app ls [] ty :: args) r
564
    | (e, _) :: r ->
565
	let v = create_vsymbol (id_user "x" loc) e.iexpr_type in
566
	let d = mk_iexpr loc ty (make (t_var v :: args) r) in
567
	IElet (v, e, d)
568
569
570
  in
  make [] el

571
572
let is_reference_type gl ty  = match ty.ty_node with
  | Ty.Tyapp (ts, _) -> Ty.ts_equal ts gl.ts_ref
573
574
  | _ -> false

575
576
577
578
(* same thing, but for an abritrary expression f (not an application)
   f [e1; e2; ...; en]
-> let x1 = e1 in ... let xn = en in (...((f x1) x2)... xn)
*)
579
let make_app gl loc ty f el =
580
581
582
  let rec make k = function
    | [] ->
	k f
583
584
    | ({ iexpr_type = ty } as e, tye) :: r when is_reference_type gl ty ->
	begin match e.iexpr_desc with
585
	  | IElocal (v, _) -> 
586
	      make (fun f -> mk_iexpr loc tye (IEapply_ref (k f, Rlocal v))) r
587
	  | IEglobal (v, _) ->
588
	      make (fun f -> mk_iexpr loc tye (IEapply_ref (k f, Rglobal v))) r
589
	  | _ ->
590
	      let v = create_vsymbol (id_user "x" loc) e.iexpr_type in
591
	      let d = 
592
		make (fun f -> mk_iexpr loc tye (IEapply_ref (k f, Rlocal v))) r
593
	      in
594
	      mk_iexpr loc ty (IElet (v, e, d))
595
	end
596
    | ({ iexpr_desc = IElocal (v, _) }, tye) :: r ->
597
	make (fun f -> mk_iexpr loc tye (IEapply (k f, v))) r
598
    | (e, tye) :: r ->
599
	let v = create_vsymbol (id_user "x" loc) e.iexpr_type in
600
601
	let d = make (fun f -> mk_iexpr loc tye (IEapply (k f, v))) r in
	mk_iexpr loc ty (IElet (v, e, d))
602
603
604
  in
  make (fun f -> f) el

605
606
607
(* [iexpr] translates dexpr into iexpr
   [env : vsymbol Mstr.t] maps strings to vsymbols for local variables *)

608
let rec iexpr gl env e =
609
  let ty = Denv.ty_of_dty e.dexpr_type in
610
611
  let d = iexpr_desc gl env e.dexpr_loc ty e.dexpr_desc in
  { iexpr_desc = d; iexpr_type = ty; iexpr_loc = e.dexpr_loc }
612

613
and iexpr_desc gl env loc ty = function
614
  | DEconstant c ->
615
      IElogic (t_const c ty)
616
617
618
619
  | DElocal (x, tyv) ->
      IElocal (Mstr.find x env, type_v gl env tyv)
  | DEglobal (ls, tyv) ->
      IEglobal (ls, type_v gl env tyv)
620
  | DElogic ls ->
621
622
      begin match ls.ls_args with
	| [] -> 
623
	    IElogic (t_app ls [] ty)
624
625
626
627
	| al -> 
	    errorm ~loc "function symbol %s is expecting %d arguments"
	      ls.ls_name.id_string (List.length al)
      end
628
  | DEapply (e1, e2) ->
629
      let f, args = decompose_app gl env e1 [iexpr gl env e2, ty] in
630
631
632
633
634
635
636
637
      begin match f.dexpr_desc with
	| DElogic ls ->
	    let n = List.length ls.ls_args in
	    if List.length args <> n then 
	      errorm ~loc "function symbol %s is expecting %d arguments"
		ls.ls_name.id_string n;
	    make_logic_app loc ty ls args
	| _ ->
638
639
	    let f = iexpr gl env f in
	    (make_app gl loc ty f args).iexpr_desc
640
      end
641
  | DEfun (bl, e1) ->
642
643
      let env, bl = map_fold_left (binder gl) env bl in
      IEfun (bl, itriple gl env e1)
644
  | DElet (x, e1, e2) ->
645
      let e1 = iexpr gl env e1 in
646
647
      let v = create_vsymbol (id_user x.id x.id_loc) e1.iexpr_type in
      let env = Mstr.add x.id v env in
648
      IElet (v, e1, iexpr gl env e2)
649
  | DEletrec (dl, e1) ->
650
      let env, dl = iletrec gl env dl in
651
652
      let e1 = iexpr gl env e1 in
      IEletrec (dl, e1)
653
654

  | DEsequence (e1, e2) ->
655
      IEsequence (iexpr gl env e1, iexpr gl env e2)
656
  | DEif (e1, e2, e3) ->
657
      IEif (iexpr gl env e1, iexpr gl env e2, iexpr gl env e3)
658
  | DEloop (la, e1) ->
659
660
      let la = 
	{ loop_invariant = 
661
	    option_map (Denv.fmla env) la.dloop_invariant;
662
	  loop_variant   = 
663
	    option_map (variant loc env) la.dloop_variant; }
664
      in
665
      IEloop (la, iexpr gl env e1)
666
  | DElazy (op, e1, e2) ->
667
      IElazy (op, iexpr gl env e1, iexpr gl env e2)
668
  | DEmatch (el, bl) ->
669
      let el = List.map (iexpr gl env) el in
670
      let branch (pl, e) = 
671
        let env, pl = map_fold_left Denv.pattern env pl in
672
        (pl, iexpr gl env e)
673
674
      in
      let bl = List.map branch bl in
675
      IEmatch (el, bl)
676
  | DEskip ->
677
      IEskip
678
  | DEabsurd ->
679
      IEabsurd
680
  | DEraise (ls, e) ->
681
      IEraise (ls, option_map (iexpr gl env) e)
682
683
684
685
686
687
688
689
690
691
  | DEtry (e, hl) ->
      let handler (ls, x, h) =
	let x, env = match x with
	  | Some x -> 
	      let ty = match ls.ls_args with [ty] -> ty | _ -> assert false in
	      let v = create_vsymbol (id_fresh x) ty in
	      Some v, Mstr.add x v env 
	  | None ->
	      None, env
	in
692
	(ls, x, iexpr gl env h)
693
      in
694
      IEtry (iexpr gl env e, List.map handler hl)
695
696

  | DEassert (k, f) ->
697
      let f = Denv.fmla env f in
698
      IEassert (k, f)
699
  | DElabel (s, e1) ->
700
      let ty = Ty.ty_app gl.ts_label [] in
701
702
      let v = create_vsymbol (id_fresh s) ty in
      let env = Mstr.add s v env in 
703
      IElabel (v, iexpr gl env e1)
704
  | DEany c ->
705
      let c = type_c gl env c in
706
      IEany c
707

708
and decompose_app gl env e args = match e.dexpr_desc with
709
710
  | DEapply (e1, e2) ->
      let ty = Denv.ty_of_dty e.dexpr_type in
711
      decompose_app gl env e1 ((iexpr gl env e2, ty) :: args)
712
713
714
  | _ ->
      e, args

715
and iletrec gl env dl =
716
717
718
  (* add all functions into env, and compute local env *)
  let step1 env ((x, dty), bl, var, t) = 
    let ty = Denv.ty_of_dty dty in
719
720
    let v = create_vsymbol (id_user x.id x.id_loc) ty in
    let env = Mstr.add x.id v env in
721
722
723
724
725
    env, (v, bl, var, t)
  in
  let env, dl = map_fold_left step1 env dl in
  (* then translate variants and bodies *)
  let step2 (v, bl, var, (_,e,_ as t)) =
726
727
728
    let loc = e.dexpr_loc in (* FIXME *)
    let env, bl = map_fold_left (binder gl) env bl in
    let var = option_map (variant loc env) var in
729
    let t = itriple gl env t in
730
731
732
733
734
735
736
737
738
739
740
    let var, t = match var with
      | None -> 
	  None, t
      | Some (phi, r) ->
	  let p, e, q = t in
	  let phi0 = create_vsymbol (id_fresh "variant") phi.t_ty in
	  let e_phi = { iexpr_desc = IElogic phi; iexpr_type = phi.t_ty; 
			iexpr_loc = e.iexpr_loc } in
	  let e = { e with iexpr_desc = IElet (phi0, e_phi, e) } in
	  Some (phi0, phi, r), (p, e, q)
    in
741
742
    (v, bl, var, t)
  in
743
744
745
  let dl = List.map step2 dl in
  (* finally, check variants are all absent or all present and consistent *)
  let error e = 
746
    errorm ~loc:e.iexpr_loc "variants must be all present or all absent"
747
748
749
750
751
752
753
  in
  begin match dl with
    | [] -> 
	assert false
    | (_, _, None, _) :: r ->
	let check_no_variant (_,_,var,(_,e,_)) = if var <> None then error e in
	List.iter check_no_variant r
754
    | (_, _, Some (_, _, ps), _) :: r ->
755
756
	let check_variant (_,_,var,(_,e,_)) = match var with
	  | None -> error e
757
	  | Some (_, _, ps') -> if not (ls_equal ps ps') then 
758
	      errorm ~loc:e.iexpr_loc 
759
760
761
762
763
		"variants must share the same order relation"
	in
	List.iter check_variant r
  end;
  env, dl
764

765
766
and itriple gl env (p, e, q) =
  let p = Denv.fmla env p in
767
768
  let e = iexpr gl env e in
  let q = post env e.iexpr_type q in
769
770
  (p, e, q)

771
772
(* pretty-printing (for debugging) *)

773
open Pp
774
775
open Pretty 

776
777
let rec print_iexpr fmt e = match e.iexpr_desc with
  | IElogic t ->
778
      print_term fmt t
779
  | IElocal (vs, _) ->
780
      fprintf fmt "<local %a>" print_vs vs
781
  | IEglobal (ls, _) ->
782
      fprintf fmt "<global %a>" print_ls ls
783
784
785
786
787
788
789
  | IEapply (e, vs) ->
      fprintf fmt "@[((%a) %a)@]" print_iexpr e print_vs vs
  | IEapply_ref (e, r) ->
      fprintf fmt "@[((%a) <ref %a>)@]" print_iexpr e print_reference r
  | IEfun (_, (_,e,_)) ->
      fprintf fmt "@[fun _ ->@ %a@]" print_iexpr e
  | IElet (v, e1, e2) ->
790
      fprintf fmt "@[let %a = %a in@ %a@]" print_vs v
791
	print_iexpr e1 print_iexpr e2
792

793
794
  | IEsequence (e1, e2) ->
      fprintf fmt "@[%a;@\n%a@]" print_iexpr e1 print_iexpr e2
795

796
797
798
  | _ ->
      fprintf fmt "<other>"

799
800
801
(* phase 3: effect inference **********)

let rec term_effect env ef t = match t.t_node with
802
  | Term.Tapp (ls, [t]) when ls_equal ls env.ls_bang ->
803
804
805
806
807
808
809
810
      let r = reference_of_term t in
      E.add_read r ef
  | _ ->
      t_fold (term_effect env) (fmla_effect env) ef t

and fmla_effect env ef f =
  f_fold (term_effect env) (fmla_effect env) ef f

811
let post_effect env ef ((v,q),ql) =
812
  let exn_effect ef (_,(_,q)) = fmla_effect env ef q in
813
814
  let ef = List.fold_left exn_effect (fmla_effect env ef q) ql in
  E.remove_reference (Rlocal v) ef
815

816
let add_local x v env = Mvs.add x v env
817
818
819
820
let add_binder env (x, v) = add_local x v env
let add_binders = List.fold_left add_binder

let make_apply loc e1 ty c =
821
  let x = create_vsymbol (id_fresh "f") e1.expr_type in
822
823
824
825
826
827
828
829
830
831
832
833
834
835
  let v = c.c_result_type and ef = c.c_effect in
  let any_c = { expr_desc = Eany c; expr_type = ty;
		expr_type_v = v; expr_effect = ef; expr_loc = loc } in
  Elet (x, e1, any_c), v, ef

let exn_check = ref true
let without_exn_check f x =
  if !exn_check then begin
    exn_check := false; 
    try let y = f x in exn_check := true; y 
    with e -> exn_check := true; raise e
  end else
    f x

836
837
838
839
840
841
842
843
844
845
846
847
(*s Pure expressions. Used in [Slazy_and] and [Slazy_or] to decide
    whether to use [strict_bool_and_] and [strict_bool_or_] or not. *)

let rec is_pure_expr e = 
  E.no_side_effect e.expr_effect &&
  match e.expr_desc with
  | Elocal _ | Elogic _ | Eskip -> true
  | Eif (e1, e2, e3) -> is_pure_expr e1 && is_pure_expr e2 && is_pure_expr e3
  | Elet (_, e1, e2) -> is_pure_expr e1 && is_pure_expr e2
  | Elabel (_, e1) -> is_pure_expr e1
  | Eany c -> E.no_side_effect c.c_effect
  | Eghost _ | Eassert _ | Etry _ | Eraise _ | Ematch _ 
848
  | Eloop _ | Esequence _ | Eletrec _ | Efun _ 
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
  | Eglobal _ | Eabsurd -> false (* TODO: improve *)

let mk_expr loc ty ef d =
  { expr_desc = d; expr_type = ty; expr_type_v = Tpure ty;
    expr_effect = ef; expr_loc = loc }

let mk_simple_expr loc ty d = mk_expr loc ty E.empty d

let mk_bool_constant loc gl ls =
  let ty = ty_app gl.ts_bool [] in
  { expr_desc = Elogic (t_app ls [] ty); expr_type = ty; expr_type_v = Tpure ty;
    expr_effect = E.empty; expr_loc = loc }

let mk_false loc gl = mk_bool_constant loc gl gl.ls_False 
let mk_true  loc gl = mk_bool_constant loc gl gl.ls_True

865
866
867
868
(* [expr] translates iexpr into expr
   [env : type_v Mvs.t] maps local variables to their types *)

let rec expr gl env e =
869
870
  let ty = e.iexpr_type in
  let loc = e.iexpr_loc in
871
  let d, v, ef = expr_desc gl env loc ty e.iexpr_desc in
872
873
874
  { expr_desc = d; expr_type = ty; 
    expr_type_v = v; expr_effect = ef; expr_loc = loc }

875
and expr_desc gl env loc ty = function
876
  | IElogic t ->
877
      let ef = term_effect gl E.empty t in
878
      Elogic t, Tpure ty, ef
879
880
  | IElocal (vs, _) ->
      let tyv = Mvs.find vs env in
881
882
883
      Elocal vs, tyv, E.empty
  | IEglobal (ls, tyv) ->
      Eglobal ls, tyv, E.empty
884
  | IEapply (e1, vs) ->
885
      let e1 = expr gl env e1 in
886
      (* printf "e1 : %a@." print_type_v e1.expr_type_v; *)
887
      let c = apply_type_v gl e1.expr_type_v vs in
888
889
      make_apply loc e1 ty c
  | IEapply_ref (e1, r) ->
890
891
      let e1 = expr gl env e1 in
      let c = apply_type_v_ref gl e1.expr_type_v r in