mlw_typing.ml 65.8 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
  uc

140
let add_pdecl_with_tuples ~wp uc pd = add_pdecl ~wp (flush_tuples uc) pd
141
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 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 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 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734
(* invariant handling *)

let env_invariant lenv svs =
  let kn = get_known lenv.mod_uc in
  let lkn = Theory.get_known (get_theory lenv.mod_uc) in
  let add_vs vs inv =
    let ity = (restore_pv vs).pv_vtv.vtv_ity in
    t_and_simp inv (Mlw_wp.full_invariant lkn kn vs ity) in
  Svs.fold add_vs svs t_true

let post_invariant lenv inv ity q =
  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
  let q = t_and_asym_simp q (t_and_simp res_inv inv) in
  Mlw_ty.create_post vs q

let spec_invariant lenv svs ity spec =
  let inv = env_invariant lenv svs in
  let post_inv = post_invariant lenv inv in
  let xpost_inv xs q = post_inv xs.xs_ity q in
  { spec with c_pre   = t_and_simp spec.c_pre inv;
              c_post  = post_inv ity spec.c_post;
              c_xpost = Mexn.mapi xpost_inv spec.c_xpost }

let ity_or_unit = function
  | VTvalue v -> v.vtv_ity
  | VTarrow _ -> ity_unit

let expr_vsset svs e =
  let add_id id _ s =
    try Svs.add (restore_pv_by_id id).pv_vs s
    with Not_found -> s in
  Mid.fold add_id e.e_varm svs

let abst_invariant lenv e q xq =
  let spec = {
    c_pre     = t_true;
    c_effect  = eff_empty;
    c_post    = q;
    c_xpost   = xq;
    c_variant = [];
    c_letrec  = 0 } in
  let ity = ity_or_unit e.e_vty in
  let svs = expr_vsset (spec_vsset spec) e in
  let spec = spec_invariant lenv svs ity spec in
  spec.c_post, spec.c_xpost

let spec_of_lambda lam = {
  c_pre     = lam.l_pre;
  c_effect  = lam.l_expr.e_effect;
  c_post    = lam.l_post;
  c_xpost   = lam.l_xpost;
  c_variant = lam.l_variant;
  c_letrec  = 0 }

let lambda_invariant lenv svs lam =
  let spec = spec_of_lambda lam in
  let add_pv s pv = Svs.add pv.pv_vs s in
  let svs = List.fold_left add_pv svs lam.l_args in
  let ity = ity_or_unit lam.l_expr.e_vty in
  let spec = spec_invariant lenv svs ity spec in
  { lam with  l_pre   = spec.c_pre;
              l_post  = spec.c_post;
              l_xpost = spec.c_xpost }

let lambda_vsset lam =
  let del_pv svs pv = Svs.remove pv.pv_vs svs in
  let svs = spec_vsset (spec_of_lambda lam) in
  let svs = expr_vsset svs lam.l_expr in
  List.fold_left del_pv svs lam.l_args

735
let rec dty_of_ty ty = match ty.ty_node with
736 737
  | Ty.Tyapp (ts, tyl) -> Denv.tyapp ts (List.map dty_of_ty tyl)
  | Ty.Tyvar v -> Denv.tyuvar v
738

739 740 741 742
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
743 744
  let f = Typing.type_fmla lenv.th_old log_denv log_vars f in
  let f = remove_old f in
745
  count_term_tuples f;
Andrei Paskevich's avatar
Andrei Paskevich committed
746
  check_at f;
747
  create_post res f
748

749 750 751
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

752
let create_pre lenv f =
753
  let f = Typing.type_fmla lenv.th_at lenv.log_denv lenv.log_vars f in
754
  count_term_tuples f;
Andrei Paskevich's avatar
Andrei Paskevich committed
755
  check_at f;
756
  f
757

758
let create_variant lenv (t,r) =
759
  let t = Typing.type_term lenv.th_at lenv.log_denv lenv.log_vars t in
760
  count_term_tuples t;
Andrei Paskevich's avatar
Andrei Paskevich committed
761
  check_at t;
762
  t, r
Andrei Paskevich's avatar
Andrei Paskevich committed
763

Andrei Paskevich's avatar
Andrei Paskevich committed
764
let add_local x lv lenv = match lv with
765
  | LetA _ ->
Andrei Paskevich's avatar
Andrei Paskevich committed
766
      { lenv with let_vars = Mstr.add x lv lenv.let_vars }
767 768
  | LetV pv ->
      let dty = dty_of_ty pv.pv_vs.vs_ty in
769
      { lenv with
Andrei Paskevich's avatar
Andrei Paskevich committed
770 771 772
        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 }
773

774 775
exception DuplicateException of xsymbol

776 777 778 779 780 781 782 783 784
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) =
785
    let f = create_xpost lenv "result" xs f in
786 787 788
    Mexn.add_new (DuplicateException xs) xs f m in
  List.fold_left add_exn Mexn.empty xq

789 790 791 792 793 794