mlw_typing.ml 53.2 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
(** 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 ->
123
          errorm ~loc:(qloc p) "unbound symbol %a" print_qualid p
124 125 126
      end
  | Ptree.PPTtuple pl ->
      ts_app (ts_tuple (List.length pl)) (List.map (dity_of_pty ~user denv) pl)
127 128 129

(** Typing program expressions *)

Andrei Paskevich's avatar
Andrei Paskevich committed
130
let dity_int  = ts_app ts_int  []
131
let dity_real = ts_app ts_real []
132
let dity_bool = ts_app ts_bool []
Andrei Paskevich's avatar
Andrei Paskevich committed
133 134
let dity_unit = ts_app ts_unit []
let dity_mark = ts_app ts_mark []
135

136
let expected_type ?(weak=false) e dity =
137
  unify ~weak e.de_type dity
138

139
let rec extract_labels labs loc e = match e.Ptree.expr_desc with
140
  | Ptree.Enamed (Ptree.Lstr s, e) -> extract_labels (Slab.add s labs) loc e
141 142 143 144
  | 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)
145
  | e -> labs, loc, e
146

147 148 149
let rec decompose_app args e = match e.Ptree.expr_desc with
  | Eapply (e1, e2) -> decompose_app (e2 :: args) e1
  | _ -> e, args
150

151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170
(* 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

171
let find_field uc (p,e) =
172 173 174
  let x = Typing.string_list_of_qualid [] p in
  try match ns_find_ps (get_namespace uc) x with
    | PL pl -> (pl,e)
175 176
    | _ -> errorm ~loc:(qloc p) "bad record field %a" print_qualid p
  with Not_found -> errorm ~loc:(qloc p) "unbound symbol %a" print_qualid p
177

178
let find_pure_field uc (p,e) =
179 180
  let x = Typing.string_list_of_qualid [] p in
  try ns_find_ls (Theory.get_namespace (get_theory uc)) x, e
181
  with Not_found -> errorm ~loc:(qloc p) "unbound symbol %a" print_qualid p
182

183 184
let pure_record uc = function
  | [] -> raise Decl.EmptyRecord
185 186 187 188 189 190
  | (p,_)::_ ->
      let x = Typing.string_list_of_qualid [] p in
      begin try ignore (ns_find_ps (get_namespace uc) x); false
      with Not_found -> true end

let hidden_pl ~loc pl =
191 192
  { de_desc = DEglobal_pl pl;
    de_type = specialize_plsymbol pl;
193
    de_loc  = loc; de_lab = Slab.empty }
194 195

let hidden_ls ~loc ls =
196 197
  { de_desc = DEglobal_ls ls;
    de_type = specialize_lsymbol ls;
198
    de_loc  = loc; de_lab = Slab.empty }
199 200

(* helper functions for let-expansion *)
201
let test_var e = match e.de_desc with
202 203 204 205 206
  | DElocal _ | DEglobal_pv _ -> true
  | _ -> false

let mk_var e =
  if test_var e then e else
207 208 209
  { de_desc = DElocal "q";
    de_type = e.de_type;
    de_loc  = e.de_loc;
210
    de_lab  = Slab.empty }
211

212 213 214 215
let mk_id s loc =
  { id = s; id_loc = loc; id_lab = [] }

let mk_dexpr desc dity loc labs =
216
  { de_desc = desc; de_type = dity; de_loc = loc; de_lab = labs }
217

Andrei Paskevich's avatar
Andrei Paskevich committed
218
let mk_let ~loc ~uloc e (desc,dity) =
219
  if test_var e then desc, dity else
Andrei Paskevich's avatar
Andrei Paskevich committed
220
  let loc = def_option loc uloc in
221
  let e1 = mk_dexpr desc dity loc Slab.empty in
222
  DElet (mk_id "q" loc, false, e, e1), dity
223

224 225 226 227 228 229 230
(* 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 }

231
let specialize_qualid uc p =
232 233 234 235 236
  let x = Typing.string_list_of_qualid [] p in
  try match ns_find_ps (get_namespace uc) x 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
237 238
    | PX xs ->
        errorm ~loc:(qloc p) "unexpected exception symbol %a" print_xs xs
239 240 241 242
  with Not_found -> try
    let ls = ns_find_ls (Theory.get_namespace (get_theory uc)) x in
    DEglobal_ls ls, specialize_lsymbol ls
  with Not_found ->
243
    errorm ~loc:(qloc p) "unbound symbol %a" print_qualid p
244

245
let find_xsymbol uc p =
Andrei Paskevich's avatar
Andrei Paskevich committed
246 247
  let x = Typing.string_list_of_qualid [] p in
  try match ns_find_ps (get_namespace uc) x with
248
    | PX xs -> xs
249
    | _ -> errorm ~loc:(qloc p) "exception symbol expected"
Andrei Paskevich's avatar
Andrei Paskevich committed
250
  with Not_found ->
251
    errorm ~loc:(qloc p) "unbound symbol %a" print_qualid p
Andrei Paskevich's avatar
Andrei Paskevich committed
252

253
let find_variant_ls uc p =
254 255
  let x = Typing.string_list_of_qualid [] p in
  try match ns_find_ps (get_namespace uc) x with
256
    | _ -> errorm ~loc:(qloc p) "%a is not a binary relation" print_qualid p
257 258 259
  with Not_found -> try
    match ns_find_ls (Theory.get_namespace (get_theory uc)) x with
      | { ls_args = [u;v]; ls_value = None } as ls when ty_equal u v -> ls
260 261
      | ls ->
          errorm ~loc:(qloc p) "%a is not a binary relation" Pretty.print_ls ls
262
  with Not_found ->
263
    errorm ~loc:(qloc p) "unbound symbol %a" print_qualid p
264

265 266 267 268 269 270 271
let find_global_vs uc p =
  let x = Typing.string_list_of_qualid [] p in
  try match ns_find_ps (get_namespace uc) x with
    | PV pv -> Some pv.pv_vs
    | _ -> None
  with Not_found -> None

272 273 274 275 276
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
277
      PPvar (Denv.create_user_id id), dity, add_var id dity denv
278
  | Ptree.PPpapp (q,ppl) ->
279
      let sym, dity = specialize_qualid denv.uc q in
280
      dpat_app denv (mk_dexpr sym dity loc Slab.empty) ppl
281
  | Ptree.PPprec fl when pure_record denv.uc fl ->
282
      let kn = Theory.get_known (get_theory denv.uc) in
283
      let fl = List.map (find_pure_field denv.uc) fl in
284 285 286 287 288
      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
      dpat_app denv (hidden_ls ~loc cs) (List.map get_val pjl)
  | Ptree.PPprec fl ->
289
      let fl = List.map (find_field denv.uc) fl in
290 291 292 293 294 295 296 297 298 299 300 301 302 303
      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
      dpat_app denv (hidden_pl ~loc cs) (List.map get_val pjl)
  | Ptree.PPptuple ppl ->
      let cs = fs_tuple (List.length ppl) in
      dpat_app denv (hidden_ls ~loc cs) ppl
  | Ptree.PPpor (pp1, pp2) ->
      let pp1, dity1, denv = dpattern denv pp1 in
      let pp2, dity2, denv = dpattern denv pp2 in
      Loc.try2 loc unify dity1 dity2;
      PPor (pp1, pp2), dity1, denv
  | Ptree.PPpas (pp, id) ->
      let pp, dity, denv = dpattern denv pp in
304
      PPas (pp, Denv.create_user_id id), dity, add_var id dity denv
305

306
and dpat_app denv ({ de_loc = loc } as de) ppl =
307 308 309
  let add_pp pp (ppl, tyl, denv) =
    let pp,ty,denv = dpattern denv pp in pp::ppl,ty::tyl,denv in
  let ppl, tyl, denv = List.fold_right add_pp ppl ([],[],denv) in
310
  let pp = match de.de_desc with
311 312
    | DEglobal_pl pl -> Mlw_expr.PPpapp (pl, ppl)
    | DEglobal_ls ls -> PPlapp (ls, ppl)
313 314
    | 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
315 316 317
    | _ -> assert false
  in
  let res = create_type_variable () in
318
  Loc.try2 loc unify de.de_type (make_arrow_type tyl res);
319 320
  pp, res, denv

321 322
(* specifications *)

323
let dbinders denv bl =
324
  let dbinder (id,gh,pty) (denv,bl,tyl) =
325 326 327
    let dity = match pty with
      | Some pty -> dity_of_pty ~user:true denv pty
      | None -> create_type_variable () in
328
    add_var id dity denv, (id,gh,dity)::bl, dity::tyl
329 330
  in
  List.fold_right dbinder bl (denv,[],[])
331 332

let deff_of_peff uc pe =
333 334 335
  { 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; }
336 337 338 339 340 341 342 343 344 345 346 347 348 349 350

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
351
      DSpecV (false,dity), dity
352 353 354 355
  | 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
356

357 358 359 360 361 362 363 364
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
*)

365
(* expressions *)
366

367 368 369
let de_unit ~loc = hidden_ls ~loc (fs_tuple 0)

let de_app e el =
370
  let res = create_type_variable () in
371
  let tyl = List.map (fun a -> a.de_type) el in
372 373 374
  expected_type e (make_arrow_type tyl res);
  DEapply (e, el), res

Andrei Paskevich's avatar
Andrei Paskevich committed
375
let rec dexpr denv e =
376
  let loc = e.Ptree.expr_loc in
377
  let labs, uloc, d = extract_labels Slab.empty denv.uloc e in
Andrei Paskevich's avatar
Andrei Paskevich committed
378
  let denv = { denv with uloc = uloc } in
379
  let d, ty = de_desc denv loc d in
Andrei Paskevich's avatar
Andrei Paskevich committed
380
  let loc = def_option loc uloc in
381
  mk_dexpr d ty loc labs
382

383
and de_desc denv loc = function
384 385
  | Ptree.Eident (Qident {id=x}) when Mstr.mem x denv.locals ->
      (* local variable *)
386 387 388
      let tvs, dity = Mstr.find x denv.locals in
      let dity = specialize_scheme tvs dity in
      DElocal x, dity
389
  | Ptree.Eident p ->
390
      specialize_qualid denv.uc p
391 392
  | Ptree.Eapply (e1, e2) ->
      let e, el = decompose_app [e2] e1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
393
      let el = List.map (dexpr denv) el in
394
      de_app (dexpr denv e) el
395
  | Ptree.Elet (id, gh, e1, e2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
396
      let e1 = dexpr denv e1 in
397 398
      let dity = e1.de_type in
      let tvars = match e1.de_desc with
Andrei Paskevich's avatar
Andrei Paskevich committed
399 400
        | DEfun _ -> denv.tvars
        | _ -> add_tvars denv.tvars dity in
401 402
      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
403
      let e2 = dexpr denv e2 in
404
      DElet (id, gh, e1, e2), e2.de_type
Andrei Paskevich's avatar
Andrei Paskevich committed
405
  | Ptree.Eletrec (rdl, e1) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
406
      let rdl = dletrec denv rdl in
407
      let add_one denv (_, { id = id }, _, dity, _) =
408 409
        { 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
410
      let e1 = dexpr denv e1 in
411
      DEletrec (rdl, e1), e1.de_type
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
412
  | Ptree.Efun (bl, tr) ->
413
      let lam, dity = dlambda denv bl None tr in
414
      DEfun lam, dity
415
  | Ptree.Ecast (e1, pty) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
416
      let e1 = dexpr denv e1 in
417
      expected_type e1 (dity_of_pty ~user:false denv pty);
418
      e1.de_desc, e1.de_type
419 420
  | Ptree.Enamed _ ->
      assert false
421
  | Ptree.Esequence (e1, e2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
422
      let e1 = dexpr denv e1 in
423
      expected_type e1 dity_unit;
Andrei Paskevich's avatar
Andrei Paskevich committed
424
      let e2 = dexpr denv e2 in
425
      DElet (mk_id "_" loc, false, e1, e2), e2.de_type
426
  | Ptree.Eif (e1, e2, e3) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
427
      let e1 = dexpr denv e1 in
428
      expected_type e1 dity_bool;
Andrei Paskevich's avatar
Andrei Paskevich committed
429 430
      let e2 = dexpr denv e2 in
      let e3 = dexpr denv e3 in
431 432
      expected_type e3 e2.de_type;
      DEif (e1, e2, e3), e2.de_type
433 434
  | Ptree.Etuple el ->
      let ls = fs_tuple (List.length el) in
Andrei Paskevich's avatar
Andrei Paskevich committed
435
      let el = List.map (dexpr denv) el in
436 437
      de_app (hidden_ls ~loc ls) el
  | Ptree.Erecord fl when pure_record denv.uc fl ->
438
      let kn = Theory.get_known (get_theory denv.uc) in
439
      let fl = List.map (find_pure_field denv.uc) fl in
440 441
      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
442
        | Some e -> dexpr denv e
443
        | None -> error ~loc (Decl.RecordFieldMissing (cs,pj)) in
444
      de_app (hidden_ls ~loc cs) (List.map get_val pjl)
445
  | Ptree.Erecord fl ->
446
      let fl = List.map (find_field denv.uc) fl in
447 448
      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
449
        | Some e -> dexpr denv e
450
        | None -> error ~loc (Decl.RecordFieldMissing (cs.pl_ls,pj.pl_ls)) in
451 452
      de_app (hidden_pl ~loc cs) (List.map get_val pjl)
  | Ptree.Eupdate (e1, fl) when pure_record denv.uc fl ->
Andrei Paskevich's avatar
Andrei Paskevich committed
453
      let e1 = dexpr denv e1 in
454 455
      let e0 = mk_var e1 in
      let kn = Theory.get_known (get_theory denv.uc) in
456
      let fl = List.map (find_pure_field denv.uc) fl in
457 458
      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
459
        | Some e -> dexpr denv e
460
        | None ->
461
            let d, dity = de_app (hidden_ls ~loc pj) [e0] in
462
            mk_dexpr d dity loc Slab.empty in
463
      let res = de_app (hidden_ls ~loc cs) (List.map get_val pjl) in
Andrei Paskevich's avatar
Andrei Paskevich committed
464
      mk_let ~loc ~uloc:denv.uloc e1 res
465
  | Ptree.Eupdate (e1, fl) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
466
      let e1 = dexpr denv e1 in
467
      let e0 = mk_var e1 in
468
      let fl = List.map (find_field denv.uc) fl in
469 470
      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
471
        | Some e -> dexpr denv e
472
        | None ->
473
            let d, dity = de_app (hidden_pl ~loc pj) [e0] in
474
            mk_dexpr d dity loc Slab.empty in
475
      let res = de_app (hidden_pl ~loc cs) (List.map get_val pjl) in
Andrei Paskevich's avatar
Andrei Paskevich committed
476
      mk_let ~loc ~uloc:denv.uloc e1 res
Andrei Paskevich's avatar
Andrei Paskevich committed
477
  | Ptree.Eassign (e1, q, e2) ->
478 479
      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
480 481
      let e1 = dexpr denv e1 in
      let e2 = dexpr denv e2 in
482
      expected_type ~weak:true e2 e1.de_type;
Andrei Paskevich's avatar
Andrei Paskevich committed
483
      DEassign (e1, e2), dity_unit
484 485 486 487 488
  | 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
489
      let e1 = dexpr denv e1 in
490 491 492
      expected_type e1 dity_bool;
      DEnot e1, dity_bool
  | Ptree.Elazy (op, e1, e2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
493 494
      let e1 = dexpr denv e1 in
      let e2 = dexpr denv e2 in
495 496 497
      expected_type e1 dity_bool;
      expected_type e2 dity_bool;
      DElazy (op, e1, e2), dity_bool
498
  | Ptree.Ematch (e1, bl) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
499
      let e1 = dexpr denv e1 in
500 501 502
      let res = create_type_variable () in
      let branch (pp,e) =
        let ppat, dity, denv = dpattern denv pp in
Andrei Paskevich's avatar
Andrei Paskevich committed
503
        let e = dexpr denv e in
504
        Loc.try2 pp.pat_loc unify dity e1.de_type;
505 506 507
        expected_type e res;
        ppat, e in
      DEmatch (e1, List.map branch bl), res
Andrei Paskevich's avatar
Andrei Paskevich committed
508 509
  | Ptree.Eraise (q, e1) ->
      let res = create_type_variable () in
510
      let xs = find_xsymbol denv.uc q in
511
      let dity = specialize_xsymbol xs in
Andrei Paskevich's avatar
Andrei Paskevich committed
512
      let e1 = match e1 with
Andrei Paskevich's avatar
Andrei Paskevich committed
513
        | Some e1 -> dexpr denv e1
514
        | None when ity_equal xs.xs_ity ity_unit -> de_unit ~loc
Andrei Paskevich's avatar
Andrei Paskevich committed
515 516 517 518
        | _ -> 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
519
      let e1 = dexpr denv e1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
520
      let branch (q, id, e) =
521
        let xs = find_xsymbol denv.uc q in
522
        let dity = specialize_xsymbol xs in
Andrei Paskevich's avatar
Andrei Paskevich committed
523 524
        let id, denv = match id with
          | Some id -> id, add_var id dity denv
525
          | None -> mk_id "void" loc, denv in
Andrei Paskevich's avatar
Andrei Paskevich committed
526
        xs, id, dexpr denv e
Andrei Paskevich's avatar
Andrei Paskevich committed
527 528
      in
      let cl = List.map branch cl in
529
      DEtry (e1, cl), e1.de_type
530
  | Ptree.Eabsurd ->
531
      DEabsurd, create_type_variable ()
532 533
  | Ptree.Eassert (ak, lexpr) ->
      DEassert (ak, lexpr), dity_unit
Andrei Paskevich's avatar
Andrei Paskevich committed
534 535
  | Ptree.Emark (id, e1) ->
      let e1 = dexpr denv e1 in
536
      DEmark (id, e1), e1.de_type
537
  | Ptree.Eany tyc ->
538 539
      let tyc, dity = dtype_c denv tyc in
      DEany tyc, dity
540 541 542
  | Ptree.Eghost e1 ->
      let e1 = dexpr denv e1 in
      DEghost e1, e1.de_type
543 544 545 546
  | 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
547 548 549 550 551 552 553 554 555 556 557 558 559 560
  | 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
561

Andrei Paskevich's avatar
Andrei Paskevich committed
562
and dletrec denv rdl =
Andrei Paskevich's avatar
Andrei Paskevich committed
563
  (* add all functions into environment *)
564
  let add_one denv (_,id,_,_,_,_) =
Andrei Paskevich's avatar
Andrei Paskevich committed
565
    let res = create_type_variable () in
566 567
    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
568
  (* then type-check all of them and unify *)
569
  let type_one (loc, id, gh, bl, var, tr) res =
570
    let lam, dity = dlambda denv bl var tr in
Andrei Paskevich's avatar
Andrei Paskevich committed
571
    Loc.try2 id.id_loc unify dity res;
572 573
    loc, id, gh, dity, lam in
  List.map2 type_one rdl tyl
Andrei Paskevich's avatar
Andrei Paskevich committed
574

575 576
and dlambda denv bl var (p, e, (q, xq)) =
  let denv,bl,tyl = dbinders denv bl in
Andrei Paskevich's avatar
Andrei Paskevich committed
577
  let e = dexpr denv e in
578 579 580
  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
581

582
(** stage 2 *)
583

Andrei Paskevich's avatar
Andrei Paskevich committed
584 585 586 587 588
type lenv = {
  mod_uc   : module_uc;
  let_vars : let_var Mstr.t;
  log_vars : vsymbol Mstr.t;
  log_denv : Typing.denv;
589 590
}

Andrei Paskevich's avatar
Andrei Paskevich committed
591
let create_lenv uc = {
592
  mod_uc   = use_export_theory uc Mlw_wp.th_mark;
593 594
  let_vars = Mstr.empty;
  log_vars = Mstr.empty;
595
  log_denv = Typing.denv_empty_with_globals (find_global_vs uc);
596 597 598 599 600 601 602 603
}

let rec dty_of_ty ty = match ty.ty_node with
  | Ty.Tyvar v ->
      Typing.create_user_type_var v.tv_name.id_string
  | Ty.Tyapp (ts, tyl) ->
      Denv.tyapp ts (List.map dty_of_ty tyl)

604 605 606 607
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
608 609
  let f = Typing.type_fmla (get_theory lenv.mod_uc) log_denv log_vars f in
  create_post res f
610 611 612 613

let create_pre lenv f =
  Typing.type_fmla (get_theory lenv.mod_uc) lenv.log_denv lenv.log_vars f

614 615 616 617
let create_variant lenv (t,r) =
  let t =
    Typing.type_term (get_theory lenv.mod_uc) lenv.log_denv lenv.log_vars t in
  { v_term = t; v_rel = r }
Andrei Paskevich's avatar
Andrei Paskevich committed
618

Andrei Paskevich's avatar
Andrei Paskevich committed
619
let add_local x lv lenv = match lv with
620
  | LetA _ ->
Andrei Paskevich's avatar
Andrei Paskevich committed
621
      { lenv with let_vars = Mstr.add x lv lenv.let_vars }
622 623
  | LetV pv ->
      let dty = dty_of_ty pv.pv_vs.vs_ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
624 625 626 627
      { 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 }
628

629 630
exception DuplicateException of xsymbol

631 632 633 634 635 636 637 638 639 640 641 642 643
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

644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 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
(* 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
        | LetV pv -> e_value pv
        | LetA _ -> errorm ~loc "%s must be a first-order value" x
      end
  | Ptree.PPvar p ->
      let x = Typing.string_list_of_qualid [] p in
      begin try match ns_find_ps (get_namespace lenv.mod_uc) x with
        | PV pv -> e_value pv
        | _ -> errorm ~loc:(qloc p) "%a is not a variable" print_qualid p
      with Not_found -> errorm ~loc "unbound variable %a" print_qualid p end
  | Ptree.PPapp (p, [e]) ->
      let e = get_eff_expr lenv e in
      let ity = (vtv_of_expr e).vtv_ity in
      let x = Typing.string_list_of_qualid [] p in
      let quit () =
        errorm ~loc:(qloc p) "%a is not a projection symbol" print_qualid p in
      begin try match ns_find_ps (get_namespace lenv.mod_uc) x with
        | PL ({pl_args = [{vtv_ity = ta}]; pl_value = {vtv_ity = tr}} as pl) ->
            let sbs = ity_match ity_subst_empty ta ity in
            let res = try ity_full_inst sbs tr with Not_found -> quit () in
            e_plapp pl [e] res
        | _ -> quit ()
      with Not_found -> try
        let th = get_theory lenv.mod_uc in
        match ns_find_ls (Theory.get_namespace th) x with
        | { ls_args = [ta]; ls_value = Some tr } as ls ->
            let sbs = ity_match ity_subst_empty (ity_of_ty ta) ity in
            let res = try ity_full_inst sbs (ity_of_ty tr) with _ -> quit () in
            e_lapp ls [e] res
        | _ -> quit ()
      with Not_found ->
        errorm ~loc:(qloc p) "unbound symbol %a" print_qualid p
      end
  | 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 =
  let e = get_eff_expr lenv le in
  let vtv = vtv_of_expr e in
  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

715 716
let rec type_c lenv gh vars dtyc =
  let result = type_v lenv gh vars dtyc.dc_result in
717 718 719
  let ty = match result with
    | SpecV v -> ty_of_ity v.vtv_ity
    | SpecA _ -> ty_unit in
720 721 722 723 724 725 726 727 728
  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
729
  { c_pre    = create_pre lenv dtyc.dc_pre;
730
    c_effect = eff;
731 732 733 734
    c_result = result;
    c_post   = create_post lenv "result" ty dtyc.dc_post;
    c_xpost  = xpost lenv dtyc.dc_xpost; }

735
and type_v lenv gh vars = function
736
  | DSpecV (ghost,v) ->
737
      let ghost = ghost || gh in
738 739 740
      SpecV (vty_value ~ghost (ity_of_dity v))
  | DSpecA (bl,tyc) ->
      let lenv, pvl = binders lenv bl in
741 742
      let add_pv s pv = vars_union s pv.pv_vtv.vtv_vars in
      let vars = List.fold_left add_pv vars pvl in
743
      SpecA (pvl, type_c lenv gh vars tyc)
744 745 746

(* expressions *)

747 748 749 750 751 752
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

753 754 755 756 757 758
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
759
  | DElocal x ->
Andrei Paskevich's avatar
Andrei Paskevich committed
760 761
      assert (Mstr.mem x lenv.let_vars);
      begin match Mstr.find x lenv.let_vars with
762
      | LetV pv -> e_value pv
763
      | LetA ps -> e_cast ps (vty_of_dity de.de_type)
764
      end
765 766
  | DElet (x, gh, { de_desc = DEfun lam }, de2) ->
      let def = expr_fun lenv x gh lam in
767
      let lenv = add_local x.id (LetA def.rec_ps) lenv in
Andrei Paskevich's avatar
Andrei Paskevich committed
768
      let e2 = expr lenv de2 in
769 770
      e_rec [def] e2
  | DEfun lam ->
771
      let x = mk_id "fn" loc in
772
      let def = expr_fun lenv x false lam in
773 774
      let e2 = e_cast def.rec_ps (VTarrow def.rec_ps.ps_vta) in
      e_rec [def] e2
775 776 777 778 779 780 781 782 783 784 785 786 787
  (* 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;
788
      let def1 = create_let_defn (Denv.create_user_id x) e1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
789 790
      let lenv = add_local x.id def1.let_var lenv in
      let e2 = expr lenv de2 in
791
      e_let def1 e2
Andrei Paskevich's avatar
Andrei Paskevich committed
792
  | DEletrec (rdl, de1) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
793
      let rdl = expr_rec lenv rdl in
794
      let add_rd { rec_ps = ps } = add_local ps.ps_name.id_string (LetA ps) in
Andrei Paskevich's avatar
Andrei Paskevich committed
795
      let e1 = expr (List.fold_right add_rd rdl lenv) de1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
796
      e_rec rdl e1
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
797
  | DEapply (de1, del) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
798
      let el = List.map (expr lenv) del in
799 800 801
      begin match de1.de_desc with
        | DEglobal_pl pls -> e_plapp pls el (ity_of_dity de.de_type)
        | DEglobal_ls ls  -> e_lapp  ls  el (ity_of_dity de.de_type)
Andrei Paskevich's avatar
Andrei Paskevich committed
802
        | _               -> e_app (expr lenv de1) el
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
803
      end
804 805 806
  | DEglobal_pv pv ->
      e_value pv
  | DEglobal_ps ps ->
807
      e_cast ps (vty_of_dity de.de_type)
Andrei Paskevich's avatar
Andrei Paskevich committed
808 809
  | DEglobal_pl pl ->
      assert (pl.pl_ls.ls_args = []);
810
      e_plapp pl [] (ity_of_dity de.de_type)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
811
  | DEglobal_ls ls ->
Andrei Paskevich's avatar
Andrei Paskevich committed
812
      assert (ls.ls_args = []);
813
      e_lapp ls [] (ity_of_dity de.de_type)
814
  | DEif (de1, de2, de3) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
815
      e_if (expr lenv de1) (expr lenv de2) (expr lenv de3)
Andrei Paskevich's avatar
Andrei Paskevich committed
816
  | DEassign (de1, de2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
817
      e_assign (expr lenv de1) (expr lenv de2)
818 819 820
  | DEconstant c ->
      e_const c
  | DElazy (LazyAnd, de1, de2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
821
      e_lazy_and (expr lenv de1) (expr lenv de2)
822
  | DElazy (LazyOr, de1, de2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
823
      e_lazy_or (expr lenv de1) (expr lenv de2)
824
  | DEnot de1 ->
Andrei Paskevich's avatar
Andrei Paskevich committed
825
      e_not (expr lenv de1)
826
  | DEmatch (de1, bl) ->
Andrei Paskevich's avatar