typing.ml 49.2 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
let find_rsymbol muc q = match find_prog_symbol muc q with RS rs -> rs
  | _ -> Loc.errorm ~loc:(qloc q) "program symbol expected"

114
115
(** Parsing types *)

116
let ty_of_pty tuc pty =
117
  let rec get_ty = function
118
    | PTtyvar {id_str = x} ->
119
        ty_var (tv_of_string x)
120
    | PTtyapp (q, tyl) ->
121
        let s = find_tysymbol tuc q in
122
        let tyl = List.map get_ty tyl in
123
        Loc.try2 ~loc:(qloc q) ty_app s tyl
124
    | PTtuple tyl ->
125
126
        let s = its_tuple (List.length tyl) in
        ty_app s.its_ts (List.map get_ty tyl)
127
    | PTarrow (ty1, ty2) ->
128
        ty_func (get_ty ty1) (get_ty ty2)
Andrei Paskevich's avatar
Andrei Paskevich committed
129
    | PTpure ty | PTparen ty ->
130
131
132
133
        get_ty ty
  in
  get_ty pty

134
135
136
137
138
139
140
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 ()

141
142
143
144
145
146
147
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
148
        Loc.try3 ~loc:(qloc q) ity_app s tyl []
149
150
151
152
    | 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
153
154
    | PTpure ty ->
        ity_purify (get_ity ty)
155
156
157
158
159
    | PTparen ty ->
        get_ity ty
  in
  get_ity pty

160
161
162
163
164
165
166
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 ()

167
(** typing using destructive type variables
168

169
170
171
172
173
174
    parsed trees        intermediate trees       typed trees
      (Ptree)                (Dterm)               (Term)
   -----------------------------------------------------------
     ppure_type  ---dty--->   dty       ---ty--->    ty
      lexpr      --dterm-->   dterm     --term-->    term
*)
175

176
177
(** Typing patterns, terms, and formulas *)

178
let create_user_id {id_str = n; id_lab = label; id_loc = loc} =
179
180
181
182
  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
183

184
185
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
186
  let cs,pjl,flm = Loc.try2 ~loc parse_record tuc.uc_known fl in
187
188
189
  let get_val pj = get_val cs pj (Mls.find_opt pj flm) in
  cs, List.map get_val pjl

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

212
let quant_var tuc (loc, id, gh, ty) =
213
  if gh then Loc.errorm ~loc "ghost variables are only allowed in programs";
214
  Opt.map create_user_id id, dty_of_opt tuc ty, Some loc
215

216
217
218
219
220
221
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))

222
223
224
225
226
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
227
let mk_var tuc n dt =
228
229
230
  let dty = match dt.dt_dty with
    | None -> dty_of_ty ty_bool
    | Some dty -> dty in
Leon Gondelman's avatar
Leon Gondelman committed
231
  Dterm.dterm tuc ?loc:dt.dt_loc (DTvar (n, dty))
232

Leon Gondelman's avatar
Leon Gondelman committed
233
234
let mk_let tuc ~loc n dt node =
  DTlet (dt, id_user n loc, Dterm.dterm tuc ~loc node)
235

Leon Gondelman's avatar
Leon Gondelman committed
236
237
let mk_closure tuc loc ls =
  let mk dt = Dterm.dterm tuc ~loc dt in
238
  let mk_v i _ =
239
240
    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
241
  let vl = Lists.mapi mk_v ls.ls_args in
Andrei Paskevich's avatar
Andrei Paskevich committed
242
  DTquant (DTlambda, vl, [], mk (DTapp (ls, List.map mk_t vl)))
243

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

393
(** typing program expressions *)
Andrei Paskevich's avatar
Andrei Paskevich committed
394

395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
open Dexpr

(* records *)

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

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

let parse_record muc fll =
  (* we assume that every rsymbol in fll was resolved
     using find_record_field, so they are all fields *)
  let ls_of_rs rs = match rs.rs_logic with
    | RLls ls -> ls | _ -> assert false in
  let rs = match fll with
    | (rs, _)::_ -> rs
    | [] -> raise EmptyRecord in
  let its = match rs.rs_cty.cty_args with
414
    | [{pv_ity = {ity_node = (Ityreg {reg_its = s} | Ityapp (s,_,_))}}] -> s
415
416
417
418
419
420
421
422
423
424
    | _ -> 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
425
    Mrs.add_new (DuplicateRecordField (ls_of_rs pj)) pj v m
426
427
428
429
430
431
432
433
434
435
436
437
438
439
    else raise (BadRecordField (ls_of_rs pj))) Mrs.empty fll in
  cs, itd.itd_fields, flm

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

(* patterns *)

let rec dpattern muc { pat_desc = desc; pat_loc = loc } =
  Dexpr.dpattern ~loc (match desc with
    | Ptree.Pwild -> DPwild
440
441
    | Ptree.Pvar (x, gh) -> DPvar (create_user_id x, gh)
    | Ptree.Papp (q, pl) ->
442
443
444
445
446
447
448
449
450
        DPapp (find_rsymbol muc q, List.map (fun p -> dpattern muc p) pl)
    | Ptree.Prec fl ->
        let get_val _ _ = function
          | Some p -> dpattern muc p
          | None -> Dexpr.dpattern DPwild in
        let cs,fl = parse_record ~loc muc get_val fl in
        DPapp (cs,fl)
    | Ptree.Ptuple pl ->
        DPapp (rs_tuple (List.length pl), List.map (dpattern muc) pl)
451
    | Ptree.Pcast (p, pty) -> DPcast (dpattern muc p, dity_of_pty muc pty)
452
    | Ptree.Pas (p, x, gh) -> DPas (dpattern muc p, create_user_id x, gh)
453
454
455
456
457
458
459
460
461
462
463
464
    | 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

465
466
467
468
469
470
471
472
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
473
  Dterm.term ~strict:true ~keep_loc:true t
Andrei Paskevich's avatar
Andrei Paskevich committed
474

475
476
477
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
478
  Dterm.fmla ~strict:true ~keep_loc:true f
Andrei Paskevich's avatar
Andrei Paskevich committed
479

480
481
let dpre muc pl lvm old =
  let dpre f = type_fmla muc lvm old f in
482
483
  List.map dpre pl

484
let dpost muc ql lvm old ity =
485
486
487
  let dpost (loc,pfl) = match pfl with
    | [{ pat_desc = Ptree.Pwild | Ptree.Ptuple [] }, f] ->
        let v = create_pvsymbol (id_fresh "result") ity in
488
        v, Loc.try3 ~loc type_fmla muc lvm old f
489
    | [{ pat_desc = Ptree.Pvar (id,false) }, f] ->
490
491
        let v = create_pvsymbol (create_user_id id) ity in
        let lvm = Mstr.add id.id_str v lvm in
492
        v, Loc.try3 ~loc type_fmla muc lvm old f
493
494
495
496
497
498
    | _ ->
        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
499
        v, Loc.try3 ~loc type_fmla muc lvm old f in
500
501
  List.map dpost ql

502
let dxpost muc ql lvm xsm old =
Andrei Paskevich's avatar
Andrei Paskevich committed
503
  let add_exn (q,pf) m =
504
505
506
507
508
    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
509
    Mxs.change (fun l -> match pf, l with
Andrei Paskevich's avatar
Andrei Paskevich committed
510
511
512
513
      | Some pf, Some l -> Some (pf :: l)
      | Some pf, None   -> Some (pf :: [])
      | None,    None   -> Some []
      | None,    Some _ -> l) xs m in
514
  let mk_xpost loc xs pfl =
Andrei Paskevich's avatar
Andrei Paskevich committed
515
    if pfl = [] then [] else
516
    dpost muc [loc,pfl] lvm old xs.xs_ity in
517
  let exn_map (loc,xpfl) =
518
519
    let m = List.fold_right add_exn xpfl Mxs.empty in
    Mxs.mapi (fun xs pfl -> mk_xpost loc xs pfl) m in
520
  let add_map ql m =
521
522
    Mxs.union (fun _ l r -> Some (l @ r)) (exn_map ql) m in
  List.fold_right add_map ql Mxs.empty
523
524
525
526
527
528
529

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 =
530
531
532
  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
533
534
535
536
537
538
  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

539
let dvariant muc varl lvm _xsm old =
540
  let dvar t = type_term muc lvm old t in
541
542
543
  let dvar (t,q) = dvar t, Opt.map (find_variant_ls muc) q in
  List.map dvar varl

544
let dspec muc sp lvm xsm old ity = {
545
546
  ds_pre     = dpre muc sp.sp_pre lvm old;
  ds_post    = dpost muc sp.sp_post lvm old ity;
547
  ds_xpost   = dxpost muc sp.sp_xpost lvm xsm old;
548
549
550
551
552
  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; }

553
let dassert muc f lvm _xsm old = type_fmla muc lvm old f
554

555
let dinvariant muc f lvm _xsm old = dpre muc f lvm old
556
557
558

(* abstract values *)

559
560
let dparam muc (_,id,gh,pty) =
  Opt.map create_user_id id, gh, dity_of_pty muc pty
561

562
563
let dbinder muc (_,id,gh,opt) =
  Opt.map create_user_id id, gh, dity_of_opt muc opt
564
565
566
567

(* expressions *)

let is_reusable de = match de.de_node with
568
  | DEvar _ | DEsym _ -> true | _ -> false
569
570
571
572
573
574
575
576

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)

577
let update_any kind e = match e.expr_desc with
578
579
  | Ptree.Eany (pl, _, pty, msk, sp) ->
      { e with expr_desc = Ptree.Eany (pl, kind, pty, msk, sp) }
580
581
582
583
584
585
  | _ -> e

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

586
587
588
589
590
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
591
  let qualid_app loc q el =
592
593
594
    let e = try DEsym (find_prog_symbol muc q) with
      | _ -> DEls_pure (find_lsymbol muc.muc_theory q) in
    expr_app loc e el
595
596
597
598
599
600
601
602
  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
603
604
  let qualid_app_pure loc q el =
    let e = match find_global_pv muc q with
605
606
      | Some v -> DEpv_pure v
      | None -> DEls_pure (find_lsymbol muc.muc_theory q) in
607
608
609
610
611
612
613
614
615
    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
616
617
618
619
620
621
  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
622
  Dexpr.dexpr ~loc begin match desc with
623
624
  | Ptree.Eident q ->
      qualid_app loc q []
625
626
  | Ptree.Eidpur q ->
      qualid_app_pure loc q []
627
628
629
630
631
  | 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 ->
632
      let e = DEsym (RS (rs_tuple (List.length el))) in
633
      expr_app loc e (List.map (dexpr muc denv) el)
634
635
636
637
638
639
640
641
642
643
644
645
  | 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
646
647
            let re = is_reusable de2 in
            let v = if re then de2 else mk_var n1 de2 in
648
649
650
            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
651
652
            let d = DEand (de12, de23) in
            if re then d else mk_let ~loc n1 de2 d
653
654
655
        | e23 ->
            apply loc de1 op1 (dexpr muc denv e23) in
      chain "q1 " "q2 " loc (dexpr muc denv e1) op1 e23
656
657
  | Ptree.Econst (Number.ConstInt _ as c) -> DEconst(c, dity_int)
  | Ptree.Econst (Number.ConstReal _ as c) -> DEconst(c, dity_real)
658
659
660
  | Ptree.Erecord fl ->
      let ls_of_rs rs = match rs.rs_logic with
        | RLls ls -> ls | _ -> assert false in
661
662
      let get_val _cs pj = function
        | None -> Loc.error ~loc (Decl.RecordFieldMissing (ls_of_rs pj))
663
664
        | Some e -> dexpr muc denv e in
      let cs,fl = parse_record ~loc muc get_val fl in
665
      expr_app loc (DEsym (RS cs)) fl
666
667
668
  | Ptree.Eupdate (e1, fl) ->
      let e1 = dexpr muc denv e1 in
      let re = is_reusable e1 in
669
      let v = if re then e1 else mk_var "q " e1 in
670
671
      let get_val _ pj = function
        | None ->
672
            let pj = Dexpr.dexpr ~loc (DEsym (RS pj)) in
673
674
675
            Dexpr.dexpr ~loc (DEapp (pj, v))
        | Some e -> dexpr muc denv e in
      let cs,fl = parse_record ~loc muc get_val fl in
676
      let d = expr_app loc (DEsym (RS cs)) fl in
677
      if re then d else mk_let ~loc "q " e1 d
678
  | Ptree.Elet (id, gh, kind, e1, e2) ->
679
680
      let e1 = update_any kind e1 in
      let kind = local_kind kind in
681
682
683
      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) ->
684
685
      let update_kind (id, gh, k, bl, pty, msk, sp, e) =
        id, gh, local_kind k, bl, pty, msk, sp, e in
686
      let fdl = List.map update_kind fdl in
687
688
      let denv, rd = drec_defn muc denv fdl in
      DErec (rd, dexpr muc denv e1)
689
  | Ptree.Efun (bl, pty, msk, sp, e) ->
690
691
692
693
694
      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
695
      let dity = dity_of_opt muc pty in
696
      let denv = denv_add_args denv bl in
697
698
      let denv = if bl = [] then denv else
        denv_add_exn denv old_mark_id dity in
699
      DEfun (bl, dity, msk, ds, dexpr muc denv e)
700
  | Ptree.Eany (pl, kind, pty, msk, sp) ->
701
702
703
704
705
      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
706
707
708
709
710
      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
711
      DEany (pl, dity_of_ity ity, msk, ds)
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
  | 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) ->
733
      let e1 = { e1 with expr_desc = Ecast (e1, PTtuple []) } in
734
735
736
737
738
739
740
741
742
743
744
745
746
747
      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
748
      let denv = denv_add_for_index denv id efrom.de_dvty in
749
      DEfor (id, efrom, dir, eto, inv, dexpr muc denv e1)
750
751
752
753
  | 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)
754
  | Ptree.Eraise (q, e1) ->
755
756
757
758
      let xs = find_dxsymbol q in
      let mb_unit = match xs with
        | DEgexn xs -> ity_equal xs.xs_ity ity_unit
        | DElexn _ -> true in
759
760
      let e1 = match e1 with
        | Some e1 -> dexpr muc denv e1
761
        | None when mb_unit -> Dexpr.dexpr ~loc (DEsym (RS rs_void))
762
763
764
765
766
        | _ -> Loc.errorm ~loc "exception argument expected" in
      DEraise (xs, e1)
  | Ptree.Etry (e1, cl) ->
      let e1 = dexpr muc denv e1 in
      let branch (q, pp, e) =
767
768
769
770
        let xs = find_dxsymbol q in
        let mb_unit = match xs with
          | DEgexn xs -> ity_equal xs.xs_ity ity_unit
          | DElexn _ -> true in
771
772
        let pp = match pp with
          | Some pp -> dpattern muc pp
773
          | None when mb_unit -> Dexpr.dpattern ~loc (DPapp (rs_void, []))
774
775
776
777
778
779
780
          | _ -> Loc.errorm ~loc "exception argument expected" in
        let denv = denv_add_pat denv pp in
        let e = dexpr muc denv e in
        xs, pp, e in
      DEtry (e1, List.map branch cl)
  | Ptree.Eghost e1 ->
      DEghost (dexpr muc denv e1)
781
782
  | Ptree.Eexn (id, pty, mask, e1) ->
      let id = create_user_id id in
783
      let dity = dity_of_pty muc pty in
784
785
786
787
      let denv = denv_add_exn denv id dity in
      DEexn (id, dity, mask, dexpr muc denv e1)
  | Ptree.Eabsurd ->
      DEabsurd
788
  | Ptree.Epure t ->
789
      let get_term lvm _xsm old = type_term muc lvm old t in
790
791
792
793
794
795
796
797
      let gvars _at q = try match find_prog_symbol muc q with
        | PV v -> Some v | _ -> None with _ -> None in
      let get_dty pure_denv =
        let dt = dterm muc.muc_theory gvars None pure_denv t in
        match dt.dt_dty with Some dty -> dty | None -> dty_bool in
      DEpure (get_term, denv_pure denv get_dty)
  | Ptree.Eassert (ak, f) ->
      DEassert (ak, dassert muc f)
798
  | Ptree.Emark (id, e1) ->
799
      let id = create_user_id id in
800
      DEmark (id, dexpr muc denv e1)
Andrei Paskevich's avatar
M.()    
Andrei Paskevich committed
801
802
803
804
  | Ptree.Escope (q, e1) ->
      let muc = open_scope muc "dummy" in
      let muc = import_scope muc (string_list_of_qualid q) in
      DElabel (dexpr muc denv e1, Slab.empty)
805
806
807
808
  | Ptree.Enamed (Lpos uloc, e1) ->
      DEuloc (dexpr muc denv e1, uloc)
  | Ptree.Enamed (Lstr lab, e1) ->
      DElabel (dexpr muc denv e1, Slab.singleton lab)
809
  | Ptree.Ecast ({expr_desc = Ptree.Econst c}, pty) ->
810
      DEconst (c, dity_of_pty muc pty)
811
  | Ptree.Ecast (e1, pty) ->
812
      let d1 = dexpr muc denv e1 in
813
      DEcast (d1, dity_of_pty muc pty)
814
  end
815
816

and drec_defn muc denv fdl =
817
  let prep (id, gh, kind, bl, pty, msk, sp, e) =
818
    let bl = List.map (dbinder muc) bl in
819
    let dity = dity_of_opt muc pty in
820
    let pre denv =
821
      let denv = denv_add_args denv bl in
822
      let denv = denv_add_exn denv old_mark_id dity in
823
824
      let dv = dvariant muc sp.sp_variant in
      dspec muc sp, dv, dexpr muc denv e in
825
    create_user_id id, gh, kind, bl, dity, msk, pre in
826
827
  Dexpr.drec_defn denv (List.map prep fdl)

828
(** Typing declarations *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
829

Andrei Paskevich's avatar
Andrei Paskevich committed
830
831
open Pdecl
open Pmodule
832

833
let add_pdecl ~vc muc d =
Andrei Paskevich's avatar
Andrei Paskevich committed
834
  if Debug.test_flag Glob.flag then Sid.iter Glob.def d.pd_news;
835
  add_pdecl ~vc muc d
Andrei Paskevich's avatar
Andrei Paskevich committed
836

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

839
840
841
842
843
844
845
846
847
848
849
850
851
852
let type_pure muc lvm denv e =
  let gvars at q = match at, q with
    | Some _, _ -> Loc.errorm ~loc:(qloc q)
        "`at' and `old' can only be used in program annotations"
    | None, Qident x -> Mstr.find_opt x.id_str lvm
    | None, Qdot _ -> None in
  dterm muc.muc_theory gvars None denv e

let type_term_pure muc lvm denv e =
  Dterm.term ~strict:true ~keep_loc:true (type_pure muc lvm denv e)

let type_fmla_pure muc lvm denv e =
  Dterm.fmla ~strict:true ~keep_loc:true (type_pure muc lvm denv e)

853
854
let check_public ~loc d name =
  if d.td_vis <> Public || d.td_mut then
Andrei Paskevich's avatar
Andrei Paskevich committed
855
    Loc.errorm ~loc "%s types cannot be abstract, private, or mutable" name;
856
857
858
  if d.td_inv <> [] then
    Loc.errorm ~loc "%s types cannot have invariants" name

859
860
861
let add_types muc tdl =
  let add m ({td_ident = {id_str =</