pgm_typing.ml 51.4 KB
Newer Older
1 2 3
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
MARCHE Claude's avatar
MARCHE Claude committed
4 5 6
(*    François Bobot                                                     *)
(*    Jean-Christophe Filliâtre                                          *)
(*    Claude Marché                                                      *)
7 8 9 10 11 12 13 14 15 16 17 18 19
(*    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 Pp
23
open Util
24
open Ident
25
open Ty
26
open Term
27
open Theory
28 29 30
open Denv
open Ptree
open Pgm_ttree
31
open Pgm_types
32
open Pgm_types.T
33
open Pgm_module
34

35
let debug = Debug.register_flag "program_typing"
36

37
exception Message of string
38 39

let error ?loc e = match loc with
40 41
  | None -> raise e
  | Some loc -> raise (Loc.Located (loc, e))
42 43 44 45 46 47 48 49 50 51 52 53

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

54 55 56
let () = Exn_printer.register (fun fmt e -> match e with
  | Message s -> fprintf fmt "%s" s
  | _ -> raise e)
57

58 59
let id_result = "result"

60
(* phase 1: typing programs (using destructive type inference) **************)
61

62
let dty_app (ts, tyl) = assert (ts.ts_def = None); tyapp (ts, tyl)
63

64 65 66 67 68 69
let find_ts uc s = ns_find_ts (get_namespace (theory_uc uc)) [s]
let find_ls uc s = ns_find_ls (get_namespace (theory_uc uc)) [s]

(* TODO: improve efficiency *)
let dty_bool uc = dty_app (find_ts uc "bool", [])
let dty_int _uc = dty_app (Ty.ts_int, [])
70
let dty_unit _uc = dty_app (ts_tuple 0, [])
71
let dty_label uc = dty_app (find_ts uc "label_", [])
72

73
(* note: local variables are simultaneously in locals (to type programs)
74
   and in denv (to type logic elements) *)
75
type denv = {
76
  uc    : uc;
77
  locals: Denv.dty Mstr.t;
78
  denv  : Typing.denv; (* for user type variables only *)
79
}
80

81 82
let create_denv uc =
  { uc = uc;
83
    locals = Mstr.empty;
84
    denv = Typing.create_denv (theory_uc uc); }
85

86 87
let specialize_effect e =
  let reference r acc = match r with
88 89
    | R.Rlocal v -> DRlocal v.pv_name.id_string :: acc
    | R.Rglobal l -> DRglobal l :: acc
90
  in
91 92 93
  { de_reads  = Sref.fold reference e.E.reads  [];
    de_writes = Sref.fold reference e.E.writes [];
    de_raises = Sexn.elements e.E.raises; }
94 95 96 97

let specialize_post ~loc htv ((v, f), ql) =
  assert (v.vs_name.id_string = "result"); (* TODO *)
  let specialize_exn (l, (v, f)) =
98
    assert
99
      (match v with Some v -> v.vs_name.id_string = "result" | None -> true);
100 101
    let ty = option_map (fun v -> Denv.specialize_ty ~loc htv v.vs_ty) v in
    (l, (ty, specialize_fmla ~loc htv f))
102
  in
103 104 105
  let ty = Denv.specialize_ty ~loc htv v.vs_ty in
  let f = specialize_fmla ~loc htv f in
  (ty, f), List.map specialize_exn ql
106

107
let rec loc_of_id id = match id.id_origin with
108
  | User loc -> loc
109
  | Derived id -> loc_of_id id
110 111 112 113 114 115
  | _ -> assert false

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

116 117 118 119
let dcurrying tyl ty =
  let make_arrow_type ty1 ty2 = dty_app (ts_arrow, [ty1; ty2]) in
  List.fold_right make_arrow_type tyl ty

120
let rec dpurify_type_v = function
121
  | DTpure ty ->
122
      ty
123
  | DTarrow (bl, c) ->
124
      dcurrying (List.map (fun (_,ty,_) -> ty) bl)
125 126
	(dpurify_type_v c.dc_result_type)

127 128 129 130
let rec specialize_type_v ~loc htv = function
  | Tpure ty ->
      DTpure (Denv.specialize_ty ~loc htv ty)
  | Tarrow (bl, c) ->
131
      DTarrow (List.map (specialize_binder ~loc htv) bl,
132 133 134 135 136 137 138 139
	       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; }

140 141 142
and specialize_binder ~loc htv v =
  let id = { id = v.pv_name.id_string;
             id_lab = v.pv_name.id_label;
143
             id_loc = loc } in
144 145
  let v = specialize_type_v ~loc htv v.pv_tv in
  id, dpurify_type_v v, v
146

147 148
let specialize_global loc x uc =
  let p = ns_find_pr (namespace uc) x in
149
  p, specialize_type_v ~loc (Htv.create 17) p.p_tv
150

151
let dot fmt () = pp_print_string fmt "."
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
152 153 154
let print_qualids = print_list dot pp_print_string
let print_qualid fmt q = 
  print_list dot pp_print_string fmt (Typing.string_list_of_qualid [] q)
155

156 157 158
let specialize_exception loc x uc =
  let s = 
    try ns_find_ex (namespace uc) x
159
    with Not_found -> errorm ~loc "@[unbound exception %a@]" print_qualids x
160
  in
161 162 163 164
  match Denv.specialize_lsymbol ~loc s with
    | tyl, Some ty -> s, tyl, ty
    | _, None -> assert false

165 166
let create_type_var loc =
  let tv = Ty.create_tvsymbol (id_user "a" loc) in
167
  tyvar (create_ty_decl_var ~loc ~user:false tv)
168

169
let add_pure_var id ty denv = match view_dty ty with
170 171
  | Tyapp (ts, _) when Ty.ts_equal ts ts_arrow -> denv
  | _ -> Typing.add_var id ty denv
172

173
let uncurrying ty =
174
  let rec uncurry acc ty = match ty.ty_node with
175
    | Ty.Tyapp (ts, [t1; t2]) when ts_equal ts ts_arrow ->
176
	uncurry (t1 :: acc) t2
177
    | _ ->
178
	List.rev acc, ty
179 180 181
  in
  uncurry [] ty

182
let expected_type e ty =
183
  if not (Denv.unify e.dexpr_type ty) then
184
    errorm ~loc:e.dexpr_loc
185
      "this expression has type %a, but is expected to have type %a"
186
      print_dty e.dexpr_type print_dty ty
187

188 189
let pure_type env = Typing.dty env.denv

190
let check_mutable_type loc dty = match view_dty dty with
191
  | Denv.Tyapp (ts, _) when is_mutable_ts ts -> 
192
      ()
193
  | _ ->
194 195
      errorm ~loc 
	"this expression has type %a, but is expected to have a mutable type"
196
	print_dty dty
197

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
198
let dreference env = function
199
  | Qident id when Mstr.mem id.id env.locals ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
200
      (* local variable *)
201 202
      let ty = Mstr.find id.id env.locals in
      check_mutable_type id.id_loc ty;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
203
      DRlocal id.id
204 205 206 207 208
  | qid ->
      let loc = Typing.qloc qid in
      let sl = Typing.string_list_of_qualid [] qid in
      let s, _ty = specialize_global loc sl env.uc in
      (* TODO check_reference_type env.uc loc ty; *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
209 210
      DRglobal s

211
let dexception uc qid =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
212 213
  let sl = Typing.string_list_of_qualid [] qid in
  let loc = Typing.qloc qid in
214
  let _, _, ty as r = specialize_exception loc sl uc in
215
  let ty_exn = dty_app (ts_exn, []) in
216
  if not (Denv.unify ty ty_exn) then
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
217
    errorm ~loc
218 219 220
      "this expression has type %a, but is expected to be an exception"
      print_dty ty;
  r
221 222

let deffect env e =
223 224
  { de_reads  = List.map (dreference env) e.Ptree.pe_reads;
    de_writes = List.map (dreference env) e.Ptree.pe_writes;
225
    de_raises =
226
      List.map (fun id -> let ls,_,_ = dexception env.uc id in ls)
227
	e.Ptree.pe_raises; }
228

229
let dpost uc (q, ql) =
230
  let dexn (id, l) =
231
    let s, _, _ = dexception uc id in s, l
232
  in
233
  q, List.map dexn ql
234

Andrei Paskevich's avatar
Andrei Paskevich committed
235 236 237
let add_local_top env x tyv =
  { env with locals = Mstr.add x tyv env.locals }

238
let add_local env x ty =
239
  { env with locals = Mstr.add x ty env.locals; }
240

241
let rec dpurify_utype_v = function
242
  | DUTpure ty ->
243
      ty
244
  | DUTarrow (bl, c) ->
245
      dcurrying (List.map (fun (_,ty,_) -> ty) bl)
246
	(dpurify_utype_v c.duc_result_type)
247

248
let rec dutype_v env = function
249
  | Ptree.Tpure pt ->
250
      DUTpure (pure_type env pt)
251
  | Ptree.Tarrow (bl, c) ->
252 253 254 255 256 257 258 259
      let env, bl = map_fold_left dubinder env bl in
      let c = dutype_c env c in
      DUTarrow (bl, c)

and dutype_c env c =
  let ty = dutype_v env c.Ptree.pc_result_type in
  { duc_result_type = ty;
    duc_effect      = deffect env c.Ptree.pc_effect;
260 261
    duc_pre         = c.Ptree.pc_pre;
    duc_post        = dpost env.uc c.Ptree.pc_post;
262
  }
263

264
and dubinder env ({id=x; id_loc=loc} as id, v) =
265
  let v = match v with
266 267
    | Some v -> dutype_v env v
    | None -> DUTpure (create_type_var loc)
268
  in
269
  let ty = dpurify_utype_v v in
270
  add_local env x ty, (id, ty, v)
271

272
let rec add_local_pat env p = match p.dp_node with
273 274 275 276 277
  | Denv.Pwild -> env
  | Denv.Pvar x -> add_local env x.id p.dp_ty
  | Denv.Papp (_, pl) -> List.fold_left add_local_pat env pl
  | Denv.Pas (p, x) -> add_local_pat (add_local env x.id p.dp_ty) p
  | Denv.Por (p, q) -> add_local_pat (add_local_pat env p) q
278

279
let dvariant env (l, p) =
280 281 282 283 284 285 286 287 288 289 290
  let relation p = 
    let s, _ = Typing.specialize_psymbol p (theory_uc env.uc) in
    let loc = Typing.qloc p in
    match s.ls_args with
      | [t1; t2] when Ty.ty_equal t1 t2 ->
	  s
      | _ ->
	  errorm ~loc "predicate %s should be a binary relation"
	    s.ls_name.id_string
  in
  l, option_map relation p
291

292
let dloop_annotation env a =
293
  { dloop_invariant = a.Ptree.loop_invariant;
294
    dloop_variant   = option_map (dvariant env) a.Ptree.loop_variant; }
295

296 297
(* [dexpr] translates ptree into dexpr *)

298
let rec dexpr env e =
299 300
  let d, ty = dexpr_desc env e.Ptree.expr_loc e.Ptree.expr_desc in
  { dexpr_desc = d; dexpr_loc = e.Ptree.expr_loc;
301
    dexpr_denv = env.denv; dexpr_type = ty; }
302

303
and dexpr_desc env loc = function
304
  | Ptree.Econstant (ConstInt _ as c) ->
305
      DEconstant c, dty_app (Ty.ts_int, [])
306
  | Ptree.Econstant (ConstReal _ as c) ->
307
      DEconstant c, dty_app (Ty.ts_real, [])
308
  | Ptree.Eident (Qident {id=x}) when Mstr.mem x env.locals ->
309
      (* local variable *)
310
      let tyv = Mstr.find x env.locals in
311
      DElocal (x, tyv), tyv
312
  | Ptree.Eident p ->
313 314 315 316
      begin try
	(* global variable *)
	let x = Typing.string_list_of_qualid [] p in
	let s, tyv = specialize_global loc x env.uc in
317 318
	let dty = dpurify_type_v tyv in
	DEglobal (s, tyv), dty
319 320 321 322 323 324 325 326
      with Not_found ->
	let s,tyl,ty = Typing.specialize_lsymbol p (theory_uc env.uc) in
	let ty = match ty with
          | Some ty -> ty
          | None -> dty_bool env.uc
	in
	DElogic s, dcurrying tyl ty
      end
327 328 329 330 331 332
  | Ptree.Elazy (op, e1, e2) ->
      let e1 = dexpr env e1 in
      expected_type e1 (dty_bool env.uc);
      let e2 = dexpr env e2 in
      expected_type e2 (dty_bool env.uc);
      DElazy (op, e1, e2), dty_bool env.uc
333
  | Ptree.Eapply (e1, e2) ->
334 335
      let e1 = dexpr env e1 in
      let e2 = dexpr env e2 in
336
      let ty2 = create_type_var loc and ty = create_type_var loc in
337
      if not (Denv.unify e1.dexpr_type (dty_app (ts_arrow, [ty2; ty])))
338
      then
339 340 341
	errorm ~loc:e1.dexpr_loc "this expression is not a function";
      expected_type e2 ty2;
      DEapply (e1, e2), ty
342
  | Ptree.Efun (bl, t) ->
343
      let env, bl = map_fold_left dubinder env bl in
344
      let (_,e,_) as t = dtriple env t in
345
      let tyl = List.map (fun (_,ty,_) -> ty) bl in
346
      let ty = dcurrying tyl e.dexpr_type in
347
      DEfun (bl, t), ty
348
  | Ptree.Elet (x, e1, e2) ->
349 350
      let e1 = dexpr env e1 in
      let ty1 = e1.dexpr_type in
351
      let env = add_local env x.id ty1 in
352 353
      let e2 = dexpr env e2 in
      DElet (x, e1, e2), e2.dexpr_type
354
  | Ptree.Eletrec (dl, e1) ->
355 356 357
      let env, dl = dletrec env dl in
      let e1 = dexpr env e1 in
      DEletrec (dl, e1), e1.dexpr_type
358
  | Ptree.Etuple el ->
359 360 361
      let n = List.length el in
      let s = Typing.fs_tuple n in
      let tyl = List.map (fun _ -> create_type_var loc) el in
362
      let ty = dty_app (Typing.ts_tuple n, tyl) in
363
      let create d ty =
364 365 366
	{ dexpr_desc = d; dexpr_denv = env.denv;
	  dexpr_type = ty; dexpr_loc = loc }
      in
367
      let apply e1 e2 ty2 =
368 369 370
	let e2 = dexpr env e2 in
	assert (Denv.unify e2.dexpr_type ty2);
	let ty = create_type_var loc in
371
	assert (Denv.unify e1.dexpr_type
372
		  (dty_app (ts_arrow, [ty2; ty])));
373 374
	create (DEapply (e1, e2)) ty
      in
375
      let e = create (DElogic s) (dcurrying tyl ty) in
376 377
      let e = List.fold_left2 apply e el tyl in
      e.dexpr_desc, ty
378

379
  | Ptree.Esequence (e1, e2) ->
380
      let e1 = dexpr env e1 in
381
      expected_type e1 (dty_unit env.uc);
382 383
      let e2 = dexpr env e2 in
      DEsequence (e1, e2), e2.dexpr_type
384
  | Ptree.Eif (e1, e2, e3) ->
385
      let e1 = dexpr env e1 in
386
      expected_type e1 (dty_bool env.uc);
387 388 389 390
      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
391
  | Ptree.Eloop (a, e1) ->
392
      let e1 = dexpr env e1 in
393 394
      expected_type e1 (dty_unit env.uc);
      DEloop (dloop_annotation env a, e1), dty_unit env.uc
395
  | Ptree.Ematch (e1, bl) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
396 397
      let e1 = dexpr env e1 in
      let ty1 = e1.dexpr_type in
398
      let ty = create_type_var loc in (* the type of all branches *)
Andrei Paskevich's avatar
Andrei Paskevich committed
399 400
      let branch (p, e) =
	let denv, p = Typing.dpat_list env.denv ty1 p in
401
	let env = { env with denv = denv } in
Andrei Paskevich's avatar
Andrei Paskevich committed
402
	let env = add_local_pat env p in
403 404
	let e = dexpr env e in
	expected_type e ty;
Andrei Paskevich's avatar
Andrei Paskevich committed
405
	p, e
406 407
      in
      let bl = List.map branch bl in
Andrei Paskevich's avatar
Andrei Paskevich committed
408
      DEmatch (e1, bl), ty
409
  | Ptree.Eskip ->
410
      DElogic (fs_tuple 0), dty_unit env.uc
411
  | Ptree.Eabsurd ->
412
      DEabsurd, create_type_var loc
413
  | Ptree.Eraise (qid, e) ->
414
      let ls, tyl, _ = dexception env.uc qid in
415
      let e = match e, tyl with
416
	| None, [] ->
417 418
	    None
	| Some _, [] ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
419
	    errorm ~loc "expection %a has no argument" print_qualid qid
420
	| None, [ty] ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
421 422
	    errorm ~loc "exception %a is expecting an argument of type %a"
	      print_qualid qid print_dty ty;
423
	| Some e, [ty] ->
424 425 426
	    let e = dexpr env e in
	    expected_type e ty;
	    Some e
427
	| _ ->
428 429 430
	    assert false
      in
      DEraise (ls, e), create_type_var loc
431
  | Ptree.Etry (e1, hl) ->
432 433
      let e1 = dexpr env e1 in
      let handler (id, x, h) =
434
	let ls, tyl, _ = dexception env.uc id in
435
	let x, env = match x, tyl with
436
	  | Some _, [] ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
437
	      errorm ~loc "expection %a has no argument" print_qualid id
438
	  | None, [] ->
439 440
	      None, env
	  | None, [ty] ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
441 442
	      errorm ~loc "exception %a is expecting an argument of type %a"
		print_qualid id print_dty ty;
443
	  | Some x, [ty] ->
444
	      Some x.id, add_local env x.id ty
445 446 447 448 449 450 451 452
	  | _ ->
	      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
453
  | Ptree.Efor (x, e1, d, e2, inv, e3) ->
454
      let e1 = dexpr env e1 in
455
      expected_type e1 (dty_int env.uc);
456
      let e2 = dexpr env e2 in
457
      expected_type e2 (dty_int env.uc);
458
      let env = add_local env x.id (dty_int env.uc) in
459
      (* let inv = option_map (dfmla env.denv) inv in *)
460
      let e3 = dexpr env e3 in
461 462
      expected_type e3 (dty_unit env.uc);
      DEfor (x, e1, d, e2, inv, e3), dty_unit env.uc
463

464
  | Ptree.Eassert (k, le) ->
465
      DEassert (k, (* dfmla env.denv *) le), dty_unit env.uc
466
  | Ptree.Elabel ({id=s}, e1) ->
467
      if Typing.mem_var s env.denv then
468
	errorm ~loc "clash with previous label %s" s;
469
      let ty = dty_label env.uc in
470
      let env = { env with denv = add_pure_var s ty env.denv } in
471
      let e1 = dexpr env e1 in
472
      DElabel (s, e1), e1.dexpr_type
473
  | Ptree.Ecast (e1, ty) ->
474 475 476 477
      let e1 = dexpr env e1 in
      let ty = pure_type env ty in
      expected_type e1 ty;
      e1.dexpr_desc, ty
478
  | Ptree.Eany c ->
479 480
      let c = dutype_c env c in
      DEany c, dpurify_utype_v c.duc_result_type
481

482 483
and dletrec env dl =
  (* add all functions into environment *)
484
  let add_one env (id, bl, var, t) =
485
    let ty = create_type_var id.id_loc in
486
    let env = add_local_top env id.id ty in
487
    env, ((id, ty), bl, var, t)
488
  in
489
  let env, dl = map_fold_left add_one env dl in
490
  (* then type-check all of them and unify *)
491
  let type_one ((id, tyres), bl, v, t) =
492
    let env, bl = map_fold_left dubinder env bl in
493
    let v = option_map (dvariant env) v in
494
    let (_,e,_) as t = dtriple env t in
495
    let tyl = List.map (fun (_,ty,_) -> ty) bl in
496
    let ty = dcurrying tyl e.dexpr_type in
497
    if not (Denv.unify ty tyres) then
498 499 500
      errorm ~loc:id.id_loc
	"this expression has type %a, but is expected to have type %a"
	print_dty ty print_dty tyres;
501
    ((id, tyres), bl, v, t)
502 503 504
  in
  env, List.map type_one dl

505
and dtriple env (p, e, q) =
506
  let e = dexpr env e in
507
  let q = dpost env.uc q in
508 509
  (p, e, q)

510
(* phase 2: remove destructive types and type annotations *****************)
511

512 513 514 515 516 517 518 519 520 521 522
let dterm env l = Typing.dterm ~localize:true env l
let dfmla env l = Typing.dfmla ~localize:true env l

type ienv = { 
  i_uc     : uc;
  i_denv   : Typing.denv;
  i_locals : ivsymbol Mstr.t;
  i_logics : vsymbol Mstr.t;
}

let create_ivsymbol id ty =
523 524
  let vs = create_vsymbol id ty in
  let ty' = purify ty in
525
  if ty_equal ty ty' then { i_pgm = vs; i_logic = vs }
526
  else { i_pgm = vs; i_logic = create_vsymbol id ty'; }
527

528 529 530 531 532 533
let rec dty_of_ty denv ty = match ty.ty_node with
  | Ty.Tyvar v -> 
      Denv.tyvar (Typing.find_user_type_var v.tv_name.id_string denv)
  | Ty.Tyapp (ts, tyl) -> 
      Denv.tyapp (ts, List.map (dty_of_ty denv) tyl)

534
let iadd_local env x ty =
535 536 537 538 539 540 541
  let v = create_ivsymbol x ty in 
  let s = v.i_pgm.vs_name.id_string in
  let dty = dty_of_ty env.i_denv v.i_logic.vs_ty in
  let env = { env with i_denv   = add_pure_var s dty env.i_denv;
		       i_locals = Mstr.add s v env.i_locals;
	               i_logics = Mstr.add s v.i_logic env.i_logics; } 
  in
542 543 544
  env, v
  
let ireference env = function
545
  | DRlocal x -> IRlocal (Mstr.find x env.i_locals)
546 547 548 549 550 551 552 553
  | DRglobal ls -> IRglobal ls

let ieffect env e = {
  ie_reads  = List.map (ireference env) e.de_reads;
  ie_writes = List.map (ireference env) e.de_writes;
  ie_raises = e.de_raises;
}

554
let pre env = Denv.fmla env.i_logics
555 556

let post env ((ty, f), ql) =
557
  let env = env.i_logics in
558 559 560
  let exn (ls, (ty, f)) =
    let v, env = match ty with
      | None ->
561
	  None, env
562 563
      | Some ty ->
	  let ty = Denv.ty_of_dty ty in
564
	  let v_result = create_vsymbol (id_fresh id_result) ty in
565
	  Some v_result, Mstr.add id_result v_result env
566
    in
567
    (ls, (v, Denv.fmla env f))
568
  in
569
  let ty = Denv.ty_of_dty ty in
570 571
  let v_result = create_vsymbol (id_fresh id_result) ty in
  let env = Mstr.add id_result v_result env in
572
  (v_result, Denv.fmla env f), List.map exn ql
573

574 575 576 577
let iterm env l =
  let t = dterm env.i_denv l in
  Denv.term env.i_logics t

578 579 580
(* TODO: should we admit an instsance of a polymorphic order relation *)
let ivariant env (t, ps) =
  let loc = t.pp_loc in
581
  let t = iterm env t in
582 583
  match ps with
    | None ->
584 585
	if not (Ty.ty_equal ty_int t.t_ty) then
	  errorm ~loc "variant should have type int";
586 587
	t, ps
    | Some { ls_args = [t1; _] } when Ty.ty_equal t1 t.t_ty ->
588
	t, ps
589
    | Some { ls_args = [t1; _] } ->
590
	errorm ~loc "@[variant has type %a, but is expected to have type %a@]"
591
	  Pretty.print_ty t.t_ty Pretty.print_ty t1
592
    | _ ->
593 594
	assert false

595
let rec itype_v env = function
596
  | DTpure ty ->
597
      ITpure (Denv.ty_of_dty ty)
598
  | DTarrow (bl, c) ->
599 600
      let env, bl = map_fold_left ibinder env bl in
      ITarrow (bl, itype_c env c)
601

602 603
and itype_c env c =
  let tyv = itype_v env c.dc_result_type in
604 605 606 607 608
  { ic_result_type = tyv;
    ic_effect      = ieffect env c.dc_effect;
    ic_pre         = pre env c.dc_pre;
    ic_post        = post env c.dc_post; }

609 610
and ibinder env (x, ty, tyv) =
  let tyv = itype_v env tyv in
611
  let ty = Denv.ty_of_dty ty in
612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662
  let env, v = iadd_local env (id_user x.id x.id_loc) ty in
  env, (v, tyv)

let ifmla env l =
  let f = dfmla env.i_denv l in
  Denv.fmla env.i_logics f

let id_result loc = id_user id_result loc

let iupost env ty (q, ql) =
  let dexn (s, l) =
    let v, env = match s.ls_args with
      | [] ->
    	  None, env
      | [ty] ->
	  let env, v = iadd_local env (id_result l.pp_loc) ty in
    	  Some v.i_logic, env
      | _ -> assert false
    in
    s, (v, ifmla env l)
  in
  let env, v = iadd_local env (id_result q.pp_loc) ty in
  (v.i_logic, ifmla env q), List.map dexn ql

let rec purify_itype_v  = function
  | ITpure ty ->
      ty
  | ITarrow (bl, c) ->
      make_arrow_type
	(List.map (fun (v,_) -> v.i_pgm.vs_ty) bl)
	(purify_itype_v c.ic_result_type)

let rec iutype_v gl env = function
  | DUTpure ty ->
      ITpure (Denv.ty_of_dty ty)
  | DUTarrow (bl, c) ->
      let env, bl = map_fold_left (iubinder gl) env bl in
      ITarrow (bl, iutype_c gl env c)

and iutype_c gl env c =
  let tyv = iutype_v gl env c.duc_result_type in
  let ty = purify_itype_v tyv in
  { ic_result_type = tyv;
    ic_effect      = ieffect env c.duc_effect;
    ic_pre         = ifmla env c.duc_pre;
    ic_post        = iupost env ty c.duc_post; }

and iubinder gl env (x, ty, tyv) =
  let tyv = iutype_v gl env tyv in
  let ty = Denv.ty_of_dty ty in
  let env, v = iadd_local env (id_user x.id x.id_loc) ty in
663 664
  env, (v, tyv)

665
let mk_iexpr loc ty d = { iexpr_desc = d; iexpr_loc = loc; iexpr_type = ty }
666

667
let mk_t_if gl f =
668 669
  let ty = ty_app (find_ts gl "bool") [] in
  t_if f (t_app (find_ls gl "True") [] ty) (t_app (find_ls gl "False") [] ty)
670

671 672 673 674 675 676 677 678 679 680
(* 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)
*)
681
let make_logic_app gl loc ty ls el =
682
  let rec make args = function
683 684 685 686 687
    | [] ->
        begin match ls.ls_value with
          | Some _ -> IElogic (t_app ls (List.rev args) ty)
          | None -> IElogic (mk_t_if gl (f_app ls (List.rev args)))
        end
688
    | ({ iexpr_desc = IElogic t }, _) :: r ->
689
	make (t :: args) r
690
    | ({ iexpr_desc = IElocal v }, _) :: r ->
691
	make (t_var v.i_pgm :: args) r
692
    | ({ iexpr_desc = IEglobal (s, _); iexpr_type = ty }, _) :: r ->
693
	make (t_app s.p_ls [] ty :: args) r
694
    | (e, _) :: r ->
695
	let v = create_ivsymbol (id_user "x" loc) e.iexpr_type in
696
	let d = mk_iexpr loc ty (make (t_var v.i_pgm :: args) r) in
697
	IElet (v, e, d)
698 699 700 701 702 703 704
  in
  make [] el

(* 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)
*)
705
let make_app _gl loc ty f el =
706 707 708
  let rec make k = function
    | [] ->
	k f
709
    | ({ iexpr_type = ty } as e, tye) :: r when is_mutable_ty ty ->
710
	begin match e.iexpr_desc with
711
	  | IElocal v ->
712
	      make (fun f -> mk_iexpr loc tye (IEapply_ref (k f, IRlocal v))) r
713
	  | IEglobal (v, _) ->
714
	      make (fun f -> mk_iexpr loc tye (IEapply_ref (k f, IRglobal v))) r
715
	  | _ ->
716
	      let v = create_ivsymbol (id_user "x" loc) e.iexpr_type in
717
	      let d =
718
		make (fun f -> mk_iexpr loc tye (IEapply_ref (k f, IRlocal v))) r
719
	      in