mlw_typing.ml 81.1 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2013   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
5 6 7 8 9 10
(*                                                                  *)
(*  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
exception DuplicateTypeVar of string
exception UnboundTypeVar of string

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

39 40
let qloc = Typing.qloc
let print_qualid = Typing.print_qualid
41 42 43

let () = Exn_printer.register (fun fmt e -> match e with
  | DuplicateTypeVar s ->
44 45 46
      Format.fprintf fmt "Type parameter %s is used twice" s
  | DuplicateProgVar s ->
      Format.fprintf fmt "Parameter %s is used twice" s
47 48
  | UnboundTypeVar s ->
      Format.fprintf fmt "Unbound type variable '%s" s
49 50 51
  | TooLateInvariant ->
      Format.fprintf fmt
        "Cannot add a type invariant after another program declaration"
52 53 54
  | _ -> raise e)

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

58 59
type denv = {
  uc     : module_uc;
60
  locals : (tvars option * dvty) Mstr.t;
61
  tvars  : tvars;
Andrei Paskevich's avatar
Andrei Paskevich committed
62
  uloc   : Ptree.loc option;
63
}
64

65 66 67 68
let create_denv uc = {
  uc     = uc;
  locals = Mstr.empty;
  tvars  = empty_tvars;
Andrei Paskevich's avatar
Andrei Paskevich committed
69
  uloc   = None;
70
}
71

72 73
(* Handle tuple symbols *)

74 75 76
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
77

78
let check_at f0 =
Andrei Paskevich's avatar
Andrei Paskevich committed
79 80 81 82 83 84 85 86 87 88 89 90
  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)

91 92
let count_term_tuples t =
  let syms_ts _ ts = match is_ts_tuple_id ts.ts_name with
93
    | Some n -> Hint.replace ht_tuple n () | _ -> () in
94 95 96
  let syms_ty _ ty = ty_s_fold syms_ts () ty in
  t_s_fold syms_ty (fun _ _ -> ()) () t

97
let flush_tuples uc =
98 99
  let kn = Theory.get_known (get_theory uc) in
  let add_tuple n _ uc =
Andrei Paskevich's avatar
Andrei Paskevich committed
100
    if Mid.mem (Ty.ts_tuple n).ts_name kn then uc
101
    else use_export_theory uc (tuple_theory n) in
102 103
  let uc = Hint.fold add_tuple ht_tuple uc in
  Hint.clear ht_tuple;
104 105
  uc

106
let add_pdecl_with_tuples ~wp uc pd = add_pdecl ~wp (flush_tuples uc) pd
107
let add_decl_with_tuples uc d = add_decl (flush_tuples uc) d
108

109 110 111
(** Namespace lookup *)

let uc_find_ls uc p =
112 113
  let ns = Theory.get_namespace (get_theory uc) in
  Typing.find_ns (fun ls -> ls.ls_name) Theory.ns_find_ls p ns
114

115
let get_id_ts = function
116
  | PT pt -> pt.its_ts.ts_name
117
  | TS ts -> ts.ts_name
Andrei Paskevich's avatar
Andrei Paskevich committed
118

119
let uc_find_ts uc p =
120
  Typing.find_ns get_id_ts ns_find_type_symbol p (get_namespace uc)
121 122 123 124 125 126 127

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
128

129
let uc_find_ps uc p =
130
  Typing.find_ns get_id_ps ns_find_prog_symbol p (get_namespace uc)
131

132 133
(** Typing type expressions *)

134
let rec dity_of_pty denv = function
135 136
  | Ptree.PPTtyvar (id, op) ->
      create_user_type_variable id op
137
  | Ptree.PPTtyapp (p, pl) ->
138
      let dl = List.map (dity_of_pty denv) pl in
139
      begin match uc_find_ts denv.uc p with
140
        | PT ts -> its_app ts dl
141
        | TS ts -> ts_app ts dl
142 143
      end
  | Ptree.PPTtuple pl ->
144
      let dl = List.map (dity_of_pty denv) pl in
145
      ts_app (ts_tuple (List.length pl)) dl
146

147 148 149
let opaque_binders acc args =
  List.fold_left (fun acc (_,_,dty) -> opaque_tvs acc dty) acc args

150 151
(** Typing program expressions *)

Andrei Paskevich's avatar
Andrei Paskevich committed
152
let dity_int  = ts_app ts_int  []
153
let dity_real = ts_app ts_real []
154
let dity_bool = ts_app ts_bool []
Andrei Paskevich's avatar
Andrei Paskevich committed
155
let dity_unit = ts_app ts_unit []
156

157
let unify_loc unify_fn loc x1 x2 = try unify_fn x1 x2 with
Andrei Paskevich's avatar
Andrei Paskevich committed
158
  | TypeMismatch (ity1,ity2,_) -> errorm ~loc
159
      "This expression has type %a,@ but is expected to have type %a"
160
      Mlw_pretty.print_ity ity2 Mlw_pretty.print_ity ity1
Andrei Paskevich's avatar
Andrei Paskevich committed
161 162 163
  | 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
164
  | exn when Debug.test_noflag Debug.stack_trace -> error ~loc exn
165

Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
166
let expected_type ?(weak=false) { de_loc = loc ; de_type = (argl,res) } dity =
167
  if argl <> [] then errorm ~loc "This expression is not a first-order value";
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
168
  unify_loc (unify ~weak) loc dity res
169

170
let rec extract_labels labs loc e = match e.Ptree.expr_desc with
171
  | Ptree.Enamed (Ptree.Lstr s, e) -> extract_labels (Slab.add s labs) loc e
172 173 174 175
  | 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)
176
  | e -> labs, loc, e
177

178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202
(* Hack alert. Since the result type in "let [rec] fn x y : ty = ..."
   is moved to Ecast and then usually lost in destructive unification,
   we try to preserve opacity annotations by moving them to binders. *)
let pass_opacity (e,_) bl =
  let rec find e = match e.Ptree.expr_desc with
    | Ptree.Ecast (_, pty) -> Some pty
    | Ptree.Enamed (_, e) -> find e
    | _ -> None in
  match find e with
  | Some pty ->
      let ht = Hstr.create 3 in
      let rec fill = function
        | Ptree.PPTtyapp (_, pl) | Ptree.PPTtuple pl -> List.iter fill pl
        | Ptree.PPTtyvar (id, true) -> Hstr.replace ht id.id ()
        | Ptree.PPTtyvar _ -> () in
      fill pty;
      if Hstr.length ht = 0 then bl else
      let rec pass = function
        | Ptree.PPTtyvar (id,op) -> Ptree.PPTtyvar (id, op || Hstr.mem ht id.id)
        | Ptree.PPTtyapp (p, pl) -> Ptree.PPTtyapp (p, List.map pass pl)
        | Ptree.PPTtuple pl -> Ptree.PPTtuple (List.map pass pl) in
      List.map (fun (loc,id,gh,pty) -> loc, id, gh, Opt.map pass pty) bl
  | None ->
      bl

203 204 205
let rec decompose_app args e = match e.Ptree.expr_desc with
  | Eapply (e1, e2) -> decompose_app (e2 :: args) e1
  | _ -> e, args
206

207 208 209 210 211 212 213
(* record parsing *)

let parse_record uc fll =
  let pl = match fll with
    | [] -> raise EmptyRecord
    | (pl,_)::_ -> pl in
  let its = match pl.pl_args with
214
    | [{ fd_ity = { ity_node = Ityapp (its,_,_) }}] -> its
215 216
    | _ -> raise (BadRecordField pl.pl_ls) in
  let cs, pjl = match find_constructors (get_known uc) its with
217
    | [cs,pjl] -> cs, List.map (Opt.get_exn (BadRecordField pl.pl_ls)) pjl
218 219 220 221 222 223 224 225 226
    | _ -> 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

227 228
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
229

230
let find_pure_field uc (p,e) = uc_find_ls uc p, e
231

232 233
let is_pure_record uc = function
  | fl :: _ -> (try ignore (find_prog_field uc fl); false with _ -> true)
234
  | [] -> raise Decl.EmptyRecord
235 236

let hidden_pl ~loc pl =
237 238
  { de_desc = DEglobal_pl pl;
    de_type = specialize_plsymbol pl;
239
    de_loc  = loc; de_lab = Slab.empty }
240 241

let hidden_ls ~loc ls =
242
  { de_desc = DEglobal_ls ls;
243
    de_type = Loc.try1 loc specialize_lsymbol ls;
244
    de_loc  = loc; de_lab = Slab.empty }
245 246

(* helper functions for let-expansion *)
247
let test_var e = match e.de_desc with
248
  | DElocal _ | DEglobal_pv _ | DEconstant _ -> true
249 250
  | _ -> false

251
let mk_var name e =
252
  if test_var e then e else
253
  { de_desc = DElocal name;
254 255
    de_type = e.de_type;
    de_loc  = e.de_loc;
256
    de_lab  = Slab.empty }
257

258 259 260
let mk_id s loc =
  { id = s; id_loc = loc; id_lab = [] }

261 262
let mk_dexpr desc dvty loc labs =
  { de_desc = desc; de_type = dvty; de_loc = loc; de_lab = labs }
263

264
let mk_let name ~loc ~uloc e (desc,dvty) =
265
  if test_var e then desc, dvty else
266
  let loc = Opt.get_def loc uloc in
267
  let e1 = mk_dexpr desc dvty loc Slab.empty in
268
  DElet (mk_id name e.de_loc, false, e, e1), dvty
269

270 271
(* patterns *)

272 273 274 275 276 277 278 279 280
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
281

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

289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307
let chainable_qualid uc p = match uc_find_ps uc p with
  | PS { ps_aty = { aty_args = [pv1;pv2]; aty_result = VTvalue ity }}
  | PS { ps_aty = { aty_args = [pv1]; aty_result =
          VTarrow { aty_args = [pv2]; aty_result = VTvalue ity }}} ->
      ity_equal ity ity_bool
      && not (ity_equal pv1.pv_ity ity_bool)
      && not (ity_equal pv2.pv_ity ity_bool)
  | LS { ls_args = [ty1;ty2]; ls_value = ty } ->
      Opt.fold (fun _ ty -> ty_equal ty ty_bool) true ty
      && not (ty_equal ty1 ty_bool)
      && not (ty_equal ty2 ty_bool)
  | PS _ | LS _ | PL _ | PV _ | XS _ -> false

let chainable_op denv op =
  op.id = "infix =" || op.id = "infix <>" ||
  match Mstr.find_opt op.id denv.locals with
  | Some (_, dvty) -> is_chainable dvty
  | None -> chainable_qualid denv.uc (Qident op)

308 309
let find_xsymbol uc p = match uc_find_ps uc p with
  | XS xs -> xs
310
  | _ -> errorm ~loc:(qloc p) "exception symbol expected"
Andrei Paskevich's avatar
Andrei Paskevich committed
311

312
let find_variant_ls uc p = match uc_find_ls uc p with
313 314
  | { 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
315

316
let find_global_vs uc p = try match uc_find_ps uc p with
317 318
  | PV pv -> Some pv.pv_vs
  | _ -> None
319
  with _ -> None
320

321 322 323 324 325 326
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

327
let rec dpattern denv ({ pat_loc = loc } as pp) dity = match pp.pat_desc with
328
  | Ptree.PPpwild ->
329
      PPwild, denv
330
  | Ptree.PPpvar id ->
331
      PPvar (Denv.create_user_id id), add_var id dity denv
332
  | Ptree.PPpapp (q,ppl) ->
333
      let sym, dvty = specialize_qualid denv.uc q in
334
      dpat_app denv loc (mk_dexpr sym dvty loc Slab.empty) ppl dity
335
  | Ptree.PPprec fl when is_pure_record denv.uc fl ->
336
      let kn = Theory.get_known (get_theory denv.uc) in
337
      let fl = List.map (find_pure_field denv.uc) fl in
338 339 340
      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
341
      dpat_app denv loc (hidden_ls ~loc cs) (List.map get_val pjl) dity
342
  | Ptree.PPprec fl ->
343
      let fl = List.map (find_prog_field denv.uc) fl in
344 345 346
      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
347
      dpat_app denv loc (hidden_pl ~loc cs) (List.map get_val pjl) dity
348 349
  | Ptree.PPptuple ppl ->
      let cs = fs_tuple (List.length ppl) in
350
      dpat_app denv loc (hidden_ls ~loc cs) ppl dity
351
  | Ptree.PPpor (lpp1, lpp2) ->
352 353 354
      let pp1, denv = dpattern denv lpp1 dity in
      let pp2, denv = dpattern denv lpp2 dity in
      PPor (pp1, pp2), denv
355
  | Ptree.PPpas (pp, id) ->
356 357 358 359 360 361 362
      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
363 364
    | 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
365
    | _ -> assert false in
366
  let argl, res = de.de_type in
367 368
  if List.length argl <> List.length ppl then
    error ~loc:gloc (Term.BadArity (ls, List.length ppl));
369 370 371 372 373 374 375 376 377
  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
378

379 380
(* specifications *)

381
let dbinders denv bl =
382 383
  let s = ref Sstr.empty in
  let dbinder (loc,id,gh,pty) (denv,bl,tyl) =
384
    let dity = match pty with
385
      | Some pty -> dity_of_pty denv pty
386 387 388 389 390 391 392 393 394 395
      | None -> create_type_variable ()
    in
    let denv, id = match id with
      | Some ({ id = x; id_loc = loc } as id) ->
          s := Loc.try3 loc Sstr.add_new (DuplicateProgVar x) x !s;
          add_var id dity denv, id
      | None ->
          denv, { id = "_"; id_loc = loc; id_lab = [] }
    in
    denv, (id,gh,dity)::bl, dity::tyl
396 397
  in
  List.fold_right dbinder bl (denv,[],[])
398

399
let mk_dpost loc = function
400
  | [{ pat_desc = PPpwild | PPptuple [] | PPpvar _ }, _ as p] -> p
401
  | l ->
402 403 404 405
      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 }
406 407

let dpost ql = List.map (fun (loc, ql) -> mk_dpost loc ql) ql
408 409

let dxpost uc ql =
410
  let add_exn (q,pat,f) m =
411
    let xs = find_xsymbol uc q in
412 413 414 415 416 417
    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
418 419 420
  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
421 422

let dvariant uc var =
423
  List.map (fun (le,q) -> le, Opt.map (find_variant_ls uc) q) var
424 425 426

let dspec uc sp = {
  ds_pre     = sp.sp_pre;
427
  ds_post    = dpost sp.sp_post;
428
  ds_xpost   = dxpost uc sp.sp_xpost;
429
  ds_writes  = sp.sp_writes;
430 431
  ds_variant = dvariant uc sp.sp_variant;
}
432

433 434 435
let rec dtype_c denv (tyv, sp) =
  let tyv, dvty = dtype_v denv tyv in
  (tyv, dspec denv.uc sp), dvty
436 437 438

and dtype_v denv = function
  | Tpure pty ->
439
      let dity = dity_of_pty denv pty in
440
      DSpecV dity, ([],dity)
441
  | Tarrow (bl,tyc) ->
442
      let bl = List.map (fun (l,i,g,t) -> l,i,g,Some t) bl in
443
      let denv,bl,tyl = dbinders denv bl in
444 445
      let tyc,(argl,res) = dtype_c denv tyc in
      DSpecA (bl,tyc), (tyl @ argl,res)
446

447
(* expressions *)
448

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
449 450 451 452 453 454 455
let add_lemma_label ~top id = function
  | Gnone -> id, false
  | Gghost -> id, true
  | Glemma when not top ->
      errorm ~loc:id.id_loc "lemma functions are only allowed at toplevel"
  | Glemma -> { id with id_lab = Lstr Mlw_wp.lemma_label :: id.id_lab }, true

456
let de_unit ~loc = hidden_ls ~loc Mlw_expr.fs_void
457

458 459 460 461 462 463 464 465 466 467 468 469 470 471
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
472

Andrei Paskevich's avatar
Andrei Paskevich committed
473
let rec dexpr denv e =
474
  let loc = e.Ptree.expr_loc in
475
  let labs, uloc, d = extract_labels Slab.empty denv.uloc e in
Andrei Paskevich's avatar
Andrei Paskevich committed
476
  let denv = { denv with uloc = uloc } in
477
  let d, ty = de_desc denv loc d in
478
  let loc = Opt.get_def loc uloc in
479
  mk_dexpr d ty loc labs
480

481
and de_desc denv loc = function
482 483 484 485 486 487
  | 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
488
  | Ptree.Eident p ->
489
      specialize_qualid denv.uc p
490 491
  | Ptree.Eapply (e1, e2) ->
      let e, el = decompose_app [e2] e1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
492
      let el = List.map (dexpr denv) el in
493
      de_app loc (dexpr denv e) el
494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524
  | Ptree.Einfix (e12, op2, e3)
  | Ptree.Einnfix (e12, op2, e3) ->
      let mk_bool (d,ty) =
        let de = mk_dexpr d ty (Opt.get_def loc denv.uloc) Slab.empty in
        expected_type de dity_bool; de in
      let make_app de1 op de2 =
        let id = Ptree.Eident (Qident op) in
        let e0 = { expr_desc = id; expr_loc = op.id_loc } in
        de_app loc (dexpr denv e0) [de1; de2] in
      let make_app de1 op de2 =
        if op.id <> "infix <>" then make_app de1 op de2 else
          let de12 = mk_bool (make_app de1 { op with id = "infix =" } de2) in
          DEnot de12, de12.de_type in
      let rec make_chain n1 n2 de1 = function
        | [op,de2] ->
            make_app de1 op de2
        | (op,de2) :: ch ->
            let v = mk_var n1 de2 in
            let de12 = mk_bool (make_app de1 op v) in
            let de23 = mk_bool (make_chain n2 n1 v ch) in
            let d = DElazy (LazyAnd, de12, de23) in
            mk_let n1 ~loc ~uloc:denv.uloc de2 (d, de12.de_type)
        | [] -> assert false in
      let rec get_chain e12 acc = match e12.expr_desc with
        | Ptree.Einfix (e1, op1, e2) when chainable_op denv op1 ->
            get_chain e1 ((op1, dexpr denv e2) :: acc)
        | _ -> e12, acc in
      let e1, ch = if chainable_op denv op2
        then get_chain e12 [op2, dexpr denv e3]
        else e12, [op2, dexpr denv e3] in
      make_chain "q1 " "q2 " (dexpr denv e1) ch
525
  | Ptree.Elet (id, gh, e1, e2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
526
      let e1 = dexpr denv e1 in
527 528 529
      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
530
      let e2 = dexpr denv e2 in
531
      DElet (id, gh, e1, e2), e2.de_type
532
  | Ptree.Eletrec (fdl, e1) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
533
      let fdl = dletrec ~top:false denv fdl in
534
      let add_one denv (id,_,dvty,_,_) = add_poly id dvty denv in
535
      let denv = List.fold_left add_one denv fdl in
Andrei Paskevich's avatar
Andrei Paskevich committed
536
      let e1 = dexpr denv e1 in
537
      DEletrec (fdl, e1), e1.de_type
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
538
  | Ptree.Efun (bl, tr) ->
539
      let denv, bl, tyl = dbinders denv (pass_opacity tr bl) in
540
      let tr, (argl, res) = dtriple denv tr in
541
      DEfun (bl, tr), (tyl @ argl, res)
542
  | Ptree.Ecast (e1, pty) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
543
      let e1 = dexpr denv e1 in
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
544
      expected_type ~weak:true e1 (dity_of_pty denv pty);
545
      e1.de_desc, e1.de_type
546 547
  | Ptree.Enamed _ ->
      assert false
548
  | Ptree.Esequence (e1, e2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
549
      let e1 = dexpr denv e1 in
550
      expected_type e1 dity_unit;
Andrei Paskevich's avatar
Andrei Paskevich committed
551
      let e2 = dexpr denv e2 in
552
      DElet (mk_id "_" loc, false, e1, e2), e2.de_type
553
  | Ptree.Eif (e1, e2, e3) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
554
      let e1 = dexpr denv e1 in
555
      expected_type e1 dity_bool;
Andrei Paskevich's avatar
Andrei Paskevich committed
556 557
      let e2 = dexpr denv e2 in
      let e3 = dexpr denv e3 in
558 559 560
      let res = create_type_variable () in
      expected_type e2 res;
      expected_type e3 res;
561
      DEif (e1, e2, e3), e2.de_type
562 563
  | Ptree.Etuple el ->
      let ls = fs_tuple (List.length el) in
Andrei Paskevich's avatar
Andrei Paskevich committed
564
      let el = List.map (dexpr denv) el in
565
      de_app loc (hidden_ls ~loc ls) el
566
  | Ptree.Erecord fl when is_pure_record denv.uc fl ->
567
      let kn = Theory.get_known (get_theory denv.uc) in
568
      let fl = List.map (find_pure_field denv.uc) fl in
569 570
      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
571
        | Some e -> dexpr denv e
572
        | None -> error ~loc (Decl.RecordFieldMissing (cs,pj)) in
573
      de_app loc (hidden_ls ~loc cs) (List.map get_val pjl)
574
  | Ptree.Erecord fl ->
575
      let fl = List.map (find_prog_field denv.uc) fl in
576 577
      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
578
        | Some e -> dexpr denv e
579
        | None -> error ~loc (Decl.RecordFieldMissing (cs.pl_ls,pj.pl_ls)) in
580
      de_app loc (hidden_pl ~loc cs) (List.map get_val pjl)
581
  | Ptree.Eupdate (e1, fl) when is_pure_record denv.uc fl ->
Andrei Paskevich's avatar
Andrei Paskevich committed
582
      let e1 = dexpr denv e1 in
583
      let e0 = mk_var "q " e1 in
584
      let kn = Theory.get_known (get_theory denv.uc) in
585
      let fl = List.map (find_pure_field denv.uc) fl in
586 587
      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
588
        | Some e -> dexpr denv e
589
        | None ->
590
            let loc = Loc.dummy_position in
591 592
            let d, dvty = de_app loc (hidden_ls ~loc pj) [e0] in
            mk_dexpr d dvty loc Slab.empty in
593
      let res = de_app loc (hidden_ls ~loc cs) (List.map get_val pjl) in
594
      mk_let "q " ~loc ~uloc:denv.uloc e1 res
595
  | Ptree.Eupdate (e1, fl) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
596
      let e1 = dexpr denv e1 in
597
      let e0 = mk_var "q " e1 in
598
      let fl = List.map (find_prog_field denv.uc) fl in
599 600
      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
601
        | Some e -> dexpr denv e
602
        | None ->
603
            let loc = Loc.dummy_position in
604 605
            let d, dvty = de_app loc (hidden_pl ~loc pj) [e0] in
            mk_dexpr d dvty loc Slab.empty in
606
      let res = de_app loc (hidden_pl ~loc cs) (List.map get_val pjl) in
607
      mk_let "q " ~loc ~uloc:denv.uloc e1 res
Andrei Paskevich's avatar
Andrei Paskevich committed
608
  | Ptree.Eassign (e1, q, e2) ->
609 610 611 612 613
      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
614 615
      let e1 = dexpr denv e1 in
      let e2 = dexpr denv e2 in
616 617
      let d, ty = de_app loc fl [e1] in
      let e0 = mk_dexpr d ty loc Slab.empty in
618
      let res = create_type_variable () in
619
      expected_type e0 res;
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
620
      expected_type ~weak:true e2 res;
621
      DEassign (pl, e1, e2), ([], dity_unit)
622
  | Ptree.Econstant (Number.ConstInt _ as c) ->
623
      DEconstant c, ([], dity_int)
624
  | Ptree.Econstant (Number.ConstReal _ as c) ->
625
      DEconstant c, ([], dity_real)
626
  | Ptree.Enot e1 ->
Andrei Paskevich's avatar
Andrei Paskevich committed
627
      let e1 = dexpr denv e1 in
628
      expected_type e1 dity_bool;
629
      DEnot e1, ([], dity_bool)
630
  | Ptree.Elazy (op, e1, e2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
631 632
      let e1 = dexpr denv e1 in
      let e2 = dexpr denv e2 in
633 634
      expected_type e1 dity_bool;
      expected_type e2 dity_bool;
635
      DElazy (op, e1, e2), ([], dity_bool)
636
  | Ptree.Ematch (e1, bl) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
637
      let e1 = dexpr denv e1 in
638
      let ety = create_type_variable () in
639
      let res = create_type_variable () in
640
      expected_type e1 ety;
641
      let branch (pp,e) =
642
        let ppat, denv = dpattern denv pp ety in
Andrei Paskevich's avatar
Andrei Paskevich committed
643
        let e = dexpr denv e in
644 645
        expected_type e res;
        ppat, e in
646
      DEmatch (e1, List.map branch bl), ([], res)
Andrei Paskevich's avatar
Andrei Paskevich committed
647
  | Ptree.Eraise (q, e1) ->
648
      let xs = find_xsymbol denv.uc q in
Andrei Paskevich's avatar
Andrei Paskevich committed
649
      let e1 = match e1 with
Andrei Paskevich's avatar
Andrei Paskevich committed
650
        | Some e1 -> dexpr denv e1
651
        | None when ity_equal xs.xs_ity ity_unit -> de_unit ~loc
Andrei Paskevich's avatar
Andrei Paskevich committed
652
        | _ -> errorm ~loc "exception argument expected" in
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
653
      expected_type e1 (specialize_xsymbol xs);
654
      DEraise (xs, e1), ([], create_type_variable ())
Andrei Paskevich's avatar
Andrei Paskevich committed
655
  | Ptree.Etry (e1, cl) ->
656
      let res = create_type_variable () in
Andrei Paskevich's avatar
Andrei Paskevich committed
657
      let e1 = dexpr denv e1 in
658
      expected_type e1 res;
659
      let branch (q, pp, e) =
660
        let xs = find_xsymbol denv.uc q in
661
        let ety = specialize_xsymbol xs in
662
        let ppat, denv = dpattern denv pp ety in
663
        let e = dexpr denv e in
664
        expected_type e res;
665
        xs, ppat, e in
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
666
      DEtry (e1, List.map branch cl), e1.de_type
667
  | Ptree.Eabsurd ->
668
      DEabsurd, ([], create_type_variable ())
669
  | Ptree.Eassert (ak, lexpr) ->
670
      DEassert (ak, lexpr), ([], dity_unit)
Andrei Paskevich's avatar
Andrei Paskevich committed
671 672
  | Ptree.Emark (id, e1) ->
      let e1 = dexpr denv e1 in
673
      DEmark (id, e1), e1.de_type
674
  | Ptree.Eany tyc ->
675 676
      let tyc, dvty = dtype_c denv tyc in
      DEany tyc, dvty
677 678 679
  | Ptree.Eghost e1 ->
      let e1 = dexpr denv e1 in
      DEghost e1, e1.de_type
680
  | Ptree.Eabstract (e1, sp) ->
681
      let e1 = dexpr denv e1 in
682 683
      let sp = dspec denv.uc sp in
      DEabstract (e1, sp), e1.de_type
684 685 686 687
  | 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
688
      DEloop (var, inv, e1), e1.de_type
689 690 691 692 693 694 695 696
  | 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
697
      DEfor (id, efrom, dir, eto, inv, e1), e1.de_type
698

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
699
and dletrec ~top denv fdl =
700
  (* add all functions into the environment *)
701
  let add_one denv (_,id,_,bl,_) =
702 703
    let argl = List.map (fun _ -> create_type_variable ()) bl in
    let dvty = argl, create_type_variable () in
704
    add_mono id dvty denv, dvty in
705
  let denv, dvtyl = Lists.map_fold_left add_one denv fdl in
706
  (* then unify the binders *)
707 708
  let bind_one (_,_,_,bl,tr) (argl,res) =
    let denv,bl,tyl = dbinders denv (pass_opacity tr bl) in
709 710
    List.iter2 unify argl tyl;
    denv,bl,tyl,res in
711
  let denvl = List.map2 bind_one fdl dvtyl in
712
  (* then type-check the bodies *)
713
  let type_one (loc,id,gh,_,tr) (denv,bl,tyl,tyv) =