pgm_typing.ml 40.1 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
let debug = Debug.register_flag "program_typing"
35

36
exception Message of string
37 38

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

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

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

57 58
let id_result = "result"

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

61 62 63 64 65
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, [])
66

67
(* note: local variables are simultaneously in locals (to type programs)
68
   and in denv (to type logic elements) *)
69 70 71 72
type denv = {
  env   : env;
  locals: dtype_v Mstr.t;
  denv  : Typing.denv;
73
}
74

75 76 77 78 79
let create_denv gl = 
  { env = gl;
    locals = Mstr.empty;
    denv = Typing.create_denv gl.uc; }

80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97
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

98 99 100 101 102 103 104 105
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 *)

106 107 108 109 110 111 112 113 114 115 116 117 118 119
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) =
120 121 122
  let id = { id = vs.vs_name.id_string;
             id_lab = vs.vs_name.id_label;
             id_loc = loc } in
123
  id, specialize_type_v ~loc htv tyv
124

125
let specialize_global loc x gl =
126
  let s, tyv = Mstr.find x gl.globals in
127
  s, specialize_type_v ~loc (Htv.create 17) tyv
128

129 130 131
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
132 133 134 135
  match Denv.specialize_lsymbol ~loc s with
    | tyl, Some ty -> s, tyl, ty
    | _, None -> assert false

136 137 138 139
let create_type_var loc =
  let tv = Ty.create_tvsymbol (id_user "a" loc) in
  Tyvar (create_ty_decl_var ~loc ~user:false tv)

Andrei Paskevich's avatar
Andrei Paskevich committed
140 141 142 143
let add_pure_var id ty env = match ty with
  | Tyapp (ts, _) when Ty.ts_equal ts env.env.ts_arrow -> env.denv
  | _ -> Typing.add_var id ty env.denv

144
let dcurrying gl tyl ty =
145
  let make_arrow_type ty1 ty2 = dty_app (gl.ts_arrow, [ty1; ty2]) in
146
  List.fold_right make_arrow_type tyl ty
147

148
let uncurrying gl ty =
149
  let rec uncurry acc ty = match ty.ty_node with
150 151 152 153
    | Ty.Tyapp (ts, [t1; t2]) when ts_equal ts gl.ts_arrow -> 
	uncurry (t1 :: acc) t2
    | _ -> 
	List.rev acc, ty
154 155 156
  in
  uncurry [] ty

157
let expected_type e ty =
158 159
  if not (Denv.unify e.dexpr_type ty) then
    errorm ~loc:e.dexpr_loc 
160
      "this expression has type %a, but is expected to have type %a"
161
      print_dty e.dexpr_type print_dty ty
162

163 164
let pure_type env = Typing.dty env.denv

165 166 167 168
let rec dpurify env = function
  | DTpure ty -> 
      ty
  | DTarrow (bl, c) -> 
169
      dcurrying env.env (List.map (fun (_,ty) -> dpurify env ty) bl)
170
	(dpurify env c.dc_result_type)
171

172
let check_reference_type gl loc ty =
173
  let ty_ref = dty_app (gl.ts_ref, [create_type_var loc]) in
174 175 176
  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
177 178 179 180 181
  
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
182
    check_reference_type env.env id.id_loc ty;
183 184 185
    DRlocal id.id
  else 
    let p = Qident id in
186 187
    let s, _, ty = Typing.specialize_fsymbol p env.env.uc in
    check_reference_type env.env id.id_loc ty;
188 189
    DRglobal s

190
let dexception env id =
191
  let _, _, ty as r = specialize_exception id.id_loc id.id env.env in
192
  let ty_exn = dty_app (env.env.ts_exn, []) in
193 194 195 196 197
  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
198 199 200 201

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;
202 203 204
    de_raises = 
      List.map (fun id -> let ls,_,_ = dexception env id in ls) 
	e.Pgm_ptree.pe_raises; }
205

206 207
let dterm env l = Typing.dterm env (Pgm_env.logic_lexpr l)
let dfmla env l = Typing.dfmla env (Pgm_env.logic_lexpr l)
208

209 210 211 212 213
let dpost env ty (q, ql) =
  let dexn (id, l) =
    let s, tyl, _ = dexception env id in
    let denv = match tyl with
      | [] -> env.denv
Andrei Paskevich's avatar
Andrei Paskevich committed
214
      | [ty] -> add_pure_var id_result ty env
215 216
      | _ -> assert false
    in
217
    s, dfmla denv l
218
  in
Andrei Paskevich's avatar
Andrei Paskevich committed
219
  let denv = add_pure_var id_result ty env in
220
  dfmla denv q, List.map dexn ql
221

Andrei Paskevich's avatar
Andrei Paskevich committed
222 223 224
let add_local_top env x tyv =
  { env with locals = Mstr.add x tyv env.locals }

225 226
let add_local env x tyv = 
  let ty = dpurify env tyv in
Andrei Paskevich's avatar
Andrei Paskevich committed
227 228
  { env with locals = Mstr.add x tyv env.locals;
             denv = add_pure_var x ty env }
229

230 231 232 233 234 235 236 237 238 239
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
240
  { dc_result_type = ty;
241
    dc_effect      = deffect env c.Pgm_ptree.pc_effect;
242
    dc_pre         = dfmla env.denv c.Pgm_ptree.pc_pre;
243
    dc_post        = dpost env (dpurify env ty) c.Pgm_ptree.pc_post;
244
  }
245

246
and dbinder env ({id=x; id_loc=loc} as id, v) =
247 248 249 250
  let v = match v with
    | Some v -> dtype_v env v 
    | None -> DTpure (create_type_var loc)
  in
251
  add_local env x v, (id, v)
252

253 254
let rec add_local_pat env p = match p.dp_node with
  | Pwild -> env
Andrei Paskevich's avatar
Andrei Paskevich committed
255 256 257 258
  | Pvar x -> add_local env x.id (DTpure p.dp_ty)
  | Papp (_, pl) -> List.fold_left add_local_pat env pl
  | Pas (p, x) -> add_local_pat (add_local env x.id (DTpure p.dp_ty)) p
  | Por (p, q) -> add_local_pat (add_local_pat env p) q
259

260 261
let dvariant env (l, p) =
  let s, _ = Typing.specialize_psymbol p env.env.uc in
262 263 264 265 266 267 268 269
  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;
270
  dterm env.denv l, s
271

272 273 274
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; }
275

276 277
(* [dexpr] translates ptree into dexpr *)

278
let rec dexpr env e = 
279
  let d, ty = dexpr_desc env e.Pgm_ptree.expr_loc e.Pgm_ptree.expr_desc in
280
  { dexpr_desc = d; dexpr_loc = e.Pgm_ptree.expr_loc;
281
    dexpr_denv = env.denv; dexpr_type = ty; }
282

283
and dexpr_desc env loc = function
284
  | Pgm_ptree.Econstant (ConstInt _ as c) ->
285
      DEconstant c, dty_app (Ty.ts_int, [])
286
  | Pgm_ptree.Econstant (ConstReal _ as c) ->
287
      DEconstant c, dty_app (Ty.ts_real, [])
288
  | Pgm_ptree.Eident (Qident {id=x}) when Mstr.mem x env.locals ->
289
      (* local variable *)
290 291
      let tyv = Mstr.find x env.locals in
      DElocal (x, tyv), dpurify env tyv
292
  | Pgm_ptree.Eident (Qident {id=x}) when Mstr.mem x env.env.globals ->
293
      (* global variable *)
294
      let s, tyv = specialize_global loc x env.env in
295
      DEglobal (s, tyv), dpurify env tyv
296
  | Pgm_ptree.Eident p ->
297 298 299 300 301
      let s,tyl,ty = Typing.specialize_lsymbol p env.env.uc in
      let ty = match ty with
        | Some ty -> ty
        | None -> dty_bool env.env
      in
302
      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)
Andrei Paskevich's avatar
Andrei Paskevich committed
371 372 373
  | Pgm_ptree.Ematch (e1, bl) ->
      let e1 = dexpr env e1 in
      let ty1 = e1.dexpr_type in
374
      let ty = create_type_var loc in (* the type of all branches *)
Andrei Paskevich's avatar
Andrei Paskevich committed
375 376
      let branch (p, e) =
	let denv, p = Typing.dpat_list env.denv ty1 p in
377
	let env = { env with denv = denv } in
Andrei Paskevich's avatar
Andrei Paskevich committed
378
	let env = add_local_pat env p in
379 380
	let e = dexpr env e in
	expected_type e ty;
Andrei Paskevich's avatar
Andrei Paskevich committed
381
	p, e
382 383
      in
      let bl = List.map branch bl in
Andrei Paskevich's avatar
Andrei Paskevich committed
384
      DEmatch (e1, bl), ty
385
  | Pgm_ptree.Eskip ->
386
      DElogic env.env.ls_unit, (dty_unit env.env)
387 388
  | Pgm_ptree.Eabsurd ->
      DEabsurd, create_type_var loc
389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406
  | 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
407 408 409 410 411 412 413 414 415 416 417 418 419
  | 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] -> 
420
	      Some x.id, add_local env x.id (DTpure ty)
421 422 423 424 425 426 427 428
	  | _ ->
	      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
429 430

  | Pgm_ptree.Eassert (k, le) ->
431
      DEassert (k, dfmla env.denv le), dty_unit env.env
432
  | Pgm_ptree.Elabel ({id=s}, e1) ->
433
      if Typing.mem_var s env.denv then 
434
	errorm ~loc "clash with previous label %s" s;
435
      let ty = dty_label env.env in
Andrei Paskevich's avatar
Andrei Paskevich committed
436
      let env = { env with denv = add_pure_var s ty env } in
437
      let e1 = dexpr env e1 in
438
      DElabel (s, e1), e1.dexpr_type
439 440 441 442 443
  | 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
444 445 446
  | Pgm_ptree.Eany c ->
      let c = dtype_c env c in
      DEany c, dpurify env c.dc_result_type
447

448 449
and dletrec env dl =
  (* add all functions into environment *)
450
  let add_one env (id, bl, var, t) = 
451
    let ty = create_type_var id.id_loc in
Andrei Paskevich's avatar
Andrei Paskevich committed
452
    let env = add_local_top env id.id (DTpure ty) in
453
    env, ((id, ty), bl, var, t)
454
  in
455
  let env, dl = map_fold_left add_one env dl in
456
  (* then type-check all of them and unify *)
457
  let type_one ((id, tyres), bl, v, t) = 
458
    let env, bl = map_fold_left dbinder env bl in
459
    let v = option_map (dvariant env) v in
460
    let (_,e,_) as t = dtriple env t in
461
    let tyl = List.map (fun (x,_) -> Typing.find_var x.id env.denv) bl in
462
    let ty = dcurrying env.env tyl e.dexpr_type in
463 464 465 466
    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;
467
    ((id, tyres), bl, v, t)
468 469 470
  in
  env, List.map type_one dl

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

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

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

484 485 486
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
487 488 489 490
  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
491

492
let pre = Denv.fmla
493

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

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

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

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

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

543
let mk_iexpr loc ty d = { iexpr_desc = d; iexpr_loc = loc; iexpr_type = ty }
544

545 546 547 548
let mk_t_if gl f =
  let ty = ty_app gl.ts_bool [] in
  t_if f (t_app gl.ls_True [] ty) (t_app gl.ls_False [] ty)

549 550 551 552 553 554 555 556 557 558
(* 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)
*)
559
let make_logic_app gl loc ty ls el =
560
  let rec make args = function
561 562 563 564 565
    | [] ->
        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
566
    | ({ iexpr_desc = IElogic t }, _) :: r ->
567
	make (t :: args) r
568
    | ({ iexpr_desc = IElocal (vs, _) }, _) :: r ->
569
	make (t_var vs :: args) r
570
    | ({ iexpr_desc = IEglobal (ls, _); iexpr_type = ty }, _) :: r ->
571
	make (t_app ls [] ty :: args) r
572
    | (e, _) :: r ->
573
	let v = create_vsymbol (id_user "x" loc) e.iexpr_type in
574
	let d = mk_iexpr loc ty (make (t_var v :: args) r) in
575
	IElet (v, e, d)
576 577 578
  in
  make [] el

579 580
let is_reference_type gl ty  = match ty.ty_node with
  | Ty.Tyapp (ts, _) -> Ty.ts_equal ts gl.ts_ref
581 582
  | _ -> false

583 584 585 586
(* 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)
*)
587
let make_app gl loc ty f el =
588 589 590
  let rec make k = function
    | [] ->
	k f
591 592
    | ({ iexpr_type = ty } as e, tye) :: r when is_reference_type gl ty ->
	begin match e.iexpr_desc with
593
	  | IElocal (v, _) -> 
594
	      make (fun f -> mk_iexpr loc tye (IEapply_ref (k f, Rlocal v))) r
595
	  | IEglobal (v, _) ->
596
	      make (fun f -> mk_iexpr loc tye (IEapply_ref (k f, Rglobal v))) r
597
	  | _ ->
598
	      let v = create_vsymbol (id_user "x" loc) e.iexpr_type in
599
	      let d = 
600
		make (fun f -> mk_iexpr loc tye (IEapply_ref (k f, Rlocal v))) r
601
	      in
602
	      mk_iexpr loc ty (IElet (v, e, d))
603
	end
604
    | ({ iexpr_desc = IElocal (v, _) }, tye) :: r ->
605
	make (fun f -> mk_iexpr loc tye (IEapply (k f, v))) r
606
    | (e, tye) :: r ->
607
	let v = create_vsymbol (id_user "x" loc) e.iexpr_type in
608 609
	let d = make (fun f -> mk_iexpr loc tye (IEapply (k f, v))) r in
	mk_iexpr loc ty (IElet (v, e, d))
610 611 612
  in
  make (fun f -> f) el

613 614 615
(* [iexpr] translates dexpr into iexpr
   [env : vsymbol Mstr.t] maps strings to vsymbols for local variables *)

616
let rec iexpr gl env e =
617
  let ty = Denv.ty_of_dty e.dexpr_type in
618 619
  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 }
620

621
and iexpr_desc gl env loc ty = function
622
  | DEconstant c ->
623
      IElogic (t_const c)
624 625 626 627
  | DElocal (x, tyv) ->
      IElocal (Mstr.find x env, type_v gl env tyv)
  | DEglobal (ls, tyv) ->
      IEglobal (ls, type_v gl env tyv)
628
  | DElogic ls ->
629 630
      begin match ls.ls_args, ls.ls_value with
	| [], Some _ ->
631
	    IElogic (t_app ls [] ty)
632 633 634
	| [], None ->
            IElogic (mk_t_if gl (f_app ls []))
	| al, _ ->
635 636 637
	    errorm ~loc "function symbol %s is expecting %d arguments"
	      ls.ls_name.id_string (List.length al)
      end
638
  | DEapply (e1, e2) ->
639
      let f, args = decompose_app gl env e1 [iexpr gl env e2, ty] in
640 641 642 643 644 645
      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;
646
	    make_logic_app gl loc ty ls args
647
	| _ ->
648 649
	    let f = iexpr gl env f in
	    (make_app gl loc ty f args).iexpr_desc
650
      end
651
  | DEfun (bl, e1) ->
652 653
      let env, bl = map_fold_left (binder gl) env bl in
      IEfun (bl, itriple gl env e1)
654
  | DElet (x, e1, e2) ->
655
      let e1 = iexpr gl env e1 in
656 657
      let v = create_vsymbol (id_user x.id x.id_loc) e1.iexpr_type in
      let env = Mstr.add x.id v env in
658
      IElet (v, e1, iexpr gl env e2)
659
  | DEletrec (dl, e1) ->
660
      let env, dl = iletrec gl env dl in
661 662
      let e1 = iexpr gl env e1 in
      IEletrec (dl, e1)
663 664

  | DEsequence (e1, e2) ->
665 666
      let vs = create_vsymbol (id_fresh "_") (ty_app gl.ts_unit []) in
      IElet (vs, iexpr gl env e1, iexpr gl env e2)
667
  | DEif (e1, e2, e3) ->
668
      IEif (iexpr gl env e1, iexpr gl env e2, iexpr gl env e3)
669
  | DEloop (la, e1) ->
670 671
      let la = 
	{ loop_invariant = 
672
	    option_map (Denv.fmla env) la.dloop_invariant;
673
	  loop_variant   = 
674
	    option_map (variant loc env) la.dloop_variant; }
675
      in
676
      IEloop (la, iexpr gl env e1)
677
  | DElazy (op, e1, e2) ->
678
      IElazy (op, iexpr gl env e1, iexpr gl env e2)
Andrei Paskevich's avatar
Andrei Paskevich committed
679 680 681 682
  | DEmatch (e1, bl) ->
      let e1 = iexpr gl env e1 in
      let branch (p, e) = 
        let env, p = Denv.pattern env p in (p, iexpr gl env e)
683 684
      in
      let bl = List.map branch bl in
Andrei Paskevich's avatar
Andrei Paskevich committed
685 686
      let v = create_vsymbol (id_user "x" loc) e1.iexpr_type in
      IElet (v, e1, mk_iexpr loc ty (IEmatch (v, bl)))
687
  | DEabsurd ->
688
      IEabsurd
689
  | DEraise (ls, e) ->
690
      IEraise (ls, option_map (iexpr gl env) e)
691 692 693 694 695 696 697 698 699 700
  | 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
701
	(ls, x, iexpr gl env h)
702
      in
703
      IEtry (iexpr gl env e, List.map handler hl)
704 705

  | DEassert (k, f) ->
706
      let f = Denv.fmla env f in
707
      IEassert (k, f)
708
  | DElabel (s, e1) ->
709
      let ty = Ty.ty_app gl.ts_label [] in
710 711
      let v = create_vsymbol (id_fresh s) ty in
      let env = Mstr.add s v env in 
712
      IElabel (v, iexpr gl env e1)
713
  | DEany c ->
714
      let c = type_c gl env c in
715
      IEany c
716

717
and decompose_app gl env e args = match e.dexpr_desc with
718 719
  | DEapply (e1, e2) ->
      let ty = Denv.ty_of_dty e.dexpr_type in
720
      decompose_app gl env e1 ((iexpr gl env e2, ty) :: args)
721 722 723
  | _ ->
      e, args

724
and iletrec gl env dl =
725 726 727
  (* 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
728 729
    let v = create_vsymbol (id_user x.id x.id_loc) ty in
    let env = Mstr.add x.id v env in
730 731 732 733 734
    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)) =
735 736 737
    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
738
    let t = itriple gl env t in
739 740 741 742 743 744 745 746 747 748 749
    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
750 751
    (v, bl, var, t)
  in
752 753 754
  let dl = List.map step2 dl in
  (* finally, check variants are all absent or all present and consistent *)
  let error e =