typing.ml 45 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1
2
3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2015   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
5
6
7
8
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
9
(*                                                                  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
10
(********************************************************************)
11

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

25
(** debug flags *)
26

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

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

33
(** symbol lookup *)
34
35

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

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

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

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

52
exception UnboundSymbol of qualid
53

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

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

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

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

75
76
77
78
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
    | RS rs -> rs.rs_name in
100
101
102
103
  find_qualid get_id_ps ns_find_prog_symbol ns p

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

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

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

111
112
(** Parsing types *)

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

131
132
133
134
135
136
137
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
138
        Loc.try3 ~loc:(qloc q) ity_app s tyl []
139
140
141
142
143
144
145
146
147
    | PTtuple tyl ->
        ity_tuple (List.map get_ity tyl)
    | PTarrow (ty1, ty2) ->
        ity_func (get_ity ty1) (get_ity ty2)
    | PTparen ty ->
        get_ity ty
  in
  get_ity pty

148
(** typing using destructive type variables
149

150
151
152
153
154
155
    parsed trees        intermediate trees       typed trees
      (Ptree)                (Dterm)               (Term)
   -----------------------------------------------------------
     ppure_type  ---dty--->   dty       ---ty--->    ty
      lexpr      --dterm-->   dterm     --term-->    term
*)
156

157
158
(** Typing patterns, terms, and formulas *)

159
let create_user_id {id_str = n; id_lab = label; id_loc = loc} =
160
161
162
163
  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
164

165
166
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
167
  let cs,pjl,flm = Loc.try2 ~loc parse_record tuc.uc_known fl in
168
169
170
  let get_val pj = get_val cs pj (Mls.find_opt pj flm) in
  cs, List.map get_val pjl

171
let rec dpattern tuc { pat_desc = desc; pat_loc = loc } =
172
  Dterm.dpattern ~loc (match desc with
173
    | Ptree.Pwild -> DPwild
174
175
    | Ptree.Pvar (x, false) -> DPvar (create_user_id x)
    | Ptree.Papp (q, pl) ->
176
177
        let pl = List.map (dpattern tuc) pl in
        DPapp (find_lsymbol tuc q, pl)
178
    | Ptree.Ptuple pl ->
179
        let pl = List.map (dpattern tuc) pl in
180
        DPapp (fs_tuple (List.length pl), pl)
181
    | Ptree.Prec fl ->
182
        let get_val _ _ = function
183
          | Some p -> dpattern tuc p
184
          | None -> Dterm.dpattern DPwild in
185
        let cs,fl = parse_record ~loc tuc get_val fl in
186
        DPapp (cs,fl)
187
    | Ptree.Pas (p, x, false) -> DPas (dpattern tuc p, create_user_id x)
188
    | Ptree.Por (p, q) -> DPor (dpattern tuc p, dpattern tuc q)
189
190
191
    | Ptree.Pcast (p, ty) -> DPcast (dpattern tuc p, ty_of_pty tuc ty)
    | Ptree.Pvar (_, true) | Ptree.Pas (_, _, true) -> Loc.errorm ~loc
        "ghost variables are only allowed in programs")
192

193
let quant_var tuc (loc, id, gh, ty) =
194
  if gh then Loc.errorm ~loc "ghost variables are only allowed in programs";
195
  let ty = match ty with
196
    | Some ty -> dty_of_ty (ty_of_pty tuc ty)
197
    | None    -> dty_fresh () in
198
  Opt.map create_user_id id, ty, Some loc
199

200
201
202
203
204
205
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))

206
207
208
209
210
211
212
213
214
215
216
217
218
219
let is_reusable dt = match dt.dt_node with
  | DTvar _ | DTgvar _ | DTconst _ | DTtrue | DTfalse -> true
  | DTapp (_,[]) -> true
  | _ -> false

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

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

220
221
222
let mk_closure loc ls =
  let mk dt = Dterm.dterm ~loc dt in
  let mk_v i _ =
223
224
    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
225
  let vl = Lists.mapi mk_v ls.ls_args in
Andrei Paskevich's avatar
Andrei Paskevich committed
226
  DTquant (DTlambda, vl, [], mk (DTapp (ls, List.map mk_t vl)))
227

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

368
(** typing program expressions *)
Andrei Paskevich's avatar
Andrei Paskevich committed
369

370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
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
389
    | [{pv_ity = {ity_node = (Ityreg {reg_its = s} | Ityapp (s,_,_))}}] -> s
390
391
392
393
394
395
396
397
398
399
    | _ -> 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
400
    Mrs.add_new (DuplicateRecordField (ls_of_rs pj)) pj v m
401
402
403
404
405
406
407
408
409
410
411
412
413
414
    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
415
416
    | Ptree.Pvar (x, gh) -> DPvar (create_user_id x, gh)
    | Ptree.Papp (q, pl) ->
417
418
419
420
421
422
423
424
425
426
        DPapp (find_rsymbol muc q, List.map (fun p -> dpattern muc p) pl)
    | Ptree.Prec fl ->
        let get_val _ _ = function
          | Some p -> dpattern muc p
          | None -> Dexpr.dpattern DPwild in
        let cs,fl = parse_record ~loc muc get_val fl in
        DPapp (cs,fl)
    | Ptree.Ptuple pl ->
        DPapp (rs_tuple (List.length pl), List.map (dpattern muc) pl)
    | Ptree.Pcast (p, pty) -> DPcast (dpattern muc p, ity_of_pty muc pty)
427
    | Ptree.Pas (p, x, gh) -> DPas (dpattern muc p, create_user_id x, gh)
428
429
430
431
432
433
434
435
436
437
438
439
    | 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

440
441
442
443
444
445
446
447
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
448
  Dterm.term ~strict:true ~keep_loc:true t
Andrei Paskevich's avatar
Andrei Paskevich committed
449

450
451
452
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
453
  Dterm.fmla ~strict:true ~keep_loc:true f
Andrei Paskevich's avatar
Andrei Paskevich committed
454

455
456
let dpre muc pl lvm old =
  let dpre f = type_fmla muc lvm old f in
457
458
  List.map dpre pl

459
let dpost muc ql lvm old ity =
460
461
462
  let dpost (loc,pfl) = match pfl with
    | [{ pat_desc = Ptree.Pwild | Ptree.Ptuple [] }, f] ->
        let v = create_pvsymbol (id_fresh "result") ity in
463
        v, Loc.try3 ~loc type_fmla muc lvm old f
464
    | [{ pat_desc = Ptree.Pvar (id,false) }, f] ->
465
466
        let v = create_pvsymbol (create_user_id id) ity in
        let lvm = Mstr.add id.id_str v lvm in
467
        v, Loc.try3 ~loc type_fmla muc lvm old f
468
469
470
471
472
473
    | _ ->
        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
474
        v, Loc.try3 ~loc type_fmla muc lvm old f in
475
476
  List.map dpost ql

477
let dxpost muc ql lvm old =
Andrei Paskevich's avatar
Andrei Paskevich committed
478
  let add_exn (q,pf) m =
479
    let xs = find_xsymbol muc q in
Andrei Paskevich's avatar
Andrei Paskevich committed
480
481
482
483
484
    Mexn.change (fun l -> match pf, l with
      | Some pf, Some l -> Some (pf :: l)
      | Some pf, None   -> Some (pf :: [])
      | None,    None   -> Some []
      | None,    Some _ -> l) xs m in
485
  let mk_xpost loc xs pfl =
Andrei Paskevich's avatar
Andrei Paskevich committed
486
    if pfl = [] then [] else
487
    dpost muc [loc,pfl] lvm old xs.xs_ity in
488
489
490
491
492
493
494
495
496
497
498
499
500
  let exn_map (loc,xpfl) =
    let m = List.fold_right add_exn xpfl Mexn.empty in
    Mexn.mapi (fun xs pfl -> mk_xpost loc xs pfl) m in
  let add_map ql m =
    Mexn.union (fun _ l r -> Some (l @ r)) (exn_map ql) m in
  List.fold_right add_map ql Mexn.empty

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

let dwrites muc wl lvm =
501
502
503
  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
504
505
506
507
508
509
  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

510
511
let dvariant muc varl lvm old =
  let dvar t = type_term muc lvm old t in
512
513
514
  let dvar (t,q) = dvar t, Opt.map (find_variant_ls muc) q in
  List.map dvar varl

515
516
517
518
let dspec muc sp lvm old ity = {
  ds_pre     = dpre muc sp.sp_pre lvm old;
  ds_post    = dpost muc sp.sp_post lvm old ity;
  ds_xpost   = dxpost muc sp.sp_xpost lvm old;
519
520
521
522
523
  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; }

524
let dassert muc f lvm old = type_fmla muc lvm old f
525

526
let dinvariant muc f lvm old = dpre muc f lvm old
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543

(* abstract values *)

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

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

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

(* expressions *)

let is_reusable de = match de.de_node with
544
  | DEvar _ | DEpv _ -> true | _ -> false
545
546
547
548
549
550
551
552

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)

553
let update_any kind e = match e.expr_desc with
554
555
  | Ptree.Eany (pl, _, pty, msk, sp) ->
      { e with expr_desc = Ptree.Eany (pl, kind, pty, msk, sp) }
556
557
558
559
560
561
  | _ -> e

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

562
563
564
565
566
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
567
568
569
570
571
  let qualid_app loc q el =
    let e = try match find_prog_symbol muc q with
      | PV pv -> DEpv pv | RS rs -> DErs rs with
      | _ -> DEls (find_lsymbol muc.muc_theory q) in
    expr_app loc e el
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
  in
  let qualid_app loc q el = match q with
    | Qident {id_str = n} ->
        (match denv_get_opt denv n with
        | Some d -> expr_app loc d el
        | None -> qualid_app loc q el)
    | _ -> qualid_app loc q el
  in
  Dexpr.dexpr ~loc (match desc with
  | Ptree.Eident q ->
      qualid_app loc q []
  | Ptree.Eidapp (q, el) ->
      qualid_app loc q (List.map (dexpr muc denv) el)
  | Ptree.Eapply (e1, e2) ->
      DEapp (dexpr muc denv e1, dexpr muc denv e2)
  | Ptree.Etuple el ->
      let e = DErs (rs_tuple (List.length el)) in
      expr_app loc e (List.map (dexpr muc denv) el)
590
591
592
593
594
595
596
597
598
599
600
601
  | 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
602
603
            let re = is_reusable de2 in
            let v = if re then de2 else mk_var n1 de2 in
604
605
606
            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
607
608
            let d = DEand (de12, de23) in
            if re then d else mk_let ~loc n1 de2 d
609
610
611
        | e23 ->
            apply loc de1 op1 (dexpr muc denv e23) in
      chain "q1 " "q2 " loc (dexpr muc denv e1) op1 e23
612
613
614
615
  | Ptree.Econst c -> DEconst c
  | Ptree.Erecord fl ->
      let ls_of_rs rs = match rs.rs_logic with
        | RLls ls -> ls | _ -> assert false in
616
617
      let get_val _cs pj = function
        | None -> Loc.error ~loc (Decl.RecordFieldMissing (ls_of_rs pj))
618
619
620
621
622
623
        | Some e -> dexpr muc denv e in
      let cs,fl = parse_record ~loc muc get_val fl in
      expr_app loc (DErs cs) fl
  | Ptree.Eupdate (e1, fl) ->
      let e1 = dexpr muc denv e1 in
      let re = is_reusable e1 in
624
      let v = if re then e1 else mk_var "q " e1 in
625
626
627
628
629
630
631
      let get_val _ pj = function
        | None ->
            let pj = Dexpr.dexpr ~loc (DErs pj) in
            Dexpr.dexpr ~loc (DEapp (pj, v))
        | Some e -> dexpr muc denv e in
      let cs,fl = parse_record ~loc muc get_val fl in
      let d = expr_app loc (DErs cs) fl in
632
      if re then d else mk_let ~loc "q " e1 d
633
  | Ptree.Elet (id, gh, kind, e1, e2) ->
634
635
      let e1 = update_any kind e1 in
      let kind = local_kind kind in
636
637
638
      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) ->
639
640
      let update_kind (id, gh, k, bl, pty, msk, sp, e) =
        id, gh, local_kind k, bl, pty, msk, sp, e in
641
      let fdl = List.map update_kind fdl in
642
643
      let denv, rd = drec_defn muc denv fdl in
      DErec (rd, dexpr muc denv e1)
644
  | Ptree.Efun (bl, pty, msk, sp, e) ->
645
646
647
648
649
650
651
652
      let bl = List.map (dbinder muc) bl in
      let e = match pty with
        | Some pty -> { e with expr_desc = Ecast (e, pty) }
        | None -> e in
      let ds = match sp.sp_variant with
        | ({term_loc = loc},_)::_ ->
            Loc.errorm ~loc "unexpected 'variant' clause"
        | _ -> dspec muc sp in
653
654
      DEfun (bl, msk, ds, dexpr muc (denv_add_args denv bl) e)
  | Ptree.Eany (pl, kind, pty, msk, sp) ->
655
656
657
658
659
      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
660
661
662
663
664
      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
665
      DEany (pl, msk, ds, dity_of_ity ity)
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
  | 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) ->
687
      let e1 = { e1 with expr_desc = Ecast (e1, PTtuple []) } in
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
      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
      let denv = denv_add_var denv id (dity_of_ity ity_int) in
      DEfor (id, efrom, dir, eto, inv, dexpr muc denv e1)
704
705
706
707
  | 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)
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
  | Ptree.Eraise (q, e1) ->
      let xs = find_xsymbol muc q in
      let e1 = match e1 with
        | Some e1 -> dexpr muc denv e1
        | None when ity_equal xs.xs_ity ity_unit ->
            Dexpr.dexpr ~loc (DErs rs_void)
        | _ -> Loc.errorm ~loc "exception argument expected" in
      DEraise (xs, e1)
  | Ptree.Etry (e1, cl) ->
      let e1 = dexpr muc denv e1 in
      let branch (q, pp, e) =
        let xs = find_xsymbol muc q in
        let pp = match pp with
          | Some pp -> dpattern muc pp
          | None when ity_equal xs.xs_ity ity_unit ->
              Dexpr.dpattern ~loc (DPapp (rs_void, []))
          | _ -> Loc.errorm ~loc "exception argument expected" in
        let denv = denv_add_pat denv pp in
        let e = dexpr muc denv e in
        xs, pp, e in
      DEtry (e1, List.map branch cl)
  | Ptree.Eghost e1 ->
      DEghost (dexpr muc denv e1)
  | Ptree.Eabsurd -> DEabsurd
  | Ptree.Eassert (ak, lexpr) ->
      DEassert (ak, dassert muc lexpr)
  | Ptree.Emark (id, e1) ->
      DEmark (create_user_id id, dexpr muc denv e1)
  | Ptree.Enamed (Lpos uloc, e1) ->
      DEuloc (dexpr muc denv e1, uloc)
  | Ptree.Enamed (Lstr lab, e1) ->
      DElabel (dexpr muc denv e1, Slab.singleton lab)
  | Ptree.Ecast (e1, pty) ->
      DEcast (dexpr muc denv e1, ity_of_pty muc pty))

and drec_defn muc denv fdl =
744
  let prep (id, gh, kind, bl, pty, msk, sp, e) =
745
746
747
748
749
750
751
    let bl = List.map (dbinder muc) bl in
    let dity = match pty with
      | Some pty -> dity_of_ity (ity_of_pty muc pty)
      | None -> dity_fresh () in
    let pre denv =
      let dv = dvariant muc sp.sp_variant in
      dspec muc sp, dv, dexpr muc denv e in
752
    create_user_id id, gh, kind, bl, dity, msk, pre in
753
754
  Dexpr.drec_defn denv (List.map prep fdl)

755
(** Typing declarations *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
756

Andrei Paskevich's avatar
Andrei Paskevich committed
757
758
open Pdecl
open Pmodule
759

760
let add_pdecl ~vc muc d =
Andrei Paskevich's avatar
Andrei Paskevich committed
761
  if Debug.test_flag Glob.flag then Sid.iter Glob.def d.pd_news;
762
  add_pdecl ~vc muc d
Andrei Paskevich's avatar
Andrei Paskevich committed
763

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

766
767
768
769
770
771
772
773
774
775
776
777
778
779
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)

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

  and parse ~loc ~alias ~alg pty =
    let rec down = function
      | PTtyvar id ->
          ity_var (tv_of_string id.id_str)
      | PTtyapp (q,tyl) ->
          let s = match q with
            | Qident {id_str = x} when Sstr.mem x alias ->
                Loc.errorm ~loc "Cyclic type definition"
884
885
            | Qident {id_str = x} when Hstr.mem hts x ->
                Hstr.find hts x
Andrei Paskevich's avatar
Andrei Paskevich committed
886
887
            | Qident {id_str = x} when Mstr.mem x alg ->
                let id, args = Mstr.find x alg in
888
                let s = create_rec_itysymbol id args in
889
                Hstr.add hts x s;
890
(*              visit ~alias ~alg x (Mstr.find x def); *)
891
                s
Andrei Paskevich's avatar
Andrei Paskevich committed
892
            | Qident {id_str = x} when Mstr.mem x def ->
893
                visit ~alias ~alg x (Mstr.find x def);
Andrei Paskevich's avatar
Andrei Paskevich committed
894
895
                Hstr.find hts x
            | _ ->
896
                find_itysymbol muc q in
897
          Loc.try3 ~loc:(qloc q) ity_app s (List.map down tyl) []
Andrei Paskevich's avatar
Andrei Paskevich committed
898
899
900
901
902
903
904
      | PTtuple tyl -> ity_tuple (List.map down tyl)
      | PTarrow (ty1,ty2) -> ity_func (down ty1) (down ty2)
      | PTparen ty -> down ty in
    down pty in

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

907
let tyl_of_params {muc_theory = tuc} pl =
Andrei Paskevich's avatar
Andrei Paskevich committed
908
909
910
  let ty_of_param (loc,_,gh,ty) =
    if gh then Loc.errorm ~loc
      "ghost parameters are not allowed in pure declarations";
911
    ty_of_pty tuc ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
912
  List.map ty_of_param pl
913

914
let add_logics muc dl =
915
  let lsymbols = Hstr.create 17 in
Jean-Christophe Filliâtre's avatar
logic    
Jean-Christophe Filliâtre committed
916
  (* 1. create all symbols and make an environment with these symbols *)
917
  let create_symbol mkk d =
918
    let id = d.ld_ident.id_str in
919
    let v = create_user_id d.ld_ident in
920
921
    let pl = tyl_of_params muc d.ld_params in
    let ty = Opt.map (ty_of_pty muc.muc_theory) d.ld_type in
922
    let ls = create_lsymbol v pl ty in
923
    Hstr.add lsymbols id ls;
924
925
    Loc.try2 ~loc:d.ld_loc add_decl mkk (create_param_decl ls) in
  let mkk = List.fold_left create_symbol muc dl in
Jean-Christophe Filliâtre's avatar
logic    
Jean-Christophe Filliâtre committed
926
  (* 2. then type-check all definitions *)
927
  let type_decl d (abst,defn) =
928
    let id = d.ld_ident.id_str in
Andrei Paskevich's avatar