pgm_typing.ml 68.7 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
open Pretty
29 30 31
open Denv
open Ptree
open Pgm_ttree
32
open Pgm_types
33
open Pgm_types.T
34
open Pgm_module
35

36
let debug = Debug.register_flag "program_typing"
37
let is_debug () = Debug.test_flag debug
38

39
exception Message of string
40 41

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

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

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

60 61
let id_result = "result"

62
(* phase 1: typing programs (using destructive type inference) **************)
63

64
let dty_app (ts, tyl) = assert (ts.ts_def = None); tyapp (ts, tyl)
65

66
let find_ts ~pure uc s =
67
  ns_find_ts (get_namespace (if pure then pure_uc uc else impure_uc uc)) [s]
68
let find_ls ~pure uc s =
69
  ns_find_ls (get_namespace (if pure then pure_uc uc else impure_uc uc)) [s]
70 71

(* TODO: improve efficiency *)
72
let dty_bool uc = dty_app (find_ts ~pure:true uc "bool", [])
73
let dty_int _uc = dty_app (Ty.ts_int, [])
74
let dty_unit _uc = dty_app (ts_tuple 0, [])
75
let dty_label uc = dty_app (find_ts ~pure:true uc "label_", [])
76

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

85
let create_denv uc =
86
  { uc = uc;
87
    locals = Mstr.empty;
88
    denv = Typing.create_denv (); }
89

90
let loc_of_id id = Util.of_option id.Ident.id_loc
91

92
let loc_of_ls ls = ls.ls_name.Ident.id_loc
93

94 95 96 97
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

98 99
type region_policy = Region_var | Region_ret | Region_glob

100
let rec create_regions ~user n =
101
  if n = 0 then
102
    []
103
  else
104 105
    let tv = create_tvsymbol (id_fresh "rho") in
    tyvar (create_ty_decl_var ~user tv) :: create_regions ~user (n - 1)
106

107 108 109 110
(* region variables are collected in the following list of lists
   so that we can check after typing that two region variables in the same
   list (i.e. for the same symbol) are not mapped to the same region *)

111 112
let region_vars = ref []

113 114 115
let new_regions_vars () =
  region_vars := Htv.create 17 :: !region_vars

116 117 118 119 120 121 122
let push_region_var tv vloc = match !region_vars with
  | [] -> assert false
  | h :: _ -> Htv.replace h tv vloc

let check_region_vars () =
  let values = Htv.create 17 in
  let check tv (v, loc) = match view_dty (tyvar v) with
123
    | Tyvar v'  ->
124 125 126 127 128 129 130 131
	let tv' = tvsymbol_of_type_var v' in
	begin try
	  let tv'' = Htv.find values tv' in
	  if not (tv_equal tv tv'') then
	    errorm ~loc "this application would create an alias";
	with Not_found ->
	  Htv.add values tv' tv
	end
132
    | Tyapp _ ->
133 134 135 136 137 138 139 140 141 142
	assert false
  in
  List.iter (fun h -> Htv.clear values; Htv.iter check h) !region_vars;
  region_vars := []

let rec specialize_ty ?(policy=Region_var) ~loc htv ty = match ty.ty_node with
  | Ty.Tyvar _ ->
      Denv.specialize_ty ~loc htv ty
  | Ty.Tyapp (ts, tl) ->
      let n = (get_mtsymbol ts).mt_regions in
143 144
      let mk_region ty = match ty.ty_node with
	| Ty.Tyvar _ when policy = Region_ret ->
145
	    tyvar (Typing.create_user_type_var "rho")
146
	| Ty.Tyvar tv when policy = Region_var ->
147 148 149 150 151
	    let v = Denv.find_type_var ~loc htv tv in
	    push_region_var tv (v, loc);
	    tyvar v
	| Ty.Tyvar tv (* policy = Region_glob *) ->
	    tyvar (create_ty_decl_var ~user:true tv)
152
	| Ty.Tyapp _ ->
153 154 155 156 157 158
	    assert false
      in
      let regions = List.map mk_region (Util.prefix n tl) in
      let tl = List.map (specialize_ty ~policy ~loc htv) (Util.chop n tl) in
      tyapp (ts, regions @ tl)

159 160 161 162
let rec specialize_type_v ?(policy=Region_var) ~loc htv = function
  | Tpure ty ->
      specialize_ty ~policy ~loc htv ty
  | Tarrow (bl, c) ->
163
      dcurrying
164 165 166
	(List.map (fun pv -> specialize_type_v ~loc htv pv.pv_tv) bl)
	(specialize_type_v ~policy:Region_ret ~loc htv c.c_result_type)

167 168 169 170
let specialize_lsymbol ?(policy=Region_var) ~loc htv s =
  List.map (specialize_ty ~policy ~loc htv) s.ls_args,
  option_map (specialize_ty ~policy:Region_ret ~loc htv) s.ls_value

171 172 173 174 175 176
let parameter x = "parameter " ^ x
let rec parameter_q = function
  | [] -> assert false
  | [x] -> [parameter x]
  | x :: q -> x :: parameter_q q

177
let dot fmt () = pp_print_string fmt "."
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
178
let print_qualids = print_list dot pp_print_string
179
let print_qualid fmt q =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
180
  print_list dot pp_print_string fmt (Typing.string_list_of_qualid [] q)
181

182
let specialize_exception loc x uc =
183
  let s =
184
    try ns_find_ex (namespace uc) x
185
    with Not_found -> errorm ~loc "@[unbound exception %a@]" print_qualids x
186
  in
187 188 189 190
  match Denv.specialize_lsymbol ~loc s with
    | tyl, Some ty -> s, tyl, ty
    | _, None -> assert false

191 192
let create_type_var loc =
  let tv = Ty.create_tvsymbol (id_user "a" loc) in
193
  tyvar (create_ty_decl_var ~loc ~user:false tv)
194

195
let add_pure_var id ty denv = match view_dty ty with
196 197
  | Tyapp (ts, _) when Ty.ts_equal ts ts_arrow -> denv
  | _ -> Typing.add_var id ty denv
198

199
let uncurrying ty =
200
  let rec uncurry acc ty = match ty.ty_node with
201
    | Ty.Tyapp (ts, [t1; t2]) when ts_equal ts ts_arrow ->
202
	uncurry (t1 :: acc) t2
203
    | _ ->
204
	List.rev acc, ty
205 206 207
  in
  uncurry [] ty

208
let expected_type e ty =
209
  if not (Denv.unify e.dexpr_type ty) then
210
    errorm ~loc:e.dexpr_loc
211
      "@[this expression has type %a,@ but is expected to have type %a@]"
212
      print_dty e.dexpr_type print_dty ty
213

214
let check_mutable_type loc dty = match view_dty dty with
215
  | Denv.Tyapp (ts, _) when is_mutable_ts ts ->
216
      ()
217
  | _ ->
218
      errorm ~loc
219
      "@[this expression has type %a,@ but is expected to have a mutable type@]"
220
	print_dty dty
221

222
let dexception uc qid =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
223 224
  let sl = Typing.string_list_of_qualid [] qid in
  let loc = Typing.qloc qid in
225
  let _, _, ty as r = specialize_exception loc sl uc in
226
  let ty_exn = dty_app (ts_exn, []) in
227
  if not (Denv.unify ty ty_exn) then
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
228
    errorm ~loc
229
      "@[this expression has type %a,@ but is expected to be an exception@]"
230 231
      print_dty ty;
  r
232

233 234 235 236
let dueffect env e =
  { du_reads  = e.Ptree.pe_reads;
    du_writes = e.Ptree.pe_writes;
    du_raises =
237
      List.map (fun id -> let ls,_,_ = dexception env.uc id in ls)
238
	e.Ptree.pe_raises; }
239

240
let dpost uc (q, ql) =
241
  let dexn (id, l) = let s, _, _ = dexception uc id in s, l in
242
  q, List.map dexn ql
243

Andrei Paskevich's avatar
Andrei Paskevich committed
244 245 246
let add_local_top env x tyv =
  { env with locals = Mstr.add x tyv env.locals }

247
let add_local env x ty =
248
  { env with locals = Mstr.add x ty env.locals; }
249

250
let rec dpurify_utype_v = function
251
  | DUTpure ty ->
252
      ty
253
  | DUTarrow (bl, c) ->
254
      dcurrying (List.map (fun (_,ty,_) -> ty) bl)
255
	(dpurify_utype_v c.duc_result_type)
256

257 258
(* user indicates whether region type variables can be instantiated *)
let rec dtype ~user env = function
259 260 261 262 263 264 265
  | PPTtyvar {id=x} ->
      tyvar (Typing.find_user_type_var x env.denv)
  | PPTtyapp (p, x) ->
      let loc = Typing.qloc x in
      let ts, a = Typing.specialize_tysymbol loc x (impure_uc env.uc) in
      let mt = get_mtsymbol ts in
      let np = List.length p in
266 267 268
      if np <> a - mt.mt_regions then
	errorm ~loc "@[the type %a expects %d argument(s),@
                       but is applied to %d argument(s)@]"
269
	  print_qualid x (a - mt.mt_regions) np;
270 271
      let tyl = List.map (dtype ~user env) p in
      let tyl = create_regions ~user mt.mt_regions @ tyl in
272 273 274 275 276 277 278 279 280 281
      begin match ts.ts_def with
	| None ->
	    tyapp (ts, tyl)
	| Some ty ->
	    let add m v t = Mtv.add v t m in
	    let s = List.fold_left2 add Mtv.empty ts.ts_args tyl in
	    Typing.type_inst s ty
      end
  | PPTtuple tyl ->
      let ts = ts_tuple (List.length tyl) in
282
      tyapp (ts, List.map (dtype ~user env) tyl)
283

284
let rec dutype_v env = function
285
  | Ptree.Tpure pt ->
286
      DUTpure (dtype ~user:true env pt)
287
  | Ptree.Tarrow (bl, c) ->
288 289 290 291 292 293 294
      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;
295
    duc_effect      = dueffect env c.Ptree.pc_effect;
296 297
    duc_pre         = c.Ptree.pc_pre;
    duc_post        = dpost env.uc c.Ptree.pc_post;
298
  }
299

300
and dubinder env ({id=x; id_loc=loc} as id, v) =
301
  let v = match v with
302 303
    | Some v -> dutype_v env v
    | None -> DUTpure (create_type_var loc)
304
  in
305
  let ty = dpurify_utype_v v in
306
  add_local env x ty, (id, ty, v)
307

308
let rec add_local_pat env p = match p.dp_node with
309 310 311 312 313
  | 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
314

315
let dvariant env (l, p) =
316
  let relation p =
317
    let s, _ = Typing.specialize_psymbol p (pure_uc env.uc) in
318 319 320 321 322 323 324 325 326
    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
327

328
let dloop_annotation env a =
329
  { dloop_invariant = a.Ptree.loop_invariant;
330
    dloop_variant   = option_map (dvariant env) a.Ptree.loop_variant; }
331

332
(***
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
333 334 335
let is_ps_ghost e = match e.dexpr_desc with
  | DEglobal (ps, _) -> T.p_equal ps ps_ghost
  | _ -> false
336
***)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
337

338 339
(* [dexpr] translates ptree into dexpr *)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
340 341 342
let rec dexpr ~ghost env e =
  let d, ty = dexpr_desc ~ghost env e.Ptree.expr_loc e.Ptree.expr_desc in
  let loc = e.Ptree.expr_loc in
343
  let e = {
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
344
    dexpr_desc = d; dexpr_loc = loc;
345
    (* dexpr_denv = env.denv;  *)dexpr_type = ty; }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
346
  in
347
  (****
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
348 349 350
  match view_dty ty with
    (* if below ghost and e has ghost type, then unghost it *)
    | Denv.Tyapp (ts, [ty']) when ghost && ts_equal ts mt_ghost.mt_abstr ->
351
	let unghost =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
352 353 354 355 356 357 358
	  let tv = specialize_type_v ~loc (Htv.create 17) ps_unghost.p_tv in
	  match tv with
	    | DTarrow ([_,tyx,_], _) ->
		if not (Denv.unify ty tyx) then assert false;
		let dtv = dpurify_type_v tv in
		{ dexpr_desc = DEglobal (ps_unghost, tv);
		  dexpr_loc = loc; dexpr_denv = env.denv; dexpr_type = dtv; }
359
	    | _ ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
360 361 362 363 364
		assert false
	in
	{ dexpr_desc = DEapply (unghost, e); dexpr_loc = e.dexpr_loc;
	  dexpr_denv = env.denv; dexpr_type = ty'; }
    | _ ->
365 366
  ****)
  e
367

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
368
and dexpr_desc ~ghost env loc = function
369
  | Ptree.Econstant (ConstInt _ as c) ->
370
      DEconstant c, dty_app (Ty.ts_int, [])
371
  | Ptree.Econstant (ConstReal _ as c) ->
372
      DEconstant c, dty_app (Ty.ts_real, [])
373
  | Ptree.Eident (Qident {id=x}) when Mstr.mem x env.locals ->
374
      (* local variable *)
375
      let tyv = Mstr.find x env.locals in
376
      DElocal (x, tyv), tyv
377
  | Ptree.Eident p ->
378
      (* global variable *)
379
      new_regions_vars ();
380
      let x = Typing.string_list_of_qualid [] p in
381 382
      let ls =
	try
383
	  ns_find_ls (get_namespace (impure_uc env.uc)) (parameter_q x)
384 385
	with Not_found -> try
	  ns_find_ls (get_namespace (impure_uc env.uc)) x
386 387
	with Not_found ->
	  errorm ~loc "unbound symbol %a" print_qualid p
388 389 390 391
      in
      let ps = get_psymbol ls in
      begin match ps.ps_kind with
	| PSvar v ->
392 393 394
	    let htv = Htv.create 17 in
	    let dty = specialize_type_v ~loc ~policy:Region_glob htv v.pv_tv in
	    DEglobal (ps, v.pv_tv, htv), dty
395
	| PSfun tv ->
396 397 398
	    let htv = Htv.create 17 in
	    let dty = specialize_type_v ~loc htv tv in
	    DEglobal (ps, tv, htv), dty
399
	| PSlogic ->
400
	    let tyl, ty = Denv.specialize_lsymbol ~loc ps.ps_impure in
401 402 403 404 405
	    let ty = match ty with
              | Some ty -> ty
              | None -> dty_bool env.uc
	    in
	    DElogic ps.ps_pure, dcurrying tyl ty
406
      end
407
  | Ptree.Elazy (op, e1, e2) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
408
      let e1 = dexpr ~ghost env e1 in
409
      expected_type e1 (dty_bool env.uc);
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
410
      let e2 = dexpr ~ghost env e2 in
411 412
      expected_type e2 (dty_bool env.uc);
      DElazy (op, e1, e2), dty_bool env.uc
413
  | Ptree.Eapply (e1, e2) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
414
      let e1 = dexpr ~ghost env e1 in
415
      let ghost = ghost (* || is_ps_ghost e1 *) in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
416
      let e2 = dexpr ~ghost env e2 in
417
      let ty2 = create_type_var loc and ty = create_type_var loc in
418
      if not (Denv.unify e1.dexpr_type (dty_app (ts_arrow, [ty2; ty]))) then
419 420 421
	errorm ~loc:e1.dexpr_loc "this expression is not a function";
      expected_type e2 ty2;
      DEapply (e1, e2), ty
422
  | Ptree.Efun (bl, t) ->
423
      let env, bl = map_fold_left dubinder env bl in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
424
      let (_,e,_) as t = dtriple ~ghost env t in
425
      let tyl = List.map (fun (_,ty,_) -> ty) bl in
426
      let ty = dcurrying tyl e.dexpr_type in
427
      DEfun (bl, t), ty
428
  | Ptree.Elet (x, e1, e2) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
429
      let e1 = dexpr ~ghost env e1 in
430
      let ty1 = e1.dexpr_type in
431
      let env = add_local env x.id ty1 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
432
      let e2 = dexpr ~ghost env e2 in
433
      DElet (x, e1, e2), e2.dexpr_type
434
  | Ptree.Eletrec (dl, e1) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
435 436
      let env, dl = dletrec ~ghost env dl in
      let e1 = dexpr ~ghost env e1 in
437
      DEletrec (dl, e1), e1.dexpr_type
438
  | Ptree.Etuple el ->
439 440 441
      let n = List.length el in
      let s = Typing.fs_tuple n in
      let tyl = List.map (fun _ -> create_type_var loc) el in
442
      let ty = dty_app (Typing.ts_tuple n, tyl) in
443
      let create d ty = { dexpr_desc = d; dexpr_type = ty; dexpr_loc = loc } in
444
      let apply e1 e2 ty2 =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
445
	let e2 = dexpr ~ghost env e2 in
446 447
	assert (Denv.unify e2.dexpr_type ty2);
	let ty = create_type_var loc in
448
	assert (Denv.unify e1.dexpr_type (dty_app (ts_arrow, [ty2; ty])));
449 450
	create (DEapply (e1, e2)) ty
      in
451
      let e = create (DElogic s) (dcurrying tyl ty) in
452 453
      let e = List.fold_left2 apply e el tyl in
      e.dexpr_desc, ty
454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475
  | Ptree.Erecord fl ->
      let _, cs, fl = Typing.list_fields (impure_uc env.uc) fl in
      new_regions_vars ();
      let tyl, ty = specialize_lsymbol ~loc (Htv.create 17) cs in
      let ty = of_option ty in
      let create d ty = { dexpr_desc = d; dexpr_type = ty; dexpr_loc = loc } in
      let constructor d f tyf = match f with
	| Some (_, f) ->
	    let f = dexpr ~ghost env f in
	    assert (Denv.unify f.dexpr_type tyf);
	    let ty = create_type_var loc in
	    assert (Denv.unify d.dexpr_type (dty_app (ts_arrow, [tyf; ty])));
	    create (DEapply (d, f)) ty
	| None ->
	    errorm ~loc "some record fields are missing"
      in
      let d =
	let ps = get_psymbol cs in
	create (DElogic ps.ps_pure) (dcurrying tyl ty)
      in
      let d = List.fold_left2 constructor d fl tyl in
      d.dexpr_desc, ty
476 477
  | Ptree.Eassign _ ->
      assert false (*TODO*)
478

479
  | Ptree.Esequence (e1, e2) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
480
      let e1 = dexpr ~ghost env e1 in
481
      expected_type e1 (dty_unit env.uc);
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
482
      let e2 = dexpr ~ghost env e2 in
483
      DEsequence (e1, e2), e2.dexpr_type
484
  | Ptree.Eif (e1, e2, e3) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
485
      let e1 = dexpr ~ghost env e1 in
486
      expected_type e1 (dty_bool env.uc);
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
487 488
      let e2 = dexpr ~ghost env e2 in
      let e3 = dexpr ~ghost env e3 in
489 490
      expected_type e3 e2.dexpr_type;
      DEif (e1, e2, e3), e2.dexpr_type
491
  | Ptree.Eloop (a, e1) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
492
      let e1 = dexpr ~ghost env e1 in
493 494
      expected_type e1 (dty_unit env.uc);
      DEloop (dloop_annotation env a, e1), dty_unit env.uc
495
  | Ptree.Ematch (e1, bl) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
496
      let e1 = dexpr ~ghost env e1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
497
      let ty1 = e1.dexpr_type in
498
      let ty = create_type_var loc in (* the type of all branches *)
Andrei Paskevich's avatar
Andrei Paskevich committed
499
      let branch (p, e) =
500
	let denv, p = Typing.dpat_list (impure_uc env.uc) env.denv ty1 p in
501
	let env = { env with denv = denv } in
Andrei Paskevich's avatar
Andrei Paskevich committed
502
	let env = add_local_pat env p in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
503
	let e = dexpr ~ghost env e in
504
	expected_type e ty;
Andrei Paskevich's avatar
Andrei Paskevich committed
505
	p, e
506 507
      in
      let bl = List.map branch bl in
Andrei Paskevich's avatar
Andrei Paskevich committed
508
      DEmatch (e1, bl), ty
509
  | Ptree.Eabsurd ->
510
      DEabsurd, create_type_var loc
511
  | Ptree.Eraise (qid, e) ->
512
      let ls, tyl, _ = dexception env.uc qid in
513
      let e = match e, tyl with
514
	| None, [] ->
515 516
	    None
	| Some _, [] ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
517
	    errorm ~loc "expection %a has no argument" print_qualid qid
518
	| None, [ty] ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
519 520
	    errorm ~loc "exception %a is expecting an argument of type %a"
	      print_qualid qid print_dty ty;
521
	| Some e, [ty] ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
522
	    let e = dexpr ~ghost env e in
523 524
	    expected_type e ty;
	    Some e
525
	| _ ->
526 527 528
	    assert false
      in
      DEraise (ls, e), create_type_var loc
529
  | Ptree.Etry (e1, hl) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
530
      let e1 = dexpr ~ghost env e1 in
531
      let handler (id, x, h) =
532
	let ls, tyl, _ = dexception env.uc id in
533
	let x, env = match x, tyl with
534
	  | Some _, [] ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
535
	      errorm ~loc "expection %a has no argument" print_qualid id
536
	  | None, [] ->
537 538
	      None, env
	  | None, [ty] ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
539 540
	      errorm ~loc "exception %a is expecting an argument of type %a"
		print_qualid id print_dty ty;
541
	  | Some x, [ty] ->
542
	      Some x.id, add_local env x.id ty
543 544 545
	  | _ ->
	      assert false
	in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
546
	let h = dexpr ~ghost env h in
547 548 549 550
	expected_type h e1.dexpr_type;
	(ls, x, h)
      in
      DEtry (e1, List.map handler hl), e1.dexpr_type
551
  | Ptree.Efor (x, e1, d, e2, inv, e3) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
552
      let e1 = dexpr ~ghost env e1 in
553
      expected_type e1 (dty_int env.uc);
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
554
      let e2 = dexpr ~ghost env e2 in
555
      expected_type e2 (dty_int env.uc);
556
      let env = add_local env x.id (dty_int env.uc) in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
557
      let e3 = dexpr ~ghost env e3 in
558 559
      expected_type e3 (dty_unit env.uc);
      DEfor (x, e1, d, e2, inv, e3), dty_unit env.uc
560

561
  | Ptree.Eassert (k, le) ->
562
      DEassert (k, le), dty_unit env.uc
563
  | Ptree.Elabel ({id=s}, e1) ->
564
      if Typing.mem_var s env.denv then
565
	errorm ~loc "clash with previous label %s" s;
566
      let ty = dty_label env.uc in
567
      let env = { env with denv = add_pure_var s ty env.denv } in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
568
      let e1 = dexpr ~ghost env e1 in
569
      DElabel (s, e1), e1.dexpr_type
570
  | Ptree.Ecast (e1, ty) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
571
      let e1 = dexpr ~ghost env e1 in
572
      let ty = dtype ~user:false env ty in
573 574
      expected_type e1 ty;
      e1.dexpr_desc, ty
575
  | Ptree.Eany c ->
576 577
      let c = dutype_c env c in
      DEany c, dpurify_utype_v c.duc_result_type
578

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
579
and dletrec ~ghost env dl =
580
  (* add all functions into environment *)
581
  let add_one env (id, bl, var, t) =
582
    let ty = create_type_var id.id_loc in
583
    let env = add_local_top env id.id ty in
584
    env, ((id, ty), bl, var, t)
585
  in
586
  let env, dl = map_fold_left add_one env dl in
587
  (* then type-check all of them and unify *)
588
  let type_one ((id, tyres), bl, v, t) =
589
    let env, bl = map_fold_left dubinder env bl in
590
    let v = option_map (dvariant env) v in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
591
    let (_,e,_) as t = dtriple ~ghost env t in
592
    let tyl = List.map (fun (_,ty,_) -> ty) bl in
593
    let ty = dcurrying tyl e.dexpr_type in
594
    if not (Denv.unify ty tyres) then
595
      errorm ~loc:id.id_loc
596
	"@[this expression has type %a,@ but is expected to have type %a@]"
597
	print_dty ty print_dty tyres;
598
    ((id, tyres), bl, v, t)
599 600 601
  in
  env, List.map type_one dl

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
602 603
and dtriple ~ghost env (p, e, q) =
  let e = dexpr ~ghost env e in
604
  let q = dpost env.uc q in
605 606
  (p, e, q)

607 608 609 610
(*** regions tables ********************************************************)

let region_types = Hts.create 17 (* ts -> int -> ty *)

611 612 613 614 615
let declare_region_type ts i ty =
  let h =
    try
      Hts.find region_types ts
    with Not_found ->
616 617 618 619 620
      let h = Hashtbl.create 17 in Hts.add region_types ts h; h
  in
  Hashtbl.add h i ty

let region_type ts i =
621 622 623
  (* eprintf "region_type: ts=%a i=%d@." Pretty.print_ts ts i; *)
  (* let mt = get_mtsymbol ts in *)
  (* eprintf "%a@." print_mt_symbol mt; *)
624 625 626 627
  Hashtbl.find (Hts.find region_types ts) i

let mutable_fields = Hts.create 17 (* ts -> field:int -> region:int *)

628 629 630 631 632
let declare_mutable_field ts i j =
  let h =
    try
      Hts.find mutable_fields ts
    with Not_found ->
633 634 635 636 637 638 639
      let h = Hashtbl.create 17 in Hts.add mutable_fields ts h; h
  in
  Hashtbl.add h i j

let mutable_field ts i =
  Hashtbl.find (Hts.find mutable_fields ts) i

640
let regions_tyapp ts nregions tyl =
641 642 643 644 645 646 647 648
  let tymatch s tv ty = Ty.ty_match s (ty_var tv) ty in
  let s = List.fold_left2 tymatch Mtv.empty ts.ts_args tyl in
  let mk i ty = match ty.ty_node with
    | Ty.Tyvar r -> R.create r (ty_inst s (region_type ts i))
    | Ty.Tyapp _ -> assert false
  in
  list_mapi mk (Util.prefix nregions tyl)

649
(* phase 2: remove destructive types and type annotations *****************)
650

651 652 653
let dterm env l = Typing.dterm ~localize:true env l
let dfmla env l = Typing.dfmla ~localize:true env l

654
type ienv = {
655
  i_uc      : uc;
656
  i_denv    : Typing.denv;
657 658 659
  i_impures : ivsymbol Mstr.t;
  i_effects : vsymbol Mstr.t;
  i_pures   : vsymbol Mstr.t;
660 661 662
}

let create_ivsymbol id ty =
663
  let vs = create_vsymbol id ty in
664
  let vse = create_vsymbol id (effectify ty) in
665
  let vsp =
666 667 668
    let ty' = purify ty in if ty_equal ty ty' then vs else create_vsymbol id ty'
  in
  { i_impure = vs; i_effect = vse; i_pure = vsp }
669

670
let rec dty_of_ty denv ty = match ty.ty_node with
671
  | Ty.Tyvar v ->
672
      Denv.tyvar (Typing.find_user_type_var v.tv_name.id_string denv)
673
  | Ty.Tyapp (ts, tyl) ->
674 675
      Denv.tyapp (ts, List.map (dty_of_ty denv) tyl)

676
let iadd_local env x ty =
677
  let v = create_ivsymbol x ty in
678
  let s = v.i_impure.vs_name.id_string in
679 680
  let env = { env with
    i_denv =
681 682 683 684
      (let dty = dty_of_ty env.i_denv v.i_pure.vs_ty in
       add_pure_var s dty env.i_denv);
    i_impures = Mstr.add s v env.i_impures;
    i_effects = Mstr.add s v.i_effect env.i_effects;
685
    i_pures = Mstr.add s v.i_pure env.i_pures; }
686
  in
687
  env, v
688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703

let rec type_effect_term env { pp_loc = loc; pp_desc = d } = match d with
  | PPvar (Qident x) when Mstr.mem x.id env.i_effects ->
      let v = Mstr.find x.id env.i_effects in
      v.vs_ty
  | PPvar q ->
      let x = Typing.string_list_of_qualid [] q in
      begin try
	let ls = ns_find_ls (get_namespace (effect_uc env.i_uc)) x in
	of_option ls.ls_value
      with Not_found ->
	errorm ~loc "unbound symbol %a" print_qualid q
      end
  | _ ->
      errorm ~loc "unsupported effect syntax"

704
let iuregion env ({ pp_loc = loc; pp_desc = d } as t) = match d with
705 706 707 708 709
  | PPapp (f, [t]) ->
      let th = effect_uc env.i_uc in
      let ls, _, _ = Typing.specialize_lsymbol f th in
      begin match Typing.is_projection th ls with
	| Some (ts, _, i) ->
710 711
	    let j =
	      try
712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731
		mutable_field ts i
	      with Not_found ->
		errorm ~loc "not a mutable record field"
	    in
	    let tloc = t.pp_loc in
	    let ty = type_effect_term env t in
	    begin match ty.ty_node with
	      | Ty.Tyapp (ts', tyl) when ts_equal ts ts' ->
		  let mt = get_mtsymbol ts in
		  let r = regions_tyapp ts mt.mt_regions tyl in
		  List.nth r j
	      | _ ->
		  errorm ~loc:tloc
	    "@[this expression has type %a,@ but is expected to have type %a@]"
		    Pretty.print_ty ty Pretty.print_ts ts
	    end
	| None ->
	    errorm ~loc "not a record field"
      end
  | _ ->
732
      let ty = type_effect_term env t in
733
      let not_mutable () = errorm ~loc
734
      "@[this expression has type %a,@ but is expected to have a mutable type@]"
735 736 737 738 739 740 741 742 743 744 745 746 747 748 749
	Pretty.print_ty ty
      in
      begin match ty.ty_node with
	| Ty.Tyapp (ts, tyl)  ->
	    let mt = get_mtsymbol ts in
	    let n = mt.mt_regions in
	    if n = 0 then not_mutable ();
	    if n > 1 then errorm ~loc
	      "ambiguous effect term (more than one region)";
	    let r = regions_tyapp ts mt.mt_regions tyl in
	    List.nth r 0
	| _ ->
	    not_mutable ()
      end

750 751 752 753
let iueffect env e = {
  ie_reads  = List.map (iuregion env) e.du_reads;
  ie_writes = List.map (iuregion env) e.du_writes;
  ie_raises = e.du_raises;