mlw_typing.ml 78.4 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 =
79
  let fvs0 = t_vars f0 in
Andrei Paskevich's avatar
Andrei Paskevich committed
80 81
  let rec check f = match f.t_node with
    | Term.Tapp (ls, _) when ls_equal ls fs_at ->
82
        let d = Mvs.set_diff (t_vars f) fvs0 in
Andrei Paskevich's avatar
Andrei Paskevich committed
83 84 85 86 87 88 89 90 91
        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)

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

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

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

110 111 112
(** Namespace lookup *)

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

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

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

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
129

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

133 134
(** Typing type expressions *)

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

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

151 152
(** Typing program expressions *)

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

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

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

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

179 180 181 182 183
let rec find_top_pty e = match e.Ptree.expr_desc with
  | Ptree.Enamed (_, e) -> find_top_pty e
  | Ptree.Ecast (_, pty) -> Some pty
  | _ -> None

184 185 186
(* 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. *)
187
let pass_opacity (e,_) bl = match find_top_pty e with
188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203
  | 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

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

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

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

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

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

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

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

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

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

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

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

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

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

271 272
(* patterns *)

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 }

281 282 283 284
let add_rec_poly id dvty tvs denv =
  let locals = Mstr.add id.id (Some tvs, dvty) denv.locals in
  { denv with locals = locals }

285 286 287 288 289 290
let add_rec_mono id dvty denv =
  (* fix type variables but not regions *)
  let tvars = add_dvty denv.tvars dvty in
  let locals = Mstr.add id.id (Some tvars, dvty) denv.locals in
  { denv with locals = locals; tvars = tvars }

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

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

300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318
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)

319 320
let find_xsymbol uc p = match uc_find_ps uc p with
  | XS xs -> xs
321
  | _ -> errorm ~loc:(qloc p) "exception symbol expected"
Andrei Paskevich's avatar
Andrei Paskevich committed
322

323
let find_variant_ls uc p = match uc_find_ls uc p with
324 325
  | { 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
326

327
let find_global_vs uc p = try match uc_find_ps uc p with
328 329
  | PV pv -> Some pv.pv_vs
  | _ -> None
330
  with _ -> None
331

332 333 334 335 336 337
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

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

390 391
(* specifications *)

392
let dbinders denv bl =
393 394
  let s = ref Sstr.empty in
  let dbinder (loc,id,gh,pty) (denv,bl,tyl) =
395
    let dity = match pty with
396
      | Some pty -> dity_of_pty denv pty
397 398 399 400
      | None -> create_type_variable ()
    in
    let denv, id = match id with
      | Some ({ id = x; id_loc = loc } as id) ->
401
          s := Loc.try3 ~loc Sstr.add_new (DuplicateProgVar x) x !s;
402 403 404 405 406
          add_var id dity denv, id
      | None ->
          denv, { id = "_"; id_loc = loc; id_lab = [] }
    in
    denv, (id,gh,dity)::bl, dity::tyl
407 408
  in
  List.fold_right dbinder bl (denv,[],[])
409

410
let mk_dpost loc = function
411
  | [{ pat_desc = PPpwild | PPptuple [] | PPpvar _ }, _ as p] -> p
412
  | l ->
413 414 415 416
      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 }
417 418

let dpost ql = List.map (fun (loc, ql) -> mk_dpost loc ql) ql
419 420

let dxpost uc ql =
421
  let add_exn (q,pat,f) m =
422
    let xs = find_xsymbol uc q in
423 424 425 426 427 428
    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
429 430 431
  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
432 433

let dvariant uc var =
434
  List.map (fun (le,q) -> le, Opt.map (find_variant_ls uc) q) var
435 436 437

let dspec uc sp = {
  ds_pre     = sp.sp_pre;
438
  ds_post    = dpost sp.sp_post;
439
  ds_xpost   = dxpost uc sp.sp_xpost;
440
  ds_reads   = sp.sp_reads;
441
  ds_writes  = sp.sp_writes;
442 443
  ds_variant = dvariant uc sp.sp_variant;
}
444

445 446 447
let rec dtype_c denv (tyv, sp) =
  let tyv, dvty = dtype_v denv tyv in
  (tyv, dspec denv.uc sp), dvty
448 449 450

and dtype_v denv = function
  | Tpure pty ->
451
      let dity = dity_of_pty denv pty in
452
      DSpecV dity, ([],dity)
453
  | Tarrow (bl,tyc) ->
454
      let bl = List.map (fun (l,i,g,t) -> l,i,g,Some t) bl in
455
      let denv,bl,tyl = dbinders denv bl in
456 457
      let tyc,(argl,res) = dtype_c denv tyc in
      DSpecA (bl,tyc), (tyl @ argl,res)
458

459
(* expressions *)
460

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
461 462 463 464 465 466 467
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

468
let de_unit ~loc = hidden_ls ~loc Mlw_expr.fs_void
469

470 471 472 473 474 475 476 477 478 479 480 481 482 483
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
484

Andrei Paskevich's avatar
Andrei Paskevich committed
485
let rec dexpr denv e =
486
  let loc = e.Ptree.expr_loc in
487
  let labs, uloc, d = extract_labels Slab.empty denv.uloc e in
Andrei Paskevich's avatar
Andrei Paskevich committed
488
  let denv = { denv with uloc = uloc } in
489
  let d, ty = de_desc denv loc d in
490
  let loc = Opt.get_def loc uloc in
491
  mk_dexpr d ty loc labs
492

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