typing.ml 53.6 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 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
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
79 80 81 82
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
83
  match (Mid.find pr.pr_name tuc.uc_known).d_node with
84
  | Dind _ when k = Paxiom -> pr
85 86 87
  | Dprop (l,_,_) when l = k -> pr
  | _ -> Loc.errorm ~loc:(qloc q) "proposition %a is not %s"
      print_qualid q (match k with
88
        | Plemma -> "a lemma" | Paxiom -> "an axiom" | Pgoal -> "a goal")
89

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

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

96 97 98
let find_prog_symbol_ns ns p =
  let get_id_ps = function
    | PV pv -> pv.pv_vs.vs_name
99 100 101 102
    | 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
103 104 105
  find_qualid get_id_ps ns_find_prog_symbol ns p


106 107
(** Parsing types *)

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

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 *)

144
let create_user_id {id_str = n; id_lab = label; id_loc = loc} =
145 146 147 148
  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
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
  Dterm.dpattern ~loc (match desc with
158
    | Ptree.Pwild -> DPwild
159 160
    | Ptree.Pvar (x, false) -> DPvar (create_user_id x)
    | Ptree.Papp (q, pl) ->
161 162
        let pl = List.map (dpattern ns km) pl in
        DPapp (find_lsymbol_ns ns q, pl)
163
    | Ptree.Ptuple pl ->
164
        let pl = List.map (dpattern ns km) pl in
165
        DPapp (fs_tuple (List.length pl), pl)
166
    | Ptree.Prec fl ->
167
        let get_val _ _ = function
168
          | Some p -> dpattern ns km p
169
          | None -> Dterm.dpattern DPwild in
170
        let cs,fl = parse_record ~loc ns km get_val fl in
171
        DPapp (cs,fl)
172
    | Ptree.Pas (p, x, false) -> DPas (dpattern ns km p, create_user_id x)
173
    | Ptree.Por (p, q) -> DPor (dpattern ns km p, dpattern ns km q)
174
    | Ptree.Pcast (p, ty) -> DPcast (dpattern ns km p, dty_of_pty ns ty)
175 176
    | Ptree.Pvar (_, true) | Ptree.Pas (_, _, true) -> Loc.errorm ~loc
        "ghost variables are only allowed in programs")
177

178
let quant_var ns (loc, id, gh, ty) =
179
  if gh then Loc.errorm ~loc "ghost variables are only allowed in programs";
180
  Opt.map create_user_id id, dty_of_opt ns ty, Some loc
181

182 183 184 185 186 187
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))

188 189 190 191 192
let is_reusable dt = match dt.dt_node with
  | DTvar _ | DTgvar _ | DTconst _ | DTtrue | DTfalse -> true
  | DTapp (_,[]) -> true
  | _ -> false

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

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

202 203
let mk_closure crcmap loc ls =
  let mk dt = Dterm.dterm crcmap ~loc dt in
204
  let mk_v i _ =
205 206
    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
207
  let vl = Lists.mapi mk_v ls.ls_args in
Andrei Paskevich's avatar
Andrei Paskevich committed
208
  DTquant (DTlambda, vl, [], mk (DTapp (ls, List.map mk_t vl)))
209

210
let rec dterm ns km crcmap gvars at denv {term_desc = desc; term_loc = loc} =
211 212
  let func_app e el =
    List.fold_left (fun e1 (loc, e2) ->
213
      DTfapp (Dterm.dterm crcmap ~loc e1, e2)) e el
214
  in
215 216 217
  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
218
    | _, [] -> func_app (mk_closure crcmap loc ls) (List.rev_append al el)
219
  in
220
  let qualid_app q el = match gvars at q with
221
    | Some v -> func_app (DTgvar v.pv_vs) el
222
    | None ->
223
        let ls = find_lsymbol_ns ns q in
224
        apply_ls (qloc q) ls [] ls.ls_args el
225
  in
226
  let qualid_app q el = match q with
227
    | Qident {id_str = n} ->
228
        (match denv_get_opt denv n with
229 230 231 232
        | Some d -> func_app d el
        | None -> qualid_app q el)
    | _ -> qualid_app q el
  in
233
  let rec unfold_app e1 e2 el = match e1.term_desc with
234
    | Ptree.Tapply (e11,e12) ->
235
        let e12 = dterm ns km crcmap gvars at denv e12 in
236
        unfold_app e11 e12 ((e1.term_loc, e2)::el)
237
    | Ptree.Tident q ->
238
        qualid_app q ((e1.term_loc, e2)::el)
239
    | _ ->
240
        func_app (DTfapp (dterm ns km crcmap gvars at denv e1, e2)) el
241
  in
242
  Dterm.dterm crcmap ~loc (match desc with
243
  | Ptree.Tident q ->
244
      qualid_app q []
245
  | Ptree.Tidapp (q, tl) ->
246
      let tl = List.map (dterm ns km crcmap gvars at denv) tl in
247
      DTapp (find_lsymbol_ns ns q, tl)
248
  | Ptree.Tapply (e1, e2) ->
249
      unfold_app e1 (dterm ns km crcmap gvars at denv e2) []
250
  | Ptree.Ttuple tl ->
251
      let tl = List.map (dterm ns km crcmap gvars at denv) tl in
252
      DTapp (fs_tuple (List.length tl), tl)
253 254 255 256 257
  | Ptree.Tinfix (e1, op1, e23)
  | Ptree.Tinnfix (e1, op1, e23) ->
      let apply loc de1 op de2 =
        if op.id_str = "infix <>" then
          let op = { op with id_str = "infix =" } in
258 259
          let ls = find_lsymbol_ns ns (Qident op) in
          DTnot (Dterm.dterm crcmap ~loc (DTapp (ls, [de1;de2])))
260
        else
261
          DTapp (find_lsymbol_ns ns (Qident op), [de1;de2]) in
262 263
      let rec chain loc de1 op1 = function
        | { term_desc = Ptree.Tinfix (e2, op2, e3); term_loc = loc23 } ->
264
            let de2 = dterm ns km crcmap gvars at denv e2 in
265
            let loc12 = loc_cutoff loc loc23 e2.term_loc in
266 267
            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
268
            DTbinop (DTand, de12, de23)
269
        | e23 ->
270 271
            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
272
  | Ptree.Tconst (Number.ConstInt _ as c) ->
273
      DTconst (c, dty_int)
Clément Fumex's avatar
Clément Fumex committed
274
  | Ptree.Tconst (Number.ConstReal _ as c) ->
275
      DTconst (c, dty_real)
276
  | Ptree.Tlet (x, e1, e2) ->
277
      let id = create_user_id x in
278
      let e1 = dterm ns km crcmap gvars at denv e1 in
279
      let denv = denv_add_let denv e1 id in
280
      let e2 = dterm ns km crcmap gvars at denv e2 in
281
      DTlet (e1, id, e2)
282
  | Ptree.Tmatch (e1, bl) ->
283
      let e1 = dterm ns km crcmap gvars at denv e1 in
284
      let branch (p, e) =
285
        let p = dpattern ns km p in
286
        let denv = denv_add_pat denv p in
287
        p, dterm ns km crcmap gvars at denv e in
288
      DTcase (e1, List.map branch bl)
289
  | Ptree.Tif (e1, e2, e3) ->
290 291 292
      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
293
      DTif (e1, e2, e3)
294
  | Ptree.Ttrue ->
295
      DTtrue
296
  | Ptree.Tfalse ->
297
      DTfalse
Andrei Paskevich's avatar
Andrei Paskevich committed
298
  | Ptree.Tnot e1 ->
299
      DTnot (dterm ns km crcmap gvars at denv e1)
Andrei Paskevich's avatar
Andrei Paskevich committed
300 301 302 303
  | 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 } ->
304
            let de2 = dterm ns km crcmap gvars at denv e2 in
Andrei Paskevich's avatar
Andrei Paskevich committed
305
            let loc12 = loc_cutoff loc loc23 e2.term_loc in
306 307
            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
308 309 310 311 312
            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 ->
313 314
            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
315 316
  | Ptree.Tbinop (e1, op, e2)
  | Ptree.Tbinnop (e1, op, e2) ->
317 318
      let e1 = dterm ns km crcmap gvars at denv e1 in
      let e2 = dterm ns km crcmap gvars at denv e2 in
319
      DTbinop (op, e1, e2)
320
  | Ptree.Tquant (q, uqu, trl, e1) ->
321
      let qvl = List.map (quant_var ns) uqu in
322
      let denv = denv_add_quant denv qvl in
323
      let dterm e = dterm ns km crcmap gvars at denv e in
324 325
      let trl = List.map (List.map dterm) trl in
      let e1 = dterm e1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
326
      DTquant (q, qvl, trl, e1)
327
  | Ptree.Trecord fl ->
328
      let get_val _cs pj = function
329
        | Some e -> dterm ns km crcmap gvars at denv e
330
        | None -> Loc.error ~loc (RecordFieldMissing pj) in
331
      let cs, fl = parse_record ~loc ns km get_val fl in
332
      DTapp (cs, fl)
333
  | Ptree.Tupdate (e1, fl) ->
334
      let e1 = dterm ns km crcmap gvars at denv e1 in
335
      let re = is_reusable e1 in
336
      let v = if re then e1 else mk_var crcmap "q " e1 in
337
      let get_val _ pj = function
338 339
        | Some e -> dterm ns km crcmap gvars at denv e
        | None -> Dterm.dterm crcmap ~loc (DTapp (pj,[v])) in
340
      let cs, fl = parse_record ~loc ns km get_val fl in
341
      let d = DTapp (cs, fl) in
342
      if re then d else mk_let crcmap ~loc "q " e1 d
343
  | Ptree.Tat (e1, l) ->
344
      DTlabel (dterm ns km crcmap gvars (Some l.id_str) denv e1, Slab.empty)
Andrei Paskevich's avatar
M.()  
Andrei Paskevich committed
345
  | Ptree.Tscope (q, e1) ->
346 347
      let ns = import_namespace ns (string_list_of_qualid q) in
      DTlabel (dterm ns km crcmap gvars at denv e1, Slab.empty)
348
  | Ptree.Tnamed (Lpos uloc, e1) ->
349
      DTuloc (dterm ns km crcmap gvars at denv e1, uloc)
350
  | Ptree.Tnamed (Lstr lab, e1) ->
351
      DTlabel (dterm ns km crcmap gvars at denv e1, Slab.singleton lab)
352
  | Ptree.Tcast ({term_desc = Ptree.Tconst c}, pty) ->
353
      DTconst (c, dty_of_pty ns pty)
354
  | Ptree.Tcast (e1, pty) ->
355 356
      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
357

358

359 360 361 362 363 364 365 366
type global_vars = string option -> Ptree.qualid -> Ity.pvsymbol option

let type_term_in_namespace ns km crcmap gvars t =
  let t = dterm ns km crcmap gvars None Dterm.denv_empty t in
  Dterm.term ~strict:true ~keep_loc:true t

let type_fmla_in_namespace ns km crcmap gvars f =
  let f = dterm ns km crcmap gvars None Dterm.denv_empty f in
367
  Dterm.fmla ~strict:true ~keep_loc:true f
Andrei Paskevich's avatar
Andrei Paskevich committed
368

369

370
(** typing program expressions *)
Andrei Paskevich's avatar
Andrei Paskevich committed
371

372 373
open Dexpr

374
let ty_of_pty tuc = ty_of_pty (get_namespace tuc)
375

376
let get_namespace muc = List.hd muc.Pmodule.muc_import
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
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

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_ns (get_namespace muc) q in
        let tyl = List.map get_ity tyl in
        Loc.try3 ~loc:(qloc q) ity_app s tyl []
    | PTtuple tyl ->
        ity_tuple (List.map get_ity tyl)
    | PTarrow (ty1, ty2) ->
        ity_func (get_ity ty1) (get_ity ty2)
    | PTpure ty ->
        ity_purify (get_ity ty)
    | PTparen ty ->
        get_ity ty
  in
  get_ity pty


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 ()

426 427 428
(* records *)

let find_record_field muc q =
429 430
  let test rs = rs.rs_field <> None in
  find_special muc test "record field" q
431 432 433 434 435 436 437 438 439 440 441 442

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
443
    | [{pv_ity = {ity_node = (Ityreg {reg_its = s} | Ityapp (s,_,_))}}] -> s
444 445 446 447 448 449 450 451 452 453
    | _ -> 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
454
    Mrs.add_new (DuplicateRecordField (ls_of_rs pj)) pj v m
455 456 457 458 459 460 461 462 463 464 465
    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 *)

466 467 468 469 470 471
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

472 473 474
let rec dpattern muc { pat_desc = desc; pat_loc = loc } =
  Dexpr.dpattern ~loc (match desc with
    | Ptree.Pwild -> DPwild
475 476
    | Ptree.Pvar (x, gh) -> DPvar (create_user_id x, gh)
    | Ptree.Papp (q, pl) ->
477
        DPapp (find_constructor muc q, List.map (dpattern muc) pl)
478 479 480 481 482 483 484 485
    | 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)
486
    | Ptree.Pcast (p, pty) -> DPcast (dpattern muc p, dity_of_pty muc pty)
487
    | Ptree.Pas (p, x, gh) -> DPas (dpattern muc p, create_user_id x, gh)
488 489
    | Ptree.Por (p, q) -> DPor (dpattern muc p, dpattern muc q))

490

491 492 493 494 495 496 497 498 499 500
(* 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

501 502 503 504 505 506 507
let mk_gvars muc lvm old = fun at q ->
  match find_local_pv muc lvm q, at with
  | Some v, Some l -> Some (old v l)
  | v, _ -> v

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

511 512
let type_fmla muc lvm old f =
  let gvars = mk_gvars muc lvm old in
513
  let f = dterm muc gvars None Dterm.denv_empty f in
514
  Dterm.fmla ~strict:true ~keep_loc:true f
Andrei Paskevich's avatar
Andrei Paskevich committed
515

516 517
let dpre muc pl lvm old =
  let dpre f = type_fmla muc lvm old f in
518 519
  List.map dpre pl

520
let dpost muc ql lvm old ity =
521 522 523
  let dpost (loc,pfl) = match pfl with
    | [{ pat_desc = Ptree.Pwild | Ptree.Ptuple [] }, f] ->
        let v = create_pvsymbol (id_fresh "result") ity in
524
        v, Loc.try3 ~loc type_fmla muc lvm old f
525
    | [{ pat_desc = Ptree.Pvar (id,false) }, f] ->
526 527
        let v = create_pvsymbol (create_user_id id) ity in
        let lvm = Mstr.add id.id_str v lvm in
528
        v, Loc.try3 ~loc type_fmla muc lvm old f
529 530 531 532 533 534
    | _ ->
        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
535
        v, Loc.try3 ~loc type_fmla muc lvm old f in
536 537
  List.map dpost ql

538
let dxpost muc ql lvm xsm old =
Andrei Paskevich's avatar
Andrei Paskevich committed
539
  let add_exn (q,pf) m =
540 541 542 543 544
    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
545
    Mxs.change (fun l -> match pf, l with
Andrei Paskevich's avatar
Andrei Paskevich committed
546 547 548 549
      | Some pf, Some l -> Some (pf :: l)
      | Some pf, None   -> Some (pf :: [])
      | None,    None   -> Some []
      | None,    Some _ -> l) xs m in
550
  let mk_xpost loc xs pfl =
Andrei Paskevich's avatar
Andrei Paskevich committed
551
    if pfl = [] then [] else
552
    dpost muc [loc,pfl] lvm old xs.xs_ity in
553
  let exn_map (loc,xpfl) =
554 555
    let m = List.fold_right add_exn xpfl Mxs.empty in
    Mxs.mapi (fun xs pfl -> mk_xpost loc xs pfl) m in
556
  let add_map ql m =
557 558
    Mxs.union (fun _ l r -> Some (l @ r)) (exn_map ql) m in
  List.fold_right add_map ql Mxs.empty
559 560 561 562 563 564 565

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 =
566 567 568
  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
569 570 571 572 573 574
  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

575
let dvariant muc varl lvm _xsm old =
576
  let dvar t = type_term muc lvm old t in
577 578 579
  let dvar (t,q) = dvar t, Opt.map (find_variant_ls muc) q in
  List.map dvar varl

580
let dspec muc sp lvm xsm old ity = {
581 582
  ds_pre     = dpre muc sp.sp_pre lvm old;
  ds_post    = dpost muc sp.sp_post lvm old ity;
583
  ds_xpost   = dxpost muc sp.sp_xpost lvm xsm old;
584 585 586 587 588
  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; }

Andrei Paskevich's avatar
Andrei Paskevich committed
589 590 591 592 593
let dspec_no_variant muc sp = match sp.sp_variant with
  | ({term_loc = loc},_)::_ ->
      Loc.errorm ~loc "unexpected 'variant' clause"
  | _ -> dspec muc sp

594
let dassert muc f lvm _xsm old = type_fmla muc lvm old f
595

596
let dinvariant muc f lvm _xsm old = dpre muc f lvm old
597 598 599

(* abstract values *)

600 601
let dparam muc (_,id,gh,pty) =
  Opt.map create_user_id id, gh, dity_of_pty muc pty
602

603 604
let dbinder muc (_,id,gh,opt) =
  Opt.map create_user_id id, gh, dity_of_opt muc opt
605 606 607 608

(* expressions *)

let is_reusable de = match de.de_node with
609
  | DEvar _ | DEsym _ -> true | _ -> false
610 611 612 613 614 615 616 617

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)

618
let update_any kind e = match e.expr_desc with
619 620
  | Ptree.Eany (pl, _, pty, msk, sp) ->
      { e with expr_desc = Ptree.Eany (pl, kind, pty, msk, sp) }
621 622 623 624 625 626
  | _ -> e

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

627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668
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
      DElabel (eff_dterm muc denv e1, Slab.empty)
  | Ptree.Tnamed (Lpos uloc, e1) ->
      DEuloc (eff_dterm muc denv e1, uloc)
  | Ptree.Tnamed (Lstr lab, e1) ->
      DElabel (eff_dterm muc denv e1, Slab.singleton lab)
  | 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 _
  | Ptree.Ttuple _ | Ptree.Tlet _ | Ptree.Tmatch _ | Ptree.Tif _
  | Ptree.Ttrue | Ptree.Tfalse | Ptree.Tnot _ | Ptree.Tbinop _ | Ptree.Tbinnop _
  | Ptree.Tquant _ | Ptree.Trecord _ | Ptree.Tupdate _ ->
      Loc.errorm ~loc "unsupported effect expression")

669 670 671 672 673
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
674
  let qualid_app loc q el =
675
    let e = try DEsym (find_prog_symbol muc q) with
676
      | _ -> DEls_pure (find_lsymbol muc.muc_theory q, false) in
677
    expr_app loc e el
678 679 680 681 682 683 684 685
  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
686 687
  let qualid_app_pure loc q el =
    let e = match find_global_pv muc q with
688
      | Some v -> DEpv_pure v
689
      | None -> DEls_pure (find_lsymbol muc.muc_theory q, true) in
690 691 692 693 694 695 696 697 698
    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
699 700 701 702 703 704
  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
705
  Dexpr.dexpr ~loc begin match desc with
706 707
  | Ptree.Eident q ->
      qualid_app loc q []
708 709
  | Ptree.Eidpur q ->
      qualid_app_pure loc q []
710 711 712 713 714
  | 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 ->
715
      let e = DEsym (RS (rs_tuple (List.length el))) in
716
      expr_app loc e (List.map (dexpr muc denv) el)
717 718 719 720 721 722 723 724 725 726 727 728
  | Ptree.Einfix (e1, op1, e23)
  | Ptree.Einnfix (e1, op1, e23) ->
      let apply loc 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 chain n1 n2 loc de1 op1 = function
        | { expr_desc = Ptree.Einfix (e2, op2, e3); expr_loc = loc23 } ->
            let de2 = dexpr muc denv e2 in
729 730
            let re = is_reusable de2 in
            let v = if re then de2 else mk_var n1 de2 in
731 732 733
            let loc12 = loc_cutoff loc loc23 e2.expr_loc in
            let de12 = Dexpr.dexpr ~loc:loc12 (apply loc12 de1 op1 v) in
            let de23 = Dexpr.dexpr ~loc:loc23 (chain n2 n1 loc23 v op2 e3) in
734 735
            let d = DEand (de12, de23) in
            if re then d else mk_let ~loc n1 de2 d
736 737 738
        | e23 ->
            apply loc de1 op1 (dexpr muc denv e23) in
      chain "q1 " "q2 " loc (dexpr muc denv e1) op1 e23
739 740 741 742 743 744 745 746
  | Ptree.Econst (Number.ConstInt _ as c) ->
      let dty = if Mts.is_empty muc.muc_theory.uc_ranges
                then dity_int else dity_fresh () in
      DEconst(c, dty)
  | Ptree.Econst (Number.ConstReal _ as c) ->
      let dty = if Mts.is_empty muc.muc_theory.uc_floats
                then dity_real else dity_fresh () in
      DEconst(c, dty)
747 748 749
  | Ptree.Erecord fl ->
      let ls_of_rs rs = match rs.rs_logic with
        | RLls ls -> ls | _ -> assert false in
750 751
      let get_val _cs pj = function
        | None -> Loc.error ~loc (Decl.RecordFieldMissing (ls_of_rs pj))
752 753
        | Some e -> dexpr muc denv e in
      let cs,fl = parse_record ~loc muc get_val fl in
754
      expr_app loc (DEsym (RS cs)) fl
755 756 757
  | Ptree.Eupdate (e1, fl) ->
      let e1 = dexpr muc denv e1 in
      let re = is_reusable e1 in
758
      let v = if re then e1 else mk_var "q " e1 in
759 760
      let get_val _ pj = function
        | None ->
761
            let pj = Dexpr.dexpr ~loc (DEsym (RS pj)) in
762 763 764
            Dexpr.dexpr ~loc (DEapp (pj, v))
        | Some e -> dexpr muc denv e in
      let cs,fl = parse_record ~loc muc get_val fl in
765
      let d = expr_app loc (DEsym (RS cs)) fl in
766
      if re then d else mk_let ~loc "q " e1 d
767
  | Ptree.Elet (id, gh, kind, e1, e2) ->
768 769
      let e1 = update_any kind e1 in
      let kind = local_kind kind in
770 771 772
      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) ->
773 774
      let update_kind (id, gh, k, bl, pty, msk, sp, e) =
        id, gh, local_kind k, bl, pty, msk, sp, e in