mlw_typing.ml 60.7 KB
Newer Older
1 2
(**************************************************************************)
(*                                                                        *)
MARCHE Claude's avatar
MARCHE Claude committed
3
(*  Copyright (C) 2010-2012                                               *)
4 5 6
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
MARCHE Claude's avatar
MARCHE Claude committed
7
(*    Guillaume Melquiond                                                 *)
8 9 10 11 12 13 14 15 16 17 18 19 20 21 22
(*    Andrei Paskevich                                                    *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)

open Why3
open Util
23
open Ident
24 25 26
open Ty
open Term
open Decl
27 28 29
open Theory
open Env
open Ptree
30
open Mlw_dtree
31
open Mlw_ty
32
open Mlw_ty.T
33 34
open Mlw_expr
open Mlw_decl
35
open Mlw_pretty
36
open Mlw_module
Andrei Paskevich's avatar
Andrei Paskevich committed
37
open Mlw_wp
38
open Mlw_dty
39

40 41
(** errors *)

42
exception DuplicateProgVar of string
43 44 45 46 47 48 49 50 51 52 53
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
54
exception UnboundSymbol of qualid
55 56 57 58

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

59 60
let qloc = Typing.qloc
let print_qualid = Typing.print_qualid
61 62 63

let () = Exn_printer.register (fun fmt e -> match e with
  | DuplicateTypeVar s ->
64 65 66
      Format.fprintf fmt "Type parameter %s is used twice" s
  | DuplicateProgVar s ->
      Format.fprintf fmt "Parameter %s is used twice" s
67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84
(*
  | 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 ->
85 86 87
      Format.fprintf fmt "Unbound type variable '%s" s
  | UnboundSymbol q ->
      Format.fprintf fmt "Unbound symbol '%a'" print_qualid q
88 89 90 91
  | _ -> raise e)

(* TODO: let type_only = Debug.test_flag Typing.debug_type_only in *)

92 93
type denv = {
  uc     : module_uc;
94
  locals : (tvars * dvty) Mstr.t;
95
  tvars  : tvars;
Andrei Paskevich's avatar
Andrei Paskevich committed
96
  uloc   : Ptree.loc option;
97
}
98

99 100 101 102
let create_denv uc = {
  uc     = uc;
  locals = Mstr.empty;
  tvars  = empty_tvars;
Andrei Paskevich's avatar
Andrei Paskevich committed
103
  uloc   = None;
104
}
105

106 107 108 109 110 111
(* Handle tuple symbols *)

let ht_tuple   = Hashtbl.create 3
let ts_tuple n = Hashtbl.replace ht_tuple n (); ts_tuple n
let fs_tuple n = Hashtbl.replace ht_tuple n (); fs_tuple n

Andrei Paskevich's avatar
Andrei Paskevich committed
112 113 114 115 116 117 118 119 120 121 122 123 124
let rec check_at f0 =
  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)

125 126 127 128 129 130
let count_term_tuples t =
  let syms_ts _ ts = match is_ts_tuple_id ts.ts_name with
    | Some n -> Hashtbl.replace ht_tuple n () | _ -> () in
  let syms_ty _ ty = ty_s_fold syms_ts () ty in
  t_s_fold syms_ty (fun _ _ -> ()) () t

131
let flush_tuples uc =
132 133 134 135 136 137
  let kn = Theory.get_known (get_theory uc) in
  let add_tuple n _ uc =
    if Mid.mem (ts_tuple n).ts_name kn then uc
    else use_export_theory uc (tuple_theory n) in
  let uc = Hashtbl.fold add_tuple ht_tuple uc in
  Hashtbl.clear ht_tuple;
138 139 140 141
  uc

let add_pdecl_with_tuples uc pd = add_pdecl (flush_tuples uc) pd
let add_decl_with_tuples uc d = add_decl (flush_tuples uc) d
142

143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159
(** Namespace lookup *)

let uc_find_ls uc p =
  let x = Typing.string_list_of_qualid [] p in
  try ns_find_ls (Theory.get_namespace (get_theory uc)) x
  with Not_found -> error ~loc:(qloc p) (UnboundSymbol p)

let uc_find_ts uc p =
  let x = Typing.string_list_of_qualid [] p in
  try ns_find_ts (get_namespace uc) x
  with Not_found -> error ~loc:(qloc p) (UnboundSymbol p)

let uc_find_ps uc p =
  let x = Typing.string_list_of_qualid [] p in
  try ns_find_ps (get_namespace uc) x
  with Not_found -> error ~loc:(qloc p) (UnboundSymbol p)

160 161
(** Typing type expressions *)

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

(** Typing program expressions *)

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

183
let unify_loc unify_fn loc x1 x2 = try unify_fn x1 x2 with
184
  | TypeMismatch (ity1,ity2) -> errorm ~loc
185 186 187
      "This expression has type %a, but is expected to have type %a"
      Mlw_pretty.print_ity ity2 Mlw_pretty.print_ity ity1
  | exn -> error ~loc exn
188

189 190 191 192 193 194 195
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
196

197
let rec extract_labels labs loc e = match e.Ptree.expr_desc with
198
  | Ptree.Enamed (Ptree.Lstr s, e) -> extract_labels (Slab.add s labs) loc e
199 200 201 202
  | 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)
203
  | e -> labs, loc, e
204

205 206 207
let rec decompose_app args e = match e.Ptree.expr_desc with
  | Eapply (e1, e2) -> decompose_app (e2 :: args) e1
  | _ -> e, args
208

209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228
(* 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
    | [cs,pjl] -> cs, List.map (exn_option (BadRecordField pl.pl_ls)) pjl
    | _ -> 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

229 230
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
231

232
let find_pure_field uc (p,e) = uc_find_ls uc p, e
233

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

let hidden_pl ~loc pl =
239 240
  { de_desc = DEglobal_pl pl;
    de_type = specialize_plsymbol pl;
241
    de_loc  = loc; de_lab = Slab.empty }
242 243

let hidden_ls ~loc ls =
244 245
  { de_desc = DEglobal_ls ls;
    de_type = specialize_lsymbol ls;
246
    de_loc  = loc; de_lab = Slab.empty }
247 248

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

let mk_var e =
  if test_var e then e else
255 256 257
  { de_desc = DElocal "q";
    de_type = e.de_type;
    de_loc  = e.de_loc;
258
    de_lab  = Slab.empty }
259

260 261 262
let mk_id s loc =
  { id = s; id_loc = loc; id_lab = [] }

263 264
let mk_dexpr desc dvty loc labs =
  { de_desc = desc; de_type = dvty; de_loc = loc; de_lab = labs }
265

266 267
let mk_let ~loc ~uloc e (desc,dvty) =
  if test_var e then desc, dvty else
Andrei Paskevich's avatar
Andrei Paskevich committed
268
  let loc = def_option loc uloc in
269 270
  let e1 = mk_dexpr desc dvty loc Slab.empty in
  DElet (mk_id "q" loc, false, e, e1), dvty
271

272 273 274
(* patterns *)

let add_var id dity denv =
275 276
  let tvars = add_dity denv.tvars dity in
  let locals = Mstr.add id.id (tvars,([],dity)) denv.locals in
277 278
  { denv with locals = locals; tvars = tvars }

279
let specialize_qualid uc p = match uc_find_ps uc p with
280
  | PV pv -> DEglobal_pv pv, ([],specialize_pvsymbol pv)
281 282 283
  | PS ps -> DEglobal_ps ps, specialize_psymbol  ps
  | PL pl -> DEglobal_pl pl, specialize_plsymbol pl
  | LS ls -> DEglobal_ls ls, specialize_lsymbol ls
284
  | XS xs -> errorm ~loc:(qloc p) "unexpected exception symbol %a" print_xs xs
285

286 287
let find_xsymbol uc p = match uc_find_ps uc p with
  | XS xs -> xs
288
  | _ -> errorm ~loc:(qloc p) "exception symbol expected"
Andrei Paskevich's avatar
Andrei Paskevich committed
289

290
let find_variant_ls uc p = match uc_find_ls uc p with
291 292
  | { 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
293

294
let find_global_vs uc p = try match uc_find_ps uc p with
295 296
  | PV pv -> Some pv.pv_vs
  | _ -> None
297
  with _ -> None
298

299 300 301 302 303
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
304
      PPvar (Denv.create_user_id id), dity, add_var id dity denv
305
  | Ptree.PPpapp (q,ppl) ->
306 307
      let sym, dvty = specialize_qualid denv.uc q in
      dpat_app denv loc (mk_dexpr sym dvty loc Slab.empty) ppl
308
  | Ptree.PPprec fl when is_pure_record denv.uc fl ->
309
      let kn = Theory.get_known (get_theory denv.uc) in
310
      let fl = List.map (find_pure_field denv.uc) fl in
311 312 313
      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
314
      dpat_app denv loc (hidden_ls ~loc cs) (List.map get_val pjl)
315
  | Ptree.PPprec fl ->
316
      let fl = List.map (find_prog_field denv.uc) fl in
317 318 319
      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
320
      dpat_app denv loc (hidden_pl ~loc cs) (List.map get_val pjl)
321 322
  | Ptree.PPptuple ppl ->
      let cs = fs_tuple (List.length ppl) in
323 324 325 326
      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
327
      unify_loc unify lpp2.pat_loc dity1 dity2;
328 329 330
      PPor (pp1, pp2), dity1, denv
  | Ptree.PPpas (pp, id) ->
      let pp, dity, denv = dpattern denv pp in
331
      PPas (pp, Denv.create_user_id id), dity, add_var id dity denv
332

333 334 335 336
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
337
  let ppl, tyl, denv = List.fold_right add_pp ppl ([],[],denv) in
338 339 340
  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
341 342
    | 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
343 344
    | _ -> assert false
  in
345 346 347 348 349
  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;
350 351
  pp, res, denv

352 353
(* specifications *)

354
let dbinders denv bl =
355
  let hv = Hashtbl.create 3 in
356
  let dbinder (id,gh,pty) (denv,bl,tyl) =
357
    if Hashtbl.mem hv id.id then raise (DuplicateProgVar id.id);
358
    Hashtbl.add hv id.id ();
359
    let dity = match pty with
360
      | Some pty -> dity_of_pty denv pty
361
      | None -> create_type_variable () in
362
    add_var id dity denv, (id,gh,dity)::bl, dity::tyl
363 364
  in
  List.fold_right dbinder bl (denv,[],[])
365 366

let deff_of_peff uc pe =
367 368 369
  { deff_reads  = pe.pe_reads;
    deff_writes = pe.pe_writes;
    deff_raises = List.map (fun (gh,q) -> gh, find_xsymbol uc q) pe.pe_raises; }
370 371 372 373

let dxpost uc ql = List.map (fun (q,f) -> find_xsymbol uc q, f) ql

let rec dtype_c denv tyc =
374
  let tyv, dvty = dtype_v denv tyc.pc_result_type in
375 376 377 378 379
  { dc_result = tyv;
    dc_effect = deff_of_peff denv.uc tyc.pc_effect;
    dc_pre    = tyc.pc_pre;
    dc_post   = fst tyc.pc_post;
    dc_xpost  = dxpost denv.uc (snd tyc.pc_post); },
380
  dvty
381 382 383

and dtype_v denv = function
  | Tpure pty ->
384
      let dity = dity_of_pty denv pty in
385
      DSpecV (false,dity), ([],dity)
386 387
  | Tarrow (bl,tyc) ->
      let denv,bl,tyl = dbinders denv bl in
388 389
      let tyc,(argl,res) = dtype_c denv tyc in
      DSpecA (bl,tyc), (tyl @ argl,res)
390

391
let dvariant uc var =
392 393
  List.map (fun (le,q) -> le, Util.option_map (find_variant_ls uc) q) var

394
(* expressions *)
395

396
let de_unit ~loc = hidden_ls ~loc (Term.fs_tuple 0)
397

398 399 400 401 402 403 404 405 406 407 408 409 410 411
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
412

Andrei Paskevich's avatar
Andrei Paskevich committed
413
let rec dexpr denv e =
414
  let loc = e.Ptree.expr_loc in
415
  let labs, uloc, d = extract_labels Slab.empty denv.uloc e in
Andrei Paskevich's avatar
Andrei Paskevich committed
416
  let denv = { denv with uloc = uloc } in
417
  let d, ty = de_desc denv loc d in
Andrei Paskevich's avatar
Andrei Paskevich committed
418
  let loc = def_option loc uloc in
419
  mk_dexpr d ty loc labs
420

421
and de_desc denv loc = function
422 423
  | Ptree.Eident (Qident {id=x}) when Mstr.mem x denv.locals ->
      (* local variable *)
424 425 426
      let tvs, dvty = Mstr.find x denv.locals in
      let dvty = specialize_scheme tvs dvty in
      DElocal x, dvty
427
  | Ptree.Eident p ->
428
      specialize_qualid denv.uc p
429 430
  | Ptree.Eapply (e1, e2) ->
      let e, el = decompose_app [e2] e1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
431
      let el = List.map (dexpr denv) el in
432
      de_app loc (dexpr denv e) el
433
  | Ptree.Elet (id, gh, e1, e2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
434
      let e1 = dexpr denv e1 in
435
      let dvty = e1.de_type in
436
      let tvars = match e1.de_desc with
Andrei Paskevich's avatar
Andrei Paskevich committed
437
        | DEfun _ -> denv.tvars
438 439
        | _ -> add_dvty denv.tvars dvty in
      let locals = Mstr.add id.id (tvars, dvty) denv.locals in
440
      let denv = { denv with locals = locals; tvars = tvars } in
Andrei Paskevich's avatar
Andrei Paskevich committed
441
      let e2 = dexpr denv e2 in
442
      DElet (id, gh, e1, e2), e2.de_type
Andrei Paskevich's avatar
Andrei Paskevich committed
443
  | Ptree.Eletrec (rdl, e1) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
444
      let rdl = dletrec denv rdl in
445 446
      let add_one denv (_, { id = id }, _, dvty, _) =
        { denv with locals = Mstr.add id (denv.tvars, dvty) denv.locals } in
447
      let denv = List.fold_left add_one denv rdl in
Andrei Paskevich's avatar
Andrei Paskevich committed
448
      let e1 = dexpr denv e1 in
449
      DEletrec (rdl, e1), e1.de_type
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
450
  | Ptree.Efun (bl, tr) ->
451
      let denv, bl, tyl = dbinders denv bl in
452
      let lam, (argl, res) = dlambda denv bl [] tr in
453
      DEfun lam, (tyl @ argl, res)
454
  | Ptree.Ecast (e1, pty) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
455
      let e1 = dexpr denv e1 in
456
      expected_type e1 (dity_of_pty denv pty);
457
      e1.de_desc, e1.de_type
458 459
  | Ptree.Enamed _ ->
      assert false
460
  | Ptree.Esequence (e1, e2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
461
      let e1 = dexpr denv e1 in
462
      expected_type e1 dity_unit;
Andrei Paskevich's avatar
Andrei Paskevich committed
463
      let e2 = dexpr denv e2 in
464
      DElet (mk_id "_" loc, false, e1, e2), e2.de_type
465
  | Ptree.Eif (e1, e2, e3) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
466
      let e1 = dexpr denv e1 in
467
      expected_type e1 dity_bool;
Andrei Paskevich's avatar
Andrei Paskevich committed
468 469
      let e2 = dexpr denv e2 in
      let e3 = dexpr denv e3 in
470 471 472
      let res = create_type_variable () in
      expected_type e2 res;
      expected_type e3 res;
473
      DEif (e1, e2, e3), e2.de_type
474 475
  | Ptree.Etuple el ->
      let ls = fs_tuple (List.length el) in
Andrei Paskevich's avatar
Andrei Paskevich committed
476
      let el = List.map (dexpr denv) el in
477
      de_app loc (hidden_ls ~loc ls) el
478
  | Ptree.Erecord fl when is_pure_record denv.uc fl ->
479
      let kn = Theory.get_known (get_theory denv.uc) in
480
      let fl = List.map (find_pure_field denv.uc) fl in
481 482
      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
483
        | Some e -> dexpr denv e
484
        | None -> error ~loc (Decl.RecordFieldMissing (cs,pj)) in
485
      de_app loc (hidden_ls ~loc cs) (List.map get_val pjl)
486
  | Ptree.Erecord fl ->
487
      let fl = List.map (find_prog_field denv.uc) fl in
488 489
      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
490
        | Some e -> dexpr denv e
491
        | None -> error ~loc (Decl.RecordFieldMissing (cs.pl_ls,pj.pl_ls)) in
492
      de_app loc (hidden_pl ~loc cs) (List.map get_val pjl)
493
  | Ptree.Eupdate (e1, fl) when is_pure_record denv.uc fl ->
Andrei Paskevich's avatar
Andrei Paskevich committed
494
      let e1 = dexpr denv e1 in
495 496
      let e0 = mk_var e1 in
      let kn = Theory.get_known (get_theory denv.uc) in
497
      let fl = List.map (find_pure_field denv.uc) fl in
498 499
      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
500
        | Some e -> dexpr denv e
501
        | None ->
502
            let loc = Loc.dummy_position in
503 504
            let d, dvty = de_app loc (hidden_ls ~loc pj) [e0] in
            mk_dexpr d dvty loc Slab.empty in
505
      let res = de_app loc (hidden_ls ~loc cs) (List.map get_val pjl) in
Andrei Paskevich's avatar
Andrei Paskevich committed
506
      mk_let ~loc ~uloc:denv.uloc e1 res
507
  | Ptree.Eupdate (e1, fl) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
508
      let e1 = dexpr denv e1 in
509
      let e0 = mk_var e1 in
510
      let fl = List.map (find_prog_field denv.uc) fl in
511 512
      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
513
        | Some e -> dexpr denv e
514
        | None ->
515
            let loc = Loc.dummy_position in
516 517
            let d, dvty = de_app loc (hidden_pl ~loc pj) [e0] in
            mk_dexpr d dvty loc Slab.empty in
518
      let res = de_app loc (hidden_pl ~loc cs) (List.map get_val pjl) in
Andrei Paskevich's avatar
Andrei Paskevich committed
519
      mk_let ~loc ~uloc:denv.uloc e1 res
Andrei Paskevich's avatar
Andrei Paskevich committed
520
  | Ptree.Eassign (e1, q, e2) ->
521 522
      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
523 524
      let e1 = dexpr denv e1 in
      let e2 = dexpr denv e2 in
525 526 527 528
      let res = create_type_variable () in
      expected_type e1 res;
      expected_type_weak e2 res;
      DEassign (e1, e2), ([], dity_unit)
529
  | Ptree.Econstant (ConstInt _ as c) ->
530
      DEconstant c, ([], dity_int)
531
  | Ptree.Econstant (ConstReal _ as c) ->
532
      DEconstant c, ([], dity_real)
533
  | Ptree.Enot e1 ->
Andrei Paskevich's avatar
Andrei Paskevich committed
534
      let e1 = dexpr denv e1 in
535
      expected_type e1 dity_bool;
536
      DEnot e1, ([], dity_bool)
537
  | Ptree.Elazy (op, e1, e2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
538 539
      let e1 = dexpr denv e1 in
      let e2 = dexpr denv e2 in
540 541
      expected_type e1 dity_bool;
      expected_type e2 dity_bool;
542
      DElazy (op, e1, e2), ([], dity_bool)
543
  | Ptree.Ematch (e1, bl) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
544
      let e1 = dexpr denv e1 in
545
      let ety = create_type_variable () in
546
      let res = create_type_variable () in
547
      expected_type e1 ety;
548 549
      let branch (pp,e) =
        let ppat, dity, denv = dpattern denv pp in
550
        unify_loc unify pp.pat_loc ety dity;
Andrei Paskevich's avatar
Andrei Paskevich committed
551
        let e = dexpr denv e in
552 553
        expected_type e res;
        ppat, e in
554
      DEmatch (e1, List.map branch bl), ([], res)
Andrei Paskevich's avatar
Andrei Paskevich committed
555
  | Ptree.Eraise (q, e1) ->
556
      let xs = find_xsymbol denv.uc q in
557
      let dity = specialize_xsymbol xs in
Andrei Paskevich's avatar
Andrei Paskevich committed
558
      let e1 = match e1 with
Andrei Paskevich's avatar
Andrei Paskevich committed
559
        | Some e1 -> dexpr denv e1
560
        | None when ity_equal xs.xs_ity ity_unit -> de_unit ~loc
Andrei Paskevich's avatar
Andrei Paskevich committed
561 562
        | _ -> errorm ~loc "exception argument expected" in
      expected_type e1 dity;
563
      DEraise (xs, e1), ([], create_type_variable ())
Andrei Paskevich's avatar
Andrei Paskevich committed
564
  | Ptree.Etry (e1, cl) ->
565
      let res = create_type_variable () in
Andrei Paskevich's avatar
Andrei Paskevich committed
566
      let e1 = dexpr denv e1 in
567
      expected_type e1 res;
Andrei Paskevich's avatar
Andrei Paskevich committed
568
      let branch (q, id, e) =
569
        let xs = find_xsymbol denv.uc q in
570
        let dity = specialize_xsymbol xs in
Andrei Paskevich's avatar
Andrei Paskevich committed
571 572
        let id, denv = match id with
          | Some id -> id, add_var id dity denv
573
          | None -> mk_id "void" loc, denv in
574
        let e = dexpr denv e in
575
        expected_type e res;
576
        xs, id, e
Andrei Paskevich's avatar
Andrei Paskevich committed
577 578
      in
      let cl = List.map branch cl in
579
      DEtry (e1, cl), e1.de_type
580
  | Ptree.Eabsurd ->
581
      DEabsurd, ([], create_type_variable ())
582
  | Ptree.Eassert (ak, lexpr) ->
583
      DEassert (ak, lexpr), ([], dity_unit)
Andrei Paskevich's avatar
Andrei Paskevich committed
584 585
  | Ptree.Emark (id, e1) ->
      let e1 = dexpr denv e1 in
586
      DEmark (id, e1), e1.de_type
587
  | Ptree.Eany tyc ->
588 589
      let tyc, dvty = dtype_c denv tyc in
      DEany tyc, dvty
590 591 592
  | Ptree.Eghost e1 ->
      let e1 = dexpr denv e1 in
      DEghost e1, e1.de_type
593 594 595 596
  | Ptree.Eabstract (e1, (q,xq)) ->
      let e1 = dexpr denv e1 in
      let xq = dxpost denv.uc xq in
      DEabstract (e1, q, xq), e1.de_type
597 598 599 600 601 602 603 604 605 606 607 608 609 610
  | 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
611

Andrei Paskevich's avatar
Andrei Paskevich committed
612
and dletrec denv rdl =
613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634
  (* add all functions into the environment *)
  let add_one denv (_,id,_,bl,_,_) =
    let argl = List.map (fun _ -> create_type_variable ()) bl in
    let dvty = argl, create_type_variable () in
    let tvars = add_dvty denv.tvars dvty in
    let locals = Mstr.add id.id (tvars, dvty) denv.locals in
    { denv with locals = locals; tvars = tvars }, dvty in
  let denv, dvtyl = Util.map_fold_left add_one denv rdl in
  (* then unify the binders *)
  let bind_one (_,_,_,bl,_,_) (argl,res) =
    let denv,bl,tyl = dbinders denv bl in
    List.iter2 unify argl tyl;
    denv,bl,tyl,res in
  let denvl = List.map2 bind_one rdl dvtyl in
  (* then type-check the bodies *)
  let type_one (loc, id, gh, _, var, tr) (denv,bl,tyl,tyv) =
    let lam, (argl, res) = dlambda denv bl var tr in
    if argl <> [] then errorm ~loc
      "The body of a recursive function must be a first-order value";
    unify_loc unify loc tyv res;
    loc, id, gh, (tyl, tyv), lam in
  List.map2 type_one rdl denvl
Andrei Paskevich's avatar
Andrei Paskevich committed
635

636
and dlambda denv bl var (p, e, (q, xq)) =
Andrei Paskevich's avatar
Andrei Paskevich committed
637
  let e = dexpr denv e in
638 639
  let var = dvariant denv.uc var in
  let xq = dxpost denv.uc xq in
640
  (bl, var, p, e, q, xq), e.de_type
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
641

642
(** stage 2 *)
643

Andrei Paskevich's avatar
Andrei Paskevich committed
644 645
type lenv = {
  mod_uc   : module_uc;
646 647
  th_at    : Theory.theory_uc;
  th_old   : Theory.theory_uc;
648
  let_vars : let_sym Mstr.t;
Andrei Paskevich's avatar
Andrei Paskevich committed
649 650
  log_vars : vsymbol Mstr.t;
  log_denv : Typing.denv;
651 652
}

Andrei Paskevich's avatar
Andrei Paskevich committed
653
let create_lenv uc = {
654 655 656
  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;
657 658
  let_vars = Mstr.empty;
  log_vars = Mstr.empty;
659
  log_denv = Typing.denv_empty_with_globals (find_global_vs uc);
660 661 662
}

let rec dty_of_ty ty = match ty.ty_node with
663 664
  | Ty.Tyapp (ts, tyl) -> Denv.tyapp ts (List.map dty_of_ty tyl)
  | Ty.Tyvar v -> Denv.tyuvar v
665

666 667 668 669
let create_post lenv x ty f =
  let res = create_vsymbol (id_fresh x) ty in
  let log_vars = Mstr.add x res lenv.log_vars in
  let log_denv = Typing.add_var x (dty_of_ty ty) lenv.log_denv in
670 671
  let f = Typing.type_fmla lenv.th_old log_denv log_vars f in
  let f = remove_old f in
672
  count_term_tuples f;
Andrei Paskevich's avatar
Andrei Paskevich committed
673
  check_at f;
674
  create_post res f
675

676 677 678
let create_xpost lenv x xs f = create_post lenv x (ty_of_ity xs.xs_ity) f
let create_post lenv x vty f = create_post lenv x (ty_of_vty vty) f

679
let create_pre lenv f =
680
  let f = Typing.type_fmla lenv.th_at lenv.log_denv lenv.log_vars f in
681
  count_term_tuples f;
Andrei Paskevich's avatar
Andrei Paskevich committed
682
  check_at f;
683
  f
684

685
let create_variant lenv (t,r) =
686
  let t = Typing.type_term lenv.th_at lenv.log_denv lenv.log_vars t in
687
  count_term_tuples t;
Andrei Paskevich's avatar
Andrei Paskevich committed
688
  check_at t;
689
  t, r
Andrei Paskevich's avatar
Andrei Paskevich committed
690

Andrei Paskevich's avatar
Andrei Paskevich committed
691
let add_local x lv lenv = match lv with
692
  | LetA _ ->
Andrei Paskevich's avatar
Andrei Paskevich committed
693
      { lenv with let_vars = Mstr.add x lv lenv.let_vars }
694 695
  | LetV pv ->
      let dty = dty_of_ty pv.pv_vs.vs_ty in
696
      { lenv with
Andrei Paskevich's avatar
Andrei Paskevich committed
697 698 699
        let_vars = Mstr.add x lv lenv.let_vars;
        log_vars = Mstr.add x pv.pv_vs lenv.log_vars;
        log_denv = Typing.add_var x dty lenv.log_denv }
700

701 702
exception DuplicateException of xsymbol

703 704 705 706 707 708 709 710 711
let binders lenv bl =
  let binder lenv (id, ghost, dity) =
    let vtv = vty_value ~ghost (ity_of_dity dity) in
    let pv = create_pvsymbol (Denv.create_user_id id) vtv in
    add_local id.id (LetV pv) lenv, pv in
  Util.map_fold_left binder lenv bl

let xpost lenv xq =
  let add_exn m (xs,f) =
712
    let f = create_xpost lenv "result" xs f in
713 714 715
    Mexn.add_new (DuplicateException xs) xs f m in
  List.fold_left add_exn Mexn.empty xq

716 717 718 719 720 721 722 723 724
(* add dummy postconditions for uncovered exceptions *)
let complete_xpost lenv eff xq =
  let xq = xpost lenv xq in
  let dummy { xs_ity = ity } () =
    let v = create_vsymbol (id_fresh "dummy") (ty_of_ity ity) in
    Mlw_ty.create_post v t_true in
  let xs = Sexn.union eff.eff_raises eff.eff_ghostx in
  Mexn.set_union xq (Mexn.mapi dummy (Mexn.set_diff xs xq))

725 726 727 728
(* TODO: devise a good grammar for effect expressions *)
let rec get_eff_expr lenv { pp_desc = d; pp_loc = loc } = match d with
  | Ptree.PPvar (Ptree.Qident {id=x}) when Mstr.mem x lenv.let_vars ->
      begin match Mstr.find x lenv.let_vars with
729
        | LetV pv -> pv.pv_vs, pv.pv_vtv
730
        | LetA _ -> errorm ~loc "'%s' must be a first-order value" x
731 732
      end
  | Ptree.PPvar p ->
733
      begin match uc_find_ps lenv.mod_uc p with
734
        | PV pv -> pv.pv_vs, pv.pv_vtv
735 736
        | _ -> errorm ~loc:(qloc p) "'%a' must be a variable" print_qualid p
      end
737
  | Ptree.PPapp (p, [le]) ->
738
      let vs, vtv = get_eff_expr lenv le in
739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759
      let quit () = errorm ~loc:le.pp_loc "This expression is not a record" in
      let pjm = match vtv.vtv_ity.ity_node with
        | Ityapp (its,_,_) ->
            let pjl = match find_constructors (get_known lenv.mod_uc) its with
              | (_,pjl)::_ -> pjl | _ -> quit () in
            let add_pj m pj = match pj with
              | Some { pl_ls = ls; pl_args = [vtva]; pl_value = vtvv } ->
                  Mls.add ls (vtva.vtv_ity, vtvv) m
              | Some _ -> assert false
              | None -> m in
            List.fold_left add_pj Mls.empty pjl
        | Itypur (ts,_) ->
            let kn = Theory.get_known (get_theory lenv.mod_uc) in
            let pjl = match Decl.find_constructors kn ts with
              | (_,pjl)::_ -> pjl | _ -> quit () in
            let add_pj m pj = match pj with
              | Some ({ ls_args = [tya]; ls_value = Some tyv } as ls) ->
                  Mls.add ls (ity_of_ty tya, vty_value (ity_of_ty tyv)) m
              | Some _ -> assert false
              | None -> m in
            List.fold_left add_pj Mls.empty pjl
760
        | _ -> quit ()