typing.ml 63.2 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-2019   --   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
let debug_ignore_useless_at = Debug.register_flag "ignore_useless_at"
34 35
  ~desc:"Remove@ warning@ for@ useless@ at/old."

36
(** symbol lookup *)
37

38 39 40 41 42

let qualid_last = function Qident x | Qdot (_, x) -> x

let use_as q = function Some x -> x | None -> qualid_last q

43
let rec qloc = function
44 45 46
  | Qdot (p, id) -> Loc.join (qloc p) id.id_loc
  | Qident id    -> id.id_loc

47 48 49
let qloc_last = function
  | Qdot (_, id) | Qident id -> id.id_loc

50
let rec print_qualid fmt = function
51
  | Qdot (p, id) ->
52 53
      Format.fprintf fmt "%a.%a" print_qualid p Ident.print_decoded id.id_str
  | Qident id -> Ident.print_decoded fmt id.id_str
54

55 56
let string_list_of_qualid q =
  let rec sloq acc = function
57 58
    | Qdot (p, id) -> sloq (id.id_str :: acc) p
    | Qident id -> id.id_str :: acc in
59
  sloq [] q
60

61
(* Type of symbol queried *)
62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85
type symbol_kind =
  | Prop
  | Type
  | Fun_pre
  | Fun
  | Predicate
  | Exc
  | Prog

let symbol_kind_to_string qs =
  match qs with
  | Prop      -> "proposition"
  | Type      -> "type"
  | Fun_pre   -> "function or predicate"
  | Fun       -> "function"
  | Predicate -> "predicate"
  | Exc       -> "exception"
  | Prog      -> "program function or variable"

(* [UnboundSymbol (s, q)]: s is the type of the qualid searched. It depends on
   the namespace queried: find_*_ns. *)
exception UnboundSymbol of (symbol_kind * qualid)

let find_qualid ~ty get_id find ns q =
86 87
  let sl = string_list_of_qualid q in
  let r = try find ns sl with Not_found ->
88
    Loc.error ~loc:(qloc q) (UnboundSymbol (ty, q)) in
89
  if Debug.test_flag Glob.flag then Glob.use ~kind:"" (qloc_last q) (get_id r);
90
  r
91

92 93 94 95 96 97
let find_prop_ns     ns q =
  find_qualid ~ty:Prop (fun pr -> pr.pr_name) ns_find_pr ns q
let find_tysymbol_ns ns q =
  find_qualid ~ty:Type (fun ts -> ts.ts_name) ns_find_ts ns q
let find_lsymbol_ns ?ty ns q =
  find_qualid ~ty:(Opt.get_def Fun_pre ty) (fun ls -> ls.ls_name) ns_find_ls ns q
98

99
let find_fsymbol_ns ns q =
100
  let ls = find_lsymbol_ns ~ty:Fun ns q in
101 102
  if ls.ls_value <> None then ls else
    Loc.error ~loc:(qloc q) (FunctionSymbolExpected ls)
103

104
let find_psymbol_ns ns q =
105
  let ls = find_lsymbol_ns ~ty:Predicate ns q in
106 107
  if ls.ls_value = None then ls else
    Loc.error ~loc:(qloc q) (PredicateSymbolExpected ls)
108

109 110 111 112
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
113 114 115 116
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
117
  match (Mid.find pr.pr_name tuc.uc_known).d_node with
118
  | Dind _ when k = Paxiom -> pr
119 120 121
  | Dprop (l,_,_) when l = k -> pr
  | _ -> Loc.errorm ~loc:(qloc q) "proposition %a is not %s"
      print_qualid q (match k with
122
        | Plemma -> "a lemma" | Paxiom -> "an axiom" | Pgoal -> "a goal")
123

Andrei Paskevich's avatar
Andrei Paskevich committed
124
let find_itysymbol_ns ns q =
125
  find_qualid ~ty:Type (fun s -> s.its_ts.ts_name) Pmodule.ns_find_its ns q
Andrei Paskevich's avatar
Andrei Paskevich committed
126

127
let find_xsymbol_ns ns q =
128
  find_qualid ~ty:Exc (fun s -> s.xs_name) Pmodule.ns_find_xs ns q
129

130 131 132
let find_prog_symbol_ns ns p =
  let get_id_ps = function
    | PV pv -> pv.pv_vs.vs_name
133 134 135 136
    | 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
137
  find_qualid ~ty:Prog get_id_ps ns_find_prog_symbol ns p
138

139 140
(** Parsing types *)

141 142 143 144 145 146 147 148 149 150
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)
151 152
  | PTref tyl ->
      ty_app ts_ref (List.map (ty_of_pty ns) tyl)
153 154 155 156 157 158 159
  | 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
160

161 162
let dty_of_pty ns pty =
  Dterm.dty_of_ty (ty_of_pty ns pty)
163

164 165
let dty_of_opt ns = function
  | Some pty -> dty_of_pty ns pty
166 167
  | None -> Dterm.dty_fresh ()

168
(** typing using destructive type variables
169

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

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

179
let create_user_prog_id {id_str = n; id_ats = attrs; id_loc = loc} =
Andrei Paskevich's avatar
Andrei Paskevich committed
180 181 182 183
  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
184

185 186 187 188 189 190
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

191 192 193
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
194 195 196
  let get_val pj = get_val cs pj (Mls.find_opt pj flm) in
  cs, List.map get_val pjl

197
let rec dpattern ns km { pat_desc = desc; pat_loc = loc } =
198 199
  match desc with
    | Ptree.Pparen p -> dpattern ns km p
200 201 202
    | Ptree.Pscope (q,p) ->
        let ns = import_namespace ns (string_list_of_qualid q) in
        dpattern ns km p
203
    | _ -> (* creative indentation ahead *)
204
  Dterm.dpattern ~loc (match desc with
205 206
    | Ptree.Pparen _
    | Ptree.Pscope _ -> assert false (* never *)
207
    | Ptree.Pwild -> DPwild
208 209
    | Ptree.Pvar x -> DPvar (create_user_id x)
    | Ptree.Papp (q,pl) ->
210 211
        let pl = List.map (dpattern ns km) pl in
        DPapp (find_lsymbol_ns ns q, pl)
212
    | Ptree.Ptuple pl ->
213
        let pl = List.map (dpattern ns km) pl in
214
        DPapp (fs_tuple (List.length pl), pl)
215
    | Ptree.Prec fl ->
216
        let get_val _ _ = function
217
          | Some p -> dpattern ns km p
218
          | None -> Dterm.dpattern DPwild in
219
        let cs,fl = parse_record ~loc ns km get_val fl in
220
        DPapp (cs,fl)
221 222 223 224 225
    | 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")
226

227
let quant_var ns (loc, id, gh, ty) =
228
  if gh then Loc.errorm ~loc "ghost variables are only allowed in programs";
229
  Opt.map create_user_id id, dty_of_opt ns ty, Some loc
230

231 232 233 234 235 236
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))

237 238 239 240 241
let is_reusable dt = match dt.dt_node with
  | DTvar _ | DTgvar _ | DTconst _ | DTtrue | DTfalse -> true
  | DTapp (_,[]) -> true
  | _ -> false

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

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

251 252
let mk_closure crcmap loc ls =
  let mk dt = Dterm.dterm crcmap ~loc dt in
253
  let mk_v i _ =
254 255
    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
256
  let vl = Lists.mapi mk_v ls.ls_args in
Andrei Paskevich's avatar
Andrei Paskevich committed
257
  DTquant (DTlambda, vl, [], mk (DTapp (ls, List.map mk_t vl)))
258

Andrei Paskevich's avatar
Andrei Paskevich committed
259 260 261 262
(* handle auto-dereference in logical terms *)

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

263 264 265 266
let rec to_deref = function
  | DTattr ({dt_node = DTvar _}, attrs)
    when Sattr.mem Pmodule.ref_attr attrs -> true (* needed for DEpure *)
  | DTattr (dt,_) | DTuloc (dt,_) | DTcast (dt,_) -> to_deref dt.dt_node
267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299
  | 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
300

301 302 303
(* track the use of labels *)
let at_uses = Hstr.create 5

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

487 488 489 490
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
491

492 493
let type_term_in_namespace ns km crcmap t =
  let t = dterm ns km crcmap no_gvars None Dterm.denv_empty t in
494 495
  Dterm.term ~strict:true ~keep_loc:true t

496 497
let type_fmla_in_namespace ns km crcmap f =
  let f = dterm ns km crcmap no_gvars None Dterm.denv_empty f in
498
  Dterm.fmla ~strict:true ~keep_loc:true f
Andrei Paskevich's avatar
Andrei Paskevich committed
499

500

501
(** typing program expressions *)
Andrei Paskevich's avatar
Andrei Paskevich committed
502

503 504
open Dexpr

505
let ty_of_pty tuc = ty_of_pty (get_namespace tuc)
506

507
let get_namespace muc = List.hd muc.Pmodule.muc_import
508
let get_namespace_export muc = List.hd muc.Pmodule.muc_export
509

510 511 512 513 514 515 516 517
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

518
let find_rsymbol muc q =
519 520
  let ns = get_namespace_export muc in
  find_qualid ~ty:Prog (fun rs -> rs.rs_name) ns_find_rs ns q
521

522 523 524 525 526 527 528 529 530 531 532 533
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

534 535 536 537 538 539 540 541 542
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)
543 544
  | PTref tyl ->
      ity_app its_ref (List.map (ity_of_pty muc) tyl) []
545 546 547 548 549 550 551 552 553 554
  | 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
555 556 557 558 559 560 561 562

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 ()

563 564 565
(* records *)

let find_record_field muc q =
566 567
  let test rs = rs.rs_field <> None in
  find_special muc test "record field" q
568 569 570 571 572 573 574 575 576 577 578 579

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
580
    | [{pv_ity = {ity_node = (Ityreg {reg_its = s} | Ityapp (s,_,_))}}] -> s
581 582 583 584 585 586 587 588 589 590
    | _ -> 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
591
    Mrs.add_new (DuplicateRecordField (ls_of_rs pj)) pj v m
592 593 594 595 596 597 598 599 600 601 602
    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 *)

603 604 605 606 607 608
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

609 610 611 612
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
613 614 615 616
    | 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
617
    | _ -> (* creative indentation ahead *)
618
  Dexpr.dpattern ~loc (match desc with
619 620
    | Ptree.Pparen _ | Ptree.Pscope _
    | Ptree.Pghost _ -> assert false (* never *)
621
    | Ptree.Pwild -> DPwild
622
    | Ptree.Pvar x -> DPvar (create_user_prog_id x, gh)
623 624
    | Ptree.Papp (q,pl) ->
        DPapp (find_constructor muc q, List.map (dpattern muc gh) pl)
625 626
    | Ptree.Prec fl ->
        let get_val _ _ = function
627
          | Some p -> dpattern muc gh p
628 629 630 631
          | None -> Dexpr.dpattern DPwild in
        let cs,fl = parse_record ~loc muc get_val fl in
        DPapp (cs,fl)
    | Ptree.Ptuple pl ->
632
        DPapp (rs_tuple (List.length pl), List.map (dpattern muc gh) pl)
633 634 635 636 637 638
    | 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))
639

640
let dpattern muc pat = dpattern muc false pat
641

642 643 644 645 646 647 648 649 650 651
(* 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

652 653
let mk_gvars muc lvm old = fun at q ->
  match find_local_pv muc lvm q, at with
654 655 656 657 658 659 660 661 662
  | 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
663 664 665

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

669 670
let type_fmla muc lvm old f =
  let gvars = mk_gvars muc lvm old in
671
  let f = dterm muc gvars None Dterm.denv_empty f in
672
  Dterm.fmla ~strict:true ~keep_loc:true f
Andrei Paskevich's avatar
Andrei Paskevich committed
673

674 675
let dpre muc pl lvm old =
  let dpre f = type_fmla muc lvm old f in
676 677
  List.map dpre pl

678
let dpost muc ql lvm old ity =
679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706
  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
707 708
  List.map dpost ql

709
let dxpost muc ql lvm xsm old =
Andrei Paskevich's avatar
Andrei Paskevich committed
710
  let add_exn (q,pf) m =
711 712 713 714 715
    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
716
    Mxs.change (fun l -> match pf, l with
Andrei Paskevich's avatar
Andrei Paskevich committed
717 718 719 720
      | Some pf, Some l -> Some (pf :: l)
      | Some pf, None   -> Some (pf :: [])
      | None,    None   -> Some []
      | None,    Some _ -> l) xs m in
721
  let mk_xpost loc xs pfl =
Andrei Paskevich's avatar
Andrei Paskevich committed
722
    if pfl = [] then [] else
723
    dpost muc [loc,pfl] lvm old xs.xs_ity in
724
  let exn_map (loc,xpfl) =
725 726
    let m = List.fold_right add_exn xpfl Mxs.empty in
    Mxs.mapi (fun xs pfl -> mk_xpost loc xs pfl) m in
727
  let add_map ql m =
728 729
    Mxs.union (fun _ l r -> Some (l @ r)) (exn_map ql) m in
  List.fold_right add_map ql Mxs.empty
730 731 732 733 734 735 736

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 =
737 738 739
  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
740 741 742 743 744 745
  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

746
let dvariant muc varl lvm _xsm old =
747
  let dvar t = type_term muc lvm old t in
748 749 750
  let dvar (t,q) = dvar t, Opt.map (find_variant_ls muc) q in
  List.map dvar varl

751
let dspec muc sp lvm xsm old ity = {
752 753
  ds_pre     = dpre muc sp.sp_pre lvm old;
  ds_post    = dpost muc sp.sp_post lvm old ity;
754
  ds_xpost   = dxpost muc sp.sp_xpost lvm xsm old;
755 756 757
  ds_reads   = dreads muc sp.sp_reads lvm;
  ds_writes  = dwrites muc sp.sp_writes lvm;
  ds_checkrw = sp.sp_checkrw;
758 759
  ds_diverge = sp.sp_diverge;
  ds_partial = sp.sp_partial; }
760

Andrei Paskevich's avatar
Andrei Paskevich committed
761 762 763 764 765
let dspec_no_variant muc sp = match sp.sp_variant with
  | ({term_loc = loc},_)::_ ->
      Loc.errorm ~loc "unexpected 'variant' clause"
  | _ -> dspec muc sp

766
let dassert muc f lvm _xsm old = type_fmla muc lvm old f
767

768
let dinvariant muc f lvm _xsm old = dpre muc f lvm old
769 770 771

(* abstract values *)

772
let dparam muc (_,id,gh,pty) =
773
  Opt.map create_user_prog_id id, gh, dity_of_pty muc pty
774

775
let dbinder muc (_,id,gh,opt) =
776
  Opt.map create_user_prog_id id, gh, dity_of_opt muc opt
777 778 779 780

(* expressions *)

let is_reusable de = match de.de_node with