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

153
(** typing using destructive type variables
154

155 156 157 158 159 160
    parsed trees        intermediate trees       typed trees
      (Ptree)                (Dterm)               (Term)
   -----------------------------------------------------------
     ppure_type  ---dty--->   dty       ---ty--->    ty
      lexpr      --dterm-->   dterm     --term-->    term
*)
161

162 163
(** Typing patterns, terms, and formulas *)

164
let create_user_id {id_str = n; id_lab = label; id_loc = loc} =
165 166 167 168
  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
169

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

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

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

205 206 207 208 209 210
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))

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

Leon Gondelman's avatar
Leon Gondelman committed
222 223
let mk_let tuc ~loc n dt node =
  DTlet (dt, id_user n loc, Dterm.dterm tuc ~loc node)
224

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

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

380
(** typing program expressions *)
Andrei Paskevich's avatar
Andrei Paskevich committed
381

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

452 453 454 455 456 457 458 459
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
460
  Dterm.term ~strict:true ~keep_loc:true t
Andrei Paskevich's avatar
Andrei Paskevich committed
461

462 463 464
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
465
  Dterm.fmla ~strict:true ~keep_loc:true f
Andrei Paskevich's avatar
Andrei Paskevich committed
466

467 468
let dpre muc pl lvm old =
  let dpre f = type_fmla muc lvm old f in
469 470
  List.map dpre pl

471
let dpost muc ql lvm old ity =
472 473 474
  let dpost (loc,pfl) = match pfl with
    | [{ pat_desc = Ptree.Pwild | Ptree.Ptuple [] }, f] ->
        let v = create_pvsymbol (id_fresh "result") ity in
475
        v, Loc.try3 ~loc type_fmla muc lvm old f
476
    | [{ pat_desc = Ptree.Pvar (id,false) }, f] ->
477 478
        let v = create_pvsymbol (create_user_id id) ity in
        let lvm = Mstr.add id.id_str v lvm in
479
        v, Loc.try3 ~loc type_fmla muc lvm old f
480 481 482 483 484 485
    | _ ->
        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
486
        v, Loc.try3 ~loc type_fmla muc lvm old f in
487 488
  List.map dpost ql

489
let dxpost muc ql lvm xsm old =
Andrei Paskevich's avatar
Andrei Paskevich committed
490
  let add_exn (q,pf) m =
491 492 493 494 495
    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
496
    Mxs.change (fun l -> match pf, l with
Andrei Paskevich's avatar
Andrei Paskevich committed
497 498 499 500
      | Some pf, Some l -> Some (pf :: l)
      | Some pf, None   -> Some (pf :: [])
      | None,    None   -> Some []
      | None,    Some _ -> l) xs m in
501
  let mk_xpost loc xs pfl =
Andrei Paskevich's avatar
Andrei Paskevich committed
502
    if pfl = [] then [] else
503
    dpost muc [loc,pfl] lvm old xs.xs_ity in
504
  let exn_map (loc,xpfl) =
505 506
    let m = List.fold_right add_exn xpfl Mxs.empty in
    Mxs.mapi (fun xs pfl -> mk_xpost loc xs pfl) m in
507
  let add_map ql m =
508 509
    Mxs.union (fun _ l r -> Some (l @ r)) (exn_map ql) m in
  List.fold_right add_map ql Mxs.empty
510 511 512 513 514 515 516

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

526
let dvariant muc varl lvm _xsm old =
527
  let dvar t = type_term muc lvm old t in
528 529 530
  let dvar (t,q) = dvar t, Opt.map (find_variant_ls muc) q in
  List.map dvar varl

531
let dspec muc sp lvm xsm old ity = {
532 533
  ds_pre     = dpre muc sp.sp_pre lvm old;
  ds_post    = dpost muc sp.sp_post lvm old ity;
534
  ds_xpost   = dxpost muc sp.sp_xpost lvm xsm old;
535 536 537 538 539
  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; }

540
let dassert muc f lvm _xsm old = type_fmla muc lvm old f
541

542
let dinvariant muc f lvm _xsm old = dpre muc f lvm old
543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559

(* 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
560
  | DEvar _ | DEsym _ -> true | _ -> false
561 562 563 564 565 566 567 568

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)

569
let update_any kind e = match e.expr_desc with
570 571
  | Ptree.Eany (pl, _, pty, msk, sp) ->
      { e with expr_desc = Ptree.Eany (pl, kind, pty, msk, sp) }
572 573 574 575 576 577
  | _ -> e

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

578 579 580 581 582
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
583
  let qualid_app loc q el =
584
    let e = try DEsym (find_prog_symbol muc q) with
585
      | _ -> DEls (find_lsymbol muc.muc_theory q) in
586
    expr_app loc e el
587 588 589 590 591 592 593 594
  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
595 596 597 598 599 600
  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
601
  Dexpr.dexpr ~loc begin match desc with
602 603 604 605 606 607 608
  | 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 ->
609
      let e = DEsym (RS (rs_tuple (List.length el))) in
610
      expr_app loc e (List.map (dexpr muc denv) el)
611 612 613 614 615 616 617 618 619 620 621 622
  | 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
623 624
            let re = is_reusable de2 in
            let v = if re then de2 else mk_var n1 de2 in
625 626 627
            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
628 629
            let d = DEand (de12, de23) in
            if re then d else mk_let ~loc n1 de2 d
630 631 632
        | e23 ->
            apply loc de1 op1 (dexpr muc denv e23) in
      chain "q1 " "q2 " loc (dexpr muc denv e1) op1 e23
633 634
  | Ptree.Econst (Number.ConstInt _ as c) -> DEconst(c, dity_int)
  | Ptree.Econst (Number.ConstReal _ as c) -> DEconst(c, dity_real)
635 636 637
  | Ptree.Erecord fl ->
      let ls_of_rs rs = match rs.rs_logic with
        | RLls ls -> ls | _ -> assert false in
638 639
      let get_val _cs pj = function
        | None -> Loc.error ~loc (Decl.RecordFieldMissing (ls_of_rs pj))
640 641
        | Some e -> dexpr muc denv e in
      let cs,fl = parse_record ~loc muc get_val fl in
642
      expr_app loc (DEsym (RS cs)) fl
643 644 645
  | Ptree.Eupdate (e1, fl) ->
      let e1 = dexpr muc denv e1 in
      let re = is_reusable e1 in
646
      let v = if re then e1 else mk_var "q " e1 in
647 648
      let get_val _ pj = function
        | None ->
649
            let pj = Dexpr.dexpr ~loc (DEsym (RS pj)) in
650 651 652
            Dexpr.dexpr ~loc (DEapp (pj, v))
        | Some e -> dexpr muc denv e in
      let cs,fl = parse_record ~loc muc get_val fl in
653
      let d = expr_app loc (DEsym (RS cs)) fl in
654
      if re then d else mk_let ~loc "q " e1 d
655
  | Ptree.Elet (id, gh, kind, e1, e2) ->
656 657
      let e1 = update_any kind e1 in
      let kind = local_kind kind in
658 659 660
      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) ->
661 662
      let update_kind (id, gh, k, bl, pty, msk, sp, e) =
        id, gh, local_kind k, bl, pty, msk, sp, e in
663
      let fdl = List.map update_kind fdl in
664 665
      let denv, rd = drec_defn muc denv fdl in
      DErec (rd, dexpr muc denv e1)
666
  | Ptree.Efun (bl, pty, msk, sp, e) ->
667 668 669 670 671 672 673 674
      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
675 676
      DEfun (bl, msk, ds, dexpr muc (denv_add_args denv bl) e)
  | Ptree.Eany (pl, kind, pty, msk, sp) ->
677 678 679 680 681
      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
682 683 684 685 686
      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
687
      DEany (pl, msk, ds, dity_of_ity ity)
688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708
  | 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) ->
709
      let e1 = { e1 with expr_desc = Ecast (e1, PTtuple []) } in
710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725
      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)
726 727 728 729
  | 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)
730
  | Ptree.Eraise (q, e1) ->
731 732 733 734
      let xs = find_dxsymbol q in
      let mb_unit = match xs with
        | DEgexn xs -> ity_equal xs.xs_ity ity_unit
        | DElexn _ -> true in
735 736
      let e1 = match e1 with
        | Some e1 -> dexpr muc denv e1
737
        | None when mb_unit -> Dexpr.dexpr ~loc (DEsym (RS rs_void))
738 739 740 741 742
        | _ -> 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) =
743 744 745 746
        let xs = find_dxsymbol q in
        let mb_unit = match xs with
          | DEgexn xs -> ity_equal xs.xs_ity ity_unit
          | DElexn _ -> true in
747 748
        let pp = match pp with
          | Some pp -> dpattern muc pp
749
          | None when mb_unit -> Dexpr.dpattern ~loc (DPapp (rs_void, []))
750 751 752 753 754 755 756
          | _ -> 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)
757 758 759 760 761 762 763
  | Ptree.Eexn (id, pty, mask, e1) ->
      let id = create_user_id id in
      let dity = dity_of_ity (ity_of_pty muc pty) in
      let denv = denv_add_exn denv id dity in
      DEexn (id, dity, mask, dexpr muc denv e1)
  | Ptree.Eabsurd ->
      DEabsurd
764
  | Ptree.Epure t ->
765
      let get_term lvm _xsm old = type_term muc lvm old t in
766 767 768 769 770 771 772 773
      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)
774 775 776 777 778 779
  | 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)
780
  | Ptree.Ecast ({expr_desc = Ptree.Econst c}, pty) ->
781 782
      let ity = ity_of_pty muc pty in
      DEconst (c, dity_of_ity ity)
783
  | Ptree.Ecast (e1, pty) ->
784
      let d1 = dexpr muc denv e1 in
785
      let ity = ity_of_pty muc pty in
786 787
      DEcast (d1, ity)
  end
788 789

and drec_defn muc denv fdl =
790
  let prep (id, gh, kind, bl, pty, msk, sp, e) =
791 792 793 794 795 796 797
    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
798
    create_user_id id, gh, kind, bl, dity, msk, pre in
799 800
  Dexpr.drec_defn denv (List.map prep fdl)

801
(** Typing declarations *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
802

Andrei Paskevich's avatar
Andrei Paskevich committed
803 804
open Pdecl
open Pmodule
805

806
let add_pdecl ~vc muc d =
Andrei Paskevich's avatar
Andrei Paskevich committed
807
  if Debug.test_flag Glob.flag then Sid.iter Glob.def d.pd_news;
808
  add_pdecl ~vc muc d
Andrei Paskevich's avatar
Andrei Paskevich committed
809

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

812 813 814 815 816 817 818 819 820 821 822 823 824 825
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)

826 827
let check_public ~loc d name =
  if d.td_vis <> Public || d.td_mut then
Andrei Paskevich's avatar
Andrei Paskevich committed
828
    Loc.errorm ~loc "%s types cannot be abstract, private, or mutable" name;
829 830 831
  if d.td_inv <> [] then
    Loc.errorm ~loc "%s types cannot have invariants" name

832 833 834
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
835 836 837 838 839 840
  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
841
    match d.td_def with
Andrei Paskevich's avatar
Andrei Paskevich committed
842
    | TDalias pty ->
Andrei Paskevich's avatar
Andrei Paskevich committed
843 844 845 846 847 848
        check_public ~loc d "Alias";
        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
Andrei Paskevich's avatar
Andrei Paskevich committed
849
    | TDalgebraic csl ->
Andrei Paskevich's avatar
Andrei Paskevich committed
850
        check_public ~loc d "Algebraic";