typing.ml 56.4 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2018   --   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 Wstdlib
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
  | Qdot (p, id) ->
44 45
      Format.fprintf fmt "%a.%a" print_qualid p Ident.print_decoded id.id_str
  | Qident id -> Ident.print_decoded fmt id.id_str
46

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

53
exception UnboundSymbol of qualid
54

55
let find_qualid get_id find ns q =
56 57 58
  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
59
  if Debug.test_flag Glob.flag then Glob.use ~kind:"" (qloc_last q) (get_id r);
60
  r
61

62 63 64
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
65

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

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

76 77 78 79
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 81 82 83
let find_prop     tuc q = find_prop_ns     (Theory.get_namespace tuc) q

let find_prop_of_kind k tuc q =
  let pr = find_prop tuc q in
Andrei Paskevich's avatar
Andrei Paskevich committed
84
  match (Mid.find pr.pr_name tuc.uc_known).d_node with
85
  | Dind _ when k = Paxiom -> pr
86 87 88
  | Dprop (l,_,_) when l = k -> pr
  | _ -> Loc.errorm ~loc:(qloc q) "proposition %a is not %s"
      print_qualid q (match k with
89
        | Plemma -> "a lemma" | Paxiom -> "an axiom" | Pgoal -> "a goal")
90

Andrei Paskevich's avatar
Andrei Paskevich committed
91 92 93
let find_itysymbol_ns ns q =
  find_qualid (fun s -> s.its_ts.ts_name) Pmodule.ns_find_its ns q

94 95 96
let find_xsymbol_ns ns q =
  find_qualid (fun s -> s.xs_name) Pmodule.ns_find_xs ns q

97 98 99
let find_prog_symbol_ns ns p =
  let get_id_ps = function
    | PV pv -> pv.pv_vs.vs_name
100 101 102 103
    | RS rs -> rs.rs_name
      (* FIXME: this is incorrect, but we cannot
        know the correct symbol at this stage *)
    | OO ss -> (Srs.choose ss).rs_name in
104 105
  find_qualid get_id_ps ns_find_prog_symbol ns p

106 107
(** Parsing types *)

108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124
let rec ty_of_pty ns = function
  | PTtyvar {id_str = x} ->
      ty_var (tv_of_string x)
  | PTtyapp (q, tyl) ->
      let ts = find_tysymbol_ns ns q in
      let tyl = List.map (ty_of_pty ns) tyl in
      Loc.try2 ~loc:(qloc q) ty_app ts tyl
  | PTtuple tyl ->
      let s = its_tuple (List.length tyl) in
      ty_app s.its_ts (List.map (ty_of_pty ns) tyl)
  | PTarrow (ty1, ty2) ->
      ty_func (ty_of_pty ns ty1) (ty_of_pty ns ty2)
  | PTscope (q, ty) ->
      let ns = import_namespace ns (string_list_of_qualid q) in
      ty_of_pty ns ty
  | PTpure ty | PTparen ty ->
      ty_of_pty ns ty
125

126 127
let dty_of_pty ns pty =
  Dterm.dty_of_ty (ty_of_pty ns pty)
128

129 130
let dty_of_opt ns = function
  | Some pty -> dty_of_pty ns pty
131 132
  | None -> Dterm.dty_fresh ()

133
(** typing using destructive type variables
134

135 136 137 138 139 140
    parsed trees        intermediate trees       typed trees
      (Ptree)                (Dterm)               (Term)
   -----------------------------------------------------------
     ppure_type  ---dty--->   dty       ---ty--->    ty
      lexpr      --dterm-->   dterm     --term-->    term
*)
141

142 143
(** Typing patterns, terms, and formulas *)

Andrei Paskevich's avatar
Andrei Paskevich committed
144 145 146 147 148
let create_user_id {id_str = n; id_ats = attrs; id_loc = loc} =
  let get_attrs (attrs, loc) = function
    | ATstr attr -> Sattr.add attr attrs, loc | ATpos loc -> attrs, loc in
  let attrs, loc = List.fold_left get_attrs (Sattr.empty, loc) attrs in
  id_user ~attrs n loc
149

150 151 152
let parse_record ~loc ns km get_val fl =
  let fl = List.map (fun (q,e) -> find_lsymbol_ns ns q, e) fl in
  let cs,pjl,flm = Loc.try2 ~loc parse_record km fl in
153 154 155
  let get_val pj = get_val cs pj (Mls.find_opt pj flm) in
  cs, List.map get_val pjl

156
let rec dpattern ns km { pat_desc = desc; pat_loc = loc } =
157 158
  match desc with
    | Ptree.Pparen p -> dpattern ns km p
159 160 161
    | Ptree.Pscope (q,p) ->
        let ns = import_namespace ns (string_list_of_qualid q) in
        dpattern ns km p
162
    | _ -> (* creative indentation ahead *)
163
  Dterm.dpattern ~loc (match desc with
164 165
    | Ptree.Pparen _
    | Ptree.Pscope _ -> assert false (* never *)
166
    | Ptree.Pwild -> DPwild
167 168
    | Ptree.Pvar x -> DPvar (create_user_id x)
    | Ptree.Papp (q,pl) ->
169 170
        let pl = List.map (dpattern ns km) pl in
        DPapp (find_lsymbol_ns ns q, pl)
171
    | Ptree.Ptuple pl ->
172
        let pl = List.map (dpattern ns km) pl in
173
        DPapp (fs_tuple (List.length pl), pl)
174
    | Ptree.Prec fl ->
175
        let get_val _ _ = function
176
          | Some p -> dpattern ns km p
177
          | None -> Dterm.dpattern DPwild in
178
        let cs,fl = parse_record ~loc ns km get_val fl in
179
        DPapp (cs,fl)
180 181 182 183 184
    | Ptree.Pas (p,x,false) -> DPas (dpattern ns km p, create_user_id x)
    | Ptree.Por (p,q) -> DPor (dpattern ns km p, dpattern ns km q)
    | Ptree.Pcast (p,ty) -> DPcast (dpattern ns km p, dty_of_pty ns ty)
    | Ptree.Pghost _ | Ptree.Pas (_,_,true) ->
        Loc.errorm ~loc "ghost patterns are only allowed in programs")
185

186
let quant_var ns (loc, id, gh, ty) =
187
  if gh then Loc.errorm ~loc "ghost variables are only allowed in programs";
188
  Opt.map create_user_id id, dty_of_opt ns ty, Some loc
189

190 191 192 193 194 195
let loc_cutoff loc13 loc23 loc2 =
  let f,l,b,e = Loc.get loc13 in
  let _,_,_,w = Loc.get loc23 in
  let _,_,_,m = Loc.get loc2 in
  Loc.user_position f l b (e - (w - m))

196 197 198 199 200
let is_reusable dt = match dt.dt_node with
  | DTvar _ | DTgvar _ | DTconst _ | DTtrue | DTfalse -> true
  | DTapp (_,[]) -> true
  | _ -> false

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

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

210 211
let mk_closure crcmap loc ls =
  let mk dt = Dterm.dterm crcmap ~loc dt in
212
  let mk_v i _ =
213 214
    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
215
  let vl = Lists.mapi mk_v ls.ls_args in
Andrei Paskevich's avatar
Andrei Paskevich committed
216
  DTquant (DTlambda, vl, [], mk (DTapp (ls, List.map mk_t vl)))
217

218 219 220
(* track the use of labels *)
let at_uses = Hstr.create 5

221
let rec dterm ns km crcmap gvars at denv {term_desc = desc; term_loc = loc} =
222 223
  let func_app e el =
    List.fold_left (fun e1 (loc, e2) ->
224
      DTfapp (Dterm.dterm crcmap ~loc e1, e2)) e el
225
  in
226 227 228
  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
229
    | _, [] -> func_app (mk_closure crcmap loc ls) (List.rev_append al el)
230
  in
231
  let qualid_app q el = match gvars at q with
232 233 234 235 236 237 238 239 240
    | Some v ->
        begin match at with
        | Some l -> (* check for impact *)
            let u = Opt.get (gvars None q) in
            if not (pv_equal v u) then
              Hstr.replace at_uses l true
        | None -> ()
        end;
        func_app (DTgvar v.pv_vs) el
241
    | None ->
242
        let ls = find_lsymbol_ns ns q in
243
        apply_ls (qloc q) ls [] ls.ls_args el
244
  in
245
  let qualid_app q el = match q with
246
    | Qident {id_str = n} ->
247
        (match denv_get_opt denv n with
248 249 250 251
        | Some d -> func_app d el
        | None -> qualid_app q el)
    | _ -> qualid_app q el
  in
252
  let rec unfold_app e1 e2 el = match e1.term_desc with
253
    | Ptree.Tapply (e11,e12) ->
254
        let e12 = dterm ns km crcmap gvars at denv e12 in
255
        unfold_app e11 e12 ((e1.term_loc, e2)::el)
256
    | Ptree.Tident q ->
257
        qualid_app q ((e1.term_loc, e2)::el)
258
    | _ ->
259
        func_app (DTfapp (dterm ns km crcmap gvars at denv e1, e2)) el
260
  in
261
  Dterm.dterm crcmap ~loc (match desc with
262
  | Ptree.Tident q ->
263
      qualid_app q []
264
  | Ptree.Tidapp (q, tl) ->
265
      let tl = List.map (dterm ns km crcmap gvars at denv) tl in
266
      DTapp (find_lsymbol_ns ns q, tl)
267
  | Ptree.Tapply (e1, e2) ->
268
      unfold_app e1 (dterm ns km crcmap gvars at denv e2) []
269
  | Ptree.Ttuple tl ->
270
      let tl = List.map (dterm ns km crcmap gvars at denv) tl in
271
      DTapp (fs_tuple (List.length tl), tl)
272 273 274
  | Ptree.Tinfix (e1, op1, e23)
  | Ptree.Tinnfix (e1, op1, e23) ->
      let apply loc de1 op de2 =
275 276
        if op.id_str = Ident.op_neq then
          let op = { op with id_str = Ident.op_equ } in
277 278
          let ls = find_lsymbol_ns ns (Qident op) in
          DTnot (Dterm.dterm crcmap ~loc (DTapp (ls, [de1;de2])))
279
        else
280
          DTapp (find_lsymbol_ns ns (Qident op), [de1;de2]) in
281 282
      let rec chain loc de1 op1 = function
        | { term_desc = Ptree.Tinfix (e2, op2, e3); term_loc = loc23 } ->
283
            let de2 = dterm ns km crcmap gvars at denv e2 in
284
            let loc12 = loc_cutoff loc loc23 e2.term_loc in
285 286
            let de12 = Dterm.dterm crcmap ~loc:loc12 (apply loc12 de1 op1 de2) in
            let de23 = Dterm.dterm crcmap ~loc:loc23 (chain loc23 de2 op2 e3) in
287
            DTbinop (DTand, de12, de23)
288
        | e23 ->
289 290
            apply loc de1 op1 (dterm ns km crcmap gvars at denv e23) in
      chain loc (dterm ns km crcmap gvars at denv e1) op1 e23
Clément Fumex's avatar
Clément Fumex committed
291
  | Ptree.Tconst (Number.ConstInt _ as c) ->
292
      DTconst (c, dty_int)
Clément Fumex's avatar
Clément Fumex committed
293
  | Ptree.Tconst (Number.ConstReal _ as c) ->
294
      DTconst (c, dty_real)
295
  | Ptree.Tlet (x, e1, e2) ->
296
      let id = create_user_id x in
297
      let e1 = dterm ns km crcmap gvars at denv e1 in
298
      let denv = denv_add_let denv e1 id in
299
      let e2 = dterm ns km crcmap gvars at denv e2 in
300
      DTlet (e1, id, e2)
301
  | Ptree.Tcase (e1, bl) ->
302
      let e1 = dterm ns km crcmap gvars at denv e1 in
303
      let branch (p, e) =
304
        let p = dpattern ns km p in
305
        let denv = denv_add_term_pat denv p e1 in
306
        p, dterm ns km crcmap gvars at denv e in
307
      DTcase (e1, List.map branch bl)
308
  | Ptree.Tif (e1, e2, e3) ->
309 310 311
      let e1 = dterm ns km crcmap gvars at denv e1 in
      let e2 = dterm ns km crcmap gvars at denv e2 in
      let e3 = dterm ns km crcmap gvars at denv e3 in
312
      DTif (e1, e2, e3)
313
  | Ptree.Ttrue ->
314
      DTtrue
315
  | Ptree.Tfalse ->
316
      DTfalse
Andrei Paskevich's avatar
Andrei Paskevich committed
317
  | Ptree.Tnot e1 ->
318
      DTnot (dterm ns km crcmap gvars at denv e1)
Andrei Paskevich's avatar
Andrei Paskevich committed
319 320 321 322
  | Ptree.Tbinop (e1, Dterm.DTiff, e23)
  | Ptree.Tbinnop (e1, Dterm.DTiff, e23) ->
      let rec chain loc de1 = function
        | { term_desc = Ptree.Tbinop (e2, DTiff, e3); term_loc = loc23 } ->
323
            let de2 = dterm ns km crcmap gvars at denv e2 in
Andrei Paskevich's avatar
Andrei Paskevich committed
324
            let loc12 = loc_cutoff loc loc23 e2.term_loc in
325 326
            let de12 = Dterm.dterm crcmap ~loc:loc12 (DTbinop (DTiff, de1, de2)) in
            let de23 = Dterm.dterm crcmap ~loc:loc23 (chain loc23 de2 e3) in
Andrei Paskevich's avatar
Andrei Paskevich committed
327 328 329 330 331
            DTbinop (DTand, de12, de23)
        | { term_desc = Ptree.Tbinop (_, DTimplies, _); term_loc = loc23 } ->
            Loc.errorm ~loc:loc23 "An unparenthesized implication cannot be \
              placed at the right hand side of an equivalence"
        | e23 ->
332 333
            DTbinop (DTiff, de1, (dterm ns km crcmap gvars at denv e23)) in
      chain loc (dterm ns km crcmap gvars at denv e1) e23
Andrei Paskevich's avatar
Andrei Paskevich committed
334 335
  | Ptree.Tbinop (e1, op, e2)
  | Ptree.Tbinnop (e1, op, e2) ->
336 337
      let e1 = dterm ns km crcmap gvars at denv e1 in
      let e2 = dterm ns km crcmap gvars at denv e2 in
338
      DTbinop (op, e1, e2)
339
  | Ptree.Tquant (q, uqu, trl, e1) ->
340
      let qvl = List.map (quant_var ns) uqu in
341
      let denv = denv_add_quant denv qvl in
342
      let dterm e = dterm ns km crcmap gvars at denv e in
343 344
      let trl = List.map (List.map dterm) trl in
      let e1 = dterm e1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
345
      DTquant (q, qvl, trl, e1)
346
  | Ptree.Trecord fl ->
347
      let get_val _cs pj = function
348
        | Some e -> dterm ns km crcmap gvars at denv e
349
        | None -> Loc.error ~loc (RecordFieldMissing pj) in
350
      let cs, fl = parse_record ~loc ns km get_val fl in
351
      DTapp (cs, fl)
352
  | Ptree.Tupdate (e1, fl) ->
353
      let e1 = dterm ns km crcmap gvars at denv e1 in
354
      let re = is_reusable e1 in
355
      let v = if re then e1 else mk_var crcmap "q " e1 in
356
      let get_val _ pj = function
357 358
        | Some e -> dterm ns km crcmap gvars at denv e
        | None -> Dterm.dterm crcmap ~loc (DTapp (pj,[v])) in
359
      let cs, fl = parse_record ~loc ns km get_val fl in
360
      let d = DTapp (cs, fl) in
361
      if re then d else mk_let crcmap ~loc "q " e1 d
362
  | Ptree.Tat (e1, ({id_str = l; id_loc = loc} as id)) ->
363
      Hstr.add at_uses l false;
364 365 366
      let id = { id with id_str = "" } in
      (* check if the label has actually been defined *)
      ignore (Loc.try2 ~loc gvars (Some l) (Qident id));
367
      let e1 = dterm ns km crcmap gvars (Some l) denv e1 in
368 369
      if not (Hstr.find at_uses l) then Loc.errorm ~loc
        "this `at'/`old' operator is never used";
370
      Hstr.remove at_uses l;
Andrei Paskevich's avatar
Andrei Paskevich committed
371
      DTattr (e1, Sattr.empty)
Andrei Paskevich's avatar
M.()  
Andrei Paskevich committed
372
  | Ptree.Tscope (q, e1) ->
373
      let ns = import_namespace ns (string_list_of_qualid q) in
Andrei Paskevich's avatar
Andrei Paskevich committed
374 375
      DTattr (dterm ns km crcmap gvars at denv e1, Sattr.empty)
  | Ptree.Tattr (ATpos uloc, e1) ->
376
      DTuloc (dterm ns km crcmap gvars at denv e1, uloc)
Andrei Paskevich's avatar
Andrei Paskevich committed
377 378
  | Ptree.Tattr (ATstr attr, e1) ->
      DTattr (dterm ns km crcmap gvars at denv e1, Sattr.singleton attr)
379
  | Ptree.Tcast ({term_desc = Ptree.Tconst c}, pty) ->
380
      DTconst (c, dty_of_pty ns pty)
381
  | Ptree.Tcast (e1, pty) ->
382 383
      let d1 = dterm ns km crcmap gvars at denv e1 in
      DTcast (d1, dty_of_pty ns pty))
Andrei Paskevich's avatar
Andrei Paskevich committed
384

385

386 387 388 389
let no_gvars at q = match at with
  | Some _ -> Loc.errorm ~loc:(qloc q)
      "`at' and `old' can only be used in program annotations"
  | None -> None
390

391 392
let type_term_in_namespace ns km crcmap t =
  let t = dterm ns km crcmap no_gvars None Dterm.denv_empty t in
393 394
  Dterm.term ~strict:true ~keep_loc:true t

395 396
let type_fmla_in_namespace ns km crcmap f =
  let f = dterm ns km crcmap no_gvars None Dterm.denv_empty f in
397
  Dterm.fmla ~strict:true ~keep_loc:true f
Andrei Paskevich's avatar
Andrei Paskevich committed
398

399

400
(** typing program expressions *)
Andrei Paskevich's avatar
Andrei Paskevich committed
401

402 403
open Dexpr

404
let ty_of_pty tuc = ty_of_pty (get_namespace tuc)
405

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

408

409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428
let dterm muc =
  let uc = muc.muc_theory in
  dterm (Theory.get_namespace uc) uc.uc_known uc.uc_crcmap

let find_xsymbol     muc q = find_xsymbol_ns     (get_namespace muc) q
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

let find_special muc test nm q =
  match find_prog_symbol muc q with
  | RS s when test s -> s
  | OO ss ->
      begin match Srs.elements (Srs.filter test ss) with
      | [s] -> s
      | _::_ -> Loc.errorm ~loc:(qloc q)
                          "Ambiguous %s notation: %a" nm print_qualid q
      | [] -> Loc.errorm ~loc:(qloc q) "Not a %s: %a" nm print_qualid q
      end
  | _ ->      Loc.errorm ~loc:(qloc q) "Not a %s: %a" nm print_qualid q

429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447
let rec ity_of_pty muc = 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 (ity_of_pty muc) tyl in
      Loc.try3 ~loc:(qloc q) ity_app s tyl []
  | PTtuple tyl ->
      ity_tuple (List.map (ity_of_pty muc) tyl)
  | PTarrow (ty1, ty2) ->
      ity_func (ity_of_pty muc ty1) (ity_of_pty muc ty2)
  | PTpure ty ->
      ity_purify (ity_of_pty muc ty)
  | PTscope (q, ty) ->
      let muc = open_scope muc "dummy" in
      let muc = import_scope muc (string_list_of_qualid q) in
      ity_of_pty muc ty
  | PTparen ty ->
      ity_of_pty muc ty
448 449 450 451 452 453 454 455

let dity_of_pty muc pty =
  Dexpr.dity_of_ity (ity_of_pty muc pty)

let dity_of_opt muc = function
  | Some pty -> dity_of_pty muc pty
  | None -> Dexpr.dity_fresh ()

456 457 458
(* records *)

let find_record_field muc q =
459 460
  let test rs = rs.rs_field <> None in
  find_special muc test "record field" q
461 462 463 464 465 466 467 468 469 470 471 472

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
473
    | [{pv_ity = {ity_node = (Ityreg {reg_its = s} | Ityapp (s,_,_))}}] -> s
474 475 476 477 478 479 480 481 482 483
    | _ -> 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
484
    Mrs.add_new (DuplicateRecordField (ls_of_rs pj)) pj v m
485 486 487 488 489 490 491 492 493 494 495
    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 *)

496 497 498 499 500 501
let find_constructor muc q =
  let test rs = match rs.rs_logic with
    | RLls {ls_constr = c} -> c > 0
    | _ -> false in
  find_special muc test "constructor" q

502 503 504 505
let rec dpattern muc gh { pat_desc = desc; pat_loc = loc } =
  match desc with
    | Ptree.Pparen p -> dpattern muc gh p
    | Ptree.Pghost p -> dpattern muc true p
506 507 508 509
    | Ptree.Pscope (q,p) ->
        let muc = open_scope muc "dummy" in
        let muc = import_scope muc (string_list_of_qualid q) in
        dpattern muc gh p
510
    | _ -> (* creative indentation ahead *)
511
  Dexpr.dpattern ~loc (match desc with
512 513
    | Ptree.Pparen _ | Ptree.Pscope _
    | Ptree.Pghost _ -> assert false (* never *)
514
    | Ptree.Pwild -> DPwild
515 516 517
    | Ptree.Pvar x -> DPvar (create_user_id x, gh)
    | Ptree.Papp (q,pl) ->
        DPapp (find_constructor muc q, List.map (dpattern muc gh) pl)
518 519
    | Ptree.Prec fl ->
        let get_val _ _ = function
520
          | Some p -> dpattern muc gh p
521 522 523 524
          | None -> Dexpr.dpattern DPwild in
        let cs,fl = parse_record ~loc muc get_val fl in
        DPapp (cs,fl)
    | Ptree.Ptuple pl ->
525 526 527 528
        DPapp (rs_tuple (List.length pl), List.map (dpattern muc gh) pl)
    | Ptree.Pcast (p,pty) -> DPcast (dpattern muc gh p, dity_of_pty muc pty)
    | Ptree.Pas (p,x,g) -> DPas (dpattern muc gh p, create_user_id x, gh || g)
    | Ptree.Por (p,q) -> DPor (dpattern muc gh p, dpattern muc gh q))
529

530
let dpattern muc pat = dpattern muc false pat
531

532 533 534 535 536 537 538 539 540 541
(* 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

542 543
let mk_gvars muc lvm old = fun at q ->
  match find_local_pv muc lvm q, at with
544 545 546 547 548 549 550 551 552
  | Some v, Some l -> Some (old l v)
  | None, Some l ->
      begin match q with
      (* normally, we have no reason to call "old" without
         a pvsymbol, but we make an exception for an empty
         ident to check if the label is valid at Tat *)
      | Qident {id_str = ""} -> Opt.map (old l) None
      | _ -> None end
  | v, None -> v
553 554 555

let type_term muc lvm old t =
  let gvars = mk_gvars muc lvm old in
556
  let t = dterm muc gvars None Dterm.denv_empty t in
557
  Dterm.term ~strict:true ~keep_loc:true t
Andrei Paskevich's avatar
Andrei Paskevich committed
558

559 560
let type_fmla muc lvm old f =
  let gvars = mk_gvars muc lvm old in
561
  let f = dterm muc gvars None Dterm.denv_empty f in
562
  Dterm.fmla ~strict:true ~keep_loc:true f
Andrei Paskevich's avatar
Andrei Paskevich committed
563

564 565
let dpre muc pl lvm old =
  let dpre f = type_fmla muc lvm old f in
566 567
  List.map dpre pl

568
let dpost muc ql lvm old ity =
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
  let mk_case loc pfl =
    let v = create_pvsymbol (id_fresh "result") ity in
    let i = { id_str = "(null)"; id_loc = loc; id_ats = [] } in
    let t = { term_desc = Tident (Qident i); term_loc = loc } in
    let f = { term_desc = Ptree.Tcase (t, pfl); term_loc = loc } in
    let lvm = Mstr.add "(null)" v lvm in
    v, Loc.try3 ~loc type_fmla muc lvm old f in
  let dpost (loc,pfl) = match pfl with
    | [pat, f] ->
        let rec unfold p = match p.pat_desc with
          | Ptree.Pparen p | Ptree.Pscope (_,p) -> unfold p
          | Ptree.Pcast (p,pty) ->
              let ty = ty_of_ity (ity_of_pty muc pty) in
              Loc.try2 ~loc:p.pat_loc ty_equal_check (ty_of_ity ity) ty;
              unfold p
          | Ptree.Ptuple [] ->
              Loc.try2 ~loc:p.pat_loc ity_equal_check ity ity_unit;
              unfold { p with pat_desc = Ptree.Pwild }
          | Ptree.Pwild ->
              let v = create_pvsymbol (id_fresh "result") ity in
              v, Loc.try3 ~loc type_fmla muc lvm old f
          | Ptree.Pvar id ->
              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 old f
          | _ -> mk_case loc pfl in
        unfold pat
    | _ -> mk_case loc pfl in
597 598
  List.map dpost ql

599
let dxpost muc ql lvm xsm old =
Andrei Paskevich's avatar
Andrei Paskevich committed
600
  let add_exn (q,pf) m =
601 602 603 604 605
    let xs = match q with
      | Qident i ->
          begin try Mstr.find i.id_str xsm with
          | Not_found -> find_xsymbol muc q end
      | _ -> find_xsymbol muc q in
606
    Mxs.change (fun l -> match pf, l with
Andrei Paskevich's avatar
Andrei Paskevich committed
607 608 609 610
      | Some pf, Some l -> Some (pf :: l)
      | Some pf, None   -> Some (pf :: [])
      | None,    None   -> Some []
      | None,    Some _ -> l) xs m in
611
  let mk_xpost loc xs pfl =
Andrei Paskevich's avatar
Andrei Paskevich committed
612
    if pfl = [] then [] else
613
    dpost muc [loc,pfl] lvm old xs.xs_ity in
614
  let exn_map (loc,xpfl) =
615 616
    let m = List.fold_right add_exn xpfl Mxs.empty in
    Mxs.mapi (fun xs pfl -> mk_xpost loc xs pfl) m in
617
  let add_map ql m =
618 619
    Mxs.union (fun _ l r -> Some (l @ r)) (exn_map ql) m in
  List.fold_right add_map ql Mxs.empty
620 621 622 623 624 625 626

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 =
627 628 629
  let old _ _ = Loc.errorm
    "`at' and `old' cannot be used in the `writes' clause" in
  let dwrites t = type_term muc lvm old t in
630 631 632 633 634 635
  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

636
let dvariant muc varl lvm _xsm old =
637
  let dvar t = type_term muc lvm old t in
638 639 640
  let dvar (t,q) = dvar t, Opt.map (find_variant_ls muc) q in
  List.map dvar varl

641
let dspec muc sp lvm xsm old ity = {
642 643
  ds_pre     = dpre muc sp.sp_pre lvm old;
  ds_post    = dpost muc sp.sp_post lvm old ity;
644
  ds_xpost   = dxpost muc sp.sp_xpost lvm xsm old;
645 646 647
  ds_reads   = dreads muc sp.sp_reads lvm;
  ds_writes  = dwrites muc sp.sp_writes lvm;
  ds_checkrw = sp.sp_checkrw;
648 649
  ds_diverge = sp.sp_diverge;
  ds_partial = sp.sp_partial; }
650

Andrei Paskevich's avatar
Andrei Paskevich committed
651 652 653 654 655
let dspec_no_variant muc sp = match sp.sp_variant with
  | ({term_loc = loc},_)::_ ->
      Loc.errorm ~loc "unexpected 'variant' clause"
  | _ -> dspec muc sp

656
let dassert muc f lvm _xsm old = type_fmla muc lvm old f
657

658
let dinvariant muc f lvm _xsm old = dpre muc f lvm old
659 660 661

(* abstract values *)

662 663
let dparam muc (_,id,gh,pty) =
  Opt.map create_user_id id, gh, dity_of_pty muc pty
664

665 666
let dbinder muc (_,id,gh,opt) =
  Opt.map create_user_id id, gh, dity_of_opt muc opt
667 668 669 670

(* expressions *)

let is_reusable de = match de.de_node with
671
  | DEvar _ | DEsym _ -> true | _ -> false
672 673 674 675 676 677 678 679

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)

680
let update_any kind e = match e.expr_desc with
681 682
  | Ptree.Eany (pl, _, pty, msk, sp) ->
      { e with expr_desc = Ptree.Eany (pl, kind, pty, msk, sp) }
683 684 685 686 687 688
  | _ -> e

let local_kind = function
  | RKfunc | RKpred -> RKlocal
  | k -> k

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
let rec eff_dterm muc denv {term_desc = desc; term_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 =
    let e = try DEsym (find_prog_symbol muc q) with
      | _ -> DEls_pure (find_lsymbol muc.muc_theory q, false) in
    expr_app loc e 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.Tident q ->
      qualid_app loc q []
  | Ptree.Tidapp (q, [e1]) ->
      qualid_app loc q [eff_dterm muc denv e1]
  | Ptree.Tapply (e1, e2) ->
      DEapp (eff_dterm muc denv e1, eff_dterm muc denv e2)
  | Ptree.Tscope (q, e1) ->
      let muc = open_scope muc "dummy" in
      let muc = import_scope muc (string_list_of_qualid q) in
Andrei Paskevich's avatar
Andrei Paskevich committed
716 717
      DEattr (eff_dterm muc denv e1, Sattr.empty)
  | Ptree.Tattr (ATpos uloc, e1) ->
718
      DEuloc (eff_dterm muc denv e1, uloc)
Andrei Paskevich's avatar
Andrei Paskevich committed
719 720
  | Ptree.Tattr (ATstr attr, e1) ->
      DEattr (eff_dterm muc denv e1, Sattr.singleton attr)
721 722 723 724 725
  | Ptree.Tcast (e1, pty) ->
      let d1 = eff_dterm muc denv e1 in
      DEcast (d1, dity_of_pty muc pty)
  | Ptree.Tat _ -> Loc.errorm ~loc "`at' and `old' cannot be used here"
  | Ptree.Tidapp _ | Ptree.Tconst _ | Ptree.Tinfix _ | Ptree.Tinnfix _
726
  | Ptree.Ttuple _ | Ptree.Tlet _ | Ptree.Tcase _ | Ptree.Tif _
727 728 729 730
  | Ptree.Ttrue | Ptree.Tfalse | Ptree.Tnot _ | Ptree.Tbinop _ | Ptree.Tbinnop _
  | Ptree.Tquant _ | Ptree.Trecord _ | Ptree.Tupdate _ ->
      Loc.errorm ~loc "unsupported effect expression")

731 732 733 734 735
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
736
  let qualid_app loc q el =
737
    let e = try DEsym (find_prog_symbol muc q) with
738
      | _ -> DEls_pure (find_lsymbol muc.muc_theory q, false) in
739
    expr_app loc e el
740 741 742 743 744 745 746 747
  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
748 749
  let qualid_app_pure loc q el =
    let e = match find_global_pv muc q with
750
      | Some v -> DEpv_pure v
751
      | None -> DEls_pure (find_lsymbol muc.muc_theory q, true) in
752 753 754 755 756 757 758 759 760
    expr_app loc e el
  in
  let qualid_app_pure loc q el = match q with
    | Qident {id_str = n} ->
        (match denv_get_pure_opt denv n with
        | Some d -> expr_app loc d el
        | None -> qualid_app_pure loc q el)
    | _ -> qualid_app_pure loc q el
  in
761 762 763 764 765 766
  let find_dxsymbol q = match q with
    | Qident {id_str = n} ->
        (try denv_get_exn denv n with _
        -> DEgexn (find_xsymbol muc q))
    | _ -> DEgexn (find_xsymbol muc q)
  in
767
  Dexpr.dexpr ~loc begin match desc with
768 769
  | Ptree.Eident q ->
      qualid_app loc q []
770 771
  | Ptree.Eidpur q ->
      qualid_app_pure loc q []
772 773 774 775 776
  | 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 ->
777
      let e = DEsym (RS (rs_tuple (List.length el))) in
778
      expr_app loc e (List.map (dexpr muc denv) el)
779 780 781
  | Ptree.Einfix (e1, op1, e23)
  | Ptree.Einnfix (e1, op1, e23) ->
      let apply loc de1 op de2 =
782 783
        if op.id_str = Ident.op_neq then
          let oq = Qident { op with id_str = Ident.op_equ } in
784 785 786 787 788 789 790
          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 chain n1 n2 loc de1 op1 = function
        | { expr_desc = Ptree.Einfix (e2, op2, e3); expr_loc = loc23 } ->
            let de2 = dexpr muc denv e2 in
791 792
            let re = is_reusable de2 in
            let v = if re then de2 else mk_var n1 de2 in
793 794 795
            let loc12 = loc_cutoff loc loc23 e2.expr_loc in
            let de12 = Dexpr.dexpr ~loc:loc12 (apply loc12 de1 op1 v) in