mlw_typing.ml 56.6 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 112 113 114 115 116 117
(* 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

118
let flush_tuples uc =
119 120 121 122 123 124
  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;
125 126 127 128
  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
129

130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146
(** 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)

147 148 149 150 151 152 153
(** 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
154 155 156
      begin match uc_find_ts denv.uc p with
        | PT ts -> its_app ~user ts dl
        | TS ts -> ts_app ts dl
157 158
      end
  | Ptree.PPTtuple pl ->
159 160
      let dl = List.map (dity_of_pty ~user denv) pl in
      ts_app (ts_tuple (List.length pl)) dl
161 162 163

(** Typing program expressions *)

Andrei Paskevich's avatar
Andrei Paskevich committed
164
let dity_int  = ts_app ts_int  []
165
let dity_real = ts_app ts_real []
166
let dity_bool = ts_app ts_bool []
Andrei Paskevich's avatar
Andrei Paskevich committed
167 168
let dity_unit = ts_app ts_unit []
let dity_mark = ts_app ts_mark []
169

170
let unify_loc unify_fn loc x1 x2 = try unify_fn x1 x2 with
171
  | TypeMismatch (ity1,ity2) -> errorm ~loc
172 173 174
      "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
175

176 177 178 179 180 181 182
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
183

184
let rec extract_labels labs loc e = match e.Ptree.expr_desc with
185
  | Ptree.Enamed (Ptree.Lstr s, e) -> extract_labels (Slab.add s labs) loc e
186 187 188 189
  | 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)
190
  | e -> labs, loc, e
191

192 193 194
let rec decompose_app args e = match e.Ptree.expr_desc with
  | Eapply (e1, e2) -> decompose_app (e2 :: args) e1
  | _ -> e, args
195

196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215
(* 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

216 217
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
218

219
let find_pure_field uc (p,e) = uc_find_ls uc p, e
220

221 222
let is_pure_record uc = function
  | fl :: _ -> (try ignore (find_prog_field uc fl); false with _ -> true)
223
  | [] -> raise Decl.EmptyRecord
224 225

let hidden_pl ~loc pl =
226 227
  { de_desc = DEglobal_pl pl;
    de_type = specialize_plsymbol pl;
228
    de_loc  = loc; de_lab = Slab.empty }
229 230

let hidden_ls ~loc ls =
231 232
  { de_desc = DEglobal_ls ls;
    de_type = specialize_lsymbol ls;
233
    de_loc  = loc; de_lab = Slab.empty }
234 235

(* helper functions for let-expansion *)
236
let test_var e = match e.de_desc with
237 238 239 240 241
  | DElocal _ | DEglobal_pv _ -> true
  | _ -> false

let mk_var e =
  if test_var e then e else
242 243 244
  { de_desc = DElocal "q";
    de_type = e.de_type;
    de_loc  = e.de_loc;
245
    de_lab  = Slab.empty }
246

247 248 249
let mk_id s loc =
  { id = s; id_loc = loc; id_lab = [] }

250 251
let mk_dexpr desc dvty loc labs =
  { de_desc = desc; de_type = dvty; de_loc = loc; de_lab = labs }
252

253 254
let mk_let ~loc ~uloc e (desc,dvty) =
  if test_var e then desc, dvty else
Andrei Paskevich's avatar
Andrei Paskevich committed
255
  let loc = def_option loc uloc in
256 257
  let e1 = mk_dexpr desc dvty loc Slab.empty in
  DElet (mk_id "q" loc, false, e, e1), dvty
258

259 260 261
(* patterns *)

let add_var id dity denv =
262 263
  let tvars = add_dity denv.tvars dity in
  let locals = Mstr.add id.id (tvars,([],dity)) denv.locals in
264 265
  { denv with locals = locals; tvars = tvars }

266
let specialize_qualid uc p = match uc_find_ps uc p with
267
  | PV pv -> DEglobal_pv pv, ([],specialize_pvsymbol pv)
268 269 270
  | PS ps -> DEglobal_ps ps, specialize_psymbol  ps
  | PL pl -> DEglobal_pl pl, specialize_plsymbol pl
  | LS ls -> DEglobal_ls ls, specialize_lsymbol ls
271
  | XS xs -> errorm ~loc:(qloc p) "unexpected exception symbol %a" print_xs xs
272

273 274
let find_xsymbol uc p = match uc_find_ps uc p with
  | XS xs -> xs
275
  | _ -> errorm ~loc:(qloc p) "exception symbol expected"
Andrei Paskevich's avatar
Andrei Paskevich committed
276

277
let find_variant_ls uc p = match uc_find_ls uc p with
278 279
  | { 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
280

281
let find_global_vs uc p = try match uc_find_ps uc p with
282 283
  | PV pv -> Some pv.pv_vs
  | _ -> None
284
  with _ -> None
285

286 287 288 289 290
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
291
      PPvar (Denv.create_user_id id), dity, add_var id dity denv
292
  | Ptree.PPpapp (q,ppl) ->
293 294
      let sym, dvty = specialize_qualid denv.uc q in
      dpat_app denv loc (mk_dexpr sym dvty loc Slab.empty) ppl
295
  | Ptree.PPprec fl when is_pure_record denv.uc fl ->
296
      let kn = Theory.get_known (get_theory denv.uc) in
297
      let fl = List.map (find_pure_field denv.uc) fl in
298 299 300
      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
301
      dpat_app denv loc (hidden_ls ~loc cs) (List.map get_val pjl)
302
  | Ptree.PPprec fl ->
303
      let fl = List.map (find_prog_field denv.uc) fl in
304 305 306
      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
307
      dpat_app denv loc (hidden_pl ~loc cs) (List.map get_val pjl)
308 309
  | Ptree.PPptuple ppl ->
      let cs = fs_tuple (List.length ppl) in
310 311 312 313
      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
314
      unify_loc unify lpp2.pat_loc dity1 dity2;
315 316 317
      PPor (pp1, pp2), dity1, denv
  | Ptree.PPpas (pp, id) ->
      let pp, dity, denv = dpattern denv pp in
318
      PPas (pp, Denv.create_user_id id), dity, add_var id dity denv
319

320 321 322 323
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
324
  let ppl, tyl, denv = List.fold_right add_pp ppl ([],[],denv) in
325 326 327
  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
328 329
    | 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
330 331
    | _ -> assert false
  in
332 333 334 335 336
  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;
337 338
  pp, res, denv

339 340
(* specifications *)

341
let dbinders denv bl =
342
  let hv = Hashtbl.create 3 in
343
  let dbinder (id,gh,pty) (denv,bl,tyl) =
344
    if Hashtbl.mem hv id.id then raise (DuplicateProgVar id.id);
345
    Hashtbl.add hv id.id ();
346 347 348
    let dity = match pty with
      | Some pty -> dity_of_pty ~user:true denv pty
      | None -> create_type_variable () in
349
    add_var id dity denv, (id,gh,dity)::bl, dity::tyl
350 351
  in
  List.fold_right dbinder bl (denv,[],[])
352 353

let deff_of_peff uc pe =
354 355 356
  { 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; }
357 358 359 360

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

let rec dtype_c denv tyc =
361
  let tyv, dvty = dtype_v denv tyc.pc_result_type in
362 363 364 365 366
  { 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); },
367
  dvty
368 369 370 371

and dtype_v denv = function
  | Tpure pty ->
      let dity = dity_of_pty ~user:true denv pty in
372
      DSpecV (false,dity), ([],dity)
373 374
  | Tarrow (bl,tyc) ->
      let denv,bl,tyl = dbinders denv bl in
375 376
      let tyc,(argl,res) = dtype_c denv tyc in
      DSpecA (bl,tyc), (tyl @ argl,res)
377

378 379 380 381 382 383 384 385
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
*)

386
(* expressions *)
387

388
let de_unit ~loc = hidden_ls ~loc (Term.fs_tuple 0)
389

390 391 392 393 394 395 396 397 398 399 400 401 402 403
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
404

Andrei Paskevich's avatar
Andrei Paskevich committed
405
let rec dexpr denv e =
406
  let loc = e.Ptree.expr_loc in
407
  let labs, uloc, d = extract_labels Slab.empty denv.uloc e in
Andrei Paskevich's avatar
Andrei Paskevich committed
408
  let denv = { denv with uloc = uloc } in
409
  let d, ty = de_desc denv loc d in
Andrei Paskevich's avatar
Andrei Paskevich committed
410
  let loc = def_option loc uloc in
411
  mk_dexpr d ty loc labs
412

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

Andrei Paskevich's avatar
Andrei Paskevich committed
604
and dletrec denv rdl =
605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626
  (* 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
627

628
and dlambda denv bl var (p, e, (q, xq)) =
Andrei Paskevich's avatar
Andrei Paskevich committed
629
  let e = dexpr denv e in
630 631
  let var = dvariant denv.uc var in
  let xq = dxpost denv.uc xq in
632
  (bl, var, p, e, q, xq), e.de_type
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
633

634
(** stage 2 *)
635

Andrei Paskevich's avatar
Andrei Paskevich committed
636 637
type lenv = {
  mod_uc   : module_uc;
638 639
  th_at    : Theory.theory_uc;
  th_old   : Theory.theory_uc;
Andrei Paskevich's avatar
Andrei Paskevich committed
640 641 642
  let_vars : let_var Mstr.t;
  log_vars : vsymbol Mstr.t;
  log_denv : Typing.denv;
643 644
}

Andrei Paskevich's avatar
Andrei Paskevich committed
645
let create_lenv uc = {
646 647 648
  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;
649 650
  let_vars = Mstr.empty;
  log_vars = Mstr.empty;
651
  log_denv = Typing.denv_empty_with_globals (find_global_vs uc);
652 653 654
}

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

658 659 660 661
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
662 663
  let f = Typing.type_fmla lenv.th_old log_denv log_vars f in
  let f = remove_old f in
664
  count_term_tuples f;
665
  create_post res f
666 667

let create_pre lenv f =
668
  let f = Typing.type_fmla lenv.th_at lenv.log_denv lenv.log_vars f in
669 670
  count_term_tuples f;
  f
671

672
let create_variant lenv (t,r) =
673
  let t = Typing.type_term lenv.th_at lenv.log_denv lenv.log_vars t in
674
  count_term_tuples t;
675
  { v_term = t; v_rel = r }
Andrei Paskevich's avatar
Andrei Paskevich committed
676

Andrei Paskevich's avatar
Andrei Paskevich committed
677
let add_local x lv lenv = match lv with
678
  | LetA _ ->
Andrei Paskevich's avatar
Andrei Paskevich committed
679
      { lenv with let_vars = Mstr.add x lv lenv.let_vars }
680 681
  | LetV pv ->
      let dty = dty_of_ty pv.pv_vs.vs_ty in
682
      { lenv with
Andrei Paskevich's avatar
Andrei Paskevich committed
683 684 685
        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 }
686

687 688
exception DuplicateException of xsymbol

689 690 691 692 693 694 695 696 697 698 699 700 701
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

702 703 704 705
(* 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
706
        | LetV pv -> pv.pv_vtv
707
        | LetA _ -> errorm ~loc "'%s' must be a first-order value" x
708 709
      end
  | Ptree.PPvar p ->
710
      begin match uc_find_ps lenv.mod_uc p with
711
        | PV pv -> pv.pv_vtv
712 713
        | _ -> errorm ~loc:(qloc p) "'%a' must be a variable" print_qualid p
      end
714
  | Ptree.PPapp (p, [le]) ->
715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736
      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
737
        | _ -> quit ()
738 739 740
      in
      let itya, vtvv =
        try Mls.find (uc_find_ls lenv.mod_uc p) pjm with Not_found ->
741
          errorm ~loc:(qloc p) "'%a' must be a field name" print_qualid p in
742
      let sbs = unify_loc (ity_match ity_subst_empty) loc itya vtv.vtv_ity in
743 744 745
      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)
746 747 748 749 750 751
  | 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 =
752
  let vtv = get_eff_expr lenv le in
753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779
  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

780 781
let rec type_c lenv gh vars dtyc =
  let result = type_v lenv gh vars dtyc.dc_result in
782 783 784
  let ty = match result with
    | SpecV v -> ty_of_ity v.vtv_ity
    | SpecA _ -> ty_unit in
785 786 787 788 789 790 791 792 793
  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
794
  { c_pre    = create_pre lenv dtyc.dc_pre;