mlw_typing.ml 78.4 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
exception UnboundSymbol of qualid
45 46 47 48

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

49 50
let qloc = Typing.qloc
let print_qualid = Typing.print_qualid
51 52 53

let () = Exn_printer.register (fun fmt e -> match e with
  | DuplicateTypeVar s ->
54 55 56
      Format.fprintf fmt "Type parameter %s is used twice" s
  | DuplicateProgVar s ->
      Format.fprintf fmt "Parameter %s is used twice" s
57 58 59
  | TooLateInvariant ->
      Format.fprintf fmt
        "Cannot add a type invariant after another program declaration"
60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77
(*
  | 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 ->
78 79 80
      Format.fprintf fmt "Unbound type variable '%s" s
  | UnboundSymbol q ->
      Format.fprintf fmt "Unbound symbol '%a'" print_qualid q
81 82 83
  | _ -> raise e)

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

87 88
type denv = {
  uc     : module_uc;
89
  locals : (tvars option * dvty) Mstr.t;
90
  tvars  : tvars;
Andrei Paskevich's avatar
Andrei Paskevich committed
91
  uloc   : Ptree.loc option;
92
}
93

94 95 96 97
let create_denv uc = {
  uc     = uc;
  locals = Mstr.empty;
  tvars  = empty_tvars;
Andrei Paskevich's avatar
Andrei Paskevich committed
98
  uloc   = None;
99
}
100

101 102
(* Handle tuple symbols *)

103 104 105
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
106

107
let check_at f0 =
Andrei Paskevich's avatar
Andrei Paskevich committed
108 109 110 111 112 113 114 115 116 117 118 119
  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)

120 121
let count_term_tuples t =
  let syms_ts _ ts = match is_ts_tuple_id ts.ts_name with
122
    | Some n -> Hint.replace ht_tuple n () | _ -> () in
123 124 125
  let syms_ty _ ty = ty_s_fold syms_ts () ty in
  t_s_fold syms_ty (fun _ _ -> ()) () t

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

135
let add_pdecl_with_tuples ~wp uc pd = add_pdecl ~wp (flush_tuples uc) pd
136
let add_decl_with_tuples uc d = add_decl (flush_tuples uc) d
137

138 139 140
(** Namespace lookup *)

let uc_find_ls uc p =
141 142
  let ns = Theory.get_namespace (get_theory uc) in
  Typing.find_ns (fun ls -> ls.ls_name) Theory.ns_find_ls p ns
143

144
let get_id_ts = function
145
  | PT pt -> pt.its_ts.ts_name
146
  | TS ts -> ts.ts_name
Andrei Paskevich's avatar
Andrei Paskevich committed
147

148
let uc_find_ts uc p =
149 150 151 152 153 154 155 156
  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
157

158
let uc_find_ps uc p =
159
  Typing.find_ns get_id_ps ns_find_ps p (get_namespace uc)
160

161 162
(** Typing type expressions *)

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

(** Typing program expressions *)

Andrei Paskevich's avatar
Andrei Paskevich committed
178
let dity_int  = ts_app ts_int  []
179
let dity_real = ts_app ts_real []
180
let dity_bool = ts_app ts_bool []
Andrei Paskevich's avatar
Andrei Paskevich committed
181
let dity_unit = ts_app ts_unit []
182

183
let unify_loc unify_fn loc x1 x2 = try unify_fn x1 x2 with
Andrei Paskevich's avatar
Andrei Paskevich committed
184
  | TypeMismatch (ity1,ity2,_) -> errorm ~loc
185
      "This expression has type %a,@ but is expected to have type %a"
186
      Mlw_pretty.print_ity ity2 Mlw_pretty.print_ity ity1
Andrei Paskevich's avatar
Andrei Paskevich committed
187 188 189
  | 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
190
  | exn when Debug.test_noflag Debug.stack_trace -> error ~loc exn
191

192 193 194 195 196 197 198
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
199

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

208 209 210
let rec decompose_app args e = match e.Ptree.expr_desc with
  | Eapply (e1, e2) -> decompose_app (e2 :: args) e1
  | _ -> e, args
211

212 213 214 215 216 217 218 219 220 221
(* record parsing *)

let parse_record uc fll =
  let pl = match fll with
    | [] -> raise EmptyRecord
    | (pl,_)::_ -> pl in
  let its = match pl.pl_args with
    | [{ vtv_ity = { ity_node = Ityapp (its,_,_) }}] -> its
    | _ -> raise (BadRecordField pl.pl_ls) in
  let cs, pjl = match find_constructors (get_known uc) its with
222
    | [cs,pjl] -> cs, List.map (Opt.get_exn (BadRecordField pl.pl_ls)) pjl
223 224 225 226 227 228 229 230 231
    | _ -> 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

232 233
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
234

235
let find_pure_field uc (p,e) = uc_find_ls uc p, e
236

237 238
let is_pure_record uc = function
  | fl :: _ -> (try ignore (find_prog_field uc fl); false with _ -> true)
239
  | [] -> raise Decl.EmptyRecord
240 241

let hidden_pl ~loc pl =
242 243
  { de_desc = DEglobal_pl pl;
    de_type = specialize_plsymbol pl;
244
    de_loc  = loc; de_lab = Slab.empty }
245 246

let hidden_ls ~loc ls =
247
  { de_desc = DEglobal_ls ls;
248
    de_type = Loc.try1 loc specialize_lsymbol ls;
249
    de_loc  = loc; de_lab = Slab.empty }
250 251

(* helper functions for let-expansion *)
252
let test_var e = match e.de_desc with
253 254 255 256 257
  | DElocal _ | DEglobal_pv _ -> true
  | _ -> false

let mk_var e =
  if test_var e then e else
258 259 260
  { de_desc = DElocal "q";
    de_type = e.de_type;
    de_loc  = e.de_loc;
261
    de_lab  = Slab.empty }
262

263 264 265
let mk_id s loc =
  { id = s; id_loc = loc; id_lab = [] }

266 267
let mk_dexpr desc dvty loc labs =
  { de_desc = desc; de_type = dvty; de_loc = loc; de_lab = labs }
268

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

275 276
(* patterns *)

277 278 279 280 281 282 283 284 285
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
286

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

294 295
let find_xsymbol uc p = match uc_find_ps uc p with
  | XS xs -> xs
296
  | _ -> errorm ~loc:(qloc p) "exception symbol expected"
Andrei Paskevich's avatar
Andrei Paskevich committed
297

298
let find_variant_ls uc p = match uc_find_ls uc p with
299 300
  | { 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
301

302
let find_global_vs uc p = try match uc_find_ps uc p with
303 304
  | PV pv -> Some pv.pv_vs
  | _ -> None
305
  with _ -> None
306

307 308 309 310 311 312
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

313
let rec dpattern denv ({ pat_loc = loc } as pp) dity = match pp.pat_desc with
314
  | Ptree.PPpwild ->
315
      PPwild, denv
316
  | Ptree.PPpvar id ->
317
      PPvar (Denv.create_user_id id), add_var id dity denv
318
  | Ptree.PPpapp (q,ppl) ->
319
      let sym, dvty = specialize_qualid denv.uc q in
320
      dpat_app denv loc (mk_dexpr sym dvty loc Slab.empty) ppl dity
321
  | Ptree.PPprec fl when is_pure_record denv.uc fl ->
322
      let kn = Theory.get_known (get_theory denv.uc) in
323
      let fl = List.map (find_pure_field denv.uc) fl in
324 325 326
      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
327
      dpat_app denv loc (hidden_ls ~loc cs) (List.map get_val pjl) dity
328
  | Ptree.PPprec fl ->
329
      let fl = List.map (find_prog_field denv.uc) fl in
330 331 332
      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
333
      dpat_app denv loc (hidden_pl ~loc cs) (List.map get_val pjl) dity
334 335
  | Ptree.PPptuple ppl ->
      let cs = fs_tuple (List.length ppl) in
336
      dpat_app denv loc (hidden_ls ~loc cs) ppl dity
337
  | Ptree.PPpor (lpp1, lpp2) ->
338 339 340
      let pp1, denv = dpattern denv lpp1 dity in
      let pp2, denv = dpattern denv lpp2 dity in
      PPor (pp1, pp2), denv
341
  | Ptree.PPpas (pp, id) ->
342 343 344 345 346 347 348
      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
349 350
    | 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
351
    | _ -> assert false in
352 353 354
  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));
355 356 357 358 359 360 361 362 363
  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
364

365 366
(* specifications *)

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

379
let mk_dpost loc = function
380
  | [{ pat_desc = PPpwild | PPptuple [] | PPpvar _ }, _ as p] -> p
381
  | l ->
382 383 384 385
      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 }
386 387

let dpost ql = List.map (fun (loc, ql) -> mk_dpost loc ql) ql
388 389

let dxpost uc ql =
390
  let add_exn (q,pat,f) m =
391
    let xs = find_xsymbol uc q in
392 393 394 395 396 397
    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
398 399 400
  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
401 402

let dvariant uc var =
403
  List.map (fun (le,q) -> le, Opt.map (find_variant_ls uc) q) var
404 405 406

let dspec uc sp = {
  ds_pre     = sp.sp_pre;
407
  ds_post    = dpost sp.sp_post;
408
  ds_xpost   = dxpost uc sp.sp_xpost;
409 410
  ds_reads   = sp.sp_reads;
  ds_writes  = sp.sp_writes;
411 412
  ds_variant = dvariant uc sp.sp_variant;
}
413

414 415 416
let rec dtype_c denv (tyv, sp) =
  let tyv, dvty = dtype_v denv tyv in
  (tyv, dspec denv.uc sp), dvty
417 418 419

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

427
(* expressions *)
428

429
let de_unit ~loc = hidden_ls ~loc Mlw_expr.fs_void
430

431 432 433 434 435 436 437 438 439 440 441 442 443 444
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
445

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

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

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

660
and dtriple denv (e, sp) =
Andrei Paskevich's avatar
Andrei Paskevich committed
661
  let e = dexpr denv e in
662 663
  let sp = dspec denv.uc sp in
  (e, sp), e.de_type
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
664

665 666 667 668 669 670 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 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 854 855 856 857 858 859 860 861 862 863
(** 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
  |