pgm_typing.ml 82.2 KB
Newer Older
1 2
(**************************************************************************)
(*                                                                        *)
MARCHE Claude's avatar
MARCHE Claude committed
3
(*  Copyright (C) 2010-2012                                               *)
4 5 6
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
MARCHE Claude's avatar
MARCHE Claude committed
7
(*    Guillaume Melquiond                                                 *)
8 9 10 11 12 13 14 15 16 17 18 19 20
(*    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.                  *)
(*                                                                        *)
(**************************************************************************)

21
open Format
22
open Why3
23
open Pp
24
open Util
25
open Ident
26
open Ty
27
open Term
28
open Theory
29
open Pretty
30 31 32
open Denv
open Ptree
open Pgm_ttree
33
open Pgm_types
34
open Pgm_types.T
35
open Pgm_module
36

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

40 41
let error = Loc.error
let errorm = Loc.errorm
42

43 44
let id_result = "result"

45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63
(* Table of record mutable fields ******************************************)

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

let declare_mutable_field ts i j =
  Pgm_wp.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 is_mutable_field ts i =
  Hashtbl.mem (Hts.find mutable_fields ts) i

64
(* phase 1: typing programs (using destructive type inference) **************)
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 = tyapp (find_ts ~pure:true uc "bool") []
Andrei Paskevich's avatar
Andrei Paskevich committed
73 74 75 76

let dty_int   = tyapp Ty.ts_int []
let dty_unit  = tyapp (Ty.ts_tuple 0) []
let dty_mark  = tyapp ts_mark []
77

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

86
let create_denv uc =
87
  { uc = uc;
88
    locals = Mstr.empty;
89
    denv = Typing.denv_empty; }
90

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

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

95
let dcurrying tyl ty =
96
  let make_arrow_type ty1 ty2 = tyapp ts_arrow [ty1; ty2] in
97 98
  List.fold_right make_arrow_type tyl ty

99 100
type region_policy = Region_var | Region_ret | Region_glob

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

109 110 111 112
(* 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 *)

113 114
let region_vars = ref []

115 116 117
let new_regions_vars () =
  region_vars := Htv.create 17 :: !region_vars

118 119 120 121 122 123
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
124 125 126 127 128 129 130 131 132
  let check_tv tv tv' loc =
    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
  in
  let check tv (v, loc) = match view_dty v with
133
    | Tyvar v'  ->
134 135 136
        check_tv tv (tvsymbol_of_type_var v') loc
    | Tyuvar tv' ->
        check_tv tv tv' loc
137
    | Tyapp _ ->
138
        assert false
139 140 141 142
  in
  List.iter (fun h -> Htv.clear values; Htv.iter check h) !region_vars;
  region_vars := []

143 144 145
let is_fresh_region r =
  r.R.r_tv.tv_name.id_string = "fresh"

146 147 148 149 150
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
151
      let mk_region ty = match ty.ty_node with
152
        | Ty.Tyvar _ when policy = Region_ret ->
153
            tyuvar (create_tvsymbol (id_fresh "fresh"))
154 155
        | Ty.Tyvar tv when policy = Region_var ->
            let v = Denv.find_type_var ~loc htv tv in
156
            push_region_var tv (tyvar v, loc);
157 158
            tyvar v
        | Ty.Tyvar tv (* policy = Region_glob *) ->
159
            tyuvar tv
160 161
        | Ty.Tyapp _ ->
            assert false
162 163 164
      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
165
      tyapp ts (regions @ tl)
166

167 168 169 170
let rec specialize_type_v ?(policy=Region_var) ~loc htv = function
  | Tpure ty ->
      specialize_ty ~policy ~loc htv ty
  | Tarrow (bl, c) ->
171 172 173 174 175 176 177 178
      (* global regions must be different from local regions *)
      let globals =
        List.fold_left
          (fun acc pv -> Sreg.diff acc pv.pv_regions)
          (Sreg.union c.c_effect.E.reads c.c_effect.E.writes) bl
      in
      Sreg.iter
        (fun r ->
179
           push_region_var r.R.r_tv (tyuvar r.R.r_tv, loc))
180
        globals;
181
      dcurrying
182 183
        (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)
184

185 186 187 188
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

189 190 191 192 193 194
let parameter x = "parameter " ^ x
let rec parameter_q = function
  | [] -> assert false
  | [x] -> [parameter x]
  | x :: q -> x :: parameter_q q

195
let dot fmt () = pp_print_string fmt "."
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
196
let print_qualids = print_list dot pp_print_string
197
let print_qualid fmt q =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
198
  print_list dot pp_print_string fmt (Typing.string_list_of_qualid [] q)
199

200
let specialize_exception loc x uc =
201
  let s =
202
    try ns_find_ex (namespace uc) x
203
    with Not_found -> errorm ~loc "@[unbound exception %a@]" print_qualids x
204
  in
205 206 207 208
  match Denv.specialize_lsymbol ~loc s with
    | tyl, Some ty -> s, tyl, ty
    | _, None -> assert false

209 210
let create_type_var loc =
  let tv = Ty.create_tvsymbol (id_user "a" loc) in
211
  tyvar (create_ty_decl_var ~loc tv)
212

213
let add_pure_var id ty denv = match view_dty ty with
214 215
  | Tyapp (ts, _) when Ty.ts_equal ts ts_arrow -> denv
  | _ -> Typing.add_var id ty denv
216

217
let uncurrying ty =
218
  let rec uncurry acc ty = match ty.ty_node with
219
    | Ty.Tyapp (ts, [t1; t2]) when ts_equal ts ts_arrow ->
220
        uncurry (t1 :: acc) t2
221
    | _ ->
222
        List.rev acc, ty
223 224 225
  in
  uncurry [] ty

226
let expected_type e ty =
227
  if not (Denv.unify e.dexpr_type ty) then
228
    errorm ~loc:e.dexpr_loc
229
      "@[this expression has type %a,@ but is expected to have type %a@]"
230
      print_dty e.dexpr_type print_dty ty
231

232
let check_mutable_type loc dty = match view_dty dty with
233
  | Denv.Tyapp (ts, _) when is_mutable_ts ts ->
234
      ()
235
  | _ ->
236
      errorm ~loc
237
      "@[this expression has type %a,@ but is expected to have a mutable type@]"
238
        print_dty dty
239

240
let dexception uc qid =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
241 242
  let sl = Typing.string_list_of_qualid [] qid in
  let loc = Typing.qloc qid in
243
  let _, _, ty as r = specialize_exception loc sl uc in
244
  let ty_exn = tyapp ts_exn [] in
245
  if not (Denv.unify ty ty_exn) then
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
246
    errorm ~loc
247
      "@[this expression has type %a,@ but is expected to be an exception@]"
248 249
      print_dty ty;
  r
250

251 252 253 254 255
let no_ghost gh =
  if gh then errorm "ghost types are not supported in this version of WhyML"

let eff_no_ghost l = List.map (fun (gh,x) -> no_ghost gh; x) l

256
let dueffect env e =
257 258
  { du_reads  = eff_no_ghost e.Ptree.pe_reads;
    du_writes = eff_no_ghost e.Ptree.pe_writes;
259
    du_raises =
260
      List.map (fun id -> let ls,_,_ = dexception env.uc id in ls)
261
        (eff_no_ghost e.Ptree.pe_raises); }
262

263
let dpost uc (q, ql) =
264
  let dexn (id, l) = let s, _, _ = dexception uc id in s, l in
265
  q, List.map dexn ql
266

Andrei Paskevich's avatar
Andrei Paskevich committed
267 268 269
let add_local_top env x tyv =
  { env with locals = Mstr.add x tyv env.locals }

270
let add_local env x ty =
271
  { env with locals = Mstr.add x ty env.locals; }
272

273
let rec dpurify_utype_v = function
274
  | DUTpure ty ->
275
      ty
276
  | DUTarrow (bl, c) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
277
      dcurrying (List.map (fun (_,ty) -> ty) bl)
278
        (dpurify_utype_v c.duc_result_type)
279

280 281
(* user indicates whether region type variables can be instantiated *)
let rec dtype ~user env = function
282
  | PPTtyvar {id=x} ->
283
      Typing.create_user_type_var x
284 285
  | PPTtyapp (p, x) ->
      let loc = Typing.qloc x in
286 287
      let ts = Typing.specialize_tysymbol loc x (impure_uc env.uc) in
      let a = List.length ts.ts_args in
288 289
      let mt = get_mtsymbol ts in
      let np = List.length p in
290
      if np <> a - mt.mt_regions then
291 292
        errorm ~loc
        "@[type %a expects %d argument(s),@ but is applied to %d argument(s)@]"
293
          print_qualid x (a - mt.mt_regions) np;
294 295
      let tyl = List.map (dtype ~user env) p in
      let tyl = create_regions ~user mt.mt_regions @ tyl in
296
      tyapp ts tyl
297 298
  | PPTtuple tyl ->
      let ts = ts_tuple (List.length tyl) in
299
      tyapp ts (List.map (dtype ~user env) tyl)
300

301
let rec dutype_v env = function
302
  | Ptree.Tpure pt ->
303
      DUTpure (dtype ~user:true env pt)
304
  | Ptree.Tarrow (bl, c) ->
305 306 307 308 309 310 311
      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;
312
    duc_effect      = dueffect env c.Ptree.pc_effect;
313 314
    duc_pre         = c.Ptree.pc_pre;
    duc_post        = dpost env.uc c.Ptree.pc_post;
315
  }
316

317 318
and dubinder env ({id=x; id_loc=loc} as id, gh, v) =
  no_ghost gh;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
319 320 321
  let ty = match v with
    | Some v -> dtype ~user:true env v
    | None -> create_type_var loc
322
  in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
323
  add_local env x ty, (id, ty)
324

325
let rec add_local_pat env p = match p.dp_node with
326 327 328 329 330
  | 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
331

332
let dvariant env (l, p) =
333
  let relation p =
334
    let s, _ = Typing.specialize_psymbol p (pure_uc env.uc) in
335 336 337
    let loc = Typing.qloc p in
    match s.ls_args with
      | [t1; t2] when Ty.ty_equal t1 t2 ->
338
          s
339
      | _ ->
340 341
          errorm ~loc "predicate %s should be a binary relation"
            s.ls_name.id_string
342 343
  in
  l, option_map relation p
344

345 346 347 348 349
let dvariants env = function
  | [] -> None
  | [v] -> Some (dvariant env v)
  | _ -> errorm "multiple variants are not supported"

350
let dloop_annotation env a =
351
  { dloop_invariant = a.Ptree.loop_invariant;
352
    dloop_variant   = dvariants env a.Ptree.loop_variant; }
353

354
(***
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
355 356 357
let is_ps_ghost e = match e.dexpr_desc with
  | DEglobal (ps, _) -> T.p_equal ps ps_ghost
  | _ -> false
358
***)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
359

Andrei Paskevich's avatar
Andrei Paskevich committed
360 361 362 363 364 365 366 367
let rec extract_labels labs loc e = match e.Ptree.expr_desc with
  | Ptree.Enamed (Ptree.Lstr s, e) -> extract_labels (s :: labs) loc e
  | Ptree.Enamed (Ptree.Lpos p, e) -> extract_labels labs (Some p) e
  | Ptree.Ecast  (e, ty) ->
      let labs, loc, d = extract_labels labs loc e in
      labs, loc, Ptree.Ecast ({ e with Ptree.expr_desc = d }, ty)
  | e -> List.rev labs, loc, e

368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396

(* compatibility functions from Typing *)

let find_qualid_ls uc p =
  let loc = Typing.qloc p in
  let sl = Typing.string_list_of_qualid [] p in
  try ns_find_ls (get_namespace uc) sl with Not_found ->
    errorm ~loc "unbound symbol %a" print_qualid p

let is_projection uc ls =
  try
    let ts = match ls.ls_args with
      | [{ty_node = Ty.Tyapp (ts,_)}] -> ts
      | _ -> raise Exit in
    match Decl.find_constructors (get_known uc) ts with
      | [cs,pjl] ->
          let find (i,r) = function
            | Some pj when ls_equal ls pj -> (succ i, i)
            | _ -> (succ i, r) in
          let (_,r) = List.fold_left find (0,-1) pjl in
          if r < 0 then None else Some (ts,cs,r)
      | _ -> None
  with Exit -> None

let list_fields uc fl =
  let field (q,e) = find_qualid_ls uc q, (Typing.qloc q, e) in
  let cs,pjl,flm = Decl.parse_record (get_known uc) (List.map field fl) in
  cs, List.map (fun pj -> Mls.find_opt pj flm) pjl

397 398
(* [dexpr] translates ptree into dexpr *)

Andrei Paskevich's avatar
Andrei Paskevich committed
399
let rec dexpr ~ghost ~userloc env e =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
400
  let loc = e.Ptree.expr_loc in
Andrei Paskevich's avatar
Andrei Paskevich committed
401 402
  let labs, userloc, d = extract_labels [] userloc e in
  let d, ty = dexpr_desc ~ghost ~userloc env loc d in
403
  let loc = def_option loc userloc in
404
  let e = {
Andrei Paskevich's avatar
Andrei Paskevich committed
405
    dexpr_desc = d; dexpr_loc = loc; dexpr_lab = labs; dexpr_type = ty; }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
406
  in
407
  (****
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
408 409 410
  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 ->
411 412 413 414 415 416 417 418 419 420 421 422 423
        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'; }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
424
    | _ ->
425 426
  ****)
  e
427

Andrei Paskevich's avatar
Andrei Paskevich committed
428
and dexpr_desc ~ghost ~userloc env loc = function
429
  | Ptree.Econstant (ConstInt _ as c) ->
430
      DEconstant c, tyapp Ty.ts_int []
431
  | Ptree.Econstant (ConstReal _ as c) ->
432
      DEconstant c, tyapp Ty.ts_real []
433
  | Ptree.Eident (Qident {id=x}) when Mstr.mem x env.locals ->
434
      (* local variable *)
435
      let tyv = Mstr.find x env.locals in
436
      DElocal (x, tyv), tyv
437
  | Ptree.Eident p ->
438
      (* global variable *)
439
      new_regions_vars ();
440
      let x = Typing.string_list_of_qualid [] p in
441
      let ls =
442 443 444 445 446 447
        try
          ns_find_ls (get_namespace (impure_uc env.uc)) (parameter_q x)
        with Not_found -> try
          ns_find_ls (get_namespace (impure_uc env.uc)) x
        with Not_found ->
          errorm ~loc "unbound symbol %a" print_qualid p
448
      in
449
      (*if ls_equal ls fs_at then errorm ~loc "at not allowed in programs";*)
450
      if ls_equal ls fs_old then errorm ~loc "old not allowed in programs";
451 452
      let ps = get_psymbol ls in
      begin match ps.ps_kind with
453 454 455 456 457 458 459 460 461
        | PSvar v ->
            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
        | PSfun tv ->
            let htv = Htv.create 17 in
            let dty = specialize_type_v ~loc htv tv in
            DEglobal (ps, tv, htv), dty
        | PSlogic ->
462
            let tyl, ty = Denv.specialize_lsymbol ~loc ls in
463
            let ty = match ty with
464 465
              | Some ty -> ty
              | None -> dty_bool env.uc
466 467
            in
            DElogic ps.ps_pure, dcurrying tyl ty
468
      end
469
  | Ptree.Elazy (op, e1, e2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
470
      let e1 = dexpr ~ghost ~userloc env e1 in
471
      expected_type e1 (dty_bool env.uc);
Andrei Paskevich's avatar
Andrei Paskevich committed
472
      let e2 = dexpr ~ghost ~userloc env e2 in
473 474
      expected_type e2 (dty_bool env.uc);
      DElazy (op, e1, e2), dty_bool env.uc
Andrei Paskevich's avatar
Andrei Paskevich committed
475 476 477 478
  | Ptree.Enot e1 ->
      let e1 = dexpr ~ghost ~userloc env e1 in
      expected_type e1 (dty_bool env.uc);
      DEnot e1, dty_bool env.uc
479
  | Ptree.Eapply (e1, e2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
480 481 482
      let e1 = dexpr ~ghost ~userloc env e1 in
      (* let ghost = ghost || is_ps_ghost e1 in *)
      let e2 = dexpr ~ghost ~userloc env e2 in
483
      let ty2 = create_type_var loc and ty = create_type_var loc in
484
      if not (Denv.unify e1.dexpr_type (tyapp ts_arrow [ty2; ty])) then
485
        errorm ~loc:e1.dexpr_loc "this expression is not a function";
486 487
      expected_type e2 ty2;
      DEapply (e1, e2), ty
488
  | Ptree.Efun (bl, t) ->
489
      let env, bl = map_fold_left dubinder env bl in
Andrei Paskevich's avatar
Andrei Paskevich committed
490
      let (_,e,_) as t = dtriple ~ghost ~userloc env t in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
491
      let tyl = List.map (fun (_,ty) -> ty) bl in
492
      let ty = dcurrying tyl e.dexpr_type in
493
      DEfun (bl, t), ty
494 495
  | Ptree.Elet (x, gh, e1, e2) ->
      no_ghost gh;
Andrei Paskevich's avatar
Andrei Paskevich committed
496
      let e1 = dexpr ~ghost ~userloc env e1 in
497
      let ty1 = e1.dexpr_type in
498
      let env = add_local env x.id ty1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
499
      let e2 = dexpr ~ghost ~userloc env e2 in
500
      DElet (x, e1, e2), e2.dexpr_type
501
  | Ptree.Eletrec (dl, e1) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
502 503
      let env, dl = dletrec ~ghost ~userloc env dl in
      let e1 = dexpr ~ghost ~userloc env e1 in
504
      DEletrec (dl, e1), e1.dexpr_type
505
  | Ptree.Etuple el ->
506
      let n = List.length el in
507
      let s = fs_tuple n in
508
      let tyl = List.map (fun _ -> create_type_var loc) el in
509
      let ty = tyapp (ts_tuple n) tyl in
510
      let uloc = def_option loc userloc in
Andrei Paskevich's avatar
Andrei Paskevich committed
511 512
      let create d ty = { dexpr_desc = d; dexpr_type = ty;
                          dexpr_loc = uloc; dexpr_lab = [] } in
513
      let apply e1 e2 ty2 =
Andrei Paskevich's avatar
Andrei Paskevich committed
514
        let e2 = dexpr ~ghost ~userloc env e2 in
515 516
        assert (Denv.unify e2.dexpr_type ty2);
        let ty = create_type_var loc in
517
        assert (Denv.unify e1.dexpr_type (tyapp ts_arrow [ty2; ty]));
518
        create (DEapply (e1, e2)) ty
519
      in
520
      let e = create (DElogic s) (dcurrying tyl ty) in
521 522
      let e = List.fold_left2 apply e el tyl in
      e.dexpr_desc, ty
523
  | Ptree.Erecord fl ->
524
      let cs, fl = list_fields (impure_uc env.uc) fl in
525 526 527
      new_regions_vars ();
      let tyl, ty = specialize_lsymbol ~loc (Htv.create 17) cs in
      let ty = of_option ty in
528
      let uloc = def_option loc userloc in
Andrei Paskevich's avatar
Andrei Paskevich committed
529 530
      let create d ty = { dexpr_desc = d; dexpr_type = ty;
                          dexpr_loc = uloc; dexpr_lab = [] } in
531
      let constructor d f tyf = match f with
532
        | Some (_, f) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
533
            let f = dexpr ~ghost ~userloc env f in
534
            expected_type f tyf;
535
            let ty = create_type_var loc in
536
            assert (Denv.unify d.dexpr_type (tyapp ts_arrow [tyf; ty]));
537 538 539
            create (DEapply (d, f)) ty
        | None ->
            errorm ~loc "some record fields are missing"
540 541
      in
      let d =
542 543
        let ps = get_psymbol cs in
        create (DElogic ps.ps_pure) (dcurrying tyl ty)
544 545 546
      in
      let d = List.fold_left2 constructor d fl tyl in
      d.dexpr_desc, ty
547
  | Ptree.Eupdate (e1, fl) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
548
      let e1 = dexpr ~ghost ~userloc env e1 in
549
      let cs, fl = list_fields (impure_uc env.uc) fl in
550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579
      let tyl, ty = Denv.specialize_lsymbol ~loc cs in
      let ty = of_option ty in
      expected_type e1 ty;
      let n = ref (-1) in
      let q = Queue.create () in
      (* prepare the pattern *)
      let pl = List.map2 (fun f ty -> match f with
        | Some _ ->
            { dp_node = Denv.Pwild ; dp_ty = ty }
        | None ->
            let x = incr n; "x:" ^ string_of_int !n in
            let i = { id = x ; id_lab = []; id_loc = loc } in
            Queue.add (x,ty) q;
            { dp_node = Denv.Pvar i ; dp_ty = ty }) fl tyl
      in
      let p = { dp_node = Denv.Papp (cs,pl) ; dp_ty = ty } in
      (* prepare the result *)
      new_regions_vars ();
      let tyl, ty = specialize_lsymbol ~loc (Htv.create 17) cs in
      let ty = of_option ty in
      (* unify pattern variable types with expected types *)
      let set_pat_var_ty f tyf = match f with
        | Some _ ->
            ()
        | None ->
            let _, xty as v = Queue.take q in
            assert (Denv.unify xty tyf);
            Queue.push v q
      in
      List.iter2 set_pat_var_ty fl tyl;
580
      let uloc = def_option loc userloc in
Andrei Paskevich's avatar
Andrei Paskevich committed
581 582
      let create d ty = { dexpr_desc = d; dexpr_type = ty;
                          dexpr_loc = uloc; dexpr_lab = [] } in
583 584
      let apply t f tyf = match f with
        | Some (_,e) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
585
            let e = dexpr ~ghost ~userloc env e in
586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602
            expected_type e tyf;
            let ty = create_type_var loc in
            assert (Denv.unify t.dexpr_type (tyapp ts_arrow [tyf; ty]));
            create (DEapply (t, e)) ty
        | None ->
            let x, _ = Queue.take q in
            let v = create (DElocal (x, tyf)) tyf in
            let ty = create_type_var loc in
            assert (Denv.unify t.dexpr_type (tyapp ts_arrow [tyf; ty]));
            create (DEapply (t, v)) ty
      in
      let t =
        let ps = get_psymbol cs in
        create (DElogic ps.ps_pure) (dcurrying tyl ty)
      in
      let t = List.fold_left2 apply t fl tyl in
      DEmatch (e1, [p, t]), ty
603
  | Ptree.Eassign (e1, q, e2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
604 605
      let e1 = dexpr ~ghost ~userloc env e1 in
      let e2 = dexpr ~ghost ~userloc env e2 in
606 607
      let x = Typing.string_list_of_qualid [] q in
      let ls =
608 609
        try ns_find_ls (get_namespace (impure_uc env.uc)) x
        with Not_found -> errorm ~loc "unbound record field %a" print_qualid q
610 611 612
      in
      new_regions_vars ();
      begin match specialize_lsymbol ~loc (Htv.create 17) ls with
613 614 615 616 617
        | [ty1], Some ty2 ->
            expected_type e1 ty1;
            expected_type e2 ty2
        | _ ->
            assert false
618
      end;
619
      begin match is_projection (impure_uc env.uc) ls with
620 621 622 623 624 625
        | Some (ts, _, i)  ->
            let mt = get_mtsymbol ts in
            let j =
              try mutable_field mt.mt_effect i
              with Not_found -> errorm ~loc "not a mutable field"
            in
Andrei Paskevich's avatar
Andrei Paskevich committed
626
            DEassign (e1, ls, j, e2), dty_unit
627 628
        | None ->
            errorm ~loc "unbound record field %a" print_qualid q
629
      end
630
  | Ptree.Esequence (e1, e2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
631
      let e1 = dexpr ~ghost ~userloc env e1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
632
      expected_type e1 dty_unit;
Andrei Paskevich's avatar
Andrei Paskevich committed
633
      let e2 = dexpr ~ghost ~userloc env e2 in
634
      DEsequence (e1, e2), e2.dexpr_type
635
  | Ptree.Eif (e1, e2, e3) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
636
      let e1 = dexpr ~ghost ~userloc env e1 in
637
      expected_type e1 (dty_bool env.uc);
Andrei Paskevich's avatar
Andrei Paskevich committed
638 639
      let e2 = dexpr ~ghost ~userloc env e2 in
      let e3 = dexpr ~ghost ~userloc env e3 in
640 641
      expected_type e3 e2.dexpr_type;
      DEif (e1, e2, e3), e2.dexpr_type
642
  | Ptree.Eloop (a, e1) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
643
      let e1 = dexpr ~ghost ~userloc env e1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
644 645
      expected_type e1 dty_unit;
      DEloop (dloop_annotation env a, e1), dty_unit
646
  | Ptree.Ematch (e1, bl) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
647
      let e1 = dexpr ~ghost ~userloc env e1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
648
      let ty1 = e1.dexpr_type in
649
      let ty = create_type_var loc in (* the type of all branches *)
Andrei Paskevich's avatar
Andrei Paskevich committed
650
      let branch (p, e) =
651 652 653
        let denv, p = Typing.dpat_list (impure_uc env.uc) env.denv ty1 p in
        let env = { env with denv = denv } in
        let env = add_local_pat env p in
Andrei Paskevich's avatar
Andrei Paskevich committed
654
        let e = dexpr ~ghost ~userloc env e in
655 656
        expected_type e ty;
        p, e
657 658
      in
      let bl = List.map branch bl in
Andrei Paskevich's avatar
Andrei Paskevich committed
659
      DEmatch (e1, bl), ty
660
  | Ptree.Eabsurd ->
661
      DEabsurd, create_type_var loc
662
  | Ptree.Eraise (qid, e) ->
663
      let ls, tyl, _ = dexception env.uc qid in
664
      let e = match e, tyl with
665 666 667 668 669 670 671 672
        | None, [] ->
            None
        | Some _, [] ->
            errorm ~loc "expection %a has no argument" print_qualid qid
        | None, [ty] ->
            errorm ~loc "exception %a is expecting an argument of type %a"
              print_qualid qid print_dty ty;
        | Some e, [ty] ->
Andrei Paskevich's avatar
Andrei Paskevich committed
673
            let e = dexpr ~ghost ~userloc env e in
674 675 676 677
            expected_type e ty;
            Some e
        | _ ->
            assert false
678 679
      in
      DEraise (ls, e), create_type_var loc
680
  | Ptree.Etry (e1, hl) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
681
      let e1 = dexpr ~ghost ~userloc env e1 in
682
      let handler (id, x, h) =
683 684 685 686 687 688 689 690 691 692 693 694 695 696
        let ls, tyl, _ = dexception env.uc id in
        let x, env = match x, tyl with
          | Some _, [] ->
              errorm ~loc "expection %a has no argument" print_qualid id
          | None, [] ->
              None, env
          | None, [ty] ->
              errorm ~loc "exception %a is expecting an argument of type %a"
                print_qualid id print_dty ty;
          | Some x, [ty] ->
              Some x.id, add_local env x.id ty
          | _ ->
              assert false
        in
Andrei Paskevich's avatar
Andrei Paskevich committed
697
        let h = dexpr ~ghost ~userloc env h in
698 699
        expected_type h e1.dexpr_type;
        (ls, x, h)
700 701
      in
      DEtry (e1, List.map handler hl), e1.dexpr_type
702
  | Ptree.Efor (x, e1, d, e2, inv, e3) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
703
      let e1 = dexpr ~ghost ~userloc env e1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
704
      expected_type e1 dty_int;
Andrei Paskevich's avatar
Andrei Paskevich committed
705
      let e2 = dexpr ~ghost ~userloc env e2 in
Andrei Paskevich's avatar
Andrei Paskevich committed
706 707
      expected_type e2 dty_int;
      let env = add_local env x.id dty_int in
Andrei Paskevich's avatar
Andrei Paskevich committed
708
      let e3 = dexpr ~ghost ~userloc env e3 in
Andrei Paskevich's avatar
Andrei Paskevich committed
709 710
      expected_type e3 dty_unit;
      DEfor (x, e1, d, e2, inv, e3), dty_unit
711
  | Ptree.Eassert (k, le) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
712
      DEassert (k, le), dty_unit
713
  | Ptree.Emark ({id=s}, e1) ->
714
      if Typing.mem_var s env.denv then
715
        errorm ~loc "clash with previous mark %s" s;
Andrei Paskevich's avatar
Andrei Paskevich committed
716
      let env = { env with denv = add_pure_var s dty_mark env.denv } in
Andrei Paskevich's avatar
Andrei Paskevich committed
717
      let e1 = dexpr ~ghost ~userloc env e1 in
718
      DEmark (s, e1), e1.dexpr_type
719
  | Ptree.Ecast (e1, ty) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
720
      let e1 = dexpr ~ghost ~userloc env e1 in
721
      let ty = dtype ~user:false env ty in
722 723
      expected_type e1 ty;
      e1.dexpr_desc, ty
724
  | Ptree.Eany c ->
725 726
      let c = dutype_c env c in
      DEany c, dpurify_utype_v c.duc_result_type
727 728 729 730
  | Ptree.Eabstract(e1,q) ->
      let e1 = dexpr ~ghost ~userloc env e1 in
      let q = dpost env.uc q in
      DEabstract(e1, q), e1.dexpr_type
731 732 733
  | Ptree.Eghost _ ->
      no_ghost true;
      assert false
Andrei Paskevich's avatar
Andrei Paskevich committed
734 735
  | Ptree.Enamed _ ->
      assert false
736

Andrei Paskevich's avatar
Andrei Paskevich committed
737
and dletrec ~ghost ~userloc env dl =
738
  (* add all functions into environment *)
739
  let add_one env (_loc, id, gh, bl, var, t) =
740
    no_ghost gh;
741
    let ty = create_type_var id.id_loc in
742
    let env = add_local_top env id.id ty in