typing.ml 59.7 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2018   --   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 Wstdlib
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 34 35
let debug_useless_at = Debug.register_flag "ignore_useless_at"
  ~desc:"Remove@ warning@ for@ useless@ at/old."

36
(** symbol lookup *)
37 38

let rec qloc = function
39 40 41
  | Qdot (p, id) -> Loc.join (qloc p) id.id_loc
  | Qident id    -> id.id_loc

42 43 44
let qloc_last = function
  | Qdot (_, id) | Qident id -> id.id_loc

45
let rec print_qualid fmt = function
46
  | Qdot (p, id) ->
47 48
      Format.fprintf fmt "%a.%a" print_qualid p Ident.print_decoded id.id_str
  | Qident id -> Ident.print_decoded fmt id.id_str
49

50 51
let string_list_of_qualid q =
  let rec sloq acc = function
52 53
    | Qdot (p, id) -> sloq (id.id_str :: acc) p
    | Qident id -> id.id_str :: acc in
54
  sloq [] q
55

56
exception UnboundSymbol of qualid
57

58
let find_qualid get_id find ns q =
59 60 61
  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
62
  if Debug.test_flag Glob.flag then Glob.use ~kind:"" (qloc_last q) (get_id r);
63
  r
64

65 66 67
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
68

69 70
let find_fsymbol_ns ns q =
  let ls = find_lsymbol_ns ns q in
71 72
  if ls.ls_value <> None then ls else
    Loc.error ~loc:(qloc q) (FunctionSymbolExpected ls)
73

74 75
let find_psymbol_ns ns q =
  let ls = find_lsymbol_ns ns q in
76 77
  if ls.ls_value = None then ls else
    Loc.error ~loc:(qloc q) (PredicateSymbolExpected ls)
78

79 80 81 82
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
83 84 85 86
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
87
  match (Mid.find pr.pr_name tuc.uc_known).d_node with
88
  | Dind _ when k = Paxiom -> pr
89 90 91
  | Dprop (l,_,_) when l = k -> pr
  | _ -> Loc.errorm ~loc:(qloc q) "proposition %a is not %s"
      print_qualid q (match k with
92
        | Plemma -> "a lemma" | Paxiom -> "an axiom" | Pgoal -> "a goal")
93

Andrei Paskevich's avatar
Andrei Paskevich committed
94 95 96
let find_itysymbol_ns ns q =
  find_qualid (fun s -> s.its_ts.ts_name) Pmodule.ns_find_its ns q

97 98 99
let find_xsymbol_ns ns q =
  find_qualid (fun s -> s.xs_name) Pmodule.ns_find_xs ns q

100 101 102
let find_prog_symbol_ns ns p =
  let get_id_ps = function
    | PV pv -> pv.pv_vs.vs_name
103 104 105 106
    | 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
107 108
  find_qualid get_id_ps ns_find_prog_symbol ns p

109 110
(** Parsing types *)

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

131 132
let dty_of_pty ns pty =
  Dterm.dty_of_ty (ty_of_pty ns pty)
133

134 135
let dty_of_opt ns = function
  | Some pty -> dty_of_pty ns pty
136 137
  | None -> Dterm.dty_fresh ()

138
(** typing using destructive type variables
139

140 141 142 143 144 145
    parsed trees        intermediate trees       typed trees
      (Ptree)                (Dterm)               (Term)
   -----------------------------------------------------------
     ppure_type  ---dty--->   dty       ---ty--->    ty
      lexpr      --dterm-->   dterm     --term-->    term
*)
146

147 148
(** Typing patterns, terms, and formulas *)

149
let create_user_prog_id {id_str = n; id_ats = attrs; id_loc = loc} =
Andrei Paskevich's avatar
Andrei Paskevich committed
150 151 152 153
  let get_attrs (attrs, loc) = function
    | ATstr attr -> Sattr.add attr attrs, loc | ATpos loc -> attrs, loc in
  let attrs, loc = List.fold_left get_attrs (Sattr.empty, loc) attrs in
  id_user ~attrs n loc
154

155 156 157 158 159 160
let create_user_id id =
  let id = create_user_prog_id id in
  if Sattr.mem Pmodule.ref_attr id.pre_attrs then Loc.errorm ?loc:id.pre_loc
    "reference markers are only admitted over program variables";
  id

161 162 163
let parse_record ~loc ns km get_val fl =
  let fl = List.map (fun (q,e) -> find_lsymbol_ns ns q, e) fl in
  let cs,pjl,flm = Loc.try2 ~loc parse_record km fl in
164 165 166
  let get_val pj = get_val cs pj (Mls.find_opt pj flm) in
  cs, List.map get_val pjl

167
let rec dpattern ns km { pat_desc = desc; pat_loc = loc } =
168 169
  match desc with
    | Ptree.Pparen p -> dpattern ns km p
170 171 172
    | Ptree.Pscope (q,p) ->
        let ns = import_namespace ns (string_list_of_qualid q) in
        dpattern ns km p
173
    | _ -> (* creative indentation ahead *)
174
  Dterm.dpattern ~loc (match desc with
175 176
    | Ptree.Pparen _
    | Ptree.Pscope _ -> assert false (* never *)
177
    | Ptree.Pwild -> DPwild
178 179
    | Ptree.Pvar x -> DPvar (create_user_id x)
    | Ptree.Papp (q,pl) ->
180 181
        let pl = List.map (dpattern ns km) pl in
        DPapp (find_lsymbol_ns ns q, pl)
182
    | Ptree.Ptuple pl ->
183
        let pl = List.map (dpattern ns km) pl in
184
        DPapp (fs_tuple (List.length pl), pl)
185
    | Ptree.Prec fl ->
186
        let get_val _ _ = function
187
          | Some p -> dpattern ns km p
188
          | None -> Dterm.dpattern DPwild in
189
        let cs,fl = parse_record ~loc ns km get_val fl in
190
        DPapp (cs,fl)
191 192 193 194 195
    | Ptree.Pas (p,x,false) -> DPas (dpattern ns km p, create_user_id x)
    | Ptree.Por (p,q) -> DPor (dpattern ns km p, dpattern ns km q)
    | Ptree.Pcast (p,ty) -> DPcast (dpattern ns km p, dty_of_pty ns ty)
    | Ptree.Pghost _ | Ptree.Pas (_,_,true) ->
        Loc.errorm ~loc "ghost patterns are only allowed in programs")
196

197
let quant_var ns (loc, id, gh, ty) =
198
  if gh then Loc.errorm ~loc "ghost variables are only allowed in programs";
199
  Opt.map create_user_id id, dty_of_opt ns ty, Some loc
200

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

207 208 209 210 211
let is_reusable dt = match dt.dt_node with
  | DTvar _ | DTgvar _ | DTconst _ | DTtrue | DTfalse -> true
  | DTapp (_,[]) -> true
  | _ -> false

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

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
229 230 231 232
(* handle auto-dereference in logical terms *)

let vs_dref vs = Sattr.mem Pmodule.ref_attr vs.vs_name.id_attrs

233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267
let to_deref = function
  | DTvar _ -> true (* needed for DEpure *)
  | DTgvar vs -> vs_dref vs
  | _ -> false

let rec underef ({dt_loc = loc} as dt) = match dt.dt_node with
  | DTuloc (dt,l) -> Dterm.dterm ?loc Coercion.empty (DTuloc (underef dt, l))
  | DTattr (dt,a) -> Dterm.dterm ?loc Coercion.empty (DTattr (underef dt, a))
  | DTcast (dt,_) -> underef dt (* already unified *)
  | DTapp (ls, [dt]) when ls_equal ls ls_ref_proj && to_deref dt.dt_node -> dt
  | _ -> raise Not_found

let undereference dt = try underef dt with Not_found ->
  Loc.errorm ?loc:dt.dt_loc "not a reference variable"

let to_underef ls el e =
  let rec down al el = match al, el with
    | (_::al), (_::el) -> down al el
    | a::_, [] when vs_dref a.pv_vs ->
        (try underef e with Not_found -> e)
    | _::_, [] -> e
    | _ -> assert false in
  match Expr.restore_rs ls with
  | rs -> down rs.rs_cty.cty_args el
  | exception Not_found -> e

let dt_app ls el =
  let rec apply al l el = match l, el with
    | ({ty_node = Tyapp (ts,_)}::l), (e::el)
      when ts_equal ts Pmodule.ts_ref ->
        (* ls may be a let-function with ref params *)
        apply (to_underef ls al e::al) l el
    | (_::l), (e::el) -> apply (e::al) l el
    | _ -> DTapp (ls, List.rev_append al el) in
  apply [] ls.ls_args el
Andrei Paskevich's avatar
Andrei Paskevich committed
268

269 270 271
(* track the use of labels *)
let at_uses = Hstr.create 5

272
let rec dterm ns km crcmap gvars at denv {term_desc = desc; term_loc = loc} =
273 274
  let func_app e el =
    List.fold_left (fun e1 (loc, e2) ->
275
      DTfapp (Dterm.dterm crcmap ~loc e1, e2)) e el
276
  in
277
  let rec apply_ls loc ls al l el = match l, el with
278 279 280 281
    | ({ty_node = Tyapp (ts,_)}::l), ((loc_e,e)::el)
      when ts_equal ts Pmodule.ts_ref ->
        (* ls may be a let-function with ref params *)
        apply_ls loc ls ((loc_e, to_underef ls al e)::al) l el
282 283
    | (_::l), (e::el) -> apply_ls loc ls (e::al) l el
    | [], _ -> func_app (DTapp (ls, List.rev_map snd al)) el
284
    | _, [] -> func_app (mk_closure crcmap loc ls) (List.rev_append al el)
285
  in
286
  let qualid_app q el = match gvars at q with
287 288 289 290 291 292 293 294
    | Some v ->
        begin match at with
        | Some l -> (* check for impact *)
            let u = Opt.get (gvars None q) in
            if not (pv_equal v u) then
              Hstr.replace at_uses l true
        | None -> ()
        end;
Andrei Paskevich's avatar
Andrei Paskevich committed
295 296 297 298 299 300
        if vs_dref v.pv_vs then
          let loc = qloc q and ls = Pmodule.ls_ref_proj in
          let e = Dterm.dterm crcmap ~loc (DTgvar v.pv_vs) in
          apply_ls loc ls [] ls.ls_args ((loc, e)::el)
        else
          func_app (DTgvar v.pv_vs) el
301
    | None ->
302
        let ls = find_lsymbol_ns ns q in
303
        apply_ls (qloc q) ls [] ls.ls_args el
304
  in
305
  let qualid_app q el = match q with
306
    | Qident {id_str = n} ->
307
        (match denv_get_opt denv n with
308 309 310 311
        | Some d -> func_app d el
        | None -> qualid_app q el)
    | _ -> qualid_app q el
  in
312
  let rec unfold_app e1 e2 el = match e1.term_desc with
313
    | Ptree.Tapply (e11,e12) ->
314
        let e12 = dterm ns km crcmap gvars at denv e12 in
315
        unfold_app e11 e12 ((e1.term_loc, e2)::el)
316
    | Ptree.Tident q ->
317
        qualid_app q ((e1.term_loc, e2)::el)
318
    | _ ->
319
        func_app (DTfapp (dterm ns km crcmap gvars at denv e1, e2)) el
320
  in
321
  Dterm.dterm crcmap ~loc (match desc with
322
  | Ptree.Tident q ->
323
      qualid_app q []
324
  | Ptree.Tidapp (q, tl) ->
325
      let tl = List.map (dterm ns km crcmap gvars at denv) tl in
326
      dt_app (find_lsymbol_ns ns q) tl
327
  | Ptree.Tapply (e1, e2) ->
328
      unfold_app e1 (dterm ns km crcmap gvars at denv e2) []
329
  | Ptree.Ttuple tl ->
330
      let tl = List.map (dterm ns km crcmap gvars at denv) tl in
331
      DTapp (fs_tuple (List.length tl), tl)
332 333 334
  | Ptree.Tinfix (e1, op1, e23)
  | Ptree.Tinnfix (e1, op1, e23) ->
      let apply loc de1 op de2 =
335 336
        if op.id_str = Ident.op_neq then
          let op = { op with id_str = Ident.op_equ } in
337
          let ls = find_lsymbol_ns ns (Qident op) in
338
          DTnot (Dterm.dterm crcmap ~loc (dt_app ls [de1;de2]))
339
        else
340
          dt_app (find_lsymbol_ns ns (Qident op)) [de1;de2] in
341 342
      let rec chain loc de1 op1 = function
        | { term_desc = Ptree.Tinfix (e2, op2, e3); term_loc = loc23 } ->
343
            let de2 = dterm ns km crcmap gvars at denv e2 in
344
            let loc12 = loc_cutoff loc loc23 e2.term_loc in
345 346
            let de12 = Dterm.dterm crcmap ~loc:loc12 (apply loc12 de1 op1 de2) in
            let de23 = Dterm.dterm crcmap ~loc:loc23 (chain loc23 de2 op2 e3) in
347
            DTbinop (DTand, de12, de23)
348
        | e23 ->
349 350
            apply loc de1 op1 (dterm ns km crcmap gvars at denv e23) in
      chain loc (dterm ns km crcmap gvars at denv e1) op1 e23
Clément Fumex's avatar
Clément Fumex committed
351
  | Ptree.Tconst (Number.ConstInt _ as c) ->
352
      DTconst (c, dty_int)
Clément Fumex's avatar
Clément Fumex committed
353
  | Ptree.Tconst (Number.ConstReal _ as c) ->
354
      DTconst (c, dty_real)
355
  | Ptree.Tlet (x, e1, e2) ->
356
      let id = create_user_id x in
357
      let e1 = dterm ns km crcmap gvars at denv e1 in
358
      let denv = denv_add_let denv e1 id in
359
      let e2 = dterm ns km crcmap gvars at denv e2 in
360
      DTlet (e1, id, e2)
361
  | Ptree.Tcase (e1, bl) ->
362
      let e1 = dterm ns km crcmap gvars at denv e1 in
363
      let branch (p, e) =
364
        let p = dpattern ns km p in
365
        let denv = denv_add_term_pat denv p e1 in
366
        p, dterm ns km crcmap gvars at denv e in
367
      DTcase (e1, List.map branch bl)
368
  | Ptree.Tif (e1, e2, e3) ->
369 370 371
      let e1 = dterm ns km crcmap gvars at denv e1 in
      let e2 = dterm ns km crcmap gvars at denv e2 in
      let e3 = dterm ns km crcmap gvars at denv e3 in
372
      DTif (e1, e2, e3)
373
  | Ptree.Ttrue ->
374
      DTtrue
375
  | Ptree.Tfalse ->
376
      DTfalse
Andrei Paskevich's avatar
Andrei Paskevich committed
377
  | Ptree.Tnot e1 ->
378
      DTnot (dterm ns km crcmap gvars at denv e1)
Andrei Paskevich's avatar
Andrei Paskevich committed
379 380 381 382
  | 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 } ->
383
            let de2 = dterm ns km crcmap gvars at denv e2 in
Andrei Paskevich's avatar
Andrei Paskevich committed
384
            let loc12 = loc_cutoff loc loc23 e2.term_loc in
385 386
            let de12 = Dterm.dterm crcmap ~loc:loc12 (DTbinop (DTiff, de1, de2)) in
            let de23 = Dterm.dterm crcmap ~loc:loc23 (chain loc23 de2 e3) in
Andrei Paskevich's avatar
Andrei Paskevich committed
387 388 389 390 391
            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 ->
392 393
            DTbinop (DTiff, de1, (dterm ns km crcmap gvars at denv e23)) in
      chain loc (dterm ns km crcmap gvars at denv e1) e23
Andrei Paskevich's avatar
Andrei Paskevich committed
394 395
  | Ptree.Tbinop (e1, op, e2)
  | Ptree.Tbinnop (e1, op, e2) ->
396 397
      let e1 = dterm ns km crcmap gvars at denv e1 in
      let e2 = dterm ns km crcmap gvars at denv e2 in
398
      DTbinop (op, e1, e2)
399
  | Ptree.Tquant (q, uqu, trl, e1) ->
400
      let qvl = List.map (quant_var ns) uqu in
401
      let denv = denv_add_quant denv qvl in
402
      let dterm e = dterm ns km crcmap gvars at denv e in
403 404
      let trl = List.map (List.map dterm) trl in
      let e1 = dterm e1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
405
      DTquant (q, qvl, trl, e1)
406
  | Ptree.Trecord fl ->
407
      let get_val _cs pj = function
408
        | Some e -> dterm ns km crcmap gvars at denv e
409
        | None -> Loc.error ~loc (RecordFieldMissing pj) in
410
      let cs, fl = parse_record ~loc ns km get_val fl in
411
      DTapp (cs, fl)
412
  | Ptree.Tupdate (e1, fl) ->
413
      let e1 = dterm ns km crcmap gvars at denv e1 in
414
      let re = is_reusable e1 in
415
      let v = if re then e1 else mk_var crcmap "q " e1 in
416
      let get_val _ pj = function
417 418
        | Some e -> dterm ns km crcmap gvars at denv e
        | None -> Dterm.dterm crcmap ~loc (DTapp (pj,[v])) in
419
      let cs, fl = parse_record ~loc ns km get_val fl in
420
      let d = DTapp (cs, fl) in
421
      if re then d else mk_let crcmap ~loc "q " e1 d
422
  | Ptree.Tat (e1, ({id_str = l; id_loc = loc} as id)) ->
423
      Hstr.add at_uses l false;
424 425 426
      let id = { id with id_str = "" } in
      (* check if the label has actually been defined *)
      ignore (Loc.try2 ~loc gvars (Some l) (Qident id));
427
      let e1 = dterm ns km crcmap gvars (Some l) denv e1 in
428 429
      if not (Hstr.find at_uses l) && Debug.test_noflag debug_useless_at then
        Warning.emit ~loc "this `at'/`old' operator is never used";
430
      Hstr.remove at_uses l;
Andrei Paskevich's avatar
Andrei Paskevich committed
431
      DTattr (e1, Sattr.empty)
Andrei Paskevich's avatar
M.()  
Andrei Paskevich committed
432
  | Ptree.Tscope (q, e1) ->
433
      let ns = import_namespace ns (string_list_of_qualid q) in
Andrei Paskevich's avatar
Andrei Paskevich committed
434
      DTattr (dterm ns km crcmap gvars at denv e1, Sattr.empty)
Andrei Paskevich's avatar
Andrei Paskevich committed
435 436 437 438
  | Ptree.Tasref q ->
      let e1 = { term_desc = Tident q; term_loc = loc } in
      let d1 = dterm ns km crcmap gvars at denv e1 in
      DTattr (undereference d1, Sattr.empty)
Andrei Paskevich's avatar
Andrei Paskevich committed
439
  | Ptree.Tattr (ATpos uloc, e1) ->
440
      DTuloc (dterm ns km crcmap gvars at denv e1, uloc)
Andrei Paskevich's avatar
Andrei Paskevich committed
441 442
  | Ptree.Tattr (ATstr attr, e1) ->
      DTattr (dterm ns km crcmap gvars at denv e1, Sattr.singleton attr)
443
  | Ptree.Tcast ({term_desc = Ptree.Tconst c}, pty) ->
444
      DTconst (c, dty_of_pty ns pty)
445
  | Ptree.Tcast (e1, pty) ->
446 447
      let d1 = dterm ns km crcmap gvars at denv e1 in
      DTcast (d1, dty_of_pty ns pty))
Andrei Paskevich's avatar
Andrei Paskevich committed
448

449 450 451 452
let no_gvars at q = match at with
  | Some _ -> Loc.errorm ~loc:(qloc q)
      "`at' and `old' can only be used in program annotations"
  | None -> None
453

454 455
let type_term_in_namespace ns km crcmap t =
  let t = dterm ns km crcmap no_gvars None Dterm.denv_empty t in
456 457
  Dterm.term ~strict:true ~keep_loc:true t

458 459
let type_fmla_in_namespace ns km crcmap f =
  let f = dterm ns km crcmap no_gvars None Dterm.denv_empty f in
460
  Dterm.fmla ~strict:true ~keep_loc:true f
Andrei Paskevich's avatar
Andrei Paskevich committed
461

462

463
(** typing program expressions *)
Andrei Paskevich's avatar
Andrei Paskevich committed
464

465 466
open Dexpr

467
let ty_of_pty tuc = ty_of_pty (get_namespace tuc)
468

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

471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490
let dterm muc =
  let uc = muc.muc_theory in
  dterm (Theory.get_namespace uc) uc.uc_known uc.uc_crcmap

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

let find_special muc test nm q =
  match find_prog_symbol muc q with
  | RS s when test s -> s
  | OO ss ->
      begin match Srs.elements (Srs.filter test ss) with
      | [s] -> s
      | _::_ -> Loc.errorm ~loc:(qloc q)
                          "Ambiguous %s notation: %a" nm print_qualid q
      | [] -> Loc.errorm ~loc:(qloc q) "Not a %s: %a" nm print_qualid q
      end
  | _ ->      Loc.errorm ~loc:(qloc q) "Not a %s: %a" nm print_qualid q

491 492 493 494 495 496 497 498 499
let rec ity_of_pty muc = 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 (ity_of_pty muc) tyl in
      Loc.try3 ~loc:(qloc q) ity_app s tyl []
  | PTtuple tyl ->
      ity_tuple (List.map (ity_of_pty muc) tyl)
500 501
  | PTref tyl ->
      ity_app its_ref (List.map (ity_of_pty muc) tyl) []
502 503 504 505 506 507 508 509 510 511
  | PTarrow (ty1, ty2) ->
      ity_func (ity_of_pty muc ty1) (ity_of_pty muc ty2)
  | PTpure ty ->
      ity_purify (ity_of_pty muc ty)
  | PTscope (q, ty) ->
      let muc = open_scope muc "dummy" in
      let muc = import_scope muc (string_list_of_qualid q) in
      ity_of_pty muc ty
  | PTparen ty ->
      ity_of_pty muc ty
512 513 514 515 516 517 518 519

let dity_of_pty muc pty =
  Dexpr.dity_of_ity (ity_of_pty muc pty)

let dity_of_opt muc = function
  | Some pty -> dity_of_pty muc pty
  | None -> Dexpr.dity_fresh ()

520 521 522
(* records *)

let find_record_field muc q =
523 524
  let test rs = rs.rs_field <> None in
  find_special muc test "record field" q
525 526 527 528 529 530 531 532 533 534 535 536

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
537
    | [{pv_ity = {ity_node = (Ityreg {reg_its = s} | Ityapp (s,_,_))}}] -> s
538 539 540 541 542 543 544 545 546 547
    | _ -> 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
548
    Mrs.add_new (DuplicateRecordField (ls_of_rs pj)) pj v m
549 550 551 552 553 554 555 556 557 558 559
    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 *)

560 561 562 563 564 565
let find_constructor muc q =
  let test rs = match rs.rs_logic with
    | RLls {ls_constr = c} -> c > 0
    | _ -> false in
  find_special muc test "constructor" q

566 567 568 569
let rec dpattern muc gh { pat_desc = desc; pat_loc = loc } =
  match desc with
    | Ptree.Pparen p -> dpattern muc gh p
    | Ptree.Pghost p -> dpattern muc true p
570 571 572 573
    | Ptree.Pscope (q,p) ->
        let muc = open_scope muc "dummy" in
        let muc = import_scope muc (string_list_of_qualid q) in
        dpattern muc gh p
574
    | _ -> (* creative indentation ahead *)
575
  Dexpr.dpattern ~loc (match desc with
576 577
    | Ptree.Pparen _ | Ptree.Pscope _
    | Ptree.Pghost _ -> assert false (* never *)
578
    | Ptree.Pwild -> DPwild
579
    | Ptree.Pvar x -> DPvar (create_user_prog_id x, gh)
580 581
    | Ptree.Papp (q,pl) ->
        DPapp (find_constructor muc q, List.map (dpattern muc gh) pl)
582 583
    | Ptree.Prec fl ->
        let get_val _ _ = function
584
          | Some p -> dpattern muc gh p
585 586 587 588
          | None -> Dexpr.dpattern DPwild in
        let cs,fl = parse_record ~loc muc get_val fl in
        DPapp (cs,fl)
    | Ptree.Ptuple pl ->
589
        DPapp (rs_tuple (List.length pl), List.map (dpattern muc gh) pl)
590 591 592 593 594 595
    | Ptree.Pcast (p,pty) ->
        DPcast (dpattern muc gh p, dity_of_pty muc pty)
    | Ptree.Pas (p,x,g) ->
        DPas (dpattern muc gh p, create_user_prog_id x, gh || g)
    | Ptree.Por (p,q) ->
        DPor (dpattern muc gh p, dpattern muc gh q))
596

597
let dpattern muc pat = dpattern muc false pat
598

599 600 601 602 603 604 605 606 607 608
(* 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

609 610
let mk_gvars muc lvm old = fun at q ->
  match find_local_pv muc lvm q, at with
611 612 613 614 615 616 617 618 619
  | Some v, Some l -> Some (old l v)
  | None, Some l ->
      begin match q with
      (* normally, we have no reason to call "old" without
         a pvsymbol, but we make an exception for an empty
         ident to check if the label is valid at Tat *)
      | Qident {id_str = ""} -> Opt.map (old l) None
      | _ -> None end
  | v, None -> v
620 621 622

let type_term muc lvm old t =
  let gvars = mk_gvars muc lvm old in
623
  let t = dterm muc gvars None Dterm.denv_empty t in
624
  Dterm.term ~strict:true ~keep_loc:true t
Andrei Paskevich's avatar
Andrei Paskevich committed
625

626 627
let type_fmla muc lvm old f =
  let gvars = mk_gvars muc lvm old in
628
  let f = dterm muc gvars None Dterm.denv_empty f in
629
  Dterm.fmla ~strict:true ~keep_loc:true f
Andrei Paskevich's avatar
Andrei Paskevich committed
630

631 632
let dpre muc pl lvm old =
  let dpre f = type_fmla muc lvm old f in
633 634
  List.map dpre pl

635
let dpost muc ql lvm old ity =
636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663
  let mk_case loc pfl =
    let v = create_pvsymbol (id_fresh "result") ity in
    let i = { id_str = "(null)"; id_loc = loc; id_ats = [] } in
    let t = { term_desc = Tident (Qident i); term_loc = loc } in
    let f = { term_desc = Ptree.Tcase (t, pfl); term_loc = loc } in
    let lvm = Mstr.add "(null)" v lvm in
    v, Loc.try3 ~loc type_fmla muc lvm old f in
  let dpost (loc,pfl) = match pfl with
    | [pat, f] ->
        let rec unfold p = match p.pat_desc with
          | Ptree.Pparen p | Ptree.Pscope (_,p) -> unfold p
          | Ptree.Pcast (p,pty) ->
              let ty = ty_of_ity (ity_of_pty muc pty) in
              Loc.try2 ~loc:p.pat_loc ty_equal_check (ty_of_ity ity) ty;
              unfold p
          | Ptree.Ptuple [] ->
              Loc.try2 ~loc:p.pat_loc ity_equal_check ity ity_unit;
              unfold { p with pat_desc = Ptree.Pwild }
          | Ptree.Pwild ->
              let v = create_pvsymbol (id_fresh "result") ity in
              v, Loc.try3 ~loc type_fmla muc lvm old f
          | Ptree.Pvar id ->
              let v = create_pvsymbol (create_user_id id) ity in
              let lvm = Mstr.add id.id_str v lvm in
              v, Loc.try3 ~loc type_fmla muc lvm old f
          | _ -> mk_case loc pfl in
        unfold pat
    | _ -> mk_case loc pfl in
664 665
  List.map dpost ql

666
let dxpost muc ql lvm xsm old =
Andrei Paskevich's avatar
Andrei Paskevich committed
667
  let add_exn (q,pf) m =
668 669 670 671 672
    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
673
    Mxs.change (fun l -> match pf, l with
Andrei Paskevich's avatar
Andrei Paskevich committed
674 675 676 677
      | Some pf, Some l -> Some (pf :: l)
      | Some pf, None   -> Some (pf :: [])
      | None,    None   -> Some []
      | None,    Some _ -> l) xs m in
678
  let mk_xpost loc xs pfl =
Andrei Paskevich's avatar
Andrei Paskevich committed
679
    if pfl = [] then [] else
680
    dpost muc [loc,pfl] lvm old xs.xs_ity in
681
  let exn_map (loc,xpfl) =
682 683
    let m = List.fold_right add_exn xpfl Mxs.empty in
    Mxs.mapi (fun xs pfl -> mk_xpost loc xs pfl) m in
684
  let add_map ql m =
685 686
    Mxs.union (fun _ l r -> Some (l @ r)) (exn_map ql) m in
  List.fold_right add_map ql Mxs.empty
687 688 689 690 691 692 693

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 =
694 695 696
  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
697 698 699 700 701 702
  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

703
let dvariant muc varl lvm _xsm old =
704
  let dvar t = type_term muc lvm old t in
705 706 707
  let dvar (t,q) = dvar t, Opt.map (find_variant_ls muc) q in
  List.map dvar varl

708
let dspec muc sp lvm xsm old ity = {
709 710
  ds_pre     = dpre muc sp.sp_pre lvm old;
  ds_post    = dpost muc sp.sp_post lvm old ity;
711
  ds_xpost   = dxpost muc sp.sp_xpost lvm xsm old;
712 713 714
  ds_reads   = dreads muc sp.sp_reads lvm;
  ds_writes  = dwrites muc sp.sp_writes lvm;
  ds_checkrw = sp.sp_checkrw;
715 716
  ds_diverge = sp.sp_diverge;
  ds_partial = sp.sp_partial; }
717

Andrei Paskevich's avatar
Andrei Paskevich committed
718 719 720 721 722
let dspec_no_variant muc sp = match sp.sp_variant with
  | ({term_loc = loc},_)::_ ->
      Loc.errorm ~loc "unexpected 'variant' clause"
  | _ -> dspec muc sp

723
let dassert muc f lvm _xsm old = type_fmla muc lvm old f
724

725
let dinvariant muc f lvm _xsm old = dpre muc f lvm old
726 727 728

(* abstract values *)

729
let dparam muc (_,id,gh,pty) =
730
  Opt.map create_user_prog_id id, gh, dity_of_pty muc pty
731

732
let dbinder muc (_,id,gh,opt) =
733
  Opt.map create_user_prog_id id, gh, dity_of_opt muc opt
734 735 736 737

(* expressions *)

let is_reusable de = match de.de_node with
738
  | DEvar _ | DEsym _ -> true | _ -> false
739

Andrei Paskevich's avatar
Andrei Paskevich committed
740 741 742
let mk_var n { de_dvty = (argl, _ as dvty); de_loc = loc } =
  let dref = List.map Util.ffalse argl, false in
  Dexpr.dexpr ?loc (DEvar (n, dvty, dref))
743 744 745 746 747

let mk_let ~loc n de node =
  let de1 = Dexpr.dexpr ~loc node in
  DElet ((id_user n loc, false, RKnone, de), de1)

748
let update_any kind e = match e.expr_desc with
749 750
  | Ptree.Eany (pl, _, pty, msk, sp) ->
      { e with expr_desc = Ptree.Eany (pl, kind, pty, msk, sp) }
751 752 753 754 755 756
  | _ -> e

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

Andrei Paskevich's avatar
Andrei Paskevich committed
757 758 759 760
let undereference ({de_loc = loc} as de) =
  try Dexpr.undereference de with Not_found ->
    Loc.errorm ?loc "not a reference variable"

761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787
let rec eff_dterm muc denv {term_desc = desc; term_loc = loc} =
  let expr_app loc e el =
    List.fold_left (fun e1 e2 ->
      DEapp (Dexpr.dexpr ~loc e1, e2)) e el
  in
  let qualid_app loc q el =
    let e = try DEsym (find_prog_symbol muc q) with
      | _ -> DEls_pure (find_lsymbol muc.muc_theory q, false) in
    expr_app loc e el
  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.Tident q ->
      qualid_app loc q []
  | Ptree.Tidapp (q, [e1]) ->
      qualid_app loc q [eff_dterm muc denv e1]
  | Ptree.Tapply (e1, e2) ->
      DEapp (eff_dterm muc denv e1, eff_dterm muc denv e2)
  | Ptree.Tscope (q, e1) ->
      let muc = open_scope muc "dummy" in
      let muc = import_scope muc (string_list_of_qualid q) in
Andrei Paskevich's avatar
Andrei Paskevich committed
788
      DEattr (eff_dterm muc denv e1, Sattr.empty)
Andrei Paskevich's avatar
Andrei Paskevich committed
789 790 791 792
  | Ptree.Tasref q ->
      let e1 = { term_desc = Tident q; term_loc = loc } in
      let d1 = eff_dterm muc denv e1 in
      DEattr (undereference d1, Sattr.empty)
Andrei Paskevich's avatar
Andrei Paskevich committed
793
  | Ptree.Tattr (ATpos uloc, e1) ->
794
      DEuloc (eff_dterm muc denv e1, uloc)
Andrei Paskevich's avatar
Andrei Paskevich committed
795 796
  | Ptree.Tattr (ATstr attr, e1) ->
      DEattr (eff_dterm muc denv e1, Sattr.singleton attr)
797 798 799 800 801
  | Ptree.Tcast (e1, pty) ->
      let d1 = eff_dterm muc denv