pgm_typing.ml 80.7 KB
Newer Older
1
2
(**************************************************************************)
(*                                                                        *)
3
(*  Copyright (C) 2010-2011                                               *)
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 Why3
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
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
(* 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

81
(* phase 1: typing programs (using destructive type inference) **************)
82

83
let find_ts ~pure uc s =
84
  ns_find_ts (get_namespace (if pure then pure_uc uc else impure_uc uc)) [s]
85
let find_ls ~pure uc s =
86
  ns_find_ls (get_namespace (if pure then pure_uc uc else impure_uc uc)) [s]
87
88

(* TODO: improve efficiency *)
89
let dty_bool uc = tyapp (find_ts ~pure:true uc "bool") []
Andrei Paskevich's avatar
Andrei Paskevich committed
90
91
92
93

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

95
(* note: local variables are simultaneously in locals (to type programs)
96
   and in denv (to type logic elements) *)
97
type denv = {
98
99
100
  uc     : uc;
  locals : Denv.dty Mstr.t;
  denv   : Typing.denv; (* for user type variables only *)
101
}
102

103
let create_denv uc =
104
  { uc = uc;
105
    locals = Mstr.empty;
106
    denv = Typing.create_denv (); }
107

108
let loc_of_id id = Util.of_option id.Ident.id_loc
109

110
let loc_of_ls ls = ls.ls_name.Ident.id_loc
111

112
let dcurrying tyl ty =
113
  let make_arrow_type ty1 ty2 = tyapp ts_arrow [ty1; ty2] in
114
115
  List.fold_right make_arrow_type tyl ty

116
117
type region_policy = Region_var | Region_ret | Region_glob

118
let rec create_regions ~user n =
119
  if n = 0 then
120
    []
121
  else
122
123
    let tv = create_tvsymbol (id_fresh "rho") in
    tyvar (create_ty_decl_var ~user tv) :: create_regions ~user (n - 1)
124

125
126
127
128
(* 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 *)

129
130
let region_vars = ref []

131
132
133
let new_regions_vars () =
  region_vars := Htv.create 17 :: !region_vars

134
135
136
137
138
139
140
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
141
    | Tyvar v'  ->
142
143
144
145
146
147
148
149
        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
150
    | Tyapp _ ->
151
        assert false
152
153
154
155
  in
  List.iter (fun h -> Htv.clear values; Htv.iter check h) !region_vars;
  region_vars := []

156
157
158
let is_fresh_region r =
  r.R.r_tv.tv_name.id_string = "fresh"

159
160
161
162
163
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
164
      let mk_region ty = match ty.ty_node with
165
        | Ty.Tyvar _ when policy = Region_ret ->
166
            tyvar (Typing.create_user_type_var "fresh")
167
168
169
170
171
172
173
174
        | 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
175
176
177
      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
178
      tyapp ts (regions @ tl)
179

180
181
182
183
let rec specialize_type_v ?(policy=Region_var) ~loc htv = function
  | Tpure ty ->
      specialize_ty ~policy ~loc htv ty
  | Tarrow (bl, c) ->
184
185
186
187
188
189
190
191
192
193
194
      (* 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 ->
           let v = create_ty_decl_var ~user:true r.R.r_tv in
           push_region_var r.R.r_tv (v, loc))
        globals;
195
      dcurrying
196
197
        (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)
198

199
200
201
202
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

203
204
205
206
207
208
let parameter x = "parameter " ^ x
let rec parameter_q = function
  | [] -> assert false
  | [x] -> [parameter x]
  | x :: q -> x :: parameter_q q

209
let dot fmt () = pp_print_string fmt "."
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
210
let print_qualids = print_list dot pp_print_string
211
let print_qualid fmt q =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
212
  print_list dot pp_print_string fmt (Typing.string_list_of_qualid [] q)
213

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

223
224
let create_type_var loc =
  let tv = Ty.create_tvsymbol (id_user "a" loc) in
225
  tyvar (create_ty_decl_var ~loc ~user:false tv)
226

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

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

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

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

254
let dexception uc qid =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
255
256
  let sl = Typing.string_list_of_qualid [] qid in
  let loc = Typing.qloc qid in
257
  let _, _, ty as r = specialize_exception loc sl uc in
258
  let ty_exn = tyapp ts_exn [] in
259
  if not (Denv.unify ty ty_exn) then
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
260
    errorm ~loc
261
      "@[this expression has type %a,@ but is expected to be an exception@]"
262
263
      print_dty ty;
  r
264

265
266
267
268
let dueffect env e =
  { du_reads  = e.Ptree.pe_reads;
    du_writes = e.Ptree.pe_writes;
    du_raises =
269
      List.map (fun id -> let ls,_,_ = dexception env.uc id in ls)
270
        e.Ptree.pe_raises; }
271

272
let dpost uc (q, ql) =
273
  let dexn (id, l) = let s, _, _ = dexception uc id in s, l in
274
  q, List.map dexn ql
275

Andrei Paskevich's avatar
Andrei Paskevich committed
276
277
278
let add_local_top env x tyv =
  { env with locals = Mstr.add x tyv env.locals }

279
let add_local env x ty =
280
  { env with locals = Mstr.add x ty env.locals; }
281

282
let rec dpurify_utype_v = function
283
  | DUTpure ty ->
284
      ty
285
  | DUTarrow (bl, c) ->
286
      dcurrying (List.map (fun (_,ty,_) -> ty) bl)
287
        (dpurify_utype_v c.duc_result_type)
288

289
290
(* user indicates whether region type variables can be instantiated *)
let rec dtype ~user env = function
291
292
293
294
295
296
297
  | 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
298
      if np <> a - mt.mt_regions then
299
300
        errorm ~loc
        "@[type %a expects %d argument(s),@ but is applied to %d argument(s)@]"
301
          print_qualid x (a - mt.mt_regions) np;
302
303
      let tyl = List.map (dtype ~user env) p in
      let tyl = create_regions ~user mt.mt_regions @ tyl in
304
      tyapp ts tyl
305
306
  | PPTtuple tyl ->
      let ts = ts_tuple (List.length tyl) in
307
      tyapp ts (List.map (dtype ~user env) tyl)
308

309
let rec dutype_v env = function
310
  | Ptree.Tpure pt ->
311
      DUTpure (dtype ~user:true env pt)
312
  | Ptree.Tarrow (bl, c) ->
313
314
315
316
317
318
319
      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;
320
    duc_effect      = dueffect env c.Ptree.pc_effect;
321
322
    duc_pre         = c.Ptree.pc_pre;
    duc_post        = dpost env.uc c.Ptree.pc_post;
323
  }
324

325
and dubinder env ({id=x; id_loc=loc} as id, v) =
326
  let v = match v with
327
328
    | Some v -> dutype_v env v
    | None -> DUTpure (create_type_var loc)
329
  in
330
  let ty = dpurify_utype_v v in
331
  add_local env x ty, (id, ty, v)
332

333
let rec add_local_pat env p = match p.dp_node with
334
335
336
337
338
  | 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
339

340
let dvariant env (l, p) =
341
  let relation p =
342
    let s, _ = Typing.specialize_psymbol p (pure_uc env.uc) in
343
344
345
    let loc = Typing.qloc p in
    match s.ls_args with
      | [t1; t2] when Ty.ty_equal t1 t2 ->
346
          s
347
      | _ ->
348
349
          errorm ~loc "predicate %s should be a binary relation"
            s.ls_name.id_string
350
351
  in
  l, option_map relation p
352

353
let dloop_annotation env a =
354
  { dloop_invariant = a.Ptree.loop_invariant;
355
    dloop_variant   = option_map (dvariant env) a.Ptree.loop_variant; }
356

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

Andrei Paskevich's avatar
Andrei Paskevich committed
363
364
365
366
367
368
369
370
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

371
372
(* [dexpr] translates ptree into dexpr *)

Andrei Paskevich's avatar
Andrei Paskevich committed
373
let rec dexpr ~ghost ~userloc env e =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
374
  let loc = e.Ptree.expr_loc in
Andrei Paskevich's avatar
Andrei Paskevich committed
375
376
377
  let labs, userloc, d = extract_labels [] userloc e in
  let d, ty = dexpr_desc ~ghost ~userloc env loc d in
  let loc = default_option loc userloc in
378
  let e = {
Andrei Paskevich's avatar
Andrei Paskevich committed
379
    dexpr_desc = d; dexpr_loc = loc; dexpr_lab = labs; dexpr_type = ty; }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
380
  in
381
  (****
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
382
383
384
  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 ->
385
386
387
388
389
390
391
392
393
394
395
396
397
        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
398
    | _ ->
399
400
  ****)
  e
401

Andrei Paskevich's avatar
Andrei Paskevich committed
402
and dexpr_desc ~ghost ~userloc env loc = function
403
  | Ptree.Econstant (ConstInt _ as c) ->
404
      DEconstant c, tyapp Ty.ts_int []
405
  | Ptree.Econstant (ConstReal _ as c) ->
406
      DEconstant c, tyapp Ty.ts_real []
407
  | Ptree.Eident (Qident {id=x}) when Mstr.mem x env.locals ->
408
      (* local variable *)
409
      let tyv = Mstr.find x env.locals in
410
      DElocal (x, tyv), tyv
411
  | Ptree.Eident p ->
412
      (* global variable *)
413
      new_regions_vars ();
414
      let x = Typing.string_list_of_qualid [] p in
415
      let ls =
416
417
418
419
420
421
        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
422
      in
423
      (*if ls_equal ls fs_at then errorm ~loc "at not allowed in programs";*)
424
      if ls_equal ls fs_old then errorm ~loc "old not allowed in programs";
425
426
      let ps = get_psymbol ls in
      begin match ps.ps_kind with
427
428
429
430
431
432
433
434
435
        | 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 ->
436
            let tyl, ty = Denv.specialize_lsymbol ~loc ls in
437
            let ty = match ty with
438
439
              | Some ty -> ty
              | None -> dty_bool env.uc
440
441
            in
            DElogic ps.ps_pure, dcurrying tyl ty
442
      end
443
  | Ptree.Elazy (op, e1, e2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
444
      let e1 = dexpr ~ghost ~userloc env e1 in
445
      expected_type e1 (dty_bool env.uc);
Andrei Paskevich's avatar
Andrei Paskevich committed
446
      let e2 = dexpr ~ghost ~userloc env e2 in
447
448
      expected_type e2 (dty_bool env.uc);
      DElazy (op, e1, e2), dty_bool env.uc
Andrei Paskevich's avatar
Andrei Paskevich committed
449
450
451
452
  | Ptree.Enot e1 ->
      let e1 = dexpr ~ghost ~userloc env e1 in
      expected_type e1 (dty_bool env.uc);
      DEnot e1, dty_bool env.uc
453
  | Ptree.Eapply (e1, e2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
454
455
456
      let e1 = dexpr ~ghost ~userloc env e1 in
      (* let ghost = ghost || is_ps_ghost e1 in *)
      let e2 = dexpr ~ghost ~userloc env e2 in
457
      let ty2 = create_type_var loc and ty = create_type_var loc in
458
      if not (Denv.unify e1.dexpr_type (tyapp ts_arrow [ty2; ty])) then
459
        errorm ~loc:e1.dexpr_loc "this expression is not a function";
460
461
      expected_type e2 ty2;
      DEapply (e1, e2), ty
462
  | Ptree.Efun (bl, t) ->
463
      let env, bl = map_fold_left dubinder env bl in
Andrei Paskevich's avatar
Andrei Paskevich committed
464
      let (_,e,_) as t = dtriple ~ghost ~userloc env t in
465
      let tyl = List.map (fun (_,ty,_) -> ty) bl in
466
      let ty = dcurrying tyl e.dexpr_type in
467
      DEfun (bl, t), ty
468
  | Ptree.Elet (x, e1, e2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
469
      let e1 = dexpr ~ghost ~userloc env e1 in
470
      let ty1 = e1.dexpr_type in
471
      let env = add_local env x.id ty1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
472
      let e2 = dexpr ~ghost ~userloc env e2 in
473
      DElet (x, e1, e2), e2.dexpr_type
474
  | Ptree.Eletrec (dl, e1) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
475
476
      let env, dl = dletrec ~ghost ~userloc env dl in
      let e1 = dexpr ~ghost ~userloc env e1 in
477
      DEletrec (dl, e1), e1.dexpr_type
478
  | Ptree.Etuple el ->
479
      let n = List.length el in
480
      let s = fs_tuple n in
481
      let tyl = List.map (fun _ -> create_type_var loc) el in
482
      let ty = tyapp (ts_tuple n) tyl in
Andrei Paskevich's avatar
Andrei Paskevich committed
483
484
485
      let uloc = default_option loc userloc in
      let create d ty = { dexpr_desc = d; dexpr_type = ty;
                          dexpr_loc = uloc; dexpr_lab = [] } in
486
      let apply e1 e2 ty2 =
Andrei Paskevich's avatar
Andrei Paskevich committed
487
        let e2 = dexpr ~ghost ~userloc env e2 in
488
489
        assert (Denv.unify e2.dexpr_type ty2);
        let ty = create_type_var loc in
490
        assert (Denv.unify e1.dexpr_type (tyapp ts_arrow [ty2; ty]));
491
        create (DEapply (e1, e2)) ty
492
      in
493
      let e = create (DElogic s) (dcurrying tyl ty) in
494
495
      let e = List.fold_left2 apply e el tyl in
      e.dexpr_desc, ty
496
497
498
499
500
  | 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
Andrei Paskevich's avatar
Andrei Paskevich committed
501
502
503
      let uloc = default_option loc userloc in
      let create d ty = { dexpr_desc = d; dexpr_type = ty;
                          dexpr_loc = uloc; dexpr_lab = [] } in
504
      let constructor d f tyf = match f with
505
        | Some (_, f) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
506
            let f = dexpr ~ghost ~userloc env f in
507
            expected_type f tyf;
508
            let ty = create_type_var loc in
509
            assert (Denv.unify d.dexpr_type (tyapp ts_arrow [tyf; ty]));
510
511
512
            create (DEapply (d, f)) ty
        | None ->
            errorm ~loc "some record fields are missing"
513
514
      in
      let d =
515
516
        let ps = get_psymbol cs in
        create (DElogic ps.ps_pure) (dcurrying tyl ty)
517
518
519
      in
      let d = List.fold_left2 constructor d fl tyl in
      d.dexpr_desc, ty
520
  | Ptree.Eupdate (e1, fl) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
521
      let e1 = dexpr ~ghost ~userloc env e1 in
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
      let _, cs, fl = Typing.list_fields (impure_uc env.uc) fl in
      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;
Andrei Paskevich's avatar
Andrei Paskevich committed
553
554
555
      let uloc = default_option loc userloc in
      let create d ty = { dexpr_desc = d; dexpr_type = ty;
                          dexpr_loc = uloc; dexpr_lab = [] } in
556
557
      let apply t f tyf = match f with
        | Some (_,e) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
558
            let e = dexpr ~ghost ~userloc env e in
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
            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
576
  | Ptree.Eassign (e1, q, e2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
577
578
      let e1 = dexpr ~ghost ~userloc env e1 in
      let e2 = dexpr ~ghost ~userloc env e2 in
579
580
      let x = Typing.string_list_of_qualid [] q in
      let ls =
581
582
        try ns_find_ls (get_namespace (impure_uc env.uc)) x
        with Not_found -> errorm ~loc "unbound record field %a" print_qualid q
583
584
585
      in
      new_regions_vars ();
      begin match specialize_lsymbol ~loc (Htv.create 17) ls with
586
587
588
589
590
        | [ty1], Some ty2 ->
            expected_type e1 ty1;
            expected_type e2 ty2
        | _ ->
            assert false
591
592
      end;
      begin match Typing.is_projection (impure_uc env.uc) ls with
593
594
595
596
597
598
        | 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
599
            DEassign (e1, ls, j, e2), dty_unit
600
601
        | None ->
            errorm ~loc "unbound record field %a" print_qualid q
602
      end
603
  | Ptree.Esequence (e1, e2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
604
      let e1 = dexpr ~ghost ~userloc env e1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
605
      expected_type e1 dty_unit;
Andrei Paskevich's avatar
Andrei Paskevich committed
606
      let e2 = dexpr ~ghost ~userloc env e2 in
607
      DEsequence (e1, e2), e2.dexpr_type
608
  | Ptree.Eif (e1, e2, e3) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
609
      let e1 = dexpr ~ghost ~userloc env e1 in
610
      expected_type e1 (dty_bool env.uc);
Andrei Paskevich's avatar
Andrei Paskevich committed
611
612
      let e2 = dexpr ~ghost ~userloc env e2 in
      let e3 = dexpr ~ghost ~userloc env e3 in
613
614
      expected_type e3 e2.dexpr_type;
      DEif (e1, e2, e3), e2.dexpr_type
615
  | Ptree.Eloop (a, e1) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
616
      let e1 = dexpr ~ghost ~userloc env e1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
617
618
      expected_type e1 dty_unit;
      DEloop (dloop_annotation env a, e1), dty_unit
619
  | Ptree.Ematch (e1, bl) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
620
      let e1 = dexpr ~ghost ~userloc env e1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
621
      let ty1 = e1.dexpr_type in
622
      let ty = create_type_var loc in (* the type of all branches *)
Andrei Paskevich's avatar
Andrei Paskevich committed
623
      let branch (p, e) =
624
625
626
        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
627
        let e = dexpr ~ghost ~userloc env e in
628
629
        expected_type e ty;
        p, e
630
631
      in
      let bl = List.map branch bl in
Andrei Paskevich's avatar
Andrei Paskevich committed
632
      DEmatch (e1, bl), ty
633
  | Ptree.Eabsurd ->
634
      DEabsurd, create_type_var loc
635
  | Ptree.Eraise (qid, e) ->
636
      let ls, tyl, _ = dexception env.uc qid in
637
      let e = match e, tyl with
638
639
640
641
642
643
644
645
        | 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
646
            let e = dexpr ~ghost ~userloc env e in
647
648
649
650
            expected_type e ty;
            Some e
        | _ ->
            assert false
651
652
      in
      DEraise (ls, e), create_type_var loc
653
  | Ptree.Etry (e1, hl) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
654
      let e1 = dexpr ~ghost ~userloc env e1 in
655
      let handler (id, x, h) =
656
657
658
659
660
661
662
663
664
665
666
667
668
669
        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
670
        let h = dexpr ~ghost ~userloc env h in
671
672
        expected_type h e1.dexpr_type;
        (ls, x, h)
673
674
      in
      DEtry (e1, List.map handler hl), e1.dexpr_type
675
  | Ptree.Efor (x, e1, d, e2, inv, e3) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
676
      let e1 = dexpr ~ghost ~userloc env e1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
677
      expected_type e1 dty_int;
Andrei Paskevich's avatar
Andrei Paskevich committed
678
      let e2 = dexpr ~ghost ~userloc env e2 in
Andrei Paskevich's avatar
Andrei Paskevich committed
679
680
      expected_type e2 dty_int;
      let env = add_local env x.id dty_int in
Andrei Paskevich's avatar
Andrei Paskevich committed
681
      let e3 = dexpr ~ghost ~userloc env e3 in
Andrei Paskevich's avatar
Andrei Paskevich committed
682
683
      expected_type e3 dty_unit;
      DEfor (x, e1, d, e2, inv, e3), dty_unit
684
  | Ptree.Eassert (k, le) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
685
      DEassert (k, le), dty_unit
686
  | Ptree.Emark ({id=s}, e1) ->
687
      if Typing.mem_var s env.denv then
688
        errorm ~loc "clash with previous mark %s" s;
Andrei Paskevich's avatar
Andrei Paskevich committed
689
      let env = { env with denv = add_pure_var s dty_mark env.denv } in
Andrei Paskevich's avatar
Andrei Paskevich committed
690
      let e1 = dexpr ~ghost ~userloc env e1 in
691
      DEmark (s, e1), e1.dexpr_type
692
  | Ptree.Ecast (e1, ty) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
693
      let e1 = dexpr ~ghost ~userloc env e1 in
694
      let ty = dtype ~user:false env ty in
695
696
      expected_type e1 ty;
      e1.dexpr_desc, ty
697
  | Ptree.Eany c ->
698
699
      let c = dutype_c env c in
      DEany c, dpurify_utype_v c.duc_result_type
Andrei Paskevich's avatar
Andrei Paskevich committed
700
701
  | Ptree.Enamed _ ->
      assert false
702

Andrei Paskevich's avatar
Andrei Paskevich committed
703
and dletrec ~ghost ~userloc env dl =
704
  (* add all functions into environment *)
705
  let add_one env (id, bl, var, t) =
706
    let ty = create_type_var id.id_loc in
707
    let env = add_local_top env id.id ty in
708
    env, ((id, ty), bl, var, t)
709
  in
710
  let env, dl = map_fold_left add_one env dl in
711
  (* then type-check all of them and unify *)
712
  let type_one ((id, tyres), bl, v, t) =
713
    let env, bl = map_fold_left dubinder env bl in
714
    let v = option_map (dvariant env) v in
Andrei Paskevich's avatar
Andrei Paskevich committed
715
    let (_,e,_) as t = dtriple ~ghost ~userloc env t in
716
    let tyl = List.map (fun (_,ty,_) -> ty) bl in
717
    let ty = dcurrying tyl e.dexpr_type in
718
    if not (Denv.unify ty tyres) then
719
      errorm ~loc:id.id_loc
720
721
        "@[this expression has type %a,@ but is expected to have type %a@]"
        print_dty ty print_dty tyres;
722
    ((id, tyres), bl, v, t)
723
724
725
  in
  env, List.map type_one dl

Andrei Paskevich's avatar
Andrei Paskevich committed
726
727
and dtriple ~ghost ~userloc env (p, e, q) =
  let e = dexpr ~ghost ~userloc env e in
728
  let q = dpost env.uc q in
729
730
  (p, e, q)

731
732
733
734
(*** regions tables ********************************************************)

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

735
736
737
738
739
let declare_region_type ts i ty =
  let h =
    try
      Hts.find region_types ts
    with Not_found ->
740
741
742
743
744
      let h = Hashtbl.create 17 in Hts.add region_types ts h; h
  in
  Hashtbl.add h i ty

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

750
let regions_tyapp ts nregions tyl =
751
752
753
754
755
756
757
758
  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)

759
(* phase 2: remove destructive types and type annotations *****************)
760

761
762
763
764
765
(* check
   1. that variables occurring in 'old' and 'at' are not local variables
   2. that 'old' is used only when old is true
*)
let check_at_fmla ?(old=false) loc f0 =
766
767
  let v = ref None in
  let rec check f = match f.t_node with
768
769
    | Term.Tapp (ls, _) when ls_equal ls fs_old && not old ->
        errorm ~loc "use of `old' not allowed here"
770
    | Term.Tapp (ls, _) when ls_equal ls fs_at || ls_equal ls fs_old ->
771
772
        let d = Mvs.set_diff f.t_vars f0.t_vars in
        Mvs.is_empty d || (v := Some (fst (Mvs.choose d)); false)
773
774
775
776
777
778
    | _ ->
        t_all check f
  in
  if not (check f0) then
    errorm ~loc "locally bound variable %a under `at'" print_vs (of_option !v)

779
780
let dterm env l = Typing.dterm ~localize:(Some None) env l
let dfmla env l = Typing.dfmla ~localize:(Some None) env l
781

782
type ienv = {
783
  i_uc      : uc;
784
  i_denv    : Typing.denv;
785
786
787
  i_impures : ivsymbol Mstr.t;
  i_effects : vsymbol Mstr.t;
  i_pures   : vsymbol Mstr.t;
788
789
790
}

let create_ivsymbol id ty =
791
  let vs = create_vsymbol id ty in
792
  let vse = create_vsymbol id (effectify ty) in
793
  let vsp =
794
795
796
    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 }
797

798
let rec dty_of_ty denv ty = match ty.ty_node with
799
  | Ty.Tyvar v ->
800
      Denv.tyvar (Typing.find_user_type_var v.tv_name.id_string denv)
801
  | Ty.Tyapp (ts, tyl) ->
802
      Denv.tyapp ts (List.map (dty_of_ty denv) tyl)
803

804
let iadd_local env x ty =
805
  let v = create_ivsymbol x ty in
806
  let s = v.i_impure.vs_name.id_string in
807
808
  let env = { env with
    i_denv =
809
810
811
812
      (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;
813
    i_pures = Mstr.add s v.i_pure env.i_pures; }
814
  in
815
  env, v
816

817
818
819
let rec type_effect_term env t =
  let loc = t.pp_loc in
  match t.pp_desc with
820
821
822
823
824
825
  | 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
826
827