mlw_typing.ml 77.9 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3 4 5 6 7 8 9 10
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2012   --   INRIA - CNRS - Paris-Sud University  *)
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)
11

12
open Stdlib
13
open Ident
14 15 16
open Ty
open Term
open Decl
17 18 19
open Theory
open Env
open Ptree
20
open Mlw_dtree
21
open Mlw_ty
22
open Mlw_ty.T
23 24
open Mlw_expr
open Mlw_decl
25
open Mlw_pretty
26
open Mlw_module
Andrei Paskevich's avatar
Andrei Paskevich committed
27
open Mlw_wp
28
open Mlw_dty
29

30 31
(** errors *)

32
exception DuplicateProgVar of string
33 34 35 36 37 38 39 40 41 42 43
exception DuplicateTypeVar of string
(*
exception PredicateExpected
exception TermExpected
exception FSymExpected of lsymbol
exception PSymExpected of lsymbol
exception ClashTheory of string
exception UnboundTheory of qualid
exception UnboundType of string list
*)
exception UnboundTypeVar of string
44
(* unused
45
exception UnboundSymbol of qualid
46
*)
47 48 49 50

let error = Loc.error
let errorm = Loc.errorm

51 52
let qloc = Typing.qloc
let print_qualid = Typing.print_qualid
53 54 55

let () = Exn_printer.register (fun fmt e -> match e with
  | DuplicateTypeVar s ->
56 57 58
      Format.fprintf fmt "Type parameter %s is used twice" s
  | DuplicateProgVar s ->
      Format.fprintf fmt "Parameter %s is used twice" s
59 60 61
  | TooLateInvariant ->
      Format.fprintf fmt
        "Cannot add a type invariant after another program declaration"
62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79
(*
  | PredicateExpected ->
      Format.fprintf fmt "syntax error: predicate expected"
  | TermExpected ->
      Format.fprintf fmt "syntax error: term expected"
  | FSymExpected ls ->
      Format.fprintf fmt "%a is not a function symbol" Pretty.print_ls ls
  | PSymExpected ls ->
      Format.fprintf fmt "%a is not a predicate symbol" Pretty.print_ls ls
  | ClashTheory s ->
      Format.fprintf fmt "Clash with previous theory %s" s
  | UnboundTheory q ->
      Format.fprintf fmt "unbound theory %a" print_qualid q
  | UnboundType sl ->
      Format.fprintf fmt "Unbound type '%a'"
        (Pp.print_list Pp.dot Pp.pp_print_string) sl
*)
  | UnboundTypeVar s ->
80
      Format.fprintf fmt "Unbound type variable '%s" s
81
(* unused
82 83
  | UnboundSymbol q ->
      Format.fprintf fmt "Unbound symbol '%a'" print_qualid q
84
*)
85 86 87
  | _ -> raise e)

(* TODO: let type_only = Debug.test_flag Typing.debug_type_only in *)
88 89
let implicit_post = Debug.register_flag "implicit_post"
  ~desc:"Generate@ a@ postcondition@ for@ pure@ functions@ without@ one."
90

91 92
type denv = {
  uc     : module_uc;
93
  locals : (tvars option * dvty) Mstr.t;
94
  tvars  : tvars;
Andrei Paskevich's avatar
Andrei Paskevich committed
95
  uloc   : Ptree.loc option;
96
}
97

98 99 100 101
let create_denv uc = {
  uc     = uc;
  locals = Mstr.empty;
  tvars  = empty_tvars;
Andrei Paskevich's avatar
Andrei Paskevich committed
102
  uloc   = None;
103
}
104

105 106
(* Handle tuple symbols *)

107 108 109
let ht_tuple   = Hint.create 3
let ts_tuple n = Hint.replace ht_tuple n (); ts_tuple n
let fs_tuple n = Hint.replace ht_tuple n (); fs_tuple n
110

111
let check_at f0 =
Andrei Paskevich's avatar
Andrei Paskevich committed
112 113 114 115 116 117 118 119 120 121 122 123
  let rec check f = match f.t_node with
    | Term.Tapp (ls, _) when ls_equal ls fs_at ->
        let d = Mvs.set_diff f.t_vars f0.t_vars in
        if not (Mvs.is_empty d) then errorm ?loc:f.t_loc
          "locally bound variable %a under `at'"
          Pretty.print_vs (fst (Mvs.choose d))
        else true
    | _ ->
        t_all check f
  in
  ignore (check f0)

124 125
let count_term_tuples t =
  let syms_ts _ ts = match is_ts_tuple_id ts.ts_name with
126
    | Some n -> Hint.replace ht_tuple n () | _ -> () in
127 128 129
  let syms_ty _ ty = ty_s_fold syms_ts () ty in
  t_s_fold syms_ty (fun _ _ -> ()) () t

130
let flush_tuples uc =
131 132
  let kn = Theory.get_known (get_theory uc) in
  let add_tuple n _ uc =
Andrei Paskevich's avatar
Andrei Paskevich committed
133
    if Mid.mem (Ty.ts_tuple n).ts_name kn then uc
134
    else use_export_theory uc (tuple_theory n) in
135 136
  let uc = Hint.fold add_tuple ht_tuple uc in
  Hint.clear ht_tuple;
137 138
  uc

139
let add_pdecl_with_tuples ~wp uc pd = add_pdecl ~wp (flush_tuples uc) pd
140
let add_decl_with_tuples uc d = add_decl (flush_tuples uc) d
141

142 143 144
(** Namespace lookup *)

let uc_find_ls uc p =
145 146
  let ns = Theory.get_namespace (get_theory uc) in
  Typing.find_ns (fun ls -> ls.ls_name) Theory.ns_find_ls p ns
147

148
let get_id_ts = function
149
  | PT pt -> pt.its_ts.ts_name
150
  | TS ts -> ts.ts_name
Andrei Paskevich's avatar
Andrei Paskevich committed
151

152
let uc_find_ts uc p =
153 154 155 156 157 158 159 160
  Typing.find_ns get_id_ts ns_find_ts p (get_namespace uc)

let get_id_ps = function
  | PV pv -> pv.pv_vs.vs_name
  | PS ps -> ps.ps_name
  | PL pl -> pl.pl_ls.ls_name
  | XS xs -> xs.xs_name
  | LS ls -> ls.ls_name
Andrei Paskevich's avatar
Andrei Paskevich committed
161

162
let uc_find_ps uc p =
163
  Typing.find_ns get_id_ps ns_find_ps p (get_namespace uc)
164

165 166
(** Typing type expressions *)

167
let rec dity_of_pty denv = function
168 169 170
  | Ptree.PPTtyvar id ->
      create_user_type_variable id
  | Ptree.PPTtyapp (pl, p) ->
171
      let dl = List.map (dity_of_pty denv) pl in
172
      begin match uc_find_ts denv.uc p with
173
        | PT ts -> its_app ts dl
174
        | TS ts -> ts_app ts dl
175 176
      end
  | Ptree.PPTtuple pl ->
177
      let dl = List.map (dity_of_pty denv) pl in
178
      ts_app (ts_tuple (List.length pl)) dl
179 180 181

(** Typing program expressions *)

Andrei Paskevich's avatar
Andrei Paskevich committed
182
let dity_int  = ts_app ts_int  []
183
let dity_real = ts_app ts_real []
184
let dity_bool = ts_app ts_bool []
Andrei Paskevich's avatar
Andrei Paskevich committed
185
let dity_unit = ts_app ts_unit []
186

187
let unify_loc unify_fn loc x1 x2 = try unify_fn x1 x2 with
Andrei Paskevich's avatar
Andrei Paskevich committed
188
  | TypeMismatch (ity1,ity2,_) -> errorm ~loc
189
      "This expression has type %a,@ but is expected to have type %a"
190
      Mlw_pretty.print_ity ity2 Mlw_pretty.print_ity ity1
Andrei Paskevich's avatar
Andrei Paskevich committed
191 192 193
  | DTypeMismatch (dity1,dity2) -> errorm ~loc
      "This expression has type %a,@ but is expected to have type %a"
      Mlw_dty.print_dity dity2 Mlw_dty.print_dity dity1
194
  | exn when Debug.test_noflag Debug.stack_trace -> error ~loc exn
195

196 197 198 199 200 201 202
let expected_type { de_loc = loc ; de_type = (argl,res) } dity =
  if argl <> [] then errorm ~loc "This expression is not a first-order value";
  unify_loc unify loc dity res

let expected_type_weak { de_loc = loc ; de_type = (argl,res) } dity =
  if argl <> [] then errorm ~loc "This expression is not a first-order value";
  unify_loc unify_weak loc dity res
203

204
let rec extract_labels labs loc e = match e.Ptree.expr_desc with
205
  | Ptree.Enamed (Ptree.Lstr s, e) -> extract_labels (Slab.add s labs) loc e
206 207 208 209
  | 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)
210
  | e -> labs, loc, e
211

212 213 214
let rec decompose_app args e = match e.Ptree.expr_desc with
  | Eapply (e1, e2) -> decompose_app (e2 :: args) e1
  | _ -> e, args
215

216 217 218 219 220 221 222
(* record parsing *)

let parse_record uc fll =
  let pl = match fll with
    | [] -> raise EmptyRecord
    | (pl,_)::_ -> pl in
  let its = match pl.pl_args with
223
    | [{ fd_ity = { ity_node = Ityapp (its,_,_) }}] -> its
224 225
    | _ -> raise (BadRecordField pl.pl_ls) in
  let cs, pjl = match find_constructors (get_known uc) its with
226
    | [cs,pjl] -> cs, List.map (Opt.get_exn (BadRecordField pl.pl_ls)) pjl
227 228 229 230 231 232 233 234 235
    | _ -> raise (BadRecordField pl.pl_ls) in
  let pjs = List.fold_left (fun s pj -> Sls.add pj.pl_ls s) Sls.empty pjl in
  let flm = List.fold_left (fun m (pj,v) -> let pj = pj.pl_ls in
    if not (Sls.mem pj pjs) then raise (BadRecordField pj) else
      Mls.add_new (DuplicateRecordField (cs.pl_ls,pj)) pj v m)
    Mls.empty fll
  in
  cs,pjl,flm

236 237
let find_prog_field uc (p,e) = match uc_find_ps uc p with PL pl -> pl, e
  | _ -> errorm ~loc:(qloc p) "'%a' is not a record field" print_qualid p
238

239
let find_pure_field uc (p,e) = uc_find_ls uc p, e
240

241 242
let is_pure_record uc = function
  | fl :: _ -> (try ignore (find_prog_field uc fl); false with _ -> true)
243
  | [] -> raise Decl.EmptyRecord
244 245

let hidden_pl ~loc pl =
246 247
  { de_desc = DEglobal_pl pl;
    de_type = specialize_plsymbol pl;
248
    de_loc  = loc; de_lab = Slab.empty }
249 250

let hidden_ls ~loc ls =
251
  { de_desc = DEglobal_ls ls;
252
    de_type = Loc.try1 loc specialize_lsymbol ls;
253
    de_loc  = loc; de_lab = Slab.empty }
254 255

(* helper functions for let-expansion *)
256
let test_var e = match e.de_desc with
257 258 259 260 261
  | DElocal _ | DEglobal_pv _ -> true
  | _ -> false

let mk_var e =
  if test_var e then e else
262 263 264
  { de_desc = DElocal "q";
    de_type = e.de_type;
    de_loc  = e.de_loc;
265
    de_lab  = Slab.empty }
266

267 268 269
let mk_id s loc =
  { id = s; id_loc = loc; id_lab = [] }

270 271
let mk_dexpr desc dvty loc labs =
  { de_desc = desc; de_type = dvty; de_loc = loc; de_lab = labs }
272

273 274
let mk_let ~loc ~uloc e (desc,dvty) =
  if test_var e then desc, dvty else
275
  let loc = Opt.get_def loc uloc in
276
  let e1 = mk_dexpr desc dvty loc Slab.empty in
277
  DElet (mk_id "q" e.de_loc, false, e, e1), dvty
278

279 280
(* patterns *)

281 282 283 284 285 286 287 288 289
let add_poly id dvty denv =
  let locals = Mstr.add id.id (Some denv.tvars, dvty) denv.locals in
  { denv with locals = locals }

let add_mono id dvty denv =
  let locals = Mstr.add id.id (None, dvty) denv.locals in
  { denv with locals = locals; tvars = add_dvty denv.tvars dvty }

let add_var id dity denv = add_mono id ([],dity) denv
290

291
let specialize_qualid uc p = match uc_find_ps uc p with
292
  | PV pv -> DEglobal_pv pv, ([],specialize_pvsymbol pv)
293 294
  | PS ps -> DEglobal_ps ps, specialize_psymbol  ps
  | PL pl -> DEglobal_pl pl, specialize_plsymbol pl
295
  | LS ls -> DEglobal_ls ls, Loc.try1 (qloc p) specialize_lsymbol ls
296
  | XS xs -> errorm ~loc:(qloc p) "unexpected exception symbol %a" print_xs xs
297

298 299
let find_xsymbol uc p = match uc_find_ps uc p with
  | XS xs -> xs
300
  | _ -> errorm ~loc:(qloc p) "exception symbol expected"
Andrei Paskevich's avatar
Andrei Paskevich committed
301

302
let find_variant_ls uc p = match uc_find_ls uc p with
303 304
  | { ls_args = [u;v]; ls_value = None } as ls when ty_equal u v -> ls
  | ls -> errorm ~loc:(qloc p) "%a is not a binary relation" Pretty.print_ls ls
305

306
let find_global_vs uc p = try match uc_find_ps uc p with
307 308
  | PV pv -> Some pv.pv_vs
  | _ -> None
309
  with _ -> None
310

311 312 313 314 315 316
let find_vs uc lvm p = match p with
  | Qdot _ -> find_global_vs uc p
  | Qident id ->
      let ovs = Mstr.find_opt id.id lvm in
      if ovs = None then find_global_vs uc p else ovs

317
let rec dpattern denv ({ pat_loc = loc } as pp) dity = match pp.pat_desc with
318
  | Ptree.PPpwild ->
319
      PPwild, denv
320
  | Ptree.PPpvar id ->
321
      PPvar (Denv.create_user_id id), add_var id dity denv
322
  | Ptree.PPpapp (q,ppl) ->
323
      let sym, dvty = specialize_qualid denv.uc q in
324
      dpat_app denv loc (mk_dexpr sym dvty loc Slab.empty) ppl dity
325
  | Ptree.PPprec fl when is_pure_record denv.uc fl ->
326
      let kn = Theory.get_known (get_theory denv.uc) in
327
      let fl = List.map (find_pure_field denv.uc) fl in
328 329 330
      let cs,pjl,flm = Loc.try2 loc Decl.parse_record kn fl in
      let wild = { pat_desc = Ptree.PPpwild; pat_loc = loc } in
      let get_val pj = Mls.find_def wild pj flm in
331
      dpat_app denv loc (hidden_ls ~loc cs) (List.map get_val pjl) dity
332
  | Ptree.PPprec fl ->
333
      let fl = List.map (find_prog_field denv.uc) fl in
334 335 336
      let cs,pjl,flm = Loc.try2 loc parse_record denv.uc fl in
      let wild = { pat_desc = Ptree.PPpwild; pat_loc = loc } in
      let get_val pj = Mls.find_def wild pj.pl_ls flm in
337
      dpat_app denv loc (hidden_pl ~loc cs) (List.map get_val pjl) dity
338 339
  | Ptree.PPptuple ppl ->
      let cs = fs_tuple (List.length ppl) in
340
      dpat_app denv loc (hidden_ls ~loc cs) ppl dity
341
  | Ptree.PPpor (lpp1, lpp2) ->
342 343 344
      let pp1, denv = dpattern denv lpp1 dity in
      let pp2, denv = dpattern denv lpp2 dity in
      PPor (pp1, pp2), denv
345
  | Ptree.PPpas (pp, id) ->
346 347 348 349 350 351 352
      let pp, denv = dpattern denv pp dity in
      PPas (pp, Denv.create_user_id id), add_var id dity denv

and dpat_app denv gloc ({ de_loc = loc } as de) ppl dity =
  let ls = match de.de_desc with
    | DEglobal_pl pl -> pl.pl_ls
    | DEglobal_ls ls -> ls
353 354
    | DEglobal_pv pv -> errorm ~loc "%a is not a constructor" print_pv pv
    | DEglobal_ps ps -> errorm ~loc "%a is not a constructor" print_ps ps
355
    | _ -> assert false in
356 357 358
  let argl, res = de.de_type in
  if List.length argl <> List.length ppl then error ~loc:gloc
    (Term.BadArity (ls, List.length argl, List.length ppl));
359 360 361 362 363 364 365 366 367
  unify_loc unify gloc res dity;
  let add_pp lp ty (ppl, denv) =
    let pp, denv = dpattern denv lp ty in pp::ppl, denv in
  let ppl, denv = List.fold_right2 add_pp ppl argl ([],denv) in
  let pp = match de.de_desc with
    | DEglobal_pl pl -> Mlw_expr.PPpapp (pl, ppl)
    | DEglobal_ls ls -> Mlw_expr.PPlapp (ls, ppl)
    | _ -> assert false in
  pp, denv
368

369 370
(* specifications *)

371
let dbinders denv bl =
372
  let hv = Hstr.create 3 in
373
  let dbinder (id,gh,pty) (denv,bl,tyl) =
374 375
    if Hstr.mem hv id.id then raise (DuplicateProgVar id.id);
    Hstr.add hv id.id ();
376
    let dity = match pty with
377
      | Some pty -> dity_of_pty denv pty
378
      | None -> create_type_variable () in
379
    add_var id dity denv, (id,gh,dity)::bl, dity::tyl
380 381
  in
  List.fold_right dbinder bl (denv,[],[])
382

383
let mk_dpost loc = function
384
  | [{ pat_desc = PPpwild | PPptuple [] | PPpvar _ }, _ as p] -> p
385
  | l ->
386 387 388 389
      let i = { id = "(null)"; id_loc = loc; id_lab = [] } in
      let p = { pat_desc = Ptree.PPpvar i; pat_loc = loc } in
      let v = { pp_desc = Ptree.PPvar (Qident i); pp_loc = loc } in
      p, { pp_desc = PPmatch (v,l); pp_loc = loc }
390 391

let dpost ql = List.map (fun (loc, ql) -> mk_dpost loc ql) ql
392 393

let dxpost uc ql =
394
  let add_exn (q,pat,f) m =
395
    let xs = find_xsymbol uc q in
396 397 398 399 400 401
    Mexn.change (function
      | Some l -> Some ((pat,f) :: l)
      | None   -> Some ((pat,f) :: [])) xs m in
  let exn_map (loc,ql) =
    let m = List.fold_right add_exn ql Mexn.empty in
    Mexn.map (fun ql -> [mk_dpost loc ql]) m in
402 403 404
  let add_map ql m =
    Mexn.union (fun _ l r -> Some (l @ r)) (exn_map ql) m in
  List.fold_right add_map ql Mexn.empty
405 406

let dvariant uc var =
407
  List.map (fun (le,q) -> le, Opt.map (find_variant_ls uc) q) var
408 409 410

let dspec uc sp = {
  ds_pre     = sp.sp_pre;
411
  ds_post    = dpost sp.sp_post;
412
  ds_xpost   = dxpost uc sp.sp_xpost;
413 414
  ds_reads   = sp.sp_reads;
  ds_writes  = sp.sp_writes;
415 416
  ds_variant = dvariant uc sp.sp_variant;
}
417

418 419 420
let rec dtype_c denv (tyv, sp) =
  let tyv, dvty = dtype_v denv tyv in
  (tyv, dspec denv.uc sp), dvty
421 422 423

and dtype_v denv = function
  | Tpure pty ->
424
      let dity = dity_of_pty denv pty in
425
      DSpecV (false,dity), ([],dity)
426 427
  | Tarrow (bl,tyc) ->
      let denv,bl,tyl = dbinders denv bl in
428 429
      let tyc,(argl,res) = dtype_c denv tyc in
      DSpecA (bl,tyc), (tyl @ argl,res)
430

431
(* expressions *)
432

433
let de_unit ~loc = hidden_ls ~loc Mlw_expr.fs_void
434

435 436 437 438 439 440 441 442 443 444 445 446 447 448
let de_app _loc e el =
  let argl, res = e.de_type in
  let rec unify_list argl el = match argl, el with
    | arg::argl, e::el when Loc.equal e.de_loc Loc.dummy_position ->
        expected_type e arg; unify_list argl el
    | arg::argl, e::el ->
        let res = unify_list argl el in expected_type e arg; res
    | argl, [] -> argl, res
    | [], _ when fst e.de_type = [] -> errorm ~loc:e.de_loc
        "This expression is not a function and cannot be applied"
    | [], _ -> errorm ~loc:e.de_loc
        "This function is applied to too many arguments"
  in
  DEapply (e, el), unify_list argl el
449

Andrei Paskevich's avatar
Andrei Paskevich committed
450
let rec dexpr denv e =
451
  let loc = e.Ptree.expr_loc in
452
  let labs, uloc, d = extract_labels Slab.empty denv.uloc e in
Andrei Paskevich's avatar
Andrei Paskevich committed
453
  let denv = { denv with uloc = uloc } in
454
  let d, ty = de_desc denv loc d in
455
  let loc = Opt.get_def loc uloc in
456
  mk_dexpr d ty loc labs
457

458
and de_desc denv loc = function
459 460 461 462 463 464
  | Ptree.Eident (Qident {id = x} as p) ->
      begin match Mstr.find_opt x denv.locals with
        | Some (Some tvs, dvty) -> DElocal x, specialize_scheme tvs dvty
        | Some (None,     dvty) -> DElocal x, dvty
        | None                  -> specialize_qualid denv.uc p
      end
465
  | Ptree.Eident p ->
466
      specialize_qualid denv.uc p
467 468
  | Ptree.Eapply (e1, e2) ->
      let e, el = decompose_app [e2] e1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
469
      let el = List.map (dexpr denv) el in
470
      de_app loc (dexpr denv e) el
471
  | Ptree.Elet (id, gh, e1, e2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
472
      let e1 = dexpr denv e1 in
473 474 475
      let denv = match e1.de_desc with
        | DEfun _ -> add_poly id e1.de_type denv
        | _       -> add_mono id e1.de_type denv in
Andrei Paskevich's avatar
Andrei Paskevich committed
476
      let e2 = dexpr denv e2 in
477
      DElet (id, gh, e1, e2), e2.de_type
478 479
  | Ptree.Eletrec (fdl, e1) ->
      let fdl = dletrec denv fdl in
480
      let add_one denv (id,_,dvty,_,_) = add_poly id dvty denv in
481
      let denv = List.fold_left add_one denv fdl in
Andrei Paskevich's avatar
Andrei Paskevich committed
482
      let e1 = dexpr denv e1 in
483
      DEletrec (fdl, e1), e1.de_type
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
484
  | Ptree.Efun (bl, tr) ->
485
      let denv, bl, tyl = dbinders denv bl in
486
      let tr, (argl, res) = dtriple denv tr in
487
      DEfun (bl, tr), (tyl @ argl, res)
488
  | Ptree.Ecast (e1, pty) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
489
      let e1 = dexpr denv e1 in
490
      expected_type_weak e1 (dity_of_pty denv pty);
491
      e1.de_desc, e1.de_type
492 493
  | Ptree.Enamed _ ->
      assert false
494
  | Ptree.Esequence (e1, e2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
495
      let e1 = dexpr denv e1 in
496
      expected_type e1 dity_unit;
Andrei Paskevich's avatar
Andrei Paskevich committed
497
      let e2 = dexpr denv e2 in
498
      DElet (mk_id "_" loc, false, e1, e2), e2.de_type
499
  | Ptree.Eif (e1, e2, e3) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
500
      let e1 = dexpr denv e1 in
501
      expected_type e1 dity_bool;
Andrei Paskevich's avatar
Andrei Paskevich committed
502 503
      let e2 = dexpr denv e2 in
      let e3 = dexpr denv e3 in
504 505 506
      let res = create_type_variable () in
      expected_type e2 res;
      expected_type e3 res;
507
      DEif (e1, e2, e3), e2.de_type
508 509
  | Ptree.Etuple el ->
      let ls = fs_tuple (List.length el) in
Andrei Paskevich's avatar
Andrei Paskevich committed
510
      let el = List.map (dexpr denv) el in
511
      de_app loc (hidden_ls ~loc ls) el
512
  | Ptree.Erecord fl when is_pure_record denv.uc fl ->
513
      let kn = Theory.get_known (get_theory denv.uc) in
514
      let fl = List.map (find_pure_field denv.uc) fl in
515 516
      let cs,pjl,flm = Loc.try2 loc Decl.parse_record kn fl in
      let get_val pj = match Mls.find_opt pj flm with
Andrei Paskevich's avatar
Andrei Paskevich committed
517
        | Some e -> dexpr denv e
518
        | None -> error ~loc (Decl.RecordFieldMissing (cs,pj)) in
519
      de_app loc (hidden_ls ~loc cs) (List.map get_val pjl)
520
  | Ptree.Erecord fl ->
521
      let fl = List.map (find_prog_field denv.uc) fl in
522 523
      let cs,pjl,flm = Loc.try2 loc parse_record denv.uc fl in
      let get_val pj = match Mls.find_opt pj.pl_ls flm with
Andrei Paskevich's avatar
Andrei Paskevich committed
524
        | Some e -> dexpr denv e
525
        | None -> error ~loc (Decl.RecordFieldMissing (cs.pl_ls,pj.pl_ls)) in
526
      de_app loc (hidden_pl ~loc cs) (List.map get_val pjl)
527
  | Ptree.Eupdate (e1, fl) when is_pure_record denv.uc fl ->
Andrei Paskevich's avatar
Andrei Paskevich committed
528
      let e1 = dexpr denv e1 in
529 530
      let e0 = mk_var e1 in
      let kn = Theory.get_known (get_theory denv.uc) in
531
      let fl = List.map (find_pure_field denv.uc) fl in
532 533
      let cs,pjl,flm = Loc.try2 loc Decl.parse_record kn fl in
      let get_val pj = match Mls.find_opt pj flm with
Andrei Paskevich's avatar
Andrei Paskevich committed
534
        | Some e -> dexpr denv e
535
        | None ->
536
            let loc = Loc.dummy_position in
537 538
            let d, dvty = de_app loc (hidden_ls ~loc pj) [e0] in
            mk_dexpr d dvty loc Slab.empty in
539
      let res = de_app loc (hidden_ls ~loc cs) (List.map get_val pjl) in
Andrei Paskevich's avatar
Andrei Paskevich committed
540
      mk_let ~loc ~uloc:denv.uloc e1 res
541
  | Ptree.Eupdate (e1, fl) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
542
      let e1 = dexpr denv e1 in
543
      let e0 = mk_var e1 in
544
      let fl = List.map (find_prog_field denv.uc) fl in
545 546
      let cs,pjl,flm = Loc.try2 loc parse_record denv.uc fl in
      let get_val pj = match Mls.find_opt pj.pl_ls flm with
Andrei Paskevich's avatar
Andrei Paskevich committed
547
        | Some e -> dexpr denv e
548
        | None ->
549
            let loc = Loc.dummy_position in
550 551
            let d, dvty = de_app loc (hidden_pl ~loc pj) [e0] in
            mk_dexpr d dvty loc Slab.empty in
552
      let res = de_app loc (hidden_pl ~loc cs) (List.map get_val pjl) in
Andrei Paskevich's avatar
Andrei Paskevich committed
553
      mk_let ~loc ~uloc:denv.uloc e1 res
Andrei Paskevich's avatar
Andrei Paskevich committed
554
  | Ptree.Eassign (e1, q, e2) ->
555 556 557 558 559
      let fl = dexpr denv { expr_desc = Eident q; expr_loc = qloc q } in
      let pl = match fl.de_desc with
        | DEglobal_pl pl -> pl
        | _ -> Loc.errorm ~loc:(qloc q) "%a is not a field name" print_qualid q
      in
Andrei Paskevich's avatar
Andrei Paskevich committed
560 561
      let e1 = dexpr denv e1 in
      let e2 = dexpr denv e2 in
562 563
      let d, ty = de_app loc fl [e1] in
      let e0 = mk_dexpr d ty loc Slab.empty in
564
      let res = create_type_variable () in
565
      expected_type e0 res;
566
      expected_type_weak e2 res;
567
      DEassign (pl, e1, e2), ([], dity_unit)
568
  | Ptree.Econstant (Number.ConstInt _ as c) ->
569
      DEconstant c, ([], dity_int)
570
  | Ptree.Econstant (Number.ConstReal _ as c) ->
571
      DEconstant c, ([], dity_real)
572
  | Ptree.Enot e1 ->
Andrei Paskevich's avatar
Andrei Paskevich committed
573
      let e1 = dexpr denv e1 in
574
      expected_type e1 dity_bool;
575
      DEnot e1, ([], dity_bool)
576
  | Ptree.Elazy (op, e1, e2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
577 578
      let e1 = dexpr denv e1 in
      let e2 = dexpr denv e2 in
579 580
      expected_type e1 dity_bool;
      expected_type e2 dity_bool;
581
      DElazy (op, e1, e2), ([], dity_bool)
582
  | Ptree.Ematch (e1, bl) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
583
      let e1 = dexpr denv e1 in
584
      let ety = create_type_variable () in
585
      let res = create_type_variable () in
586
      expected_type e1 ety;
587
      let branch (pp,e) =
588
        let ppat, denv = dpattern denv pp ety in
Andrei Paskevich's avatar
Andrei Paskevich committed
589
        let e = dexpr denv e in
590 591
        expected_type e res;
        ppat, e in
592
      DEmatch (e1, List.map branch bl), ([], res)
Andrei Paskevich's avatar
Andrei Paskevich committed
593
  | Ptree.Eraise (q, e1) ->
594
      let xs = find_xsymbol denv.uc q in
Andrei Paskevich's avatar
Andrei Paskevich committed
595
      let e1 = match e1 with
Andrei Paskevich's avatar
Andrei Paskevich committed
596
        | Some e1 -> dexpr denv e1
597
        | None when ity_equal xs.xs_ity ity_unit -> de_unit ~loc
Andrei Paskevich's avatar
Andrei Paskevich committed
598
        | _ -> errorm ~loc "exception argument expected" in
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
599
      expected_type e1 (specialize_xsymbol xs);
600
      DEraise (xs, e1), ([], create_type_variable ())
Andrei Paskevich's avatar
Andrei Paskevich committed
601
  | Ptree.Etry (e1, cl) ->
602
      let res = create_type_variable () in
Andrei Paskevich's avatar
Andrei Paskevich committed
603
      let e1 = dexpr denv e1 in
604
      expected_type e1 res;
605
      let branch (q, pp, e) =
606
        let xs = find_xsymbol denv.uc q in
607
        let ety = specialize_xsymbol xs in
608
        let ppat, denv = dpattern denv pp ety in
609
        let e = dexpr denv e in
610
        expected_type e res;
611
        xs, ppat, e in
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
612
      DEtry (e1, List.map branch cl), e1.de_type
613
  | Ptree.Eabsurd ->
614
      DEabsurd, ([], create_type_variable ())
615
  | Ptree.Eassert (ak, lexpr) ->
616
      DEassert (ak, lexpr), ([], dity_unit)
Andrei Paskevich's avatar
Andrei Paskevich committed
617 618
  | Ptree.Emark (id, e1) ->
      let e1 = dexpr denv e1 in
619
      DEmark (id, e1), e1.de_type
620
  | Ptree.Eany tyc ->
621 622
      let tyc, dvty = dtype_c denv tyc in
      DEany tyc, dvty
623 624 625
  | Ptree.Eghost e1 ->
      let e1 = dexpr denv e1 in
      DEghost e1, e1.de_type
626
  | Ptree.Eabstract (e1, sp) ->
627
      let e1 = dexpr denv e1 in
628 629
      let sp = dspec denv.uc sp in
      DEabstract (e1, sp), e1.de_type
630 631 632 633
  | Ptree.Eloop ({ loop_invariant = inv; loop_variant = var }, e1) ->
      let e1 = dexpr denv e1 in
      let var = dvariant denv.uc var in
      expected_type e1 dity_unit;
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
634
      DEloop (var, inv, e1), e1.de_type
635 636 637 638 639 640 641 642
  | Ptree.Efor (id, efrom, dir, eto, inv, e1) ->
      let efrom = dexpr denv efrom in
      let eto = dexpr denv eto in
      let denv = add_var id dity_int denv in
      let e1 = dexpr denv e1 in
      expected_type efrom dity_int;
      expected_type eto dity_int;
      expected_type e1 dity_unit;
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
643
      DEfor (id, efrom, dir, eto, inv, e1), e1.de_type
644

645
and dletrec denv fdl =
646
  (* add all functions into the environment *)
647
  let add_one denv (_,id,_,bl,_) =
648 649
    let argl = List.map (fun _ -> create_type_variable ()) bl in
    let dvty = argl, create_type_variable () in
650
    add_mono id dvty denv, dvty in
651
  let denv, dvtyl = Lists.map_fold_left add_one denv fdl in
652
  (* then unify the binders *)
653
  let bind_one (_,_,_,bl,_) (argl,res) =
654 655 656
    let denv,bl,tyl = dbinders denv bl in
    List.iter2 unify argl tyl;
    denv,bl,tyl,res in
657
  let denvl = List.map2 bind_one fdl dvtyl in
658
  (* then type-check the bodies *)
659 660
  let type_one (loc,id,gh,_,tr) (denv,bl,tyl,tyv) =
    let tr, (argl, res) = dtriple denv tr in
661 662 663
    if argl <> [] then errorm ~loc
      "The body of a recursive function must be a first-order value";
    unify_loc unify loc tyv res;
664
    id, gh, (tyl, tyv), bl, tr in
665
  List.map2 type_one fdl denvl
Andrei Paskevich's avatar
Andrei Paskevich committed
666

667
and dtriple denv (e, sp) =
Andrei Paskevich's avatar
Andrei Paskevich committed
668
  let e = dexpr denv e in
669 670
  let sp = dspec denv.uc sp in
  (e, sp), e.de_type
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
671

672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720
(** stage 1.5 *)

(* After the stage 1, we know precisely the types of all binders
   and program expressions. However, the regions in recursive functions
   might be over-unified, since we do not support recursive polymorphism.
   For example, the letrec below will require that a and b share the region.

     let rec main a b : int = if !a = 0 then main b a else 5

   To avoid this, we retype the whole dexpr generated at the stage 1.
   Every binder keeps its previous type with all regions refreshed.
   Every non-arrow expression keeps its previous type modulo regions.
   When we type-check recursive functions, we add them to the denv
   as polymorphic, but freeze every type variable. In other words,
   only regions are specialized during recursive calls. *)

let add_preid id dity denv =
  add_var (mk_id (Ident.preid_name id) Loc.dummy_position) dity denv

let rec rpattern denv pp dity = match pp with
  | PPwild -> denv
  | PPvar id -> add_preid id dity denv
  | PPlapp (ls, ppl) -> rpat_app denv (specialize_lsymbol ls) ppl dity
  | PPpapp (pl, ppl) -> rpat_app denv (specialize_plsymbol pl) ppl dity
  | PPor (pp1, pp2) -> rpattern (rpattern denv pp1 dity) pp2 dity
  | PPas (pp1, id) -> add_preid id dity (rpattern denv pp1 dity)

and rpat_app denv (argl,res) ppl dity =
  unify res dity;
  List.fold_left2 rpattern denv ppl argl

let rbinders denv bl =
  let rbinder (id,gh,dity) (denv,bl,tyl) =
    let dity = dity_refresh dity in
    add_var id dity denv, (id,gh,dity)::bl, dity::tyl in
  List.fold_right rbinder bl (denv,[],[])

let rec rtype_c denv (tyv, sp) =
  let tyv, dvty = rtype_v denv tyv in (tyv, sp), dvty

and rtype_v denv = function
  | DSpecV (gh, dity) ->
      let dity = dity_refresh dity in
      DSpecV (gh,dity), ([],dity)
  | DSpecA (bl,tyc) ->
      let denv,bl,tyl = rbinders denv bl in
      let tyc,(argl,res) = rtype_c denv tyc in
      DSpecA (bl,tyc), (tyl @ argl,res)

Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
721 722 723 724 725
let rec rexpr denv ({ de_type = (argl,res) } as de) =
  let desc, dvty = re_desc denv de in
  let de = { de with de_desc = desc; de_type = dvty } in
  if argl = [] then expected_type_weak de (dity_refresh res);
  de
726 727

and re_desc denv de = match de.de_desc with
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
728 729
  | DElocal x as d ->
      let dvty = match Mstr.find x denv.locals with
730 731
        | Some tvs, dvty -> specialize_scheme tvs dvty
        |