mlw_typing.ml 71.2 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3 4 5 6 7 8 9 10
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2012   --   INRIA - CNRS - Paris-Sud University  *)
(*                                                                  *)
(*  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.                           *)
(*                                                                  *)
(********************************************************************)
11

12
open Stdlib
13
open Ident
14 15 16
open Ty
open Term
open Decl
17 18 19
open Theory
open Env
open Ptree
20
open Mlw_dtree
21
open Mlw_ty
22
open Mlw_ty.T
23 24
open Mlw_expr
open Mlw_decl
25
open Mlw_pretty
26
open Mlw_module
Andrei Paskevich's avatar
Andrei Paskevich committed
27
open Mlw_wp
28
open Mlw_dty
29

30 31
(** errors *)

32
exception DuplicateProgVar of string
33 34 35 36 37 38 39 40 41 42 43
exception DuplicateTypeVar of string
(*
exception PredicateExpected
exception TermExpected
exception FSymExpected of lsymbol
exception PSymExpected of lsymbol
exception ClashTheory of string
exception UnboundTheory of qualid
exception UnboundType of string list
*)
exception UnboundTypeVar of string
44
exception UnboundSymbol of qualid
45 46 47 48

let error = Loc.error
let errorm = Loc.errorm

49 50
let qloc = Typing.qloc
let print_qualid = Typing.print_qualid
51 52 53

let () = Exn_printer.register (fun fmt e -> match e with
  | DuplicateTypeVar s ->
54 55 56
      Format.fprintf fmt "Type parameter %s is used twice" s
  | DuplicateProgVar s ->
      Format.fprintf fmt "Parameter %s is used twice" s
57 58 59
  | TooLateInvariant ->
      Format.fprintf fmt
        "Cannot add a type invariant after another program declaration"
60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77
(*
  | PredicateExpected ->
      Format.fprintf fmt "syntax error: predicate expected"
  | TermExpected ->
      Format.fprintf fmt "syntax error: term expected"
  | FSymExpected ls ->
      Format.fprintf fmt "%a is not a function symbol" Pretty.print_ls ls
  | PSymExpected ls ->
      Format.fprintf fmt "%a is not a predicate symbol" Pretty.print_ls ls
  | ClashTheory s ->
      Format.fprintf fmt "Clash with previous theory %s" s
  | UnboundTheory q ->
      Format.fprintf fmt "unbound theory %a" print_qualid q
  | UnboundType sl ->
      Format.fprintf fmt "Unbound type '%a'"
        (Pp.print_list Pp.dot Pp.pp_print_string) sl
*)
  | UnboundTypeVar s ->
78 79 80
      Format.fprintf fmt "Unbound type variable '%s" s
  | UnboundSymbol q ->
      Format.fprintf fmt "Unbound symbol '%a'" print_qualid q
81 82 83
  | _ -> raise e)

(* TODO: let type_only = Debug.test_flag Typing.debug_type_only in *)
84 85
let implicit_post = Debug.register_flag "implicit_post"
  ~desc:"Generate@ a@ postcondition@ for@ pure@ functions@ without@ one."
86

87 88
type denv = {
  uc     : module_uc;
89
  locals : (tvars option * dvty) Mstr.t;
90
  tvars  : tvars;
Andrei Paskevich's avatar
Andrei Paskevich committed
91
  uloc   : Ptree.loc option;
92
}
93

94 95 96 97
let create_denv uc = {
  uc     = uc;
  locals = Mstr.empty;
  tvars  = empty_tvars;
Andrei Paskevich's avatar
Andrei Paskevich committed
98
  uloc   = None;
99
}
100

101 102
(* Handle tuple symbols *)

103 104 105
let ht_tuple   = Hint.create 3
let ts_tuple n = Hint.replace ht_tuple n (); ts_tuple n
let fs_tuple n = Hint.replace ht_tuple n (); fs_tuple n
106

107
let check_at f0 =
Andrei Paskevich's avatar
Andrei Paskevich committed
108 109 110 111 112 113 114 115 116 117 118 119
  let rec check f = match f.t_node with
    | Term.Tapp (ls, _) when ls_equal ls fs_at ->
        let d = Mvs.set_diff f.t_vars f0.t_vars in
        if not (Mvs.is_empty d) then errorm ?loc:f.t_loc
          "locally bound variable %a under `at'"
          Pretty.print_vs (fst (Mvs.choose d))
        else true
    | _ ->
        t_all check f
  in
  ignore (check f0)

120 121
let count_term_tuples t =
  let syms_ts _ ts = match is_ts_tuple_id ts.ts_name with
122
    | Some n -> Hint.replace ht_tuple n () | _ -> () in
123 124 125
  let syms_ty _ ty = ty_s_fold syms_ts () ty in
  t_s_fold syms_ty (fun _ _ -> ()) () t

126
let flush_tuples uc =
127 128
  let kn = Theory.get_known (get_theory uc) in
  let add_tuple n _ uc =
Andrei Paskevich's avatar
Andrei Paskevich committed
129
    if Mid.mem (Ty.ts_tuple n).ts_name kn then uc
130
    else use_export_theory uc (tuple_theory n) in
131 132
  let uc = Hint.fold add_tuple ht_tuple uc in
  Hint.clear ht_tuple;
133 134
  uc

135
let add_pdecl_with_tuples ~wp uc pd = add_pdecl ~wp (flush_tuples uc) pd
136
let add_decl_with_tuples uc d = add_decl (flush_tuples uc) d
137

138 139 140
(** Namespace lookup *)

let uc_find_ls uc p =
141 142
  let ns = Theory.get_namespace (get_theory uc) in
  Typing.find_ns (fun ls -> ls.ls_name) Theory.ns_find_ls p ns
143

144
let get_id_ts = function
145
  | PT pt -> pt.its_ts.ts_name
146
  | TS ts -> ts.ts_name
Andrei Paskevich's avatar
Andrei Paskevich committed
147

148
let uc_find_ts uc p =
149 150 151 152 153 154 155 156
  Typing.find_ns get_id_ts ns_find_ts p (get_namespace uc)

let get_id_ps = function
  | PV pv -> pv.pv_vs.vs_name
  | PS ps -> ps.ps_name
  | PL pl -> pl.pl_ls.ls_name
  | XS xs -> xs.xs_name
  | LS ls -> ls.ls_name
Andrei Paskevich's avatar
Andrei Paskevich committed
157

158
let uc_find_ps uc p =
159
  Typing.find_ns get_id_ps ns_find_ps p (get_namespace uc)
160

161 162
(** Typing type expressions *)

163
let rec dity_of_pty denv = function
164 165 166
  | Ptree.PPTtyvar id ->
      create_user_type_variable id
  | Ptree.PPTtyapp (pl, p) ->
167
      let dl = List.map (dity_of_pty denv) pl in
168
      begin match uc_find_ts denv.uc p with
169
        | PT ts -> its_app ts dl
170
        | TS ts -> ts_app ts dl
171 172
      end
  | Ptree.PPTtuple pl ->
173
      let dl = List.map (dity_of_pty denv) pl in
174
      ts_app (ts_tuple (List.length pl)) dl
175 176 177

(** Typing program expressions *)

Andrei Paskevich's avatar
Andrei Paskevich committed
178
let dity_int  = ts_app ts_int  []
179
let dity_real = ts_app ts_real []
180
let dity_bool = ts_app ts_bool []
Andrei Paskevich's avatar
Andrei Paskevich committed
181
let dity_unit = ts_app ts_unit []
182

183
let unify_loc unify_fn loc x1 x2 = try unify_fn x1 x2 with
Andrei Paskevich's avatar
Andrei Paskevich committed
184
  | TypeMismatch (ity1,ity2,_) -> errorm ~loc
185
      "This expression has type %a,@ but is expected to have type %a"
186
      Mlw_pretty.print_ity ity2 Mlw_pretty.print_ity ity1
Andrei Paskevich's avatar
Andrei Paskevich committed
187 188 189
  | DTypeMismatch (dity1,dity2) -> errorm ~loc
      "This expression has type %a,@ but is expected to have type %a"
      Mlw_dty.print_dity dity2 Mlw_dty.print_dity dity1
190
  | exn when Debug.test_noflag Debug.stack_trace -> error ~loc exn
191

192 193 194 195 196 197 198
let expected_type { de_loc = loc ; de_type = (argl,res) } dity =
  if argl <> [] then errorm ~loc "This expression is not a first-order value";
  unify_loc unify loc dity res

let expected_type_weak { de_loc = loc ; de_type = (argl,res) } dity =
  if argl <> [] then errorm ~loc "This expression is not a first-order value";
  unify_loc unify_weak loc dity res
199

200
let rec extract_labels labs loc e = match e.Ptree.expr_desc with
201
  | Ptree.Enamed (Ptree.Lstr s, e) -> extract_labels (Slab.add s labs) loc e
202 203 204 205
  | Ptree.Enamed (Ptree.Lpos p, e) -> extract_labels labs (Some p) e
  | Ptree.Ecast  (e, ty) ->
      let labs, loc, d = extract_labels labs loc e in
      labs, loc, Ptree.Ecast ({ e with Ptree.expr_desc = d }, ty)
206
  | e -> labs, loc, e
207

208 209 210
let rec decompose_app args e = match e.Ptree.expr_desc with
  | Eapply (e1, e2) -> decompose_app (e2 :: args) e1
  | _ -> e, args
211

212 213 214 215 216 217 218 219 220 221
(* record parsing *)

let parse_record uc fll =
  let pl = match fll with
    | [] -> raise EmptyRecord
    | (pl,_)::_ -> pl in
  let its = match pl.pl_args with
    | [{ vtv_ity = { ity_node = Ityapp (its,_,_) }}] -> its
    | _ -> raise (BadRecordField pl.pl_ls) in
  let cs, pjl = match find_constructors (get_known uc) its with
222
    | [cs,pjl] -> cs, List.map (Opt.get_exn (BadRecordField pl.pl_ls)) pjl
223 224 225 226 227 228 229 230 231
    | _ -> raise (BadRecordField pl.pl_ls) in
  let pjs = List.fold_left (fun s pj -> Sls.add pj.pl_ls s) Sls.empty pjl in
  let flm = List.fold_left (fun m (pj,v) -> let pj = pj.pl_ls in
    if not (Sls.mem pj pjs) then raise (BadRecordField pj) else
      Mls.add_new (DuplicateRecordField (cs.pl_ls,pj)) pj v m)
    Mls.empty fll
  in
  cs,pjl,flm

232 233
let find_prog_field uc (p,e) = match uc_find_ps uc p with PL pl -> pl, e
  | _ -> errorm ~loc:(qloc p) "'%a' is not a record field" print_qualid p
234

235
let find_pure_field uc (p,e) = uc_find_ls uc p, e
236

237 238
let is_pure_record uc = function
  | fl :: _ -> (try ignore (find_prog_field uc fl); false with _ -> true)
239
  | [] -> raise Decl.EmptyRecord
240 241

let hidden_pl ~loc pl =
242 243
  { de_desc = DEglobal_pl pl;
    de_type = specialize_plsymbol pl;
244
    de_loc  = loc; de_lab = Slab.empty }
245 246

let hidden_ls ~loc ls =
247
  { de_desc = DEglobal_ls ls;
248
    de_type = Loc.try1 loc specialize_lsymbol ls;
249
    de_loc  = loc; de_lab = Slab.empty }
250 251

(* helper functions for let-expansion *)
252
let test_var e = match e.de_desc with
253 254 255 256 257
  | DElocal _ | DEglobal_pv _ -> true
  | _ -> false

let mk_var e =
  if test_var e then e else
258 259 260
  { de_desc = DElocal "q";
    de_type = e.de_type;
    de_loc  = e.de_loc;
261
    de_lab  = Slab.empty }
262

263 264 265
let mk_id s loc =
  { id = s; id_loc = loc; id_lab = [] }

266 267
let mk_dexpr desc dvty loc labs =
  { de_desc = desc; de_type = dvty; de_loc = loc; de_lab = labs }
268

269 270
let mk_let ~loc ~uloc e (desc,dvty) =
  if test_var e then desc, dvty else
271
  let loc = Opt.get_def loc uloc in
272
  let e1 = mk_dexpr desc dvty loc Slab.empty in
273
  DElet (mk_id "q" e.de_loc, false, e, e1), dvty
274

275 276
(* patterns *)

277 278 279 280 281 282 283 284 285
let add_poly id dvty denv =
  let locals = Mstr.add id.id (Some denv.tvars, dvty) denv.locals in
  { denv with locals = locals }

let add_mono id dvty denv =
  let locals = Mstr.add id.id (None, dvty) denv.locals in
  { denv with locals = locals; tvars = add_dvty denv.tvars dvty }

let add_var id dity denv = add_mono id ([],dity) denv
286

287
let specialize_qualid uc p = match uc_find_ps uc p with
288
  | PV pv -> DEglobal_pv pv, ([],specialize_pvsymbol pv)
289 290
  | PS ps -> DEglobal_ps ps, specialize_psymbol  ps
  | PL pl -> DEglobal_pl pl, specialize_plsymbol pl
291
  | LS ls -> DEglobal_ls ls, Loc.try1 (qloc p) specialize_lsymbol ls
292
  | XS xs -> errorm ~loc:(qloc p) "unexpected exception symbol %a" print_xs xs
293

294 295
let find_xsymbol uc p = match uc_find_ps uc p with
  | XS xs -> xs
296
  | _ -> errorm ~loc:(qloc p) "exception symbol expected"
Andrei Paskevich's avatar
Andrei Paskevich committed
297

298
let find_variant_ls uc p = match uc_find_ls uc p with
299 300
  | { ls_args = [u;v]; ls_value = None } as ls when ty_equal u v -> ls
  | ls -> errorm ~loc:(qloc p) "%a is not a binary relation" Pretty.print_ls ls
301

302
let find_global_vs uc p = try match uc_find_ps uc p with
303 304
  | PV pv -> Some pv.pv_vs
  | _ -> None
305
  with _ -> None
306

307 308 309 310 311 312
let find_vs uc lvm p = match p with
  | Qdot _ -> find_global_vs uc p
  | Qident id ->
      let ovs = Mstr.find_opt id.id lvm in
      if ovs = None then find_global_vs uc p else ovs

313 314 315 316 317
let rec dpattern denv ({ pat_loc = loc } as pp) = match pp.pat_desc with
  | Ptree.PPpwild ->
      PPwild, create_type_variable (), denv
  | Ptree.PPpvar id ->
      let dity = create_type_variable () in
318
      PPvar (Denv.create_user_id id), dity, add_var id dity denv
319
  | Ptree.PPpapp (q,ppl) ->
320 321
      let sym, dvty = specialize_qualid denv.uc q in
      dpat_app denv loc (mk_dexpr sym dvty loc Slab.empty) ppl
322
  | Ptree.PPprec fl when is_pure_record denv.uc fl ->
323
      let kn = Theory.get_known (get_theory denv.uc) in
324
      let fl = List.map (find_pure_field denv.uc) fl in
325 326 327
      let cs,pjl,flm = Loc.try2 loc Decl.parse_record kn fl in
      let wild = { pat_desc = Ptree.PPpwild; pat_loc = loc } in
      let get_val pj = Mls.find_def wild pj flm in
328
      dpat_app denv loc (hidden_ls ~loc cs) (List.map get_val pjl)
329
  | Ptree.PPprec fl ->
330
      let fl = List.map (find_prog_field denv.uc) fl in
331 332 333
      let cs,pjl,flm = Loc.try2 loc parse_record denv.uc fl in
      let wild = { pat_desc = Ptree.PPpwild; pat_loc = loc } in
      let get_val pj = Mls.find_def wild pj.pl_ls flm in
334
      dpat_app denv loc (hidden_pl ~loc cs) (List.map get_val pjl)
335 336
  | Ptree.PPptuple ppl ->
      let cs = fs_tuple (List.length ppl) in
337 338 339 340
      dpat_app denv loc (hidden_ls ~loc cs) ppl
  | Ptree.PPpor (lpp1, lpp2) ->
      let pp1, dity1, denv = dpattern denv lpp1 in
      let pp2, dity2, denv = dpattern denv lpp2 in
341
      unify_loc unify lpp2.pat_loc dity1 dity2;
342 343 344
      PPor (pp1, pp2), dity1, denv
  | Ptree.PPpas (pp, id) ->
      let pp, dity, denv = dpattern denv pp in
345
      PPas (pp, Denv.create_user_id id), dity, add_var id dity denv
346

347 348 349 350
and dpat_app denv gloc ({ de_loc = loc } as de) ppl =
  let add_pp lp (ppl, tyl, denv) =
    let pp, ty, denv = dpattern denv lp in
    pp::ppl, (lp.pat_loc,ty)::tyl, denv in
351
  let ppl, tyl, denv = List.fold_right add_pp ppl ([],[],denv) in
352 353 354
  let pp, ls = match de.de_desc with
    | DEglobal_pl pl -> Mlw_expr.PPpapp (pl, ppl), pl.pl_ls
    | DEglobal_ls ls -> Mlw_expr.PPlapp (ls, ppl), ls
355 356
    | DEglobal_pv pv -> errorm ~loc "%a is not a constructor" print_pv pv
    | DEglobal_ps ps -> errorm ~loc "%a is not a constructor" print_ps ps
357 358
    | _ -> assert false
  in
359 360 361 362 363
  let argl, res = de.de_type in
  if List.length argl <> List.length ppl then error ~loc:gloc
    (Term.BadArity (ls, List.length argl, List.length ppl));
  let unify_arg ta (loc,tv) = unify_loc unify loc ta tv in
  List.iter2 unify_arg argl tyl;
364 365
  pp, res, denv

366 367
(* specifications *)

368
let dbinders denv bl =
369
  let hv = Hstr.create 3 in
370
  let dbinder (id,gh,pty) (denv,bl,tyl) =
371 372
    if Hstr.mem hv id.id then raise (DuplicateProgVar id.id);
    Hstr.add hv id.id ();
373
    let dity = match pty with
374
      | Some pty -> dity_of_pty denv pty
375
      | None -> create_type_variable () in
376
    add_var id dity denv, (id,gh,dity)::bl, dity::tyl
377 378
  in
  List.fold_right dbinder bl (denv,[],[])
379

380
let mk_dpost loc = function
381
  | [{ pat_desc = PPpwild | PPptuple [] | PPpvar _ }, _ as p] -> p
382
  | l ->
383 384 385 386
      let i = { id = "(null)"; id_loc = loc; id_lab = [] } in
      let p = { pat_desc = Ptree.PPpvar i; pat_loc = loc } in
      let v = { pp_desc = Ptree.PPvar (Qident i); pp_loc = loc } in
      p, { pp_desc = PPmatch (v,l); pp_loc = loc }
387 388

let dpost ql = List.map (fun (loc, ql) -> mk_dpost loc ql) ql
389 390

let dxpost uc ql =
391
  let add_exn (q,pat,f) m =
392
    let xs = find_xsymbol uc q in
393 394 395 396 397 398
    Mexn.change (function
      | Some l -> Some ((pat,f) :: l)
      | None   -> Some ((pat,f) :: [])) xs m in
  let exn_map (loc,ql) =
    let m = List.fold_right add_exn ql Mexn.empty in
    Mexn.map (fun ql -> [mk_dpost loc ql]) m in
399 400 401
  let add_map ql m =
    Mexn.union (fun _ l r -> Some (l @ r)) (exn_map ql) m in
  List.fold_right add_map ql Mexn.empty
402 403

let dvariant uc var =
404
  List.map (fun (le,q) -> le, Opt.map (find_variant_ls uc) q) var
405 406 407

let dspec uc sp = {
  ds_pre     = sp.sp_pre;
408
  ds_post    = dpost sp.sp_post;
409
  ds_xpost   = dxpost uc sp.sp_xpost;
410 411
  ds_reads   = sp.sp_reads;
  ds_writes  = sp.sp_writes;
412 413
  ds_variant = dvariant uc sp.sp_variant;
}
414

415 416 417
let rec dtype_c denv (tyv, sp) =
  let tyv, dvty = dtype_v denv tyv in
  (tyv, dspec denv.uc sp), dvty
418 419 420

and dtype_v denv = function
  | Tpure pty ->
421
      let dity = dity_of_pty denv pty in
422
      DSpecV (false,dity), ([],dity)
423 424
  | Tarrow (bl,tyc) ->
      let denv,bl,tyl = dbinders denv bl in
425 426
      let tyc,(argl,res) = dtype_c denv tyc in
      DSpecA (bl,tyc), (tyl @ argl,res)
427

428
(* expressions *)
429

430
let de_unit ~loc = hidden_ls ~loc Mlw_expr.fs_void
431

432 433 434 435 436 437 438 439 440 441 442 443 444 445
let de_app _loc e el =
  let argl, res = e.de_type in
  let rec unify_list argl el = match argl, el with
    | arg::argl, e::el when Loc.equal e.de_loc Loc.dummy_position ->
        expected_type e arg; unify_list argl el
    | arg::argl, e::el ->
        let res = unify_list argl el in expected_type e arg; res
    | argl, [] -> argl, res
    | [], _ when fst e.de_type = [] -> errorm ~loc:e.de_loc
        "This expression is not a function and cannot be applied"
    | [], _ -> errorm ~loc:e.de_loc
        "This function is applied to too many arguments"
  in
  DEapply (e, el), unify_list argl el
446

Andrei Paskevich's avatar
Andrei Paskevich committed
447
let rec dexpr denv e =
448
  let loc = e.Ptree.expr_loc in
449
  let labs, uloc, d = extract_labels Slab.empty denv.uloc e in
Andrei Paskevich's avatar
Andrei Paskevich committed
450
  let denv = { denv with uloc = uloc } in
451
  let d, ty = de_desc denv loc d in
452
  let loc = Opt.get_def loc uloc in
453
  mk_dexpr d ty loc labs
454

455
and de_desc denv loc = function
456 457 458 459 460 461
  | Ptree.Eident (Qident {id = x} as p) ->
      begin match Mstr.find_opt x denv.locals with
        | Some (Some tvs, dvty) -> DElocal x, specialize_scheme tvs dvty
        | Some (None,     dvty) -> DElocal x, dvty
        | None                  -> specialize_qualid denv.uc p
      end
462
  | Ptree.Eident p ->
463
      specialize_qualid denv.uc p
464 465
  | Ptree.Eapply (e1, e2) ->
      let e, el = decompose_app [e2] e1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
466
      let el = List.map (dexpr denv) el in
467
      de_app loc (dexpr denv e) el
468
  | Ptree.Elet (id, gh, e1, e2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
469
      let e1 = dexpr denv e1 in
470 471 472
      let denv = match e1.de_desc with
        | DEfun _ -> add_poly id e1.de_type denv
        | _       -> add_mono id e1.de_type denv in
Andrei Paskevich's avatar
Andrei Paskevich committed
473
      let e2 = dexpr denv e2 in
474
      DElet (id, gh, e1, e2), e2.de_type
475 476
  | Ptree.Eletrec (fdl, e1) ->
      let fdl = dletrec denv fdl in
477
      let add_one denv (id,_,dvty,_,_) = add_poly id dvty denv in
478
      let denv = List.fold_left add_one denv fdl in
Andrei Paskevich's avatar
Andrei Paskevich committed
479
      let e1 = dexpr denv e1 in
480
      DEletrec (fdl, e1), e1.de_type
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
481
  | Ptree.Efun (bl, tr) ->
482
      let denv, bl, tyl = dbinders denv bl in
483
      let tr, (argl, res) = dtriple denv tr in
484
      DEfun (bl, tr), (tyl @ argl, res)
485
  | Ptree.Ecast (e1, pty) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
486
      let e1 = dexpr denv e1 in
487
      expected_type e1 (dity_of_pty denv pty);
488
      e1.de_desc, e1.de_type
489 490
  | Ptree.Enamed _ ->
      assert false
491
  | Ptree.Esequence (e1, e2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
492
      let e1 = dexpr denv e1 in
493
      expected_type e1 dity_unit;
Andrei Paskevich's avatar
Andrei Paskevich committed
494
      let e2 = dexpr denv e2 in
495
      DElet (mk_id "_" loc, false, e1, e2), e2.de_type
496
  | Ptree.Eif (e1, e2, e3) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
497
      let e1 = dexpr denv e1 in
498
      expected_type e1 dity_bool;
Andrei Paskevich's avatar
Andrei Paskevich committed
499 500
      let e2 = dexpr denv e2 in
      let e3 = dexpr denv e3 in
501 502 503
      let res = create_type_variable () in
      expected_type e2 res;
      expected_type e3 res;
504
      DEif (e1, e2, e3), e2.de_type
505 506
  | Ptree.Etuple el ->
      let ls = fs_tuple (List.length el) in
Andrei Paskevich's avatar
Andrei Paskevich committed
507
      let el = List.map (dexpr denv) el in
508
      de_app loc (hidden_ls ~loc ls) el
509
  | Ptree.Erecord fl when is_pure_record denv.uc fl ->
510
      let kn = Theory.get_known (get_theory denv.uc) in
511
      let fl = List.map (find_pure_field denv.uc) fl in
512 513
      let cs,pjl,flm = Loc.try2 loc Decl.parse_record kn fl in
      let get_val pj = match Mls.find_opt pj flm with
Andrei Paskevich's avatar
Andrei Paskevich committed
514
        | Some e -> dexpr denv e
515
        | None -> error ~loc (Decl.RecordFieldMissing (cs,pj)) in
516
      de_app loc (hidden_ls ~loc cs) (List.map get_val pjl)
517
  | Ptree.Erecord fl ->
518
      let fl = List.map (find_prog_field denv.uc) fl in
519 520
      let cs,pjl,flm = Loc.try2 loc parse_record denv.uc fl in
      let get_val pj = match Mls.find_opt pj.pl_ls flm with
Andrei Paskevich's avatar
Andrei Paskevich committed
521
        | Some e -> dexpr denv e
522
        | None -> error ~loc (Decl.RecordFieldMissing (cs.pl_ls,pj.pl_ls)) in
523
      de_app loc (hidden_pl ~loc cs) (List.map get_val pjl)
524
  | Ptree.Eupdate (e1, fl) when is_pure_record denv.uc fl ->
Andrei Paskevich's avatar
Andrei Paskevich committed
525
      let e1 = dexpr denv e1 in
526 527
      let e0 = mk_var e1 in
      let kn = Theory.get_known (get_theory denv.uc) in
528
      let fl = List.map (find_pure_field denv.uc) fl in
529 530
      let cs,pjl,flm = Loc.try2 loc Decl.parse_record kn fl in
      let get_val pj = match Mls.find_opt pj flm with
Andrei Paskevich's avatar
Andrei Paskevich committed
531
        | Some e -> dexpr denv e
532
        | None ->
533
            let loc = Loc.dummy_position in
534 535
            let d, dvty = de_app loc (hidden_ls ~loc pj) [e0] in
            mk_dexpr d dvty loc Slab.empty in
536
      let res = de_app loc (hidden_ls ~loc cs) (List.map get_val pjl) in
Andrei Paskevich's avatar
Andrei Paskevich committed
537
      mk_let ~loc ~uloc:denv.uloc e1 res
538
  | Ptree.Eupdate (e1, fl) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
539
      let e1 = dexpr denv e1 in
540
      let e0 = mk_var e1 in
541
      let fl = List.map (find_prog_field denv.uc) fl in
542 543
      let cs,pjl,flm = Loc.try2 loc parse_record denv.uc fl in
      let get_val pj = match Mls.find_opt pj.pl_ls flm with
Andrei Paskevich's avatar
Andrei Paskevich committed
544
        | Some e -> dexpr denv e
545
        | None ->
546
            let loc = Loc.dummy_position in
547 548
            let d, dvty = de_app loc (hidden_pl ~loc pj) [e0] in
            mk_dexpr d dvty loc Slab.empty in
549
      let res = de_app loc (hidden_pl ~loc cs) (List.map get_val pjl) in
Andrei Paskevich's avatar
Andrei Paskevich committed
550
      mk_let ~loc ~uloc:denv.uloc e1 res
Andrei Paskevich's avatar
Andrei Paskevich committed
551
  | Ptree.Eassign (e1, q, e2) ->
552 553
      let fl = { expr_desc = Eident q; expr_loc = loc } in
      let e1 = { expr_desc = Eapply (fl,e1); expr_loc = loc } in
Andrei Paskevich's avatar
Andrei Paskevich committed
554 555
      let e1 = dexpr denv e1 in
      let e2 = dexpr denv e2 in
556 557 558 559
      let res = create_type_variable () in
      expected_type e1 res;
      expected_type_weak e2 res;
      DEassign (e1, e2), ([], dity_unit)
560
  | Ptree.Econstant (Number.ConstInt _ as c) ->
561
      DEconstant c, ([], dity_int)
562
  | Ptree.Econstant (Number.ConstReal _ as c) ->
563
      DEconstant c, ([], dity_real)
564
  | Ptree.Enot e1 ->
Andrei Paskevich's avatar
Andrei Paskevich committed
565
      let e1 = dexpr denv e1 in
566
      expected_type e1 dity_bool;
567
      DEnot e1, ([], dity_bool)
568
  | Ptree.Elazy (op, e1, e2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
569 570
      let e1 = dexpr denv e1 in
      let e2 = dexpr denv e2 in
571 572
      expected_type e1 dity_bool;
      expected_type e2 dity_bool;
573
      DElazy (op, e1, e2), ([], dity_bool)
574
  | Ptree.Ematch (e1, bl) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
575
      let e1 = dexpr denv e1 in
576
      let ety = create_type_variable () in
577
      let res = create_type_variable () in
578
      expected_type e1 ety;
579 580
      let branch (pp,e) =
        let ppat, dity, denv = dpattern denv pp in
581
        unify_loc unify pp.pat_loc ety dity;
Andrei Paskevich's avatar
Andrei Paskevich committed
582
        let e = dexpr denv e in
583 584
        expected_type e res;
        ppat, e in
585
      DEmatch (e1, List.map branch bl), ([], res)
Andrei Paskevich's avatar
Andrei Paskevich committed
586
  | Ptree.Eraise (q, e1) ->
587
      let xs = find_xsymbol denv.uc q in
588
      let dity = specialize_xsymbol xs in
Andrei Paskevich's avatar
Andrei Paskevich committed
589
      let e1 = match e1 with
Andrei Paskevich's avatar
Andrei Paskevich committed
590
        | Some e1 -> dexpr denv e1
591
        | None when ity_equal xs.xs_ity ity_unit -> de_unit ~loc
Andrei Paskevich's avatar
Andrei Paskevich committed
592 593
        | _ -> errorm ~loc "exception argument expected" in
      expected_type e1 dity;
594
      DEraise (xs, e1), ([], create_type_variable ())
Andrei Paskevich's avatar
Andrei Paskevich committed
595
  | Ptree.Etry (e1, cl) ->
596
      let res = create_type_variable () in
Andrei Paskevich's avatar
Andrei Paskevich committed
597
      let e1 = dexpr denv e1 in
598
      expected_type e1 res;
599
      let branch (q, pp, e) =
600
        let xs = find_xsymbol denv.uc q in
601 602 603
        let ety = specialize_xsymbol xs in
        let ppat, dity, denv = dpattern denv pp in
        unify_loc unify pp.pat_loc ety dity;
604
        let e = dexpr denv e in
605
        expected_type e res;
606
        xs, ppat, e in
Andrei Paskevich's avatar
Andrei Paskevich committed
607
      let cl = List.map branch cl in
608
      DEtry (e1, cl), e1.de_type
609
  | Ptree.Eabsurd ->
610
      DEabsurd, ([], create_type_variable ())
611
  | Ptree.Eassert (ak, lexpr) ->
612
      DEassert (ak, lexpr), ([], dity_unit)
Andrei Paskevich's avatar
Andrei Paskevich committed
613 614
  | Ptree.Emark (id, e1) ->
      let e1 = dexpr denv e1 in
615
      DEmark (id, e1), e1.de_type
616
  | Ptree.Eany tyc ->
617 618
      let tyc, dvty = dtype_c denv tyc in
      DEany tyc, dvty
619 620 621
  | Ptree.Eghost e1 ->
      let e1 = dexpr denv e1 in
      DEghost e1, e1.de_type
622
  | Ptree.Eabstract (e1, sp) ->
623
      let e1 = dexpr denv e1 in
624 625
      let sp = dspec denv.uc sp in
      DEabstract (e1, sp), e1.de_type
626 627 628 629 630 631 632 633 634 635 636 637 638 639
  | Ptree.Eloop ({ loop_invariant = inv; loop_variant = var }, e1) ->
      let e1 = dexpr denv e1 in
      let var = dvariant denv.uc var in
      expected_type e1 dity_unit;
      DEloop (var,inv,e1), e1.de_type
  | Ptree.Efor (id, efrom, dir, eto, inv, e1) ->
      let efrom = dexpr denv efrom in
      let eto = dexpr denv eto in
      let denv = add_var id dity_int denv in
      let e1 = dexpr denv e1 in
      expected_type efrom dity_int;
      expected_type eto dity_int;
      expected_type e1 dity_unit;
      DEfor (id,efrom,dir,eto,inv,e1), e1.de_type
640

641
and dletrec denv fdl =
642
  (* add all functions into the environment *)
643
  let add_one denv (_,id,_,bl,_) =
644 645
    let argl = List.map (fun _ -> create_type_variable ()) bl in
    let dvty = argl, create_type_variable () in
646
    add_mono id dvty denv, dvty in
647
  let denv, dvtyl = Lists.map_fold_left add_one denv fdl in
648
  (* then unify the binders *)
649
  let bind_one (_,_,_,bl,_) (argl,res) =
650 651 652
    let denv,bl,tyl = dbinders denv bl in
    List.iter2 unify argl tyl;
    denv,bl,tyl,res in
653
  let denvl = List.map2 bind_one fdl dvtyl in
654
  (* then type-check the bodies *)
655 656
  let type_one (loc,id,gh,_,tr) (denv,bl,tyl,tyv) =
    let tr, (argl, res) = dtriple denv tr in
657 658 659
    if argl <> [] then errorm ~loc
      "The body of a recursive function must be a first-order value";
    unify_loc unify loc tyv res;
660
    id, gh, (tyl, tyv), bl, tr in
661
  List.map2 type_one fdl denvl
Andrei Paskevich's avatar
Andrei Paskevich committed
662

663
and dtriple denv (e, sp) =
Andrei Paskevich's avatar
Andrei Paskevich committed
664
  let e = dexpr denv e in
665 666
  let sp = dspec denv.uc sp in
  (e, sp), e.de_type
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
667

668
(** stage 2 *)
669

Andrei Paskevich's avatar
Andrei Paskevich committed
670 671
type lenv = {
  mod_uc   : module_uc;
672 673
  th_at    : Theory.theory_uc;
  th_old   : Theory.theory_uc;
674
  let_vars : let_sym Mstr.t;
Andrei Paskevich's avatar
Andrei Paskevich committed
675
  log_vars : vsymbol Mstr.t;
676 677
}

Andrei Paskevich's avatar
Andrei Paskevich committed
678
let create_lenv uc = {
679 680 681
  mod_uc   = uc;
  th_at    = Theory.use_export (get_theory uc) Mlw_wp.th_mark_at;
  th_old   = Theory.use_export (get_theory uc) Mlw_wp.th_mark_old;
682 683 684 685
  let_vars = Mstr.empty;
  log_vars = Mstr.empty;
}

686 687
(* invariant handling *)

Andrei Paskevich's avatar
Andrei Paskevich committed
688
let env_invariant lenv eff pvs =
689 690
  let kn = get_known lenv.mod_uc in
  let lkn = Theory.get_known (get_theory lenv.mod_uc) in
691
  let regs = Sreg.union eff.eff_writes eff.eff_ghostw in
Andrei Paskevich's avatar
Andrei Paskevich committed
692 693
  let add_pv pv (pinv,qinv) =
    let ity = pv.pv_vtv.vtv_ity in
694
    let written r = reg_occurs r ity.ity_vars in
Andrei Paskevich's avatar
Andrei Paskevich committed
695
    let inv = Mlw_wp.full_invariant lkn kn pv.pv_vs ity in
696 697 698 699
    let qinv = (* we reprove invariants for modified non-reset variables *)
      if Sreg.exists written regs && not (eff_stale_region eff ity.ity_vars)
      then t_and_simp qinv inv else qinv in
    t_and_simp pinv inv, qinv
700
  in
Andrei Paskevich's avatar
Andrei Paskevich committed
701
  Spv.fold add_pv pvs (t_true,t_true)
702

703 704 705 706 707 708 709 710 711 712 713 714 715 716
let rec check_reset rvs t = match t.t_node with
  | Tvar vs when Svs.mem vs rvs ->
      errorm "The variable %s is reset and can only be used \
        under `old' in the postcondition" vs.vs_name.id_string
  | Tapp (ls,_) when ls_equal ls fs_at -> false
  | Tlet _ | Tcase _ | Teps _ | Tquant _ ->
      let rvs = Mvs.set_inter rvs t.t_vars in
      if Mvs.is_empty rvs then false else
      t_any (check_reset rvs) t
  | _ ->
      t_any (check_reset rvs) t

let post_invariant lenv rvs inv ity q =
  ignore (check_reset rvs q);
717 718 719 720
  let vs, q = open_post q in
  let kn = get_known lenv.mod_uc in
  let lkn = Theory.get_known (get_theory lenv.mod_uc) in
  let res_inv = Mlw_wp.full_invariant lkn kn vs ity in
721