typing.ml 45.9 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
4
(*  Copyright 2010-2016   --   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)
Andrei Paskevich's avatar
Andrei Paskevich committed
126
    | PTpure ty | 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
    | 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
143 144
    | PTpure ty ->
        ity_purify (get_ity ty)
145 146 147 148 149
    | PTparen ty ->
        get_ity ty
  in
  get_ity pty

150
(** typing using destructive type variables
151

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

159 160
(** Typing patterns, terms, and formulas *)

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

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

173
let rec dpattern tuc { pat_desc = desc; pat_loc = loc } =
174
  Dterm.dpattern ~loc (match desc with
175
    | Ptree.Pwild -> DPwild
176 177
    | Ptree.Pvar (x, false) -> DPvar (create_user_id x)
    | Ptree.Papp (q, pl) ->
178 179
        let pl = List.map (dpattern tuc) pl in
        DPapp (find_lsymbol tuc q, pl)
180
    | Ptree.Ptuple pl ->
181
        let pl = List.map (dpattern tuc) pl in
182
        DPapp (fs_tuple (List.length pl), pl)
183
    | Ptree.Prec fl ->
184
        let get_val _ _ = function
185
          | Some p -> dpattern tuc p
186
          | None -> Dterm.dpattern DPwild in
187
        let cs,fl = parse_record ~loc tuc get_val fl in
188
        DPapp (cs,fl)
189
    | Ptree.Pas (p, x, false) -> DPas (dpattern tuc p, create_user_id x)
190
    | Ptree.Por (p, q) -> DPor (dpattern tuc p, dpattern tuc q)
191 192 193
    | 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")
194

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

202 203 204 205 206 207
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))

208 209 210 211 212
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
213
let mk_var tuc n dt =
214 215 216
  let dty = match dt.dt_dty with
    | None -> dty_of_ty ty_bool
    | Some dty -> dty in
Leon Gondelman's avatar
Leon Gondelman committed
217
  Dterm.dterm tuc ?loc:dt.dt_loc (DTvar (n, dty))
218

Leon Gondelman's avatar
Leon Gondelman committed
219 220
let mk_let tuc ~loc n dt node =
  DTlet (dt, id_user n loc, Dterm.dterm tuc ~loc node)
221

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

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

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

372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390
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
391
    | [{pv_ity = {ity_node = (Ityreg {reg_its = s} | Ityapp (s,_,_))}}] -> s
392 393 394 395 396 397 398 399 400 401
    | _ -> 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
402
    Mrs.add_new (DuplicateRecordField (ls_of_rs pj)) pj v m
403 404 405 406 407 408 409 410 411 412 413 414 415 416
    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
417 418
    | Ptree.Pvar (x, gh) -> DPvar (create_user_id x, gh)
    | Ptree.Papp (q, pl) ->
419 420 421 422 423 424 425 426 427 428
        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)
429
    | Ptree.Pas (p, x, gh) -> DPas (dpattern muc p, create_user_id x, gh)
430 431 432 433 434 435 436 437 438 439 440 441
    | 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

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

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

457 458
let dpre muc pl lvm old =
  let dpre f = type_fmla muc lvm old f in
459 460
  List.map dpre pl

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

479
let dxpost muc ql lvm old =
Andrei Paskevich's avatar
Andrei Paskevich committed
480
  let add_exn (q,pf) m =
481
    let xs = find_xsymbol muc q in
Andrei Paskevich's avatar
Andrei Paskevich committed
482 483 484 485 486
    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
487
  let mk_xpost loc xs pfl =
Andrei Paskevich's avatar
Andrei Paskevich committed
488
    if pfl = [] then [] else
489
    dpost muc [loc,pfl] lvm old xs.xs_ity in
490 491 492 493 494 495 496 497 498 499 500 501 502
  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 =
503 504 505
  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
506 507 508 509 510 511
  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

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

517 518 519 520
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;
521 522 523 524 525
  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; }

526
let dassert muc f lvm old = type_fmla muc lvm old f
527

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

(* 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
546
  | DEvar _ | DEpv _ -> true | _ -> false
547 548 549 550 551 552 553 554

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)

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

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

564 565 566 567 568
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
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
572
      | _ -> DEls (find_lsymbol muc.muc_theory q) in
573
    expr_app loc e el
574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591
  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)
592 593 594 595 596 597 598 599 600 601 602 603
  | 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
604 605
            let re = is_reusable de2 in
            let v = if re then de2 else mk_var n1 de2 in
606 607 608
            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
609 610
            let d = DEand (de12, de23) in
            if re then d else mk_let ~loc n1 de2 d
611 612 613
        | e23 ->
            apply loc de1 op1 (dexpr muc denv e23) in
      chain "q1 " "q2 " loc (dexpr muc denv e1) op1 e23
614 615 616 617
  | Ptree.Econst c -> DEconst c
  | Ptree.Erecord fl ->
      let ls_of_rs rs = match rs.rs_logic with
        | RLls ls -> ls | _ -> assert false in
618 619
      let get_val _cs pj = function
        | None -> Loc.error ~loc (Decl.RecordFieldMissing (ls_of_rs pj))
620 621 622 623 624 625
        | 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
626
      let v = if re then e1 else mk_var "q " e1 in
627 628 629 630 631 632 633
      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
634
      if re then d else mk_let ~loc "q " e1 d
635
  | Ptree.Elet (id, gh, kind, e1, e2) ->
636 637
      let e1 = update_any kind e1 in
      let kind = local_kind kind in
638 639 640
      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) ->
641 642
      let update_kind (id, gh, k, bl, pty, msk, sp, e) =
        id, gh, local_kind k, bl, pty, msk, sp, e in
643
      let fdl = List.map update_kind fdl in
644 645
      let denv, rd = drec_defn muc denv fdl in
      DErec (rd, dexpr muc denv e1)
646
  | Ptree.Efun (bl, pty, msk, sp, e) ->
647 648 649 650 651 652 653 654
      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
655 656
      DEfun (bl, msk, ds, dexpr muc (denv_add_args denv bl) e)
  | Ptree.Eany (pl, kind, pty, msk, sp) ->
657 658 659 660 661
      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
662 663 664 665 666
      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
667
      DEany (pl, msk, ds, dity_of_ity ity)
668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688
  | 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) ->
689
      let e1 = { e1 with expr_desc = Ecast (e1, PTtuple []) } in
690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705
      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)
706 707 708 709
  | 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)
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 744 745
  | 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 =
746
  let prep (id, gh, kind, bl, pty, msk, sp, e) =
747 748 749 750 751 752 753
    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
754
    create_user_id id, gh, kind, bl, dity, msk, pre in
755 756
  Dexpr.drec_defn denv (List.map prep fdl)

757
(** Typing declarations *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
758

Andrei Paskevich's avatar
Andrei Paskevich committed
759 760
open Pdecl
open Pmodule
761

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

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

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

782 783 784
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
785 786 787 788 789 790
  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
791
    match d.td_def with
Andrei Paskevich's avatar
Andrei Paskevich committed
792 793
    | TDalias pty ->
        if d.td_vis <> Public || d.td_mut then Loc.errorm ~loc
794
          "Alias types cannot be abstract, private, or mutable";
Andrei Paskevich's avatar
Andrei Paskevich committed
795 796 797 798 799 800 801 802 803
        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
804
          "Algebraic types cannot be abstract, private, or mutable";
Andrei Paskevich's avatar
Andrei Paskevich committed
805 806 807 808 809
        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
810 811 812 813 814
        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
815
              let ity = parse ~loc ~alias ~alg pty in
816
              let v = try Hstr.find hfd nm with Not_found ->
Andrei Paskevich's avatar
Andrei Paskevich committed
817
                let v = create_pvsymbol (create_user_id id) ~ghost ity in
818
                Hstr.add hfd nm v;
Andrei Paskevich's avatar
Andrei Paskevich committed
819 820
                v in
              if not (ity_equal v.pv_ity ity && ghost = v.pv_ghost) then
821 822
                Loc.errorm ~loc "Conflicting definitions for field %s" nm;
              nms, (true, v)
Andrei Paskevich's avatar
Andrei Paskevich committed
823 824
          | None ->
              let ity = parse ~loc ~alias ~alg pty in
825 826 827 828 829 830 831 832 833 834 835 836
              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
837
(*      if not (Hstr.mem htd x) then *)
Andrei Paskevich's avatar
Andrei Paskevich committed
838 839 840 841
        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 ->
842
            let itd = create_plain_variant_decl id args csl in
Andrei Paskevich's avatar
Andrei Paskevich committed
843 844 845 846
            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
847 848 849 850 851
        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
852 853 854
          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
855 856
          nms, (fd.f_mutable, create_pvsymbol id ~ghost ity) in
        let _,fl = Lists.map_fold_left get_fd Sstr.empty fl in
857
(*      if not (Hstr.mem htd x) then *)
Andrei Paskevich's avatar
Andrei Paskevich committed
858 859 860
        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
861
              "Recursive types cannot be abstract, private, or mutable";
Andrei Paskevich's avatar
Andrei Paskevich committed
862 863 864 865 866 867
            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 ->
868 869 870
            (* 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
871
            let add_fd m (_, v) = Mstr.add v.pv_vs.vs_name.id_string v m in
Andrei Paskevich's avatar
Andrei Paskevich committed
872
            let gvars = List.fold_left add_fd Mstr.empty fl in
873 874
            let type_inv f = type_fmla_pure muc gvars Dterm.denv_empty f in
            let invl = List.map type_inv d.td_inv in
875
            let itd = create_plain_record_decl ~priv ~mut id args fl invl in
Andrei Paskevich's avatar
Andrei Paskevich committed
876 877 878 879 880 881 882 883 884 885
            Hstr.add hts x itd.itd_its; Hstr.add htd x itd end

  and