typing.ml 46.2 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2015   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
5 6 7 8
(*                                                                  *)
(*  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.                           *)
9
(*                                                                  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
10
(********************************************************************)
11

12
open Stdlib
13
open Ident
14
open Ptree
15
open Ty
16
open Term
Andrei Paskevich's avatar
Andrei Paskevich committed
17
open Decl
18
open Theory
19
open Dterm
Andrei Paskevich's avatar
Andrei Paskevich committed
20
open Ity
21
open Expr
22 23
open Pdecl
open Pmodule
Andrei Paskevich's avatar
Andrei Paskevich committed
24

25
(** debug flags *)
26

27
let debug_parse_only = Debug.register_flag "parse_only"
Andrei Paskevich's avatar
Andrei Paskevich committed
28
  ~desc:"Stop@ after@ parsing."
29

30
let debug_type_only  = Debug.register_flag "type_only"
Andrei Paskevich's avatar
Andrei Paskevich committed
31
  ~desc:"Stop@ after@ type-checking."
32

33
(** symbol lookup *)
34 35

let rec qloc = function
36 37 38
  | Qdot (p, id) -> Loc.join (qloc p) id.id_loc
  | Qident id    -> id.id_loc

39 40 41
let qloc_last = function
  | Qdot (_, id) | Qident id -> id.id_loc

42
let rec print_qualid fmt = function
43 44
  | Qdot (p, id) -> Format.fprintf fmt "%a.%s" print_qualid p id.id_str
  | Qident id    -> Format.fprintf fmt "%s" id.id_str
45

46 47
let string_list_of_qualid q =
  let rec sloq acc = function
48 49
    | Qdot (p, id) -> sloq (id.id_str :: acc) p
    | Qident id -> id.id_str :: acc in
50
  sloq [] q
51

52
exception UnboundSymbol of qualid
53

54
let find_qualid get_id find ns q =
55 56 57
  let sl = string_list_of_qualid q in
  let r = try find ns sl with Not_found ->
    Loc.error ~loc:(qloc q) (UnboundSymbol q) in
58
  if Debug.test_flag Glob.flag then Glob.use (qloc_last q) (get_id r);
59
  r
60

61 62 63
let find_prop_ns     ns q = find_qualid (fun pr -> pr.pr_name) ns_find_pr ns q
let find_tysymbol_ns ns q = find_qualid (fun ts -> ts.ts_name) ns_find_ts ns q
let find_lsymbol_ns  ns q = find_qualid (fun ls -> ls.ls_name) ns_find_ls ns q
64

65 66
let find_fsymbol_ns ns q =
  let ls = find_lsymbol_ns ns q in
67 68
  if ls.ls_value <> None then ls else
    Loc.error ~loc:(qloc q) (FunctionSymbolExpected ls)
69

70 71
let find_psymbol_ns ns q =
  let ls = find_lsymbol_ns ns q in
72 73
  if ls.ls_value = None then ls else
    Loc.error ~loc:(qloc q) (PredicateSymbolExpected ls)
74

75 76 77 78 79
let find_prop     tuc q = find_prop_ns     (Theory.get_namespace tuc) q
let find_tysymbol tuc q = find_tysymbol_ns (Theory.get_namespace tuc) q
let find_lsymbol  tuc q = find_lsymbol_ns  (Theory.get_namespace tuc) q
let find_fsymbol  tuc q = find_fsymbol_ns  (Theory.get_namespace tuc) q
let find_psymbol  tuc q = find_psymbol_ns  (Theory.get_namespace tuc) q
80

Andrei Paskevich's avatar
Andrei Paskevich committed
81 82 83
let find_itysymbol_ns ns q =
  find_qualid (fun s -> s.its_ts.ts_name) Pmodule.ns_find_its ns q

84 85 86
let find_xsymbol_ns ns q =
  find_qualid (fun s -> s.xs_name) Pmodule.ns_find_xs ns q

87 88 89
let find_prog_symbol_ns ns p =
  let get_id_ps = function
    | PV pv -> pv.pv_vs.vs_name
90
    | RS rs -> rs.rs_name in
91 92 93 94
  find_qualid get_id_ps ns_find_prog_symbol ns p

let get_namespace muc = List.hd muc.Pmodule.muc_import

95
let find_xsymbol     muc q = find_xsymbol_ns     (get_namespace muc) q
96 97
let find_itysymbol   muc q = find_itysymbol_ns   (get_namespace muc) q
let find_prog_symbol muc q = find_prog_symbol_ns (get_namespace muc) q
Andrei Paskevich's avatar
Andrei Paskevich committed
98

99 100 101
let find_rsymbol muc q = match find_prog_symbol muc q with RS rs -> rs
  | _ -> Loc.errorm ~loc:(qloc q) "program symbol expected"

102 103
(** Parsing types *)

104
let ty_of_pty tuc pty =
105
  let rec get_ty = function
106
    | PTtyvar {id_str = x} ->
107
        ty_var (tv_of_string x)
108
    | PTtyapp (q, tyl) ->
109
        let s = find_tysymbol tuc q in
110
        let tyl = List.map get_ty tyl in
111
        Loc.try2 ~loc:(qloc q) ty_app s tyl
112
    | PTtuple tyl ->
113 114
        let s = its_tuple (List.length tyl) in
        ty_app s.its_ts (List.map get_ty tyl)
115
    | PTarrow (ty1, ty2) ->
116
        ty_func (get_ty ty1) (get_ty ty2)
117
    | PTparen ty ->
118 119 120 121
        get_ty ty
  in
  get_ty pty

122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138
let ity_of_pty muc pty =
  let rec get_ity = function
    | PTtyvar {id_str = x} ->
        ity_var (tv_of_string x)
    | PTtyapp (q, tyl) ->
        let s = find_itysymbol muc q in
        let tyl = List.map get_ity tyl in
        Loc.try2 ~loc:(qloc q) ity_app_fresh s tyl
    | PTtuple tyl ->
        ity_tuple (List.map get_ity tyl)
    | PTarrow (ty1, ty2) ->
        ity_func (get_ity ty1) (get_ity ty2)
    | PTparen ty ->
        get_ity ty
  in
  get_ity pty

139
(** typing using destructive type variables
140

141 142 143 144 145 146
    parsed trees        intermediate trees       typed trees
      (Ptree)                (Dterm)               (Term)
   -----------------------------------------------------------
     ppure_type  ---dty--->   dty       ---ty--->    ty
      lexpr      --dterm-->   dterm     --term-->    term
*)
147

148 149
(** Typing patterns, terms, and formulas *)

150
let create_user_id {id_str = n; id_lab = label; id_loc = loc} =
151 152 153 154
  let get_labels (label, loc) = function
    | Lstr lab -> Slab.add lab label, loc | Lpos loc -> label, loc in
  let label,loc = List.fold_left get_labels (Slab.empty,loc) label in
  id_user ~label n loc
155

156 157 158
let parse_record ~loc tuc get_val fl =
  let fl = List.map (fun (q,e) -> find_lsymbol tuc q, e) fl in
  let cs,pjl,flm = Loc.try2 ~loc parse_record (get_known tuc) fl in
159 160 161
  let get_val pj = get_val cs pj (Mls.find_opt pj flm) in
  cs, List.map get_val pjl

162
let rec dpattern tuc { pat_desc = desc; pat_loc = loc } =
163
  Dterm.dpattern ~loc (match desc with
164 165 166
    | Ptree.Pwild -> DPwild
    | Ptree.Pvar x -> DPvar (create_user_id x)
    | Ptree.Papp (q,pl) ->
167 168
        let pl = List.map (dpattern tuc) pl in
        DPapp (find_lsymbol tuc q, pl)
169
    | Ptree.Ptuple pl ->
170
        let pl = List.map (dpattern tuc) pl in
171
        DPapp (fs_tuple (List.length pl), pl)
172
    | Ptree.Prec fl ->
173
        let get_val _ _ = function
174
          | Some p -> dpattern tuc p
175
          | None -> Dterm.dpattern DPwild in
176
        let cs,fl = parse_record ~loc tuc get_val fl in
177
        DPapp (cs,fl)
178 179 180
    | Ptree.Pas (p, x) -> DPas (dpattern tuc p, create_user_id x)
    | Ptree.Por (p, q) -> DPor (dpattern tuc p, dpattern tuc q)
    | Ptree.Pcast (p, ty) -> DPcast (dpattern tuc p, ty_of_pty tuc ty))
181

182
let quant_var tuc (loc, id, gh, ty) =
183 184
  assert (not gh);
  let ty = match ty with
185
    | Some ty -> dty_of_ty (ty_of_pty tuc ty)
186
    | None    -> dty_fresh () in
187
  Opt.map create_user_id id, ty, Some loc
188

189 190 191 192 193 194 195 196 197 198 199 200 201 202
let is_reusable dt = match dt.dt_node with
  | DTvar _ | DTgvar _ | DTconst _ | DTtrue | DTfalse -> true
  | DTapp (_,[]) -> true
  | _ -> false

let mk_var n dt =
  let dty = match dt.dt_dty with
    | None -> dty_of_ty ty_bool
    | Some dty -> dty in
  Dterm.dterm ?loc:dt.dt_loc (DTvar (n, dty))

let mk_let ~loc n dt node =
  DTlet (dt, id_user n loc, Dterm.dterm ~loc node)

203
let chainable_op tuc op =
204
  (* non-bool -> non-bool -> bool *)
205
  op.id_str = "infix =" || op.id_str = "infix <>" ||
206
  match find_lsymbol tuc (Qident op) with
207 208 209 210 211
  | {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)
  | _ -> false
212

213 214 215
let mk_closure loc ls =
  let mk dt = Dterm.dterm ~loc dt in
  let mk_v i _ =
216 217
    Some (id_user ("y" ^ string_of_int i) loc), dty_fresh (), None in
  let mk_t (id, dty, _) = mk (DTvar ((Opt.get id).pre_name, dty)) in
218
  let vl = Lists.mapi mk_v ls.ls_args in
Andrei Paskevich's avatar
Andrei Paskevich committed
219
  DTquant (DTlambda, vl, [], mk (DTapp (ls, List.map mk_t vl)))
220

221
let rec dterm tuc gvars denv {term_desc = desc; term_loc = loc} =
222 223 224
  let func_app e el =
    List.fold_left (fun e1 (loc, e2) ->
      DTfapp (Dterm.dterm ~loc e1, e2)) e el
225
  in
226 227 228 229
  let rec apply_ls loc ls al l el = match l, el with
    | (_::l), (e::el) -> apply_ls loc ls (e::al) l el
    | [], _ -> func_app (DTapp (ls, List.rev_map snd al)) el
    | _, [] -> func_app (mk_closure loc ls) (List.rev_append al el)
230
  in
231
  let qualid_app q el = match gvars q with
232
    | Some v -> func_app (DTgvar v.pv_vs) el
233
    | None ->
234
        let ls = find_lsymbol tuc q in
235
        apply_ls (qloc q) ls [] ls.ls_args el
236
  in
237
  let qualid_app q el = match q with
238
    | Qident {id_str = n} ->
239
        (match denv_get_opt denv n with
240 241 242 243
        | Some d -> func_app d el
        | None -> qualid_app q el)
    | _ -> qualid_app q el
  in
244 245
  let rec unfold_app e1 e2 el = match e1.term_desc with
    | Tapply (e11,e12) ->
246
        let e12 = dterm tuc gvars denv e12 in
247 248 249
        unfold_app e11 e12 ((e1.term_loc, e2)::el)
    | Tident q ->
        qualid_app q ((e1.term_loc, e2)::el)
250
    | _ ->
251
        func_app (DTfapp (dterm tuc gvars denv e1, e2)) el
252
  in
253
  Dterm.dterm ~loc (match desc with
254
  | Ptree.Tident q ->
255
      qualid_app q []
256
  | Ptree.Tidapp (q, tl) ->
257 258
      let tl = List.map (dterm tuc gvars denv) tl in
      DTapp (find_lsymbol tuc q, tl)
259
  | Ptree.Tapply (e1, e2) ->
260
      unfold_app e1 (dterm tuc gvars denv e2) []
261
  | Ptree.Ttuple tl ->
262
      let tl = List.map (dterm tuc gvars denv) tl in
263
      DTapp (fs_tuple (List.length tl), tl)
264 265 266 267
  | Ptree.Tinfix (e12, op2, e3)
  | Ptree.Tinnfix (e12, op2, e3) ->
      let make_app de1 op de2 = if op.id_str = "infix <>" then
        let op = { op with id_str = "infix =" } in
268
        let ls = find_lsymbol tuc (Qident op) in
269 270
        DTnot (Dterm.dterm ~loc (DTapp (ls, [de1;de2])))
      else
271
        DTapp (find_lsymbol tuc (Qident op), [de1;de2])
272 273 274 275 276 277 278
      in
      let rec make_chain de1 = function
        | [op,de2] ->
            make_app de1 op de2
        | (op,de2) :: ch ->
            let de12 = Dterm.dterm ~loc (make_app de1 op de2) in
            let de23 = Dterm.dterm ~loc (make_chain de2 ch) in
279
            DTbinop (DTand, de12, de23)
280
        | [] -> assert false in
281
      let rec get_chain e12 acc = match e12.term_desc with
282 283
        | Tinfix (e1, op1, e2) when chainable_op tuc op1 ->
            get_chain e1 ((op1, dterm tuc gvars denv e2) :: acc)
284
        | _ -> e12, acc in
285 286
      let ch = [op2, dterm tuc gvars denv e3] in
      let e1, ch = if chainable_op tuc op2
287
        then get_chain e12 ch else e12, ch in
288
      make_chain (dterm tuc gvars denv e1) ch
289
  | Ptree.Tconst c ->
290
      DTconst c
291
  | Ptree.Tlet (x, e1, e2) ->
292
      let id = create_user_id x in
293
      let e1 = dterm tuc gvars denv e1 in
294
      let denv = denv_add_let denv e1 id in
295
      let e2 = dterm tuc gvars denv e2 in
296
      DTlet (e1, id, e2)
297
  | Ptree.Tmatch (e1, bl) ->
298
      let e1 = dterm tuc gvars denv e1 in
299
      let branch (p, e) =
300
        let p = dpattern tuc p in
301
        let denv = denv_add_pat denv p in
302
        p, dterm tuc gvars denv e in
303
      DTcase (e1, List.map branch bl)
304
  | Ptree.Tif (e1, e2, e3) ->
305 306 307
      let e1 = dterm tuc gvars denv e1 in
      let e2 = dterm tuc gvars denv e2 in
      let e3 = dterm tuc gvars denv e3 in
308
      DTif (e1, e2, e3)
309
  | Ptree.Ttrue ->
310
      DTtrue
311
  | Ptree.Tfalse ->
312
      DTfalse
313
  | Ptree.Tunop (Ptree.Tnot, e1) ->
314
      DTnot (dterm tuc gvars denv e1)
315
  | Ptree.Tbinop (e1, op, e2) ->
316 317
      let e1 = dterm tuc gvars denv e1 in
      let e2 = dterm tuc gvars denv e2 in
318
      let op = match op with
319 320 321 322 323 324
        | Ptree.Tand -> DTand
        | Ptree.Tand_asym -> DTand_asym
        | Ptree.Tor -> DTor
        | Ptree.Tor_asym -> DTor_asym
        | Ptree.Timplies -> DTimplies
        | Ptree.Tiff -> DTiff in
325
      DTbinop (op, e1, e2)
326
  | Ptree.Tquant (q, uqu, trl, e1) ->
327
      let qvl = List.map (quant_var tuc) uqu in
328
      let denv = denv_add_quant denv qvl in
329
      let dterm e = dterm tuc gvars denv e in
330 331
      let trl = List.map (List.map dterm) trl in
      let e1 = dterm e1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
332 333 334 335 336
      let q = match q with
        | Ptree.Tforall -> DTforall
        | Ptree.Texists -> DTexists
        | Ptree.Tlambda -> DTlambda in
      DTquant (q, qvl, trl, e1)
337
  | Ptree.Trecord fl ->
338
      let get_val cs pj = function
339
        | Some e -> dterm tuc gvars denv e
340
        | None -> Loc.error ~loc (RecordFieldMissing (cs,pj)) in
341
      let cs, fl = parse_record ~loc tuc get_val fl in
342
      DTapp (cs, fl)
343
  | Ptree.Tupdate (e1, fl) ->
344
      let e1 = dterm tuc gvars denv e1 in
345 346
      let re = is_reusable e1 in
      let v = if re then e1 else mk_var "_q " e1 in
347
      let get_val _ pj = function
348
        | Some e -> dterm tuc gvars denv e
349
        | None -> Dterm.dterm ~loc (DTapp (pj,[v])) in
350
      let cs, fl = parse_record ~loc tuc get_val fl in
351 352
      let d = DTapp (cs, fl) in
      if re then d else mk_let ~loc "_q " e1 d
353
  | Ptree.Tnamed (Lpos uloc, e1) ->
354
      DTuloc (dterm tuc gvars denv e1, uloc)
355
  | Ptree.Tnamed (Lstr lab, e1) ->
356
      DTlabel (dterm tuc gvars denv e1, Slab.singleton lab)
357
  | Ptree.Tcast (e1, ty) ->
358
      DTcast (dterm tuc gvars denv e1, ty_of_pty tuc ty))
359

360
(** typing program expressions *)
Andrei Paskevich's avatar
Andrei Paskevich committed
361

362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435
open Dexpr

(* records *)

let find_record_field muc q =
  match find_prog_symbol muc q with RS ({rs_field = Some _} as s) -> s
  | _ -> Loc.errorm ~loc:(qloc q) "Not a record field: %a" print_qualid q

let find_record_field2 muc (q,e) = find_record_field muc q, e

let parse_record muc fll =
  (* we assume that every rsymbol in fll was resolved
     using find_record_field, so they are all fields *)
  let ls_of_rs rs = match rs.rs_logic with
    | RLls ls -> ls | _ -> assert false in
  let rs = match fll with
    | (rs, _)::_ -> rs
    | [] -> raise EmptyRecord in
  let its = match rs.rs_cty.cty_args with
    | [{pv_ity = {ity_node = (Ityreg {reg_its = its}
        | Ityapp (its,_,_) | Itypur (its,_))}}] -> its
    | _ -> raise (BadRecordField (ls_of_rs rs)) in
  let itd = find_its_defn muc.muc_known its in
  let check v s = match s.rs_field with
    | Some u -> pv_equal v u
    | _ -> false in
  let cs = match itd.itd_constructors with
    | [cs] when Lists.equal check cs.rs_cty.cty_args itd.itd_fields -> cs
    | _ -> raise (BadRecordField (ls_of_rs rs)) in
  let pjs = Srs.of_list itd.itd_fields in
  let flm = List.fold_left (fun m (pj,v) -> if Srs.mem pj pjs then
    Mrs.add_new (DuplicateRecordField (ls_of_rs cs, ls_of_rs pj)) pj v m
    else raise (BadRecordField (ls_of_rs pj))) Mrs.empty fll in
  cs, itd.itd_fields, flm

let parse_record ~loc muc get_val fl =
  let fl = List.map (find_record_field2 muc) fl in
  let cs,pjl,flm = Loc.try2 ~loc parse_record muc fl in
  let get_val pj = get_val cs pj (Mrs.find_opt pj flm) in
  cs, List.map get_val pjl

(* patterns *)

let rec dpattern muc { pat_desc = desc; pat_loc = loc } =
  Dexpr.dpattern ~loc (match desc with
    | Ptree.Pwild -> DPwild
    | Ptree.Pvar x -> DPvar (create_user_id x)
    | Ptree.Papp (q,pl) ->
        DPapp (find_rsymbol muc q, List.map (fun p -> dpattern muc p) pl)
    | Ptree.Prec fl ->
        let get_val _ _ = function
          | Some p -> dpattern muc p
          | None -> Dexpr.dpattern DPwild in
        let cs,fl = parse_record ~loc muc get_val fl in
        DPapp (cs,fl)
    | Ptree.Ptuple pl ->
        DPapp (rs_tuple (List.length pl), List.map (dpattern muc) pl)
    | Ptree.Pcast (p, pty) -> DPcast (dpattern muc p, ity_of_pty muc pty)
    | Ptree.Pas (p, x) -> DPas (dpattern muc p, create_user_id x)
    | Ptree.Por (p, q) -> DPor (dpattern muc p, dpattern muc q))

(* specifications *)

let find_global_pv muc q = try match find_prog_symbol muc q with
  | PV v -> Some v | _ -> None with _ -> None

let find_local_pv muc lvm q = match q with
  | Qdot _ -> find_global_pv muc q
  | Qident id -> let ovs = Mstr.find_opt id.id_str lvm in
      if ovs = None then find_global_pv muc q else ovs

let type_term muc lvm t =
  let gvars p = find_local_pv muc lvm p in
  let t = dterm muc.muc_theory gvars Dterm.denv_empty t in
436
  Dterm.term ~strict:true ~keep_loc:true t
Andrei Paskevich's avatar
Andrei Paskevich committed
437

438 439 440
let type_fmla muc lvm f =
  let gvars p = find_local_pv muc lvm p in
  let f = dterm muc.muc_theory gvars Dterm.denv_empty f in
441
  Dterm.fmla ~strict:true ~keep_loc:true f
Andrei Paskevich's avatar
Andrei Paskevich committed
442

443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 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 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634
let dpre muc pl lvm =
  let dpre f = type_fmla muc lvm f in
  List.map dpre pl

let dpost muc ql lvm ity =
  let dpost (loc,pfl) = match pfl with
    | [{ pat_desc = Ptree.Pwild | Ptree.Ptuple [] }, f] ->
        let v = create_pvsymbol (id_fresh "result") ity in
        v, Loc.try3 ~loc type_fmla muc lvm f
    | [{ pat_desc = Ptree.Pvar id }, f] ->
        let v = create_pvsymbol (create_user_id id) ity in
        let lvm = Mstr.add id.id_str v lvm in
        v, Loc.try3 ~loc type_fmla muc lvm f
    | _ ->
        let v = create_pvsymbol (id_fresh "result") ity in
        let i = { id_str = "(null)"; id_loc = loc; id_lab = [] } in
        let t = { term_desc = Tident (Qident i); term_loc = loc } in
        let f = { term_desc = Tmatch (t, pfl); term_loc = loc } in
        let lvm = Mstr.add "(null)" v lvm in
        v, Loc.try3 ~loc type_fmla muc lvm f in
  List.map dpost ql

let dxpost muc ql lvm =
  let add_exn (q,pat,f) m =
    let xs = find_xsymbol muc q in
    Mexn.change (function
      | Some l -> Some ((pat,f) :: l)
      | None   -> Some ((pat,f) :: [])) xs m in
  let mk_xpost loc xs pfl =
    dpost muc [loc,pfl] lvm xs.xs_ity in
  let exn_map (loc,xpfl) =
    let m = List.fold_right add_exn xpfl Mexn.empty in
    Mexn.mapi (fun xs pfl -> mk_xpost loc xs pfl) m in
  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

let dreads muc rl lvm =
  let dreads q = match find_local_pv muc lvm q with Some v -> v
    | None -> Loc.errorm ~loc:(qloc q) "Not a variable: %a" print_qualid q in
  List.map dreads rl

let dwrites muc wl lvm =
  let dwrites t = type_term muc lvm t in
  List.map dwrites wl

let find_variant_ls muc q = match find_lsymbol muc.muc_theory q with
  | { ls_args = [u;v]; ls_value = None } as ls when ty_equal u v -> ls
  | s -> Loc.errorm ~loc:(qloc q) "Not an order relation: %a" Pretty.print_ls s

let dvariant muc varl lvm _regold =
  let dvar t = type_term muc lvm t in
  let dvar (t,q) = dvar t, Opt.map (find_variant_ls muc) q in
  List.map dvar varl

let dspec muc sp lvm _regold ity = {
  ds_pre     = dpre muc sp.sp_pre lvm;
  ds_post    = dpost muc sp.sp_post lvm ity;
  ds_xpost   = dxpost muc sp.sp_xpost lvm;
  ds_reads   = dreads muc sp.sp_reads lvm;
  ds_writes  = dwrites muc sp.sp_writes lvm;
  ds_checkrw = sp.sp_checkrw;
  ds_diverge = sp.sp_diverge; }

let dassert muc f lvm _regold = type_fmla muc lvm f

let dinvariant muc f lvm _regold = dpre muc f lvm

(* abstract values *)

let dbinder muc id gh pty =
  let id = Opt.map create_user_id id in
  let dity = match pty with
    | Some pty -> dity_of_ity (ity_of_pty muc pty)
    | None -> dity_fresh () in
  id, gh, dity

let dparam muc (_,id,gh,pty) = dbinder muc id gh (Some pty)

let dbinder muc (_,id,gh,pty) = dbinder muc id gh pty

(* expressions *)

let is_reusable de = match de.de_node with
  | DEvar _ | DEpv _ | DEconst _ | DEtrue | DEfalse -> true
  | DErs {rs_logic = (RLls _|RLpv _); rs_cty = cty} ->
      cty.cty_args = [] && cty.cty_result.ity_pure
  | _ -> false

let mk_var n de =
  Dexpr.dexpr ?loc:de.de_loc (DEvar (n, de.de_dvty))

let mk_let ~loc n de node =
  let de1 = Dexpr.dexpr ~loc node in
  DElet ((id_user n loc, false, RKnone, de), de1)

let chainable_rs = function
  | {rs_cty = { cty_args = [pv1;pv2]; cty_result = ity}} ->
      ity_equal ity ity_bool
      && not (ity_equal pv1.pv_ity ity_bool)
      && not (ity_equal pv2.pv_ity ity_bool)
  | _ -> false

let chainable_qualid muc p = match find_prog_symbol muc p with
  | RS s -> chainable_rs s
  | _ -> false

let chainable_op muc denv op =
  (* non-bool -> non-bool -> bool *)
  op.id_str = "infix =" || op.id_str = "infix <>" ||
  match denv_get_opt denv op.id_str with
  | Some (DEvar (_,t)) -> dvty_is_chainable t
  | Some (DErs s) -> chainable_rs s
  | Some _ -> false (* can never happen *)
  | None -> chainable_qualid muc (Qident op)

let rec dexpr muc denv {expr_desc = desc; expr_loc = loc} =
  let expr_app loc e el =
    List.fold_left (fun e1 e2 ->
      DEapp (Dexpr.dexpr ~loc e1, e2)) e el
  in
  let qualid_app loc q el = match find_prog_symbol muc q with
    | PV pv -> expr_app loc (DEpv pv) el
    | RS rs -> expr_app loc (DErs rs) el
  in
  let qualid_app loc q el = match q with
    | Qident {id_str = n} ->
        (match denv_get_opt denv n with
        | Some d -> expr_app loc d el
        | None -> qualid_app loc q el)
    | _ -> qualid_app loc q el
  in
  Dexpr.dexpr ~loc (match desc with
  | Ptree.Eident q ->
      qualid_app loc q []
  | Ptree.Eidapp (q, el) ->
      qualid_app loc q (List.map (dexpr muc denv) el)
  | Ptree.Eapply (e1, e2) ->
      DEapp (dexpr muc denv e1, dexpr muc denv e2)
  | Ptree.Etuple el ->
      let e = DErs (rs_tuple (List.length el)) in
      expr_app loc e (List.map (dexpr muc denv) el)
  | Ptree.Einfix (e12, op2, e3)
  | Ptree.Einnfix (e12, op2, e3) ->
      let make_app de1 op de2 = if op.id_str = "infix <>" then
        let oq = Qident { op with id_str = "infix =" } in
        let dt = qualid_app op.id_loc oq [de1; de2] in
        DEnot (Dexpr.dexpr ~loc dt)
      else
        qualid_app op.id_loc (Qident op) [de1; de2]
      in
      let rec make_chain n1 n2 de1 = function
        | [op,de2] ->
            make_app de1 op de2
        | (op,de2) :: ch ->
            let re = is_reusable de2 in
            let v = if re then de2 else mk_var n1 de2 in
            let de12 = Dexpr.dexpr ~loc (make_app de1 op v) in
            let de23 = Dexpr.dexpr ~loc (make_chain n2 n1 v ch) in
            let d = DEand (de12, de23) in
            if re then d else mk_let ~loc n1 de2 d
        | [] -> assert false in
      let rec get_chain e12 acc = match e12.expr_desc with
        | Ptree.Einfix (e1, op1, e2) when chainable_op muc denv op1 ->
            get_chain e1 ((op1, dexpr muc denv e2) :: acc)
        | _ -> e12, acc in
      let ch = [op2, dexpr muc denv e3] in
      let e1, ch = if chainable_op muc denv op2
        then get_chain e12 ch else e12, ch in
      make_chain "q1 " "q2 " (dexpr muc denv e1) ch
  | Ptree.Econst c -> DEconst c
  | Ptree.Erecord fl ->
      let ls_of_rs rs = match rs.rs_logic with
        | RLls ls -> ls | _ -> assert false in
      let get_val cs pj = function
        | None -> Loc.error ~loc
            (Decl.RecordFieldMissing (ls_of_rs cs, ls_of_rs pj))
        | Some e -> dexpr muc denv e in
      let cs,fl = parse_record ~loc muc get_val fl in
      expr_app loc (DErs cs) fl
  | Ptree.Eupdate (e1, fl) ->
      let e1 = dexpr muc denv e1 in
      let re = is_reusable e1 in
      let v = if re then e1 else mk_var "_q " e1 in
      let get_val _ pj = function
        | None ->
            let pj = Dexpr.dexpr ~loc (DErs pj) in
            Dexpr.dexpr ~loc (DEapp (pj, v))
        | Some e -> dexpr muc denv e in
      let cs,fl = parse_record ~loc muc get_val fl in
      let d = expr_app loc (DErs cs) fl in
      if re then d else mk_let ~loc "_q " e1 d
635
  | Ptree.Elet (id, gh, kind, e1, e2) ->
636 637 638 639 640
      let ld = create_user_id id, gh, kind, dexpr muc denv e1 in
      DElet (ld, dexpr muc (denv_add_let denv ld) e2)
  | Ptree.Erec (fdl, e1) ->
      let denv, rd = drec_defn muc denv fdl in
      DErec (rd, dexpr muc denv e1)
641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657
  | Ptree.Efun (bl, pty, sp, e) ->
      let bl = List.map (dbinder muc) bl in
      let e = match pty with
        | Some pty -> { e with expr_desc = Ecast (e, pty) }
        | None -> e in
      let ds = match sp.sp_variant with
        | ({term_loc = loc},_)::_ ->
            Loc.errorm ~loc "unexpected 'variant' clause"
        | _ -> dspec muc sp in
      DEfun (bl, ds, dexpr muc (denv_add_args denv bl) e)
  | Ptree.Eany (pl, pty, sp) ->
      let pl = List.map (dparam muc) pl in
      let ds = match sp.sp_variant with
        | ({term_loc = loc},_)::_ ->
            Loc.errorm ~loc "unexpected 'variant' clause"
        | _ -> dspec muc sp in
      DEany (pl, ds, dity_of_ity (ity_of_pty muc pty))
658 659 660 661 662 663 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
  | Ptree.Ematch (e1, bl) ->
      let e1 = dexpr muc denv e1 in
      let branch (pp, e) =
        let pp = dpattern muc pp in
        let denv = denv_add_pat denv pp in
        pp, dexpr muc denv e in
      DEcase (e1, List.map branch bl)
  | Ptree.Eif (e1, e2, e3) ->
      let e1 = dexpr muc denv e1 in
      let e2 = dexpr muc denv e2 in
      let e3 = dexpr muc denv e3 in
      DEif (e1, e2, e3)
  | Ptree.Enot e1 ->
      DEnot (dexpr muc denv e1)
  | Ptree.Eand (e1, e2) ->
      DEand (dexpr muc denv e1, dexpr muc denv e2)
  | Ptree.Eor (e1, e2) ->
      DEor (dexpr muc denv e1, dexpr muc denv e2)
  | Ptree.Etrue -> DEtrue
  | Ptree.Efalse -> DEfalse
  | Ptree.Esequence (e1, e2) ->
      let e1 = dexpr muc denv e1 in
      let e2 = dexpr muc denv e2 in
      DElet ((id_user "_" loc, false, RKnone, e1), e2)
  | Ptree.Eloop (inv, var, e1) ->
      let e1 = dexpr muc denv e1 in
      let inv = dinvariant muc inv in
      let var = dvariant muc var in
      DEwhile (Dexpr.dexpr DEtrue, inv, var, e1)
  | Ptree.Ewhile (e1, inv, var, e2) ->
      let e1 = dexpr muc denv e1 in
      let e2 = dexpr muc denv e2 in
      let inv = dinvariant muc inv in
      let var = dvariant muc var in
      DEwhile (e1, inv, var, e2)
  | Ptree.Efor (id, efrom, dir, eto, inv, e1) ->
      let efrom = dexpr muc denv efrom in
      let eto = dexpr muc denv eto in
      let inv = dinvariant muc inv in
      let id = create_user_id id in
      let denv = denv_add_var denv id (dity_of_ity ity_int) in
      DEfor (id, efrom, dir, eto, inv, dexpr muc denv e1)
  | Ptree.Eassign (e1, q, e2) ->
      DEassign [dexpr muc denv e1, find_record_field muc q, dexpr muc denv e2]
  | Ptree.Eraise (q, e1) ->
      let xs = find_xsymbol muc q in
      let e1 = match e1 with
        | Some e1 -> dexpr muc denv e1
        | None when ity_equal xs.xs_ity ity_unit ->
            Dexpr.dexpr ~loc (DErs rs_void)
        | _ -> Loc.errorm ~loc "exception argument expected" in
      DEraise (xs, e1)
  | Ptree.Etry (e1, cl) ->
      let e1 = dexpr muc denv e1 in
      let branch (q, pp, e) =
        let xs = find_xsymbol muc q in
        let pp = match pp with
          | Some pp -> dpattern muc pp
          | None when ity_equal xs.xs_ity ity_unit ->
              Dexpr.dpattern ~loc (DPapp (rs_void, []))
          | _ -> Loc.errorm ~loc "exception argument expected" in
        let denv = denv_add_pat denv pp in
        let e = dexpr muc denv e in
        xs, pp, e in
      DEtry (e1, List.map branch cl)
  | Ptree.Eghost e1 ->
      DEghost (dexpr muc denv e1)
  | Ptree.Eabsurd -> DEabsurd
  | Ptree.Eassert (ak, lexpr) ->
      DEassert (ak, dassert muc lexpr)
  | Ptree.Emark (id, e1) ->
      DEmark (create_user_id id, dexpr muc denv e1)
  | Ptree.Enamed (Lpos uloc, e1) ->
      DEuloc (dexpr muc denv e1, uloc)
  | Ptree.Enamed (Lstr lab, e1) ->
      DElabel (dexpr muc denv e1, Slab.singleton lab)
  | Ptree.Ecast (e1, pty) ->
      DEcast (dexpr muc denv e1, ity_of_pty muc pty))

and drec_defn muc denv fdl =
738
  let prep (id, gh, kind, bl, pty, sp, e) =
739 740 741 742 743 744 745 746 747 748
    let bl = List.map (dbinder muc) bl in
    let dity = match pty with
      | Some pty -> dity_of_ity (ity_of_pty muc pty)
      | None -> dity_fresh () in
    let pre denv =
      let dv = dvariant muc sp.sp_variant in
      dspec muc sp, dv, dexpr muc denv e in
    create_user_id id, gh, kind, bl, dity, pre in
  Dexpr.drec_defn denv (List.map prep fdl)

749
(** Typing declarations *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
750

Andrei Paskevich's avatar
Andrei Paskevich committed
751 752
open Pdecl
open Pmodule
753

754
let add_pdecl ~vc muc d =
Andrei Paskevich's avatar
Andrei Paskevich committed
755
  if Debug.test_flag Glob.flag then Sid.iter Glob.def d.pd_news;
756
  add_pdecl ~vc muc d
Andrei Paskevich's avatar
Andrei Paskevich committed
757

758
let add_decl muc d = add_pdecl ~vc:false muc (create_pure_decl d)
Andrei Paskevich's avatar
Andrei Paskevich committed
759

760 761 762
let add_types muc tdl =
  let add m ({td_ident = {id_str = x}; td_loc = loc} as d) =
    Mstr.add_new (Loc.Located (loc, ClashSymbol x)) x d m in
Andrei Paskevich's avatar
Andrei Paskevich committed
763 764 765 766 767 768
  let def = List.fold_left add Mstr.empty tdl in
  let hts = Hstr.create 5 in
  let htd = Hstr.create 5 in
  let rec visit ~alias ~alg x d = if not (Hstr.mem htd x) then
    let id = create_user_id d.td_ident and loc = d.td_loc in
    let args = List.map (fun id -> tv_of_string id.id_str) d.td_params in
769
    match d.td_def with
Andrei Paskevich's avatar
Andrei Paskevich committed
770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792
    | TDabstract ->
        if d.td_inv <> [] then Loc.errorm ~loc
          "Abstract non-record types cannot have invariants";
        let itd = create_abstract_type_decl id args d.td_mut in
        Hstr.add hts x itd.itd_its; Hstr.add htd x itd
    | TDalias pty ->
        if d.td_vis <> Public || d.td_mut then Loc.errorm ~loc
          "Alias types cannot be abstract, private. or mutable";
        if d.td_inv <> [] then Loc.errorm ~loc
          "Alias types cannot have invariants";
        let alias = Sstr.add x alias in
        let ity = parse ~loc ~alias ~alg pty in
        if not (Hstr.mem htd x) then
        let itd = create_alias_decl id args ity in
        Hstr.add hts x itd.itd_its; Hstr.add htd x itd
    | TDalgebraic csl ->
        if d.td_vis <> Public || d.td_mut then Loc.errorm ~loc
          "Algebraic types cannot be abstract, private. or mutable";
        if d.td_inv <> [] then Loc.errorm ~loc
          "Algebraic types cannot have invariants";
        let hfd = Hstr.create 5 in
        let alias = Sstr.empty in
        let alg = Mstr.add x (id,args) alg in
793 794 795 796 797
        let get_pj nms (_, id, ghost, pty) = match id with
          | Some ({id_str = nm} as id) ->
              let exn = Loc.Located (id.id_loc, Loc.Message ("Field " ^
                nm ^ " is used more than once in the same constructor")) in
              let nms = Sstr.add_new exn nm nms in
Andrei Paskevich's avatar
Andrei Paskevich committed
798
              let ity = parse ~loc ~alias ~alg pty in
799
              let v = try Hstr.find hfd nm with Not_found ->
Andrei Paskevich's avatar
Andrei Paskevich committed
800
                let v = create_pvsymbol (create_user_id id) ~ghost ity in
801
                Hstr.add hfd nm v;
Andrei Paskevich's avatar
Andrei Paskevich committed
802 803
                v in
              if not (ity_equal v.pv_ity ity && ghost = v.pv_ghost) then
804 805
                Loc.errorm ~loc "Conflicting definitions for field %s" nm;
              nms, (true, v)
Andrei Paskevich's avatar
Andrei Paskevich committed
806 807
          | None ->
              let ity = parse ~loc ~alias ~alg pty in
808 809 810 811 812 813 814 815 816 817 818 819 820
              nms, (false, create_pvsymbol (id_fresh "a") ~ghost ity) in
        let get_cs oms (_, id, pjl) =
          let nms, pjl = Lists.map_fold_left get_pj Sstr.empty pjl in
          if Sstr.equal oms nms then create_user_id id, pjl else
            let df = Sstr.union (Sstr.diff oms nms) (Sstr.diff nms oms) in
            Loc.errorm ~loc "Field %s is missing in some constructors"
              (Sstr.choose df) in
        let csl = match csl with
          | (_, id, pjl)::csl ->
              let oms, pjl = Lists.map_fold_left get_pj Sstr.empty pjl in
              (create_user_id id, pjl) :: List.map (get_cs oms) csl
          | [] -> assert false in
        if not (Hstr.mem htd x) then
Andrei Paskevich's avatar
Andrei Paskevich committed
821 822 823 824 825 826 827 828 829
        begin match try Some (Hstr.find hts x) with Not_found -> None with
        | Some s ->
            Hstr.add htd x (create_rec_variant_decl s csl)
        | None ->
            let itd = create_flat_variant_decl id args csl in
            Hstr.add hts x itd.itd_its; Hstr.add htd x itd end
    | TDrecord fl ->
        let alias = Sstr.empty in
        let alg = Mstr.add x (id,args) alg in
830 831 832 833 834
        let get_fd nms fd =
          let {id_str = nm; id_loc = loc} = fd.f_ident in
          let exn = Loc.Located (loc, Loc.Message ("Field " ^
            nm ^ " is used more than once in a record")) in
          let nms = Sstr.add_new exn nm nms in
Andrei Paskevich's avatar
Andrei Paskevich committed
835 836 837
          let id = create_user_id fd.f_ident in
          let ity = parse ~loc ~alias ~alg fd.f_pty in
          let ghost = d.td_vis = Abstract || fd.f_ghost in
838 839 840
          nms, (fd.f_mutable, create_pvsymbol id ~ghost ity) in
        let _,fl = Lists.map_fold_left get_fd Sstr.empty fl in
        if not (Hstr.mem htd x) then
Andrei Paskevich's avatar
Andrei Paskevich committed
841 842 843 844 845 846 847 848 849 850 851
        begin match try Some (Hstr.find hts x) with Not_found -> None with
        | Some s ->
            if d.td_vis <> Public || d.td_mut then Loc.errorm ~loc
              "Recursive types cannot be abstract, private. or mutable";
            if d.td_inv <> [] then Loc.errorm ~loc
              "Recursive types cannot have invariants";
            let get_fd (mut, fd) = if mut then Loc.errorm ~loc
              "Recursive types cannot have mutable fields" else fd in
            Hstr.add htd x (create_rec_record_decl s (List.map get_fd fl))
        | None ->
            let priv = d.td_vis <> Public and mut = d.td_mut in
852
            let add_fd m (_, v) = Mstr.add v.pv_vs.vs_name.id_string v m in
Andrei Paskevich's avatar
Andrei Paskevich committed
853 854
            let gvars = List.fold_left add_fd Mstr.empty fl in
            let gvars q = match q with
855 856 857 858 859
              | Qident x -> Mstr.find_opt x.id_str gvars
              | _ -> None in
            let invl = List.map (fun f ->
              Dterm.fmla ~strict:true ~keep_loc:true
                (dterm muc.muc_theory gvars Dterm.denv_empty f)) d.td_inv in
Andrei Paskevich's avatar
Andrei Paskevich committed
860 861 862 863 864 865 866 867 868 869 870
            let itd = create_flat_record_decl id args priv mut fl invl in
            Hstr.add hts x itd.itd_its; Hstr.add htd x itd end

  and parse ~loc ~alias ~alg pty =
    let rec down = function
      | PTtyvar id ->
          ity_var (tv_of_string id.id_str)
      | PTtyapp (q,tyl) ->
          let s = match q with
            | Qident {id_str = x} when Sstr.mem x alias ->
                Loc.errorm ~loc "Cyclic type definition"
871 872
            | Qident {id_str = x} when Hstr.mem hts x ->
                Hstr.find hts x
Andrei Paskevich's avatar
Andrei Paskevich committed
873 874 875
            | Qident {id_str = x} when Mstr.mem x alg ->
                let id, args = Mstr.find x alg in
                let s = create_itysymbol_pure id args in
876 877 878
                Hstr.add hts x s;
                visit ~alias ~alg x (Mstr.find x def);
                s
Andrei Paskevich's avatar
Andrei Paskevich committed
879
            | Qident {id_str = x} when Mstr.mem x def ->
880
                visit ~alias ~alg x (Mstr.find x def);
Andrei Paskevich's avatar
Andrei Paskevich committed
881 882
                Hstr.find hts x
            | _ ->
883
                find_itysymbol muc q in
Andrei Paskevich's avatar
Andrei Paskevich committed
884 885 886 887 888 889 890 891
          Loc.try2 ~loc:(qloc q) ity_app_fresh s (List.map down tyl)
      | PTtuple tyl -> ity_tuple (List.map down tyl)
      | PTarrow (ty1,ty2) -> ity_func (down ty1) (down ty2)
      | PTparen ty -> down ty in
    down pty in

  Mstr.iter (visit ~alias:Mstr.empty ~alg:Mstr.empty) def;
  let tdl = List.map (fun d -> Hstr.find htd d.td_ident.id_str) tdl in
892
  add_pdecl ~vc:true muc (create_type_decl tdl)
893

894
let tyl_of_params tuc pl =
Andrei Paskevich's avatar
Andrei Paskevich committed
895 896 897
  let ty_of_param (loc,_,gh,ty) =
    if gh then Loc.errorm ~loc
      "ghost parameters are not allowed in pure declarations";
898
    ty_of_pty tuc ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
899
  List.map ty_of_param pl
900

901 902
let add_logics muc dl =
  let tuc = muc.muc_theory in
903
  let lsymbols = Hstr.create 17 in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
904
  (* 1. create all symbols and make an environment with these symbols *)
905
  let create_symbol muc d =
906
    let id = d.ld_ident.id_str in
907
    let v = create_user_id d.ld_ident in
908 909
    let pl = tyl_of_params tuc d.ld_params in
    let ty = Opt.map (ty_of_pty tuc) d.ld_type in
910
    let ls = create_lsymbol v pl ty in
911
    Hstr.add lsymbols id ls;
912 913
    Loc.try2 ~loc:d.ld_loc add_decl muc (create_param_decl ls) in
  let tuc = (List.fold_left create_symbol muc dl).muc_theory in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
914
  (* 2. then type-check all definitions *)
915
  let type_decl d (abst,defn) =
916
    let id = d.ld_ident.id_str in
917
    let ls = Hstr.find lsymbols id in
918
    let create_var (loc,x,_,_) ty =
919
      let id = match x with
920
        | Some id -> create_user_id id
921 922
        | None -> id_user "_" loc in
      create_vsymbol id ty in
923
    let vl = List.map2 create_var d.ld_params ls.ls_args in
924
    let add_var mvs (_,x,_,_) vs = match x with
925
      | Some {id_str = x} -> Mstr.add_new (DuplicateVar x) x (DTgvar vs) mvs
926
      | None -> mvs in
927
    let denv = List.fold_left2 add_var Dterm.denv_empty d.ld_params vl in
928 929 930
    match d.ld_def, d.ld_type with
    | None, _ -> ls :: abst, defn
    | Some e, None -> (* predicate *)
931
        let f = dterm tuc (fun _ -> None) denv e in
932
        let f = fmla ~strict:true ~keep_loc:true f in
933
        abst, (make_ls_defn ls vl f) :: defn