typing.ml 49.6 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
MARCHE Claude's avatar
MARCHE Claude committed
4
(*  Copyright 2010-2017   --   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 106
  find_qualid get_id_ps ns_find_prog_symbol ns p

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

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

111 112 113 114 115 116 117 118 119 120 121
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
122

123 124
(** Parsing types *)

125
let ty_of_pty tuc pty =
126
  let rec get_ty = function
127
    | PTtyvar {id_str = x} ->
128
        ty_var (tv_of_string x)
129
    | PTtyapp (q, tyl) ->
130
        let s = find_tysymbol tuc q in
131
        let tyl = List.map get_ty tyl in
132
        Loc.try2 ~loc:(qloc q) ty_app s tyl
133
    | PTtuple tyl ->
134 135
        let s = its_tuple (List.length tyl) in
        ty_app s.its_ts (List.map get_ty tyl)
136
    | PTarrow (ty1, ty2) ->
137
        ty_func (get_ty ty1) (get_ty ty2)
Andrei Paskevich's avatar
Andrei Paskevich committed
138
    | PTpure ty | PTparen ty ->
139 140 141 142
        get_ty ty
  in
  get_ty pty

143 144 145 146 147 148 149
let dty_of_pty tuc pty =
  Dterm.dty_of_ty (ty_of_pty tuc pty)

let dty_of_opt tuc = function
  | Some pty -> dty_of_pty tuc pty
  | None -> Dterm.dty_fresh ()

150 151 152 153 154 155 156
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
157
        Loc.try3 ~loc:(qloc q) ity_app s tyl []
158 159 160 161
    | PTtuple tyl ->
        ity_tuple (List.map get_ity tyl)
    | PTarrow (ty1, ty2) ->
        ity_func (get_ity ty1) (get_ity ty2)
Andrei Paskevich's avatar
Andrei Paskevich committed
162 163
    | PTpure ty ->
        ity_purify (get_ity ty)
164 165 166 167 168
    | PTparen ty ->
        get_ity ty
  in
  get_ity pty

169 170 171 172 173 174 175
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 ()

176
(** typing using destructive type variables
177

178 179 180 181 182 183
    parsed trees        intermediate trees       typed trees
      (Ptree)                (Dterm)               (Term)
   -----------------------------------------------------------
     ppure_type  ---dty--->   dty       ---ty--->    ty
      lexpr      --dterm-->   dterm     --term-->    term
*)
184

185 186
(** Typing patterns, terms, and formulas *)

187
let create_user_id {id_str = n; id_lab = label; id_loc = loc} =
188 189 190 191
  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
192

193 194
let parse_record ~loc tuc get_val fl =
  let fl = List.map (fun (q,e) -> find_lsymbol tuc q, e) fl in
Andrei Paskevich's avatar
Andrei Paskevich committed
195
  let cs,pjl,flm = Loc.try2 ~loc parse_record tuc.uc_known fl in
196 197 198
  let get_val pj = get_val cs pj (Mls.find_opt pj flm) in
  cs, List.map get_val pjl

199
let rec dpattern tuc { pat_desc = desc; pat_loc = loc } =
200
  Dterm.dpattern ~loc (match desc with
201
    | Ptree.Pwild -> DPwild
202 203
    | Ptree.Pvar (x, false) -> DPvar (create_user_id x)
    | Ptree.Papp (q, pl) ->
204 205
        let pl = List.map (dpattern tuc) pl in
        DPapp (find_lsymbol tuc q, pl)
206
    | Ptree.Ptuple pl ->
207
        let pl = List.map (dpattern tuc) pl in
208
        DPapp (fs_tuple (List.length pl), pl)
209
    | Ptree.Prec fl ->
210
        let get_val _ _ = function
211
          | Some p -> dpattern tuc p
212
          | None -> Dterm.dpattern DPwild in
213
        let cs,fl = parse_record ~loc tuc get_val fl in
214
        DPapp (cs,fl)
215
    | Ptree.Pas (p, x, false) -> DPas (dpattern tuc p, create_user_id x)
216
    | Ptree.Por (p, q) -> DPor (dpattern tuc p, dpattern tuc q)
217
    | Ptree.Pcast (p, ty) -> DPcast (dpattern tuc p, dty_of_pty tuc ty)
218 219
    | Ptree.Pvar (_, true) | Ptree.Pas (_, _, true) -> Loc.errorm ~loc
        "ghost variables are only allowed in programs")
220

221
let quant_var tuc (loc, id, gh, ty) =
222
  if gh then Loc.errorm ~loc "ghost variables are only allowed in programs";
223
  Opt.map create_user_id id, dty_of_opt tuc ty, Some loc
224

225 226 227 228 229 230
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))

231 232 233 234 235
let is_reusable dt = match dt.dt_node with
  | DTvar _ | DTgvar _ | DTconst _ | DTtrue | DTfalse -> true
  | DTapp (_,[]) -> true
  | _ -> false

Leon Gondelman's avatar
Leon Gondelman committed
236
let mk_var tuc n dt =
237 238 239
  let dty = match dt.dt_dty with
    | None -> dty_of_ty ty_bool
    | Some dty -> dty in
Leon Gondelman's avatar
Leon Gondelman committed
240
  Dterm.dterm tuc ?loc:dt.dt_loc (DTvar (n, dty))
241

Leon Gondelman's avatar
Leon Gondelman committed
242 243
let mk_let tuc ~loc n dt node =
  DTlet (dt, id_user n loc, Dterm.dterm tuc ~loc node)
244

Leon Gondelman's avatar
Leon Gondelman committed
245 246
let mk_closure tuc loc ls =
  let mk dt = Dterm.dterm tuc ~loc dt in
247
  let mk_v i _ =
248 249
    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
250
  let vl = Lists.mapi mk_v ls.ls_args in
Andrei Paskevich's avatar
Andrei Paskevich committed
251
  DTquant (DTlambda, vl, [], mk (DTapp (ls, List.map mk_t vl)))
252

253
let rec dterm tuc gvars at denv {term_desc = desc; term_loc = loc} =
254 255
  let func_app e el =
    List.fold_left (fun e1 (loc, e2) ->
Leon Gondelman's avatar
Leon Gondelman committed
256
      DTfapp (Dterm.dterm tuc ~loc e1, e2)) e el
257
  in
258 259 260
  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
Leon Gondelman's avatar
Leon Gondelman committed
261
    | _, [] -> func_app (mk_closure tuc loc ls) (List.rev_append al el)
262
  in
263
  let qualid_app q el = match gvars at q with
264
    | Some v -> func_app (DTgvar v.pv_vs) el
265
    | None ->
266
        let ls = find_lsymbol tuc q in
267
        apply_ls (qloc q) ls [] ls.ls_args el
268
  in
269
  let qualid_app q el = match q with
270
    | Qident {id_str = n} ->
271
        (match denv_get_opt denv n with
272 273 274 275
        | Some d -> func_app d el
        | None -> qualid_app q el)
    | _ -> qualid_app q el
  in
276
  let rec unfold_app e1 e2 el = match e1.term_desc with
277 278
    | Ptree.Tapply (e11,e12) ->
        let e12 = dterm tuc gvars at denv e12 in
279
        unfold_app e11 e12 ((e1.term_loc, e2)::el)
280
    | Ptree.Tident q ->
281
        qualid_app q ((e1.term_loc, e2)::el)
282
    | _ ->
283
        func_app (DTfapp (dterm tuc gvars at denv e1, e2)) el
284
  in
Leon Gondelman's avatar
Leon Gondelman committed
285
  Dterm.dterm tuc ~loc (match desc with
286
  | Ptree.Tident q ->
287
      qualid_app q []
288
  | Ptree.Tidapp (q, tl) ->
289
      let tl = List.map (dterm tuc gvars at denv) tl in
290
      DTapp (find_lsymbol tuc q, tl)
291
  | Ptree.Tapply (e1, e2) ->
292
      unfold_app e1 (dterm tuc gvars at denv e2) []
293
  | Ptree.Ttuple tl ->
294
      let tl = List.map (dterm tuc gvars at denv) tl in
295
      DTapp (fs_tuple (List.length tl), tl)
296 297 298 299 300 301
  | 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
          let ls = find_lsymbol tuc (Qident op) in
Leon Gondelman's avatar
Leon Gondelman committed
302
          DTnot (Dterm.dterm tuc ~loc (DTapp (ls, [de1;de2])))
303 304 305 306 307 308
        else
          DTapp (find_lsymbol tuc (Qident op), [de1;de2]) in
      let rec chain loc de1 op1 = function
        | { term_desc = Ptree.Tinfix (e2, op2, e3); term_loc = loc23 } ->
            let de2 = dterm tuc gvars at denv e2 in
            let loc12 = loc_cutoff loc loc23 e2.term_loc in
Leon Gondelman's avatar
Leon Gondelman committed
309 310
            let de12 = Dterm.dterm tuc ~loc:loc12 (apply loc12 de1 op1 de2) in
            let de23 = Dterm.dterm tuc ~loc:loc23 (chain loc23 de2 op2 e3) in
311
            DTbinop (DTand, de12, de23)
312 313 314
        | e23 ->
            apply loc de1 op1 (dterm tuc gvars at denv e23) in
      chain loc (dterm tuc gvars at denv e1) op1 e23
Clément Fumex's avatar
Clément Fumex committed
315
  | Ptree.Tconst (Number.ConstInt _ as c) ->
316
      DTconst (c, dty_int)
Clément Fumex's avatar
Clément Fumex committed
317
  | Ptree.Tconst (Number.ConstReal _ as c) ->
318
      DTconst (c, dty_real)
319
  | Ptree.Tlet (x, e1, e2) ->
320
      let id = create_user_id x in
321
      let e1 = dterm tuc gvars at denv e1 in
322
      let denv = denv_add_let denv e1 id in
323
      let e2 = dterm tuc gvars at denv e2 in
324
      DTlet (e1, id, e2)
325
  | Ptree.Tmatch (e1, bl) ->
326
      let e1 = dterm tuc gvars at denv e1 in
327
      let branch (p, e) =
328
        let p = dpattern tuc p in
329
        let denv = denv_add_pat denv p in
330
        p, dterm tuc gvars at denv e in
331
      DTcase (e1, List.map branch bl)
332
  | Ptree.Tif (e1, e2, e3) ->
333 334 335
      let e1 = dterm tuc gvars at denv e1 in
      let e2 = dterm tuc gvars at denv e2 in
      let e3 = dterm tuc gvars at denv e3 in
336
      DTif (e1, e2, e3)
337
  | Ptree.Ttrue ->
338
      DTtrue
339
  | Ptree.Tfalse ->
340
      DTfalse
Andrei Paskevich's avatar
Andrei Paskevich committed
341
  | Ptree.Tnot e1 ->
342
      DTnot (dterm tuc gvars at denv e1)
Andrei Paskevich's avatar
Andrei Paskevich committed
343 344 345 346 347 348
  | 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 } ->
            let de2 = dterm tuc gvars at denv e2 in
            let loc12 = loc_cutoff loc loc23 e2.term_loc in
Leon Gondelman's avatar
Leon Gondelman committed
349 350
            let de12 = Dterm.dterm tuc ~loc:loc12 (DTbinop (DTiff, de1, de2)) in
            let de23 = Dterm.dterm tuc ~loc:loc23 (chain loc23 de2 e3) in
Andrei Paskevich's avatar
Andrei Paskevich committed
351 352 353 354 355 356 357 358 359
            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 ->
            DTbinop (DTiff, de1, (dterm tuc gvars at denv e23)) in
      chain loc (dterm tuc gvars at denv e1) e23
  | Ptree.Tbinop (e1, op, e2)
  | Ptree.Tbinnop (e1, op, e2) ->
360 361
      let e1 = dterm tuc gvars at denv e1 in
      let e2 = dterm tuc gvars at denv e2 in
362
      DTbinop (op, e1, e2)
363
  | Ptree.Tquant (q, uqu, trl, e1) ->
364
      let qvl = List.map (quant_var tuc) uqu in
365
      let denv = denv_add_quant denv qvl in
366
      let dterm e = dterm tuc gvars at denv e in
367 368
      let trl = List.map (List.map dterm) trl in
      let e1 = dterm e1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
369
      DTquant (q, qvl, trl, e1)
370
  | Ptree.Trecord fl ->
371
      let get_val _cs pj = function
372
        | Some e -> dterm tuc gvars at denv e
373
        | None -> Loc.error ~loc (RecordFieldMissing pj) in
374
      let cs, fl = parse_record ~loc tuc get_val fl in
375
      DTapp (cs, fl)
376
  | Ptree.Tupdate (e1, fl) ->
377
      let e1 = dterm tuc gvars at denv e1 in
378
      let re = is_reusable e1 in
Leon Gondelman's avatar
Leon Gondelman committed
379
      let v = if re then e1 else mk_var tuc "q " e1 in
380
      let get_val _ pj = function
381
        | Some e -> dterm tuc gvars at denv e
Leon Gondelman's avatar
Leon Gondelman committed
382
        | None -> Dterm.dterm tuc ~loc (DTapp (pj,[v])) in
383
      let cs, fl = parse_record ~loc tuc get_val fl in
384
      let d = DTapp (cs, fl) in
Leon Gondelman's avatar
Leon Gondelman committed
385
      if re then d else mk_let tuc ~loc "q " e1 d
386 387
  | Ptree.Tat (e1, l) ->
      DTlabel (dterm tuc gvars (Some l.id_str) denv e1, Slab.empty)
Andrei Paskevich's avatar
M.()  
Andrei Paskevich committed
388 389 390 391
  | Ptree.Tscope (q, e1) ->
      let tuc = Theory.open_scope tuc "dummy" in
      let tuc = Theory.import_scope tuc (string_list_of_qualid q) in
      DTlabel (dterm tuc gvars at denv e1, Slab.empty)
392
  | Ptree.Tnamed (Lpos uloc, e1) ->
393
      DTuloc (dterm tuc gvars at denv e1, uloc)
394
  | Ptree.Tnamed (Lstr lab, e1) ->
395
      DTlabel (dterm tuc gvars at denv e1, Slab.singleton lab)
396
  | Ptree.Tcast ({term_desc = Ptree.Tconst c}, pty) ->
397
      DTconst (c, dty_of_pty tuc pty)
398 399
  | Ptree.Tcast (e1, pty) ->
      let d1 = dterm tuc gvars at denv e1 in
400
      DTcast (d1, dty_of_pty tuc pty))
401

402
(** typing program expressions *)
Andrei Paskevich's avatar
Andrei Paskevich committed
403

404 405 406 407 408
open Dexpr

(* records *)

let find_record_field muc q =
409 410
  let test rs = rs.rs_field <> None in
  find_special muc test "record field" q
411 412 413 414 415 416 417 418 419 420 421 422

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
423
    | [{pv_ity = {ity_node = (Ityreg {reg_its = s} | Ityapp (s,_,_))}}] -> s
424 425 426 427 428 429 430 431 432 433
    | _ -> 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
434
    Mrs.add_new (DuplicateRecordField (ls_of_rs pj)) pj v m
435 436 437 438 439 440 441 442 443 444 445
    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 *)

446 447 448 449 450 451
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

452 453 454
let rec dpattern muc { pat_desc = desc; pat_loc = loc } =
  Dexpr.dpattern ~loc (match desc with
    | Ptree.Pwild -> DPwild
455 456
    | Ptree.Pvar (x, gh) -> DPvar (create_user_id x, gh)
    | Ptree.Papp (q, pl) ->
457
        DPapp (find_constructor muc q, List.map (dpattern muc) pl)
458 459 460 461 462 463 464 465
    | 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)
466
    | Ptree.Pcast (p, pty) -> DPcast (dpattern muc p, dity_of_pty muc pty)
467
    | Ptree.Pas (p, x, gh) -> DPas (dpattern muc p, create_user_id x, gh)
468 469 470 471 472 473 474 475 476 477 478 479
    | 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

480 481 482 483 484 485 486 487
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
  let t = dterm muc.muc_theory gvars None Dterm.denv_empty t in
488
  Dterm.term ~strict:true ~keep_loc:true t
Andrei Paskevich's avatar
Andrei Paskevich committed
489

490 491 492
let type_fmla muc lvm old f =
  let gvars = mk_gvars muc lvm old in
  let f = dterm muc.muc_theory gvars None Dterm.denv_empty f in
493
  Dterm.fmla ~strict:true ~keep_loc:true f
Andrei Paskevich's avatar
Andrei Paskevich committed
494

495 496
let dpre muc pl lvm old =
  let dpre f = type_fmla muc lvm old f in
497 498
  List.map dpre pl

499
let dpost muc ql lvm old ity =
500 501 502
  let dpost (loc,pfl) = match pfl with
    | [{ pat_desc = Ptree.Pwild | Ptree.Ptuple [] }, f] ->
        let v = create_pvsymbol (id_fresh "result") ity in
503
        v, Loc.try3 ~loc type_fmla muc lvm old f
504
    | [{ pat_desc = Ptree.Pvar (id,false) }, f] ->
505 506
        let v = create_pvsymbol (create_user_id id) ity in
        let lvm = Mstr.add id.id_str v lvm in
507
        v, Loc.try3 ~loc type_fmla muc lvm old f
508 509 510 511 512 513
    | _ ->
        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
514
        v, Loc.try3 ~loc type_fmla muc lvm old f in
515 516
  List.map dpost ql

517
let dxpost muc ql lvm xsm old =
Andrei Paskevich's avatar
Andrei Paskevich committed
518
  let add_exn (q,pf) m =
519 520 521 522 523
    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
524
    Mxs.change (fun l -> match pf, l with
Andrei Paskevich's avatar
Andrei Paskevich committed
525 526 527 528
      | Some pf, Some l -> Some (pf :: l)
      | Some pf, None   -> Some (pf :: [])
      | None,    None   -> Some []
      | None,    Some _ -> l) xs m in
529
  let mk_xpost loc xs pfl =
Andrei Paskevich's avatar
Andrei Paskevich committed
530
    if pfl = [] then [] else
531
    dpost muc [loc,pfl] lvm old xs.xs_ity in
532
  let exn_map (loc,xpfl) =
533 534
    let m = List.fold_right add_exn xpfl Mxs.empty in
    Mxs.mapi (fun xs pfl -> mk_xpost loc xs pfl) m in
535
  let add_map ql m =
536 537
    Mxs.union (fun _ l r -> Some (l @ r)) (exn_map ql) m in
  List.fold_right add_map ql Mxs.empty
538 539 540 541 542 543 544

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 =
545 546 547
  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
548 549 550 551 552 553
  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

554
let dvariant muc varl lvm _xsm old =
555
  let dvar t = type_term muc lvm old t in
556 557 558
  let dvar (t,q) = dvar t, Opt.map (find_variant_ls muc) q in
  List.map dvar varl

559
let dspec muc sp lvm xsm old ity = {
560 561
  ds_pre     = dpre muc sp.sp_pre lvm old;
  ds_post    = dpost muc sp.sp_post lvm old ity;
562
  ds_xpost   = dxpost muc sp.sp_xpost lvm xsm old;
563 564 565 566 567
  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; }

568
let dassert muc f lvm _xsm old = type_fmla muc lvm old f
569

570
let dinvariant muc f lvm _xsm old = dpre muc f lvm old
571 572 573

(* abstract values *)

574 575
let dparam muc (_,id,gh,pty) =
  Opt.map create_user_id id, gh, dity_of_pty muc pty
576

577 578
let dbinder muc (_,id,gh,opt) =
  Opt.map create_user_id id, gh, dity_of_opt muc opt
579 580 581 582

(* expressions *)

let is_reusable de = match de.de_node with
583
  | DEvar _ | DEsym _ -> true | _ -> false
584 585 586 587 588 589 590 591

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)

592
let update_any kind e = match e.expr_desc with
593 594
  | Ptree.Eany (pl, _, pty, msk, sp) ->
      { e with expr_desc = Ptree.Eany (pl, kind, pty, msk, sp) }
595 596 597 598 599 600
  | _ -> e

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

601 602 603 604 605
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
606
  let qualid_app loc q el =
607
    let e = try DEsym (find_prog_symbol muc q) with
608
      | _ -> DEls_pure (find_lsymbol muc.muc_theory q, false) in
609
    expr_app loc e el
610 611 612 613 614 615 616 617
  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
618 619
  let qualid_app_pure loc q el =
    let e = match find_global_pv muc q with
620
      | Some v -> DEpv_pure v
621
      | None -> DEls_pure (find_lsymbol muc.muc_theory q, true) in
622 623 624 625 626 627 628 629 630
    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
631 632 633 634 635 636
  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
637
  Dexpr.dexpr ~loc begin match desc with
638 639
  | Ptree.Eident q ->
      qualid_app loc q []
640 641
  | Ptree.Eidpur q ->
      qualid_app_pure loc q []
642 643 644 645 646
  | 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 ->
647
      let e = DEsym (RS (rs_tuple (List.length el))) in
648
      expr_app loc e (List.map (dexpr muc denv) el)
649 650 651 652 653 654 655 656 657 658 659 660
  | 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
661 662
            let re = is_reusable de2 in
            let v = if re then de2 else mk_var n1 de2 in
663 664 665
            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
666 667
            let d = DEand (de12, de23) in
            if re then d else mk_let ~loc n1 de2 d
668 669 670
        | e23 ->
            apply loc de1 op1 (dexpr muc denv e23) in
      chain "q1 " "q2 " loc (dexpr muc denv e1) op1 e23
671 672
  | Ptree.Econst (Number.ConstInt _ as c) -> DEconst(c, dity_int)
  | Ptree.Econst (Number.ConstReal _ as c) -> DEconst(c, dity_real)
673 674 675
  | Ptree.Erecord fl ->
      let ls_of_rs rs = match rs.rs_logic with
        | RLls ls -> ls | _ -> assert false in
676 677
      let get_val _cs pj = function
        | None -> Loc.error ~loc (Decl.RecordFieldMissing (ls_of_rs pj))
678 679
        | Some e -> dexpr muc denv e in
      let cs,fl = parse_record ~loc muc get_val fl in
680
      expr_app loc (DEsym (RS cs)) fl
681 682 683
  | Ptree.Eupdate (e1, fl) ->
      let e1 = dexpr muc denv e1 in
      let re = is_reusable e1 in
684
      let v = if re then e1 else mk_var "q " e1 in
685 686
      let get_val _ pj = function
        | None ->
687
            let pj = Dexpr.dexpr ~loc (DEsym (RS pj)) in
688 689 690
            Dexpr.dexpr ~loc (DEapp (pj, v))
        | Some e -> dexpr muc denv e in
      let cs,fl = parse_record ~loc muc get_val fl in
691
      let d = expr_app loc (DEsym (RS cs)) fl in
692
      if re then d else mk_let ~loc "q " e1 d
693
  | Ptree.Elet (id, gh, kind, e1, e2) ->
694 695
      let e1 = update_any kind e1 in
      let kind = local_kind kind in
696 697 698
      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) ->
699 700
      let update_kind (id, gh, k, bl, pty, msk, sp, e) =
        id, gh, local_kind k, bl, pty, msk, sp, e in
701
      let fdl = List.map update_kind fdl in
702 703
      let denv, rd = drec_defn muc denv fdl in
      DErec (rd, dexpr muc denv e1)
704
  | Ptree.Efun (bl, pty, msk, sp, e) ->
705 706 707 708 709
      let bl = List.map (dbinder muc) bl in
      let ds = match sp.sp_variant with
        | ({term_loc = loc},_)::_ ->
            Loc.errorm ~loc "unexpected 'variant' clause"
        | _ -> dspec muc sp in
710
      let dity = dity_of_opt muc pty in
711
      let denv = denv_add_args denv bl in
712 713
      let denv = if bl = [] then denv else
        denv_add_exn denv old_mark_id dity in
714
      DEfun (bl, dity, msk, ds, dexpr muc denv e)
715
  | Ptree.Eany (pl, kind, pty, msk, sp) ->
716 717 718 719 720
      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
721 722 723 724 725
      let ity = match kind, pty with
        | _, Some pty -> ity_of_pty muc pty
        | RKlemma, None -> ity_unit
        | RKpred, None -> ity_bool
        | _ -> Loc.errorm ~loc "cannot determine the type of the result" in
726
      DEany (pl, dity_of_ity ity, msk, ds)
727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747
  | 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) ->
748
      let e1 = { e1 with expr_desc = Ecast (e1, PTtuple []) } in
749 750 751 752 753 754 755 756 757 758 759 760 761 762
      let e1 = dexpr muc denv e1 in
      let e2 = dexpr muc denv e2 in
      DElet ((id_user "_" loc, false, RKnone, e1), e2)
  | 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
763
      let denv = denv_add_for_index denv id efrom.de_dvty in
764
      DEfor (id, efrom, dir, eto, inv, dexpr muc denv e1)
765 766 767 768
  | Ptree.Eassign asl ->
      let mk_assign (e1,q,e2) =
        dexpr muc denv e1, find_record_field muc q, dexpr muc denv e2 in
      DEassign (List.map mk_assign asl)
769
  | Ptree.Eraise (q, e1) ->