pgm_typing.ml 67.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
let is_debug () = Debug.test_flag debug
37

38
exception Message of string
39 40

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

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

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

59 60
let id_result = "result"

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

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

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

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

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

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

let specialize_post ~loc htv ((v, f), ql) =
  assert (v.vs_name.id_string = "result"); (* TODO *)
  let specialize_exn (l, (v, f)) =
92
    assert
93
      (match v with Some v -> v.vs_name.id_string = "result" | None -> true);
94 95
    let ty = option_map (fun v -> Denv.specialize_ty ~loc htv v.vs_ty) v in
    (l, (ty, specialize_fmla ~loc htv f))
96
  in
97 98 99
  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
100

101
let loc_of_id id = Util.of_option id.Ident.id_loc
102

103
let loc_of_ls ls = ls.ls_name.Ident.id_loc
104

105 106 107 108
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

109
let rec dpurify_type_v = function
110
  | DTpure ty ->
111
      ty
112
  | DTarrow (bl, c) ->
113
      dcurrying (List.map (fun (_,ty,_) -> ty) bl)
114 115
	(dpurify_type_v c.dc_result_type)

116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179
type region_policy = Region_var | Region_ret | Region_glob

let rec create_regions n =
  if n = 0 then 
    []
  else 
    tyvar (Typing.create_user_type_var "rho") :: create_regions (n - 1)

let region_vars = ref []

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
    | Tyvar v'  -> 
	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
    | Tyapp _ -> 
	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
      let mk_region ty = match ty.ty_node with 
	| Ty.Tyvar _ when policy = Region_ret -> 
	    tyvar (Typing.create_user_type_var "rho")
	| Ty.Tyvar tv when policy = Region_var -> 
	    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)
	| Ty.Tyapp _ -> 
	    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)

let specialize_effect ~loc htv e =
  let region r acc = 
    let tv = find_type_var ~loc htv r.R.r_tv in
    let ty = specialize_ty ~loc htv r.R.r_ty in
    { dr_tv = tv; dr_ty = ty } :: acc 
  in
  { de_reads  = Sreg.fold region e.E.reads  [];
    de_writes = Sreg.fold region e.E.writes [];
    de_raises = Sexn.elements e.E.raises; }

let rec specialize_type_v ?(policy=Region_var) ~loc htv = function
180
  | Tpure ty ->
181
      DTpure (specialize_ty ~policy ~loc htv ty)
182
  | Tarrow (bl, c) ->
183
      DTarrow (List.map (specialize_binder ~loc htv) bl,
184 185 186
	       specialize_type_c ~loc htv c)

and specialize_type_c ~loc htv c =
187 188 189
  { dc_result_type = 
      specialize_type_v ~policy:Region_ret ~loc htv c.c_result_type;
    dc_effect      = specialize_effect ~loc htv c.c_effect;
190 191 192
    dc_pre         = specialize_fmla ~loc htv c.c_pre;
    dc_post        = specialize_post ~loc htv c.c_post; }

193
and specialize_binder ~loc htv v =
194 195 196 197
  let id = {
    id = v.pv_name.id_string;
    id_lab = List.map (fun l -> Lstr l) v.pv_name.id_label;
    (* FIXME? We do the same here as in Denv.ident_of_vs *)
198
    id_loc = Util.default_option loc v.pv_name.Ident.id_loc }
199
  in
200 201
  let v = specialize_type_v ~loc htv v.pv_tv in
  id, dpurify_type_v v, v
202

203
let specialize_global loc x uc =
204
  region_vars := Htv.create 17 :: !region_vars;
205
  let p = ns_find_pr (namespace uc) x in
206 207 208 209 210
  match p with
    | PSvar v ->
	p, specialize_type_v ~loc ~policy:Region_glob (Htv.create 17) v.pv_tv
    | PSfun f ->
	p, specialize_type_v ~loc (Htv.create 17) f.p_tv
211

212
let dot fmt () = pp_print_string fmt "."
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
213 214 215
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)
216

217 218 219
let specialize_exception loc x uc =
  let s = 
    try ns_find_ex (namespace uc) x
220
    with Not_found -> errorm ~loc "@[unbound exception %a@]" print_qualids x
221
  in
222 223 224 225
  match Denv.specialize_lsymbol ~loc s with
    | tyl, Some ty -> s, tyl, ty
    | _, None -> assert false

226 227
let create_type_var loc =
  let tv = Ty.create_tvsymbol (id_user "a" loc) in
228
  tyvar (create_ty_decl_var ~loc ~user:false tv)
229

230
let add_pure_var id ty denv = match view_dty ty with
231 232
  | Tyapp (ts, _) when Ty.ts_equal ts ts_arrow -> denv
  | _ -> Typing.add_var id ty denv
233

234
let uncurrying ty =
235
  let rec uncurry acc ty = match ty.ty_node with
236
    | Ty.Tyapp (ts, [t1; t2]) when ts_equal ts ts_arrow ->
237
	uncurry (t1 :: acc) t2
238
    | _ ->
239
	List.rev acc, ty
240 241 242
  in
  uncurry [] ty

243
let expected_type e ty =
244
  if not (Denv.unify e.dexpr_type ty) then
245
    errorm ~loc:e.dexpr_loc
246
      "this expression has type %a, but is expected to have type %a"
247
      print_dty e.dexpr_type print_dty ty
248

249
let check_mutable_type loc dty = match view_dty dty with
250
  | Denv.Tyapp (ts, _) when is_mutable_ts ts -> 
251
      ()
252
  | _ ->
253 254
      errorm ~loc 
	"this expression has type %a, but is expected to have a mutable type"
255
	print_dty dty
256

257 258 259 260 261 262
let check_mutable_dtype_v loc = function
  | DTpure dty -> check_mutable_type loc dty
  | DTarrow _ -> 
      errorm ~loc 
	"this expression is a function, but is expected to have a mutable type"

263
let dexception uc qid =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
264 265
  let sl = Typing.string_list_of_qualid [] qid in
  let loc = Typing.qloc qid in
266
  let _, _, ty as r = specialize_exception loc sl uc in
267
  let ty_exn = dty_app (ts_exn, []) in
268
  if not (Denv.unify ty ty_exn) then
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
269
    errorm ~loc
270 271 272
      "this expression has type %a, but is expected to be an exception"
      print_dty ty;
  r
273

274 275 276 277
let dueffect env e =
  { du_reads  = e.Ptree.pe_reads;
    du_writes = e.Ptree.pe_writes;
    du_raises =
278
      List.map (fun id -> let ls,_,_ = dexception env.uc id in ls)
279
	e.Ptree.pe_raises; }
280

281
let dpost uc (q, ql) =
282
  let dexn (id, l) =
283
    let s, _, _ = dexception uc id in s, l
284
  in
285
  q, List.map dexn ql
286

Andrei Paskevich's avatar
Andrei Paskevich committed
287 288 289
let add_local_top env x tyv =
  { env with locals = Mstr.add x tyv env.locals }

290
let add_local env x ty =
291
  { env with locals = Mstr.add x ty env.locals; }
292

293
let rec dpurify_utype_v = function
294
  | DUTpure ty ->
295
      ty
296
  | DUTarrow (bl, c) ->
297
      dcurrying (List.map (fun (_,ty,_) -> ty) bl)
298
	(dpurify_utype_v c.duc_result_type)
299

300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325
let rec dtype env = function
  | 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
      if np <> a - mt.mt_regions then 
	errorm ~loc "@[the type %a expects %d argument(s),@ 
                       but is applied to %d argument(s)@]"  
	  print_qualid x (a - mt.mt_regions) np;
      let tyl = List.map (dtype env) p in
      let tyl = create_regions mt.mt_regions @ tyl in
      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
      tyapp (ts, List.map (dtype env) tyl)

326
let rec dutype_v env = function
327
  | Ptree.Tpure pt ->
328
      DUTpure (dtype env pt)
329
  | Ptree.Tarrow (bl, c) ->
330 331 332 333 334 335 336
      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;
337
    duc_effect      = dueffect env c.Ptree.pc_effect;
338 339
    duc_pre         = c.Ptree.pc_pre;
    duc_post        = dpost env.uc c.Ptree.pc_post;
340
  }
341

342
and dubinder env ({id=x; id_loc=loc} as id, v) =
343
  let v = match v with
344 345
    | Some v -> dutype_v env v
    | None -> DUTpure (create_type_var loc)
346
  in
347
  let ty = dpurify_utype_v v in
348
  add_local env x ty, (id, ty, v)
349

350
let rec add_local_pat env p = match p.dp_node with
351 352 353 354 355
  | 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
356

357
let dvariant env (l, p) =
358
  let relation p = 
359
    let s, _ = Typing.specialize_psymbol p (pure_uc env.uc) in
360 361 362 363 364 365 366 367 368
    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
369

370
let dloop_annotation env a =
371
  { dloop_invariant = a.Ptree.loop_invariant;
372
    dloop_variant   = option_map (dvariant env) a.Ptree.loop_variant; }
373

374
(***
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
375 376 377
let is_ps_ghost e = match e.dexpr_desc with
  | DEglobal (ps, _) -> T.p_equal ps ps_ghost
  | _ -> false
378
***)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
379

380 381
(* [dexpr] translates ptree into dexpr *)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
382 383 384 385 386
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
  let e = { 
    dexpr_desc = d; dexpr_loc = loc;
387
    (* dexpr_denv = env.denv;  *)dexpr_type = ty; }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
388
  in
389
  (****
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406
  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 ->
	let unghost = 
	  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; }
	    | _ -> 
		assert false
	in
	{ dexpr_desc = DEapply (unghost, e); dexpr_loc = e.dexpr_loc;
	  dexpr_denv = env.denv; dexpr_type = ty'; }
    | _ ->
407 408
  ****)
  e
409

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
410
and dexpr_desc ~ghost env loc = function
411
  | Ptree.Econstant (ConstInt _ as c) ->
412
      DEconstant c, dty_app (Ty.ts_int, [])
413
  | Ptree.Econstant (ConstReal _ as c) ->
414
      DEconstant c, dty_app (Ty.ts_real, [])
415
  | Ptree.Eident (Qident {id=x}) when Mstr.mem x env.locals ->
416
      (* local variable *)
417
      let tyv = Mstr.find x env.locals in
418
      DElocal (x, tyv), tyv
419
  | Ptree.Eident p ->
420 421 422 423
      begin try
	(* global variable *)
	let x = Typing.string_list_of_qualid [] p in
	let s, tyv = specialize_global loc x env.uc in
424 425
	let dty = dpurify_type_v tyv in
	DEglobal (s, tyv), dty
426
      with Not_found ->
427
	let s,tyl,ty = Typing.specialize_lsymbol p (pure_uc env.uc) in
428 429 430 431 432 433
	let ty = match ty with
          | Some ty -> ty
          | None -> dty_bool env.uc
	in
	DElogic s, dcurrying tyl ty
      end
434
  | Ptree.Elazy (op, e1, e2) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
435
      let e1 = dexpr ~ghost env e1 in
436
      expected_type e1 (dty_bool env.uc);
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
437
      let e2 = dexpr ~ghost env e2 in
438 439
      expected_type e2 (dty_bool env.uc);
      DElazy (op, e1, e2), dty_bool env.uc
440
  | Ptree.Eapply (e1, e2) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
441
      let e1 = dexpr ~ghost env e1 in
442
      let ghost = ghost (* || is_ps_ghost e1 *) in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
443
      let e2 = dexpr ~ghost env e2 in
444
      let ty2 = create_type_var loc and ty = create_type_var loc in
445
      if not (Denv.unify e1.dexpr_type (dty_app (ts_arrow, [ty2; ty]))) then
446 447 448
	errorm ~loc:e1.dexpr_loc "this expression is not a function";
      expected_type e2 ty2;
      DEapply (e1, e2), ty
449
  | Ptree.Efun (bl, t) ->
450
      let env, bl = map_fold_left dubinder env bl in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
451
      let (_,e,_) as t = dtriple ~ghost env t in
452
      let tyl = List.map (fun (_,ty,_) -> ty) bl in
453
      let ty = dcurrying tyl e.dexpr_type in
454
      DEfun (bl, t), ty
455
  | Ptree.Elet (x, e1, e2) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
456
      let e1 = dexpr ~ghost env e1 in
457
      let ty1 = e1.dexpr_type in
458
      let env = add_local env x.id ty1 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
459
      let e2 = dexpr ~ghost env e2 in
460
      DElet (x, e1, e2), e2.dexpr_type
461
  | Ptree.Eletrec (dl, e1) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
462 463
      let env, dl = dletrec ~ghost env dl in
      let e1 = dexpr ~ghost env e1 in
464
      DEletrec (dl, e1), e1.dexpr_type
465
  | Ptree.Etuple el ->
466 467 468
      let n = List.length el in
      let s = Typing.fs_tuple n in
      let tyl = List.map (fun _ -> create_type_var loc) el in
469
      let ty = dty_app (Typing.ts_tuple n, tyl) in
470
      let create d ty =
471
	{ dexpr_desc = d; (* dexpr_denv = env.denv; *)
472 473
	  dexpr_type = ty; dexpr_loc = loc }
      in
474
      let apply e1 e2 ty2 =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
475
	let e2 = dexpr ~ghost env e2 in
476 477
	assert (Denv.unify e2.dexpr_type ty2);
	let ty = create_type_var loc in
478
	assert (Denv.unify e1.dexpr_type
479
		  (dty_app (ts_arrow, [ty2; ty])));
480 481
	create (DEapply (e1, e2)) ty
      in
482
      let e = create (DElogic s) (dcurrying tyl ty) in
483 484
      let e = List.fold_left2 apply e el tyl in
      e.dexpr_desc, ty
485

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

571
  | Ptree.Eassert (k, le) ->
572
      DEassert (k, (* dfmla env.denv *) le), dty_unit env.uc
573
  | Ptree.Elabel ({id=s}, e1) ->
574
      if Typing.mem_var s env.denv then
575
	errorm ~loc "clash with previous label %s" s;
576
      let ty = dty_label env.uc in
577
      let env = { env with denv = add_pure_var s ty env.denv } in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
578
      let e1 = dexpr ~ghost env e1 in
579
      DElabel (s, e1), e1.dexpr_type
580
  | Ptree.Ecast (e1, ty) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
581
      let e1 = dexpr ~ghost env e1 in
582
      let ty = dtype env ty in
583 584
      expected_type e1 ty;
      e1.dexpr_desc, ty
585
  | Ptree.Eany c ->
586 587
      let c = dutype_c env c in
      DEany c, dpurify_utype_v c.duc_result_type
588

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
612 613
and dtriple ~ghost env (p, e, q) =
  let e = dexpr ~ghost env e in
614
  let q = dpost env.uc q in
615 616
  (p, e, q)

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
(*** regions tables ********************************************************)

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

let declare_region_type ts i ty = 
  let h = 
    try 
      Hts.find region_types ts 
    with Not_found -> 
      let h = Hashtbl.create 17 in Hts.add region_types ts h; h
  in
  Hashtbl.add h i ty

let region_type ts i =
(*   eprintf "region_type: ts=%a i=%d@." Pretty.print_ts ts i; *)
(*   let mt = get_mtsymbol ts in *)
(*   eprintf "%a@." print_mt_symbol mt; *)
  Hashtbl.find (Hts.find region_types ts) i

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

let declare_mutable_field ts i j = 
  let h = 
    try 
      Hts.find mutable_fields ts 
    with Not_found -> 
      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

let regions_tyapp ts nregions tyl = 
  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)

659
(* phase 2: remove destructive types and type annotations *****************)
660

661 662 663 664
let dterm env l = Typing.dterm ~localize:true env l
let dfmla env l = Typing.dfmla ~localize:true env l

type ienv = { 
665 666 667 668 669
  i_uc      : uc;
  i_denv : Typing.denv;
  i_impures : ivsymbol Mstr.t;
  i_effects : vsymbol Mstr.t;
  i_pures   : vsymbol Mstr.t;
670 671 672
}

let create_ivsymbol id ty =
673
  let vs = create_vsymbol id ty in
674 675 676 677 678
  let vse = create_vsymbol id (effectify ty) in
  let vsp = 
    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 }
679

680 681 682 683 684 685
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)

686
let iadd_local env x ty =
687
  let v = create_ivsymbol x ty in 
688 689 690 691 692 693 694 695 696 697 698
  let s = v.i_impure.vs_name.id_string in
  let env = { env with 
    i_denv = 
      (let dty = dty_of_ty env.i_denv v.i_pure.vs_ty in
       add_pure_var s dty env.i_denv);
(*     i_denv_effect =  *)
(*       (let dty = dty_of_ty env.i_denv_effect v.i_effect.vs_ty in *)
(*        add_pure_var s dty env.i_denv_effect); *)
    i_impures = Mstr.add s v env.i_impures;
    i_effects = Mstr.add s v.i_effect env.i_effects;
    i_pures = Mstr.add s v.i_pure env.i_pures; } 
699
  in
700
  env, v
701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763

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"

let iuregion env { pp_loc = loc; pp_desc = d } = match d with
  | 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) ->
	    let j = 
	      try 
		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
  | _ ->
      errorm ~loc "unsupported effect syntax"
(***
  | Qident id when Mstr.mem id.id env.locals ->
      (* local variable *)
      let ty = Mstr.find id.id env.locals in
      check_mutable_type id.id_loc ty;
      DRlocal id.id
  | qid ->
      let loc = Typing.qloc qid in
      let sl = Typing.string_list_of_qualid [] qid in
      try
	let s, ty = specialize_global loc sl env.uc in
	check_mutable_dtype_v loc ty;
	DRglobal s
      with Not_found ->
	errorm ~loc "unbound variable %a" print_qualid qid
***)
(***
  | DRlocal x -> IRlocal (Mstr.find x env.i_impures)
764
  | DRglobal ls -> IRglobal ls
765
***)
766

767 768 769 770
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;
771 772
}

773
let pre env = Denv.fmla env.i_pures
774 775

let post env ((ty, f), ql) =
776
  let env = env.i_pures in
777 778 779
  let exn (ls, (ty, f)) =
    let v, env = match ty with
      | None ->
780
	  None, env
781 782
      | Some ty ->
	  let ty = Denv.ty_of_dty ty in
783
	  let v_result = create_vsymbol (id_fresh id_result) ty in
784
	  Some v_result, Mstr.add id_result v_result env
785
    in
786
    (ls, (v, Denv.fmla env f))
787
  in
788
  let ty = Denv.ty_of_dty ty in
789 790
  let v_result = create_vsymbol (id_fresh id_result) ty in
  let env = Mstr.add id_result v_result env in
Jean-Christophe Filliâtre's avatar