mlw_typing.ml 55.3 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 54 55 56 57 58
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
exception UnboundSymbol of string list

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 85 86 87 88 89 90 91 92
(*
  | 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 ->
      Format.fprintf fmt "unbound type variable '%s" s
  | UnboundSymbol sl ->
      Format.fprintf fmt "Unbound symbol '%a'"
        (Pp.print_list Pp.dot Format.pp_print_string) sl
  | _ -> raise e)

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

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

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

107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127
(* 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

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

let add_pdecl_with_tuples uc pd =
  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;
  add_pdecl uc pd

128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143
(** Typing type expressions *)

let rec dity_of_pty ~user denv = function
  | Ptree.PPTtyvar id ->
      create_user_type_variable id
  | Ptree.PPTtyapp (pl, p) ->
      let dl = List.map (dity_of_pty ~user denv) pl in
      let x = Typing.string_list_of_qualid [] p in
      begin
        try
          let its = ns_find_it (get_namespace denv.uc) x in
          its_app ~user its dl
        with Not_found -> try
          let ts = ns_find_ts (Theory.get_namespace (get_theory denv.uc)) x in
          ts_app ts dl
        with Not_found ->
144
          errorm ~loc:(qloc p) "unbound symbol %a" print_qualid p
145 146 147
      end
  | Ptree.PPTtuple pl ->
      ts_app (ts_tuple (List.length pl)) (List.map (dity_of_pty ~user denv) pl)
148 149 150

(** Typing program expressions *)

Andrei Paskevich's avatar
Andrei Paskevich committed
151
let dity_int  = ts_app ts_int  []
152
let dity_real = ts_app ts_real []
153
let dity_bool = ts_app ts_bool []
Andrei Paskevich's avatar
Andrei Paskevich committed
154 155
let dity_unit = ts_app ts_unit []
let dity_mark = ts_app ts_mark []
156

157 158
let unify_loc loc fn_unify x1 x2 =
  try fn_unify x1 x2 with
159
    | TypeMismatch (ity1,ity2) ->
160
        errorm ~loc "This expression has type %a, \
161
          but is expected to have type %a"
162 163 164 165 166
        Mlw_pretty.print_ity ity2 Mlw_pretty.print_ity ity1
    | exn -> error ~loc exn

let expected_type ?(weak=false) e dity =
  unify_loc e.de_loc (unify ~weak) dity e.de_type
167

168
let rec extract_labels labs loc e = match e.Ptree.expr_desc with
169
  | Ptree.Enamed (Ptree.Lstr s, e) -> extract_labels (Slab.add s labs) loc e
170 171 172 173
  | 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)
174
  | e -> labs, loc, e
175

176 177 178
let rec decompose_app args e = match e.Ptree.expr_desc with
  | Eapply (e1, e2) -> decompose_app (e2 :: args) e1
  | _ -> e, args
179

180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206
(* namespace lookup *)

let uc_find_ls uc p =
  let x = Typing.string_list_of_qualid [] p in
  ns_find_ls (Theory.get_namespace (get_theory uc)) x

let uc_find_prgs uc p =
  let x = Typing.string_list_of_qualid [] p in
  ns_find_ps (get_namespace uc) x

exception LS of lsymbol

let uc_find_ps_or_ls uc p =
  let x = Typing.string_list_of_qualid [] p in
  try ns_find_ps (get_namespace uc) x with Not_found ->
  (* we didn't find p in the module namespace *)
  let ls = ns_find_ls (Theory.get_namespace (get_theory uc)) x in
  (* and we did find it in the pure theory *)
  if Mid.mem ls.ls_name (get_known uc) then
    (* but it was defined in a program declaration! *)
    error ~loc:(qloc p) (HiddenPLS ls);
  (* fine, it's just a pure lsymbol *)
  raise (LS ls)

let uc_find_ps uc p =
  try uc_find_ps_or_ls uc p with LS _ -> raise Not_found

207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226
(* 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

227 228 229
let find_field uc (p,e) = try match uc_find_ps uc p with
  | PL pl -> (pl,e)
  | _ -> errorm ~loc:(qloc p) "bad record field %a" print_qualid p
230
  with Not_found -> errorm ~loc:(qloc p) "unbound symbol %a" print_qualid p
231

232
let find_pure_field uc (p,e) = try uc_find_ls uc p, e
233
  with Not_found -> errorm ~loc:(qloc p) "unbound symbol %a" print_qualid p
234

235 236
let pure_record uc = function
  | [] -> raise Decl.EmptyRecord
237
  | (p,_)::_ -> (try ignore (uc_find_ps uc p); false with Not_found -> true)
238 239

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

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

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

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

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

let mk_dexpr desc dity loc labs =
265
  { de_desc = desc; de_type = dity; de_loc = loc; de_lab = labs }
266

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

273 274 275 276 277 278 279
(* patterns *)

let add_var id dity denv =
  let tvars = add_tvars denv.tvars dity in
  let locals = Mstr.add id.id (tvars,dity) denv.locals in
  { denv with locals = locals; tvars = tvars }

280 281 282 283 284 285 286 287 288 289 290 291 292
let specialize_qualid uc p = try match uc_find_ps_or_ls uc p with
  | PV pv -> DEglobal_pv pv, specialize_pvsymbol pv
  | PS ps -> DEglobal_ps ps, specialize_psymbol  ps
  | PL pl -> DEglobal_pl pl, specialize_plsymbol pl
  | PX xs -> errorm ~loc:(qloc p) "unexpected exception symbol %a" print_xs xs
  with
  | LS ls -> DEglobal_ls ls, specialize_lsymbol ls
  | Not_found -> errorm ~loc:(qloc p) "unbound symbol %a" print_qualid p

let find_xsymbol uc p = try match uc_find_prgs uc p with
  | PX xs -> xs
  | _ -> errorm ~loc:(qloc p) "exception symbol expected"
  with Not_found -> errorm ~loc:(qloc p) "unbound symbol %a" print_qualid p
Andrei Paskevich's avatar
Andrei Paskevich committed
293

294 295 296 297
let find_variant_ls uc p = try match uc_find_ls uc p with
  | { 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
  with Not_found -> errorm ~loc:(qloc p) "unbound symbol %a" print_qualid p
298

299 300 301
let find_global_vs uc p = try match uc_find_prgs uc p with
  | PV pv -> Some pv.pv_vs
  | _ -> None
302 303
  with Not_found -> None

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

338 339 340 341
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
342
  let ppl, tyl, denv = List.fold_right add_pp ppl ([],[],denv) in
343
  let pp = match de.de_desc with
344 345
    | DEglobal_pl pl -> Mlw_expr.PPpapp (pl, ppl)
    | DEglobal_ls ls -> PPlapp (ls, ppl)
346 347
    | 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
348 349 350
    | _ -> assert false
  in
  let res = create_type_variable () in
351
  Loc.try2 gloc unify_list de.de_type tyl res;
352 353
  pp, res, denv

354 355
(* specifications *)

356
let dbinders denv bl =
357
  let hv = Hashtbl.create 3 in
358
  let dbinder (id,gh,pty) (denv,bl,tyl) =
359 360
    if Hashtbl.mem hv id.id then errorm "duplicate argument %s" id.id;
    Hashtbl.add hv id.id ();
361 362 363
    let dity = match pty with
      | Some pty -> dity_of_pty ~user:true denv pty
      | None -> create_type_variable () in
364
    add_var id dity denv, (id,gh,dity)::bl, dity::tyl
365 366
  in
  List.fold_right dbinder bl (denv,[],[])
367 368

let deff_of_peff uc pe =
369 370 371
  { 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; }
372 373 374 375 376 377 378 379 380 381 382 383 384 385 386

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

let rec dtype_c denv tyc =
  let tyv, dity = dtype_v denv tyc.pc_result_type in
  { 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); },
  dity

and dtype_v denv = function
  | Tpure pty ->
      let dity = dity_of_pty ~user:true denv pty in
387
      DSpecV (false,dity), dity
388 389 390 391
  | Tarrow (bl,tyc) ->
      let denv,bl,tyl = dbinders denv bl in
      let tyc,dity = dtype_c denv tyc in
      DSpecA (bl,tyc), make_arrow_type tyl dity
392

393 394 395 396 397 398 399 400
let dvariant uc = function
  | Some (le, Some q) -> [le, Some (find_variant_ls uc q)]
  | Some (le, None) -> [le, None]
  | None -> []
(* TODO: accept a list of variants in the surface language
  List.map (fun (le,q) -> le, Util.option_map (find_variant_ls uc) q) var
*)

401
(* expressions *)
402

403
let de_unit ~loc = hidden_ls ~loc (Term.fs_tuple 0)
404

405
let de_app loc e el =
406
  let res = create_type_variable () in
407 408
  let tyl = List.map (fun a -> (a.de_loc, a.de_type)) el in
  Loc.try2 loc unify_list e.de_type tyl res;
409 410
  DEapply (e, el), res

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
602
and dletrec denv rdl =
Andrei Paskevich's avatar
Andrei Paskevich committed
603
  (* add all functions into environment *)
604
  let add_one denv (_,id,_,_,_,_) =
Andrei Paskevich's avatar
Andrei Paskevich committed
605
    let res = create_type_variable () in
606 607
    add_var id res denv, res in
  let denv, tyl = Util.map_fold_left add_one denv rdl in
Andrei Paskevich's avatar
Andrei Paskevich committed
608
  (* then type-check all of them and unify *)
609
  let type_one (loc, id, gh, bl, var, tr) res =
610
    let lam, dity = dlambda denv bl var tr in
Andrei Paskevich's avatar
Andrei Paskevich committed
611
    Loc.try2 id.id_loc unify dity res;
612 613
    loc, id, gh, dity, lam in
  List.map2 type_one rdl tyl
Andrei Paskevich's avatar
Andrei Paskevich committed
614

615 616
and dlambda denv bl var (p, e, (q, xq)) =
  let denv,bl,tyl = dbinders denv bl in
Andrei Paskevich's avatar
Andrei Paskevich committed
617
  let e = dexpr denv e in
618 619 620
  let var = dvariant denv.uc var in
  let xq = dxpost denv.uc xq in
  (bl, var, p, e, q, xq), make_arrow_type tyl e.de_type
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
621

622
(** stage 2 *)
623

Andrei Paskevich's avatar
Andrei Paskevich committed
624 625 626 627 628
type lenv = {
  mod_uc   : module_uc;
  let_vars : let_var Mstr.t;
  log_vars : vsymbol Mstr.t;
  log_denv : Typing.denv;
629 630
}

Andrei Paskevich's avatar
Andrei Paskevich committed
631
let create_lenv uc = {
632
  mod_uc   = use_export_theory uc Mlw_wp.th_mark;
633 634
  let_vars = Mstr.empty;
  log_vars = Mstr.empty;
635
  log_denv = Typing.denv_empty_with_globals (find_global_vs uc);
636 637 638
}

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

642
let create_post lenv x ty f =
643
  let th = get_theory lenv.mod_uc in
644 645 646
  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
647 648
  let f = Typing.type_fmla th log_denv log_vars f in
  count_term_tuples f;
649
  create_post res f
650 651

let create_pre lenv f =
652 653 654 655
  let th = get_theory lenv.mod_uc in
  let f = Typing.type_fmla th lenv.log_denv lenv.log_vars f in
  count_term_tuples f;
  f
656

657
let create_variant lenv (t,r) =
658 659 660
  let th = get_theory lenv.mod_uc in
  let t = Typing.type_term th lenv.log_denv lenv.log_vars t in
  count_term_tuples t;
661
  { v_term = t; v_rel = r }
Andrei Paskevich's avatar
Andrei Paskevich committed
662

Andrei Paskevich's avatar
Andrei Paskevich committed
663
let add_local x lv lenv = match lv with
664
  | LetA _ ->
Andrei Paskevich's avatar
Andrei Paskevich committed
665
      { lenv with let_vars = Mstr.add x lv lenv.let_vars }
666 667
  | LetV pv ->
      let dty = dty_of_ty pv.pv_vs.vs_ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
668 669 670 671
      { mod_uc   = lenv.mod_uc;
        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 }
672

673 674
exception DuplicateException of xsymbol

675 676 677 678 679 680 681 682 683 684 685 686 687
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) =
    let f = create_post lenv "result" (ty_of_ity xs.xs_ity) f in
    Mexn.add_new (DuplicateException xs) xs f m in
  List.fold_left add_exn Mexn.empty xq

688 689 690 691
(* 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
692
        | LetV pv -> pv.pv_vtv
693 694 695
        | LetA _ -> errorm ~loc "%s must be a first-order value" x
      end
  | Ptree.PPvar p ->
696 697
      begin try match uc_find_prgs lenv.mod_uc p with
        | PV pv -> pv.pv_vtv
698 699
        | _ -> errorm ~loc:(qloc p) "%a is not a variable" print_qualid p
      with Not_found -> errorm ~loc "unbound variable %a" print_qualid p end
700
  | Ptree.PPapp (p, [le]) ->
701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722
      let vtv = get_eff_expr lenv le in
      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
723
        | _ -> quit ()
724 725 726 727 728 729 730 731
      in
      let itya, vtvv =
        try Mls.find (uc_find_ls lenv.mod_uc p) pjm with Not_found ->
          errorm ~loc:(qloc p) "%a is not a field name" print_qualid p in
      let sbs = unify_loc loc (ity_match ity_subst_empty) itya vtv.vtv_ity in
      let mut = Util.option_map (reg_full_inst sbs) vtvv.vtv_mut in
      let ghost = vtv.vtv_ghost || vtvv.vtv_ghost in
      vty_value ~ghost ?mut (ity_full_inst sbs vtvv.vtv_ity)
732 733 734 735 736 737
  | Ptree.PPcast (e,_) | Ptree.PPnamed (_,e) ->
      get_eff_expr lenv e
  | _ ->
      errorm ~loc "unsupported effect expression"

let get_eff_regs lenv fn eff ghost le =
738
  let 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 760 761 762 763 764 765
  let ghost = ghost || vtv.vtv_ghost in
  match vtv.vtv_mut, vtv.vtv_ity.ity_node with
  | Some reg, _ ->
      fn eff ?ghost:(Some ghost) reg
  | None, Ityapp (its,_,(_::_ as regl)) ->
      let add_arg regs vtv = match vtv.vtv_mut with
        | Some r when vtv.vtv_ghost -> Sreg.add r regs | _ -> regs in
      let add_cs regs (cs,_) = List.fold_left add_arg regs cs.pl_args in
      let csl = find_constructors (get_known lenv.mod_uc) its in
      let ghost_regs = List.fold_left add_cs Sreg.empty csl in
      let add_reg eff reg0 reg =
        let ghost = ghost || Sreg.mem reg0 ghost_regs in
        fn eff ?ghost:(Some ghost) reg
      in
      List.fold_left2 add_reg eff its.its_regs regl
  | _ ->
      errorm ~loc:le.pp_loc "mutable expression expected"

let eff_of_deff lenv deff =
  let add_read eff (gh,e) = get_eff_regs lenv eff_read eff gh e in
  let eff = List.fold_left add_read eff_empty deff.deff_reads in
  let add_write eff (gh,e) = get_eff_regs lenv eff_write eff gh e in
  let eff = List.fold_left add_write eff deff.deff_writes in
  let add_raise eff (gh,xs) = eff_raise eff ~ghost:gh xs in
  let eff = List.fold_left add_raise eff deff.deff_raises in
  eff

766 767
let rec type_c lenv gh vars dtyc =
  let result = type_v lenv gh vars dtyc.dc_result in
768 769 770
  let ty = match result with
    | SpecV v -> ty_of_ity v.vtv_ity
    | SpecA _ -> ty_unit in
771 772 773 774 775 776 777 778 779
  let eff = eff_of_deff lenv dtyc.dc_effect in
  (* reset every new region in the result *)
  let eff = match result with
    | SpecV v ->
        let rec add_reg r eff =
          if reg_occurs r vars then eff else eff_reset (add_ity r.reg_ity eff) r
        and add_ity ity eff = Sreg.fold add_reg ity.ity_vars.vars_reg eff in
        add_ity v.vtv_ity eff
    | SpecA _ -> eff in
780
  { c_pre    = create_pre lenv dtyc.dc_pre;
781
    c_effect = eff;
782 783 784 785
    c_result = result;
    c_post   = create_post lenv "result" ty dtyc.dc_post;
    c_xpost  = xpost lenv dtyc.dc_xpost; }

786
and type_v lenv gh vars = function
787
  | DSpecV (ghost,v) ->
788
      let ghost = ghost || gh in
789 790 791
      SpecV (vty_value ~ghost (ity_of_dity v))
  | DSpecA (bl,tyc) ->
      let lenv, pvl = binders lenv bl in
792 793
      let add_pv s pv = vars_union s pv.pv_vtv.vtv_vars in
      let vars = List.fold_left add_pv vars pvl in
794
      SpecA (pvl, type_c lenv gh vars tyc)
795 796 797

(* expressions *)

798 799 800 801 802 803
let vty_ghostify gh vty =
  if gh && not (vty_ghost vty) then vty_ghostify vty else vty

let e_ghostify gh e =
  if gh && not (vty_ghost e.e_vty) then e_ghost e else e

804 805 806 807 808 809
let rec expr lenv de =
  let loc = de.de_loc in
  let e = Loc.try3 loc expr_desc lenv loc de in
  e_label ~loc de.de_lab e

and expr_desc lenv loc de = match de.de_desc with
810
  | DElocal x ->
Andrei Paskevich's avatar
Andrei Paskevich committed
811 812
      assert (Mstr.mem x lenv.let_vars);
      begin match Mstr.find x lenv.let_vars with
813
      | LetV pv -> e_value pv
814
      | LetA ps -> e_cast ps (vty_of_dity de.de_type)
815
      end
816 817
  | DElet (x, gh, { de_desc = DEfun lam }, de2) ->
      let def = expr_fun lenv x gh lam in
818
      let lenv = add_local x.id (LetA def.rec_ps) lenv in
Andrei Paskevich's avatar
Andrei Paskevich committed
819
      let e2 = expr lenv de2 in
820 821
      e_rec [def] e2
  | DEfun lam ->
822
      let x = mk_id "fn" loc in
823
      let def = expr_fun lenv x false lam in
824 825
      let e2 = e_cast def.rec_ps (VTarrow def.rec_ps.ps_vta) in
      e_rec [def] e2
826 827 828 829 830 831 832 833 834 835 836 837 838
  (* FIXME? (ghost "lab" fun x -> ...) loses the label "lab" *)
  | DEghost { de_desc = DEfun lam } ->
      let x = mk_id "fn" loc in
      let def = expr_fun lenv x true lam in
      let e2 = e_cast def.rec_ps (VTarrow def.rec_ps.ps_vta) in
      e_rec [def] e2
  | DElet (x, gh, de1, de2) ->
      let e1 = e_ghostify gh (expr lenv de1) in
      begin match e1.e_vty with
        | VTarrow { vta_ghost = true } when not gh ->
            errorm ~loc "%s must be a ghost function" x.id
        | _ -> ()
      end;
839
      let def1 = create_let_defn (Denv.create_user_id x) e1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
840 841
      let lenv = add_local x.id def1.let_var lenv in
      let e2 = expr lenv de2 in
842
      e_let def1 e2
Andrei Paskevich's avatar
Andrei Paskevich committed
843
  | DEletrec (rdl, de1) ->