mlw_typing.ml 81.7 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3 4 5 6 7 8 9 10
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2012   --   INRIA - CNRS - Paris-Sud University  *)
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)
11

12
open Stdlib
13
open Ident
14 15 16
open Ty
open Term
open Decl
17 18 19
open Theory
open Env
open Ptree
20
open Mlw_dtree
21
open Mlw_ty
22
open Mlw_ty.T
23 24
open Mlw_expr
open Mlw_decl
25
open Mlw_pretty
26
open Mlw_module
Andrei Paskevich's avatar
Andrei Paskevich committed
27
open Mlw_wp
28
open Mlw_dty
29

30 31
(** errors *)

32
exception DuplicateProgVar of string
33 34 35 36 37 38 39 40 41 42 43
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
44
(* unused
45
exception UnboundSymbol of qualid
46
*)
47 48 49 50

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

51 52
let qloc = Typing.qloc
let print_qualid = Typing.print_qualid
53 54 55

let () = Exn_printer.register (fun fmt e -> match e with
  | DuplicateTypeVar s ->
56 57 58
      Format.fprintf fmt "Type parameter %s is used twice" s
  | DuplicateProgVar s ->
      Format.fprintf fmt "Parameter %s is used twice" s
59 60 61
  | TooLateInvariant ->
      Format.fprintf fmt
        "Cannot add a type invariant after another program declaration"
62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79
(*
  | 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 ->
80
      Format.fprintf fmt "Unbound type variable '%s" s
81
(* unused
82 83
  | UnboundSymbol q ->
      Format.fprintf fmt "Unbound symbol '%a'" print_qualid q
84
*)
85 86 87
  | _ -> raise e)

(* TODO: let type_only = Debug.test_flag Typing.debug_type_only in *)
88 89
let implicit_post = Debug.register_flag "implicit_post"
  ~desc:"Generate@ a@ postcondition@ for@ pure@ functions@ without@ one."
90

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

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

105 106
(* Handle tuple symbols *)

107 108 109
let ht_tuple   = Hint.create 3
let ts_tuple n = Hint.replace ht_tuple n (); ts_tuple n
let fs_tuple n = Hint.replace ht_tuple n (); fs_tuple n
110

111
let check_at f0 =
Andrei Paskevich's avatar
Andrei Paskevich committed
112 113 114 115 116 117 118 119 120 121 122 123
  let rec check f = match f.t_node with
    | Term.Tapp (ls, _) when ls_equal ls fs_at ->
        let d = Mvs.set_diff f.t_vars f0.t_vars in
        if not (Mvs.is_empty d) then errorm ?loc:f.t_loc
          "locally bound variable %a under `at'"
          Pretty.print_vs (fst (Mvs.choose d))
        else true
    | _ ->
        t_all check f
  in
  ignore (check f0)

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

130
let flush_tuples uc =
131 132
  let kn = Theory.get_known (get_theory uc) in
  let add_tuple n _ uc =
Andrei Paskevich's avatar
Andrei Paskevich committed
133
    if Mid.mem (Ty.ts_tuple n).ts_name kn then uc
134
    else use_export_theory uc (tuple_theory n) in
135 136
  let uc = Hint.fold add_tuple ht_tuple uc in
  Hint.clear ht_tuple;
137 138
  uc

139
let add_pdecl_with_tuples ~wp uc pd = add_pdecl ~wp (flush_tuples uc) pd
140
let add_decl_with_tuples uc d = add_decl (flush_tuples uc) d
141

142 143 144
(** Namespace lookup *)

let uc_find_ls uc p =
145 146
  let ns = Theory.get_namespace (get_theory uc) in
  Typing.find_ns (fun ls -> ls.ls_name) Theory.ns_find_ls p ns
147

148
let get_id_ts = function
149
  | PT pt -> pt.its_ts.ts_name
150
  | TS ts -> ts.ts_name
Andrei Paskevich's avatar
Andrei Paskevich committed
151

152
let uc_find_ts uc p =
153
  Typing.find_ns get_id_ts ns_find_type_symbol p (get_namespace uc)
154 155 156 157 158 159 160

let get_id_ps = function
  | PV pv -> pv.pv_vs.vs_name
  | PS ps -> ps.ps_name
  | PL pl -> pl.pl_ls.ls_name
  | XS xs -> xs.xs_name
  | LS ls -> ls.ls_name
Andrei Paskevich's avatar
Andrei Paskevich committed
161

162
let uc_find_ps uc p =
163
  Typing.find_ns get_id_ps ns_find_prog_symbol p (get_namespace uc)
164

165 166
(** Typing type expressions *)

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

180 181 182
let opaque_binders acc args =
  List.fold_left (fun acc (_,_,dty) -> opaque_tvs acc dty) acc args

183 184
(** Typing program expressions *)

Andrei Paskevich's avatar
Andrei Paskevich committed
185
let dity_int  = ts_app ts_int  []
186
let dity_real = ts_app ts_real []
187
let dity_bool = ts_app ts_bool []
Andrei Paskevich's avatar
Andrei Paskevich committed
188
let dity_unit = ts_app ts_unit []
189

190
let unify_loc unify_fn loc x1 x2 = try unify_fn x1 x2 with
Andrei Paskevich's avatar
Andrei Paskevich committed
191
  | TypeMismatch (ity1,ity2,_) -> errorm ~loc
192
      "This expression has type %a,@ but is expected to have type %a"
193
      Mlw_pretty.print_ity ity2 Mlw_pretty.print_ity ity1
Andrei Paskevich's avatar
Andrei Paskevich committed
194 195 196
  | DTypeMismatch (dity1,dity2) -> errorm ~loc
      "This expression has type %a,@ but is expected to have type %a"
      Mlw_dty.print_dity dity2 Mlw_dty.print_dity dity1
197
  | exn when Debug.test_noflag Debug.stack_trace -> error ~loc exn
198

199 200 201 202 203 204 205
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
206

207
let rec extract_labels labs loc e = match e.Ptree.expr_desc with
208
  | Ptree.Enamed (Ptree.Lstr s, e) -> extract_labels (Slab.add s labs) loc e
209 210 211 212
  | 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)
213
  | e -> labs, loc, e
214

215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239
(* Hack alert. Since the result type in "let [rec] fn x y : ty = ..."
   is moved to Ecast and then usually lost in destructive unification,
   we try to preserve opacity annotations by moving them to binders. *)
let pass_opacity (e,_) bl =
  let rec find e = match e.Ptree.expr_desc with
    | Ptree.Ecast (_, pty) -> Some pty
    | Ptree.Enamed (_, e) -> find e
    | _ -> None in
  match find e with
  | Some pty ->
      let ht = Hstr.create 3 in
      let rec fill = function
        | Ptree.PPTtyapp (_, pl) | Ptree.PPTtuple pl -> List.iter fill pl
        | Ptree.PPTtyvar (id, true) -> Hstr.replace ht id.id ()
        | Ptree.PPTtyvar _ -> () in
      fill pty;
      if Hstr.length ht = 0 then bl else
      let rec pass = function
        | Ptree.PPTtyvar (id,op) -> Ptree.PPTtyvar (id, op || Hstr.mem ht id.id)
        | Ptree.PPTtyapp (p, pl) -> Ptree.PPTtyapp (p, List.map pass pl)
        | Ptree.PPTtuple pl -> Ptree.PPTtuple (List.map pass pl) in
      List.map (fun (loc,id,gh,pty) -> loc, id, gh, Opt.map pass pty) bl
  | None ->
      bl

240 241 242
let rec decompose_app args e = match e.Ptree.expr_desc with
  | Eapply (e1, e2) -> decompose_app (e2 :: args) e1
  | _ -> e, args
243

244 245 246 247 248 249 250
(* record parsing *)

let parse_record uc fll =
  let pl = match fll with
    | [] -> raise EmptyRecord
    | (pl,_)::_ -> pl in
  let its = match pl.pl_args with
251
    | [{ fd_ity = { ity_node = Ityapp (its,_,_) }}] -> its
252 253
    | _ -> raise (BadRecordField pl.pl_ls) in
  let cs, pjl = match find_constructors (get_known uc) its with
254
    | [cs,pjl] -> cs, List.map (Opt.get_exn (BadRecordField pl.pl_ls)) pjl
255 256 257 258 259 260 261 262 263
    | _ -> 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

264 265
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
266

267
let find_pure_field uc (p,e) = uc_find_ls uc p, e
268

269 270
let is_pure_record uc = function
  | fl :: _ -> (try ignore (find_prog_field uc fl); false with _ -> true)
271
  | [] -> raise Decl.EmptyRecord
272 273

let hidden_pl ~loc pl =
274 275
  { de_desc = DEglobal_pl pl;
    de_type = specialize_plsymbol pl;
276
    de_loc  = loc; de_lab = Slab.empty }
277 278

let hidden_ls ~loc ls =
279
  { de_desc = DEglobal_ls ls;
280
    de_type = Loc.try1 loc specialize_lsymbol ls;
281
    de_loc  = loc; de_lab = Slab.empty }
282 283

(* helper functions for let-expansion *)
284
let test_var e = match e.de_desc with
285
  | DElocal _ | DEglobal_pv _ | DEconstant _ -> true
286 287
  | _ -> false

288
let mk_var name e =
289
  if test_var e then e else
290
  { de_desc = DElocal name;
291 292
    de_type = e.de_type;
    de_loc  = e.de_loc;
293
    de_lab  = Slab.empty }
294

295 296 297
let mk_id s loc =
  { id = s; id_loc = loc; id_lab = [] }

298 299
let mk_dexpr desc dvty loc labs =
  { de_desc = desc; de_type = dvty; de_loc = loc; de_lab = labs }
300

301
let mk_let name ~loc ~uloc e (desc,dvty) =
302
  if test_var e then desc, dvty else
303
  let loc = Opt.get_def loc uloc in
304
  let e1 = mk_dexpr desc dvty loc Slab.empty in
305
  DElet (mk_id name e.de_loc, false, e, e1), dvty
306

307 308
(* patterns *)

309 310 311 312 313 314 315 316 317
let add_poly id dvty denv =
  let locals = Mstr.add id.id (Some denv.tvars, dvty) denv.locals in
  { denv with locals = locals }

let add_mono id dvty denv =
  let locals = Mstr.add id.id (None, dvty) denv.locals in
  { denv with locals = locals; tvars = add_dvty denv.tvars dvty }

let add_var id dity denv = add_mono id ([],dity) denv
318

319
let specialize_qualid uc p = match uc_find_ps uc p with
320
  | PV pv -> DEglobal_pv pv, ([],specialize_pvsymbol pv)
321 322
  | PS ps -> DEglobal_ps ps, specialize_psymbol  ps
  | PL pl -> DEglobal_pl pl, specialize_plsymbol pl
323
  | LS ls -> DEglobal_ls ls, Loc.try1 (qloc p) specialize_lsymbol ls
324
  | XS xs -> errorm ~loc:(qloc p) "unexpected exception symbol %a" print_xs xs
325

326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344
let chainable_qualid uc p = match uc_find_ps uc p with
  | PS { ps_aty = { aty_args = [pv1;pv2]; aty_result = VTvalue ity }}
  | PS { ps_aty = { aty_args = [pv1]; aty_result =
          VTarrow { aty_args = [pv2]; aty_result = VTvalue ity }}} ->
      ity_equal ity ity_bool
      && not (ity_equal pv1.pv_ity ity_bool)
      && not (ity_equal pv2.pv_ity ity_bool)
  | LS { ls_args = [ty1;ty2]; ls_value = ty } ->
      Opt.fold (fun _ ty -> ty_equal ty ty_bool) true ty
      && not (ty_equal ty1 ty_bool)
      && not (ty_equal ty2 ty_bool)
  | PS _ | LS _ | PL _ | PV _ | XS _ -> false

let chainable_op denv op =
  op.id = "infix =" || op.id = "infix <>" ||
  match Mstr.find_opt op.id denv.locals with
  | Some (_, dvty) -> is_chainable dvty
  | None -> chainable_qualid denv.uc (Qident op)

345 346
let find_xsymbol uc p = match uc_find_ps uc p with
  | XS xs -> xs
347
  | _ -> errorm ~loc:(qloc p) "exception symbol expected"
Andrei Paskevich's avatar
Andrei Paskevich committed
348

349
let find_variant_ls uc p = match uc_find_ls uc p with
350 351
  | { 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
352

353
let find_global_vs uc p = try match uc_find_ps uc p with
354 355
  | PV pv -> Some pv.pv_vs
  | _ -> None
356
  with _ -> None
357

358 359 360 361 362 363
let find_vs uc lvm p = match p with
  | Qdot _ -> find_global_vs uc p
  | Qident id ->
      let ovs = Mstr.find_opt id.id lvm in
      if ovs = None then find_global_vs uc p else ovs

364
let rec dpattern denv ({ pat_loc = loc } as pp) dity = match pp.pat_desc with
365
  | Ptree.PPpwild ->
366
      PPwild, denv
367
  | Ptree.PPpvar id ->
368
      PPvar (Denv.create_user_id id), add_var id dity denv
369
  | Ptree.PPpapp (q,ppl) ->
370
      let sym, dvty = specialize_qualid denv.uc q in
371
      dpat_app denv loc (mk_dexpr sym dvty loc Slab.empty) ppl dity
372
  | Ptree.PPprec fl when is_pure_record denv.uc fl ->
373
      let kn = Theory.get_known (get_theory denv.uc) in
374
      let fl = List.map (find_pure_field denv.uc) fl in
375 376 377
      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
378
      dpat_app denv loc (hidden_ls ~loc cs) (List.map get_val pjl) dity
379
  | Ptree.PPprec fl ->
380
      let fl = List.map (find_prog_field denv.uc) fl in
381 382 383
      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
384
      dpat_app denv loc (hidden_pl ~loc cs) (List.map get_val pjl) dity
385 386
  | Ptree.PPptuple ppl ->
      let cs = fs_tuple (List.length ppl) in
387
      dpat_app denv loc (hidden_ls ~loc cs) ppl dity
388
  | Ptree.PPpor (lpp1, lpp2) ->
389 390 391
      let pp1, denv = dpattern denv lpp1 dity in
      let pp2, denv = dpattern denv lpp2 dity in
      PPor (pp1, pp2), denv
392
  | Ptree.PPpas (pp, id) ->
393 394 395 396 397 398 399
      let pp, denv = dpattern denv pp dity in
      PPas (pp, Denv.create_user_id id), add_var id dity denv

and dpat_app denv gloc ({ de_loc = loc } as de) ppl dity =
  let ls = match de.de_desc with
    | DEglobal_pl pl -> pl.pl_ls
    | DEglobal_ls ls -> ls
400 401
    | 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
402
    | _ -> assert false in
403 404 405
  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));
406 407 408 409 410 411 412 413 414
  unify_loc unify gloc res dity;
  let add_pp lp ty (ppl, denv) =
    let pp, denv = dpattern denv lp ty in pp::ppl, denv in
  let ppl, denv = List.fold_right2 add_pp ppl argl ([],denv) in
  let pp = match de.de_desc with
    | DEglobal_pl pl -> Mlw_expr.PPpapp (pl, ppl)
    | DEglobal_ls ls -> Mlw_expr.PPlapp (ls, ppl)
    | _ -> assert false in
  pp, denv
415

416 417
(* specifications *)

418
let dbinders denv bl =
419 420
  let s = ref Sstr.empty in
  let dbinder (loc,id,gh,pty) (denv,bl,tyl) =
421
    let dity = match pty with
422
      | Some pty -> dity_of_pty denv pty
423 424 425 426 427 428 429 430 431 432
      | None -> create_type_variable ()
    in
    let denv, id = match id with
      | Some ({ id = x; id_loc = loc } as id) ->
          s := Loc.try3 loc Sstr.add_new (DuplicateProgVar x) x !s;
          add_var id dity denv, id
      | None ->
          denv, { id = "_"; id_loc = loc; id_lab = [] }
    in
    denv, (id,gh,dity)::bl, dity::tyl
433 434
  in
  List.fold_right dbinder bl (denv,[],[])
435

436
let mk_dpost loc = function
437
  | [{ pat_desc = PPpwild | PPptuple [] | PPpvar _ }, _ as p] -> p
438
  | l ->
439 440 441 442
      let i = { id = "(null)"; id_loc = loc; id_lab = [] } in
      let p = { pat_desc = Ptree.PPpvar i; pat_loc = loc } in
      let v = { pp_desc = Ptree.PPvar (Qident i); pp_loc = loc } in
      p, { pp_desc = PPmatch (v,l); pp_loc = loc }
443 444

let dpost ql = List.map (fun (loc, ql) -> mk_dpost loc ql) ql
445 446

let dxpost uc ql =
447
  let add_exn (q,pat,f) m =
448
    let xs = find_xsymbol uc q in
449 450 451 452 453 454
    Mexn.change (function
      | Some l -> Some ((pat,f) :: l)
      | None   -> Some ((pat,f) :: [])) xs m in
  let exn_map (loc,ql) =
    let m = List.fold_right add_exn ql Mexn.empty in
    Mexn.map (fun ql -> [mk_dpost loc ql]) m in
455 456 457
  let add_map ql m =
    Mexn.union (fun _ l r -> Some (l @ r)) (exn_map ql) m in
  List.fold_right add_map ql Mexn.empty
458 459

let dvariant uc var =
460
  List.map (fun (le,q) -> le, Opt.map (find_variant_ls uc) q) var
461 462 463

let dspec uc sp = {
  ds_pre     = sp.sp_pre;
464
  ds_post    = dpost sp.sp_post;
465
  ds_xpost   = dxpost uc sp.sp_xpost;
466 467
  ds_reads   = sp.sp_reads;
  ds_writes  = sp.sp_writes;
468 469
  ds_variant = dvariant uc sp.sp_variant;
}
470

471 472 473
let rec dtype_c denv (tyv, sp) =
  let tyv, dvty = dtype_v denv tyv in
  (tyv, dspec denv.uc sp), dvty
474 475 476

and dtype_v denv = function
  | Tpure pty ->
477
      let dity = dity_of_pty denv pty in
478
      DSpecV dity, ([],dity)
479
  | Tarrow (bl,tyc) ->
480
      let bl = List.map (fun (l,i,g,t) -> l,i,g,Some t) bl in
481
      let denv,bl,tyl = dbinders denv bl in
482 483
      let tyc,(argl,res) = dtype_c denv tyc in
      DSpecA (bl,tyc), (tyl @ argl,res)
484

485
(* expressions *)
486

487
let de_unit ~loc = hidden_ls ~loc Mlw_expr.fs_void
488

489 490 491 492 493 494 495 496 497 498 499 500 501 502
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
503

Andrei Paskevich's avatar
Andrei Paskevich committed
504
let rec dexpr denv e =
505
  let loc = e.Ptree.expr_loc in
506
  let labs, uloc, d = extract_labels Slab.empty denv.uloc e in
Andrei Paskevich's avatar
Andrei Paskevich committed
507
  let denv = { denv with uloc = uloc } in
508
  let d, ty = de_desc denv loc d in
509
  let loc = Opt.get_def loc uloc in
510
  mk_dexpr d ty loc labs
511

512
and de_desc denv loc = function
513 514 515 516 517 518
  | Ptree.Eident (Qident {id = x} as p) ->
      begin match Mstr.find_opt x denv.locals with
        | Some (Some tvs, dvty) -> DElocal x, specialize_scheme tvs dvty
        | Some (None,     dvty) -> DElocal x, dvty
        | None                  -> specialize_qualid denv.uc p
      end
519
  | Ptree.Eident p ->
520
      specialize_qualid denv.uc p
521 522
  | Ptree.Eapply (e1, e2) ->
      let e, el = decompose_app [e2] e1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
523
      let el = List.map (dexpr denv) el in
524
      de_app loc (dexpr denv e) el
525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555
  | Ptree.Einfix (e12, op2, e3)
  | Ptree.Einnfix (e12, op2, e3) ->
      let mk_bool (d,ty) =
        let de = mk_dexpr d ty (Opt.get_def loc denv.uloc) Slab.empty in
        expected_type de dity_bool; de in
      let make_app de1 op de2 =
        let id = Ptree.Eident (Qident op) in
        let e0 = { expr_desc = id; expr_loc = op.id_loc } in
        de_app loc (dexpr denv e0) [de1; de2] in
      let make_app de1 op de2 =
        if op.id <> "infix <>" then make_app de1 op de2 else
          let de12 = mk_bool (make_app de1 { op with id = "infix =" } de2) in
          DEnot de12, de12.de_type in
      let rec make_chain n1 n2 de1 = function
        | [op,de2] ->
            make_app de1 op de2
        | (op,de2) :: ch ->
            let v = mk_var n1 de2 in
            let de12 = mk_bool (make_app de1 op v) in
            let de23 = mk_bool (make_chain n2 n1 v ch) in
            let d = DElazy (LazyAnd, de12, de23) in
            mk_let n1 ~loc ~uloc:denv.uloc de2 (d, de12.de_type)
        | [] -> assert false in
      let rec get_chain e12 acc = match e12.expr_desc with
        | Ptree.Einfix (e1, op1, e2) when chainable_op denv op1 ->
            get_chain e1 ((op1, dexpr denv e2) :: acc)
        | _ -> e12, acc in
      let e1, ch = if chainable_op denv op2
        then get_chain e12 [op2, dexpr denv e3]
        else e12, [op2, dexpr denv e3] in
      make_chain "q1 " "q2 " (dexpr denv e1) ch
556
  | Ptree.Elet (id, gh, e1, e2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
557
      let e1 = dexpr denv e1 in
558 559 560
      let denv = match e1.de_desc with
        | DEfun _ -> add_poly id e1.de_type denv
        | _       -> add_mono id e1.de_type denv in
Andrei Paskevich's avatar
Andrei Paskevich committed
561
      let e2 = dexpr denv e2 in
562
      DElet (id, gh, e1, e2), e2.de_type
563 564
  | Ptree.Eletrec (fdl, e1) ->
      let fdl = dletrec denv fdl in
565
      let add_one denv (id,_,dvty,_,_) = add_poly id dvty denv in
566
      let denv = List.fold_left add_one denv fdl in
Andrei Paskevich's avatar
Andrei Paskevich committed
567
      let e1 = dexpr denv e1 in
568
      DEletrec (fdl, e1), e1.de_type
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
569
  | Ptree.Efun (bl, tr) ->
570
      let denv, bl, tyl = dbinders denv (pass_opacity tr bl) in
571
      let tr, (argl, res) = dtriple denv tr in
572
      DEfun (bl, tr), (tyl @ argl, res)
573
  | Ptree.Ecast (e1, pty) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
574
      let e1 = dexpr denv e1 in
575
      expected_type_weak e1 (dity_of_pty denv pty);
576
      e1.de_desc, e1.de_type
577 578
  | Ptree.Enamed _ ->
      assert false
579
  | Ptree.Esequence (e1, e2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
580
      let e1 = dexpr denv e1 in
581
      expected_type e1 dity_unit;
Andrei Paskevich's avatar
Andrei Paskevich committed
582
      let e2 = dexpr denv e2 in
583
      DElet (mk_id "_" loc, false, e1, e2), e2.de_type
584
  | Ptree.Eif (e1, e2, e3) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
585
      let e1 = dexpr denv e1 in
586
      expected_type e1 dity_bool;
Andrei Paskevich's avatar
Andrei Paskevich committed
587 588
      let e2 = dexpr denv e2 in
      let e3 = dexpr denv e3 in
589 590 591
      let res = create_type_variable () in
      expected_type e2 res;
      expected_type e3 res;
592
      DEif (e1, e2, e3), e2.de_type
593 594
  | Ptree.Etuple el ->
      let ls = fs_tuple (List.length el) in
Andrei Paskevich's avatar
Andrei Paskevich committed
595
      let el = List.map (dexpr denv) el in
596
      de_app loc (hidden_ls ~loc ls) el
597
  | Ptree.Erecord fl when is_pure_record denv.uc fl ->
598
      let kn = Theory.get_known (get_theory denv.uc) in
599
      let fl = List.map (find_pure_field denv.uc) fl in
600 601
      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
602
        | Some e -> dexpr denv e
603
        | None -> error ~loc (Decl.RecordFieldMissing (cs,pj)) in
604
      de_app loc (hidden_ls ~loc cs) (List.map get_val pjl)
605
  | Ptree.Erecord fl ->
606
      let fl = List.map (find_prog_field denv.uc) fl in
607 608
      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
609
        | Some e -> dexpr denv e
610
        | None -> error ~loc (Decl.RecordFieldMissing (cs.pl_ls,pj.pl_ls)) in
611
      de_app loc (hidden_pl ~loc cs) (List.map get_val pjl)
612
  | Ptree.Eupdate (e1, fl) when is_pure_record denv.uc fl ->
Andrei Paskevich's avatar
Andrei Paskevich committed
613
      let e1 = dexpr denv e1 in
614
      let e0 = mk_var "q " e1 in
615
      let kn = Theory.get_known (get_theory denv.uc) in
616
      let fl = List.map (find_pure_field denv.uc) fl in
617 618
      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
619
        | Some e -> dexpr denv e
620
        | None ->
621
            let loc = Loc.dummy_position in
622 623
            let d, dvty = de_app loc (hidden_ls ~loc pj) [e0] in
            mk_dexpr d dvty loc Slab.empty in
624
      let res = de_app loc (hidden_ls ~loc cs) (List.map get_val pjl) in
625
      mk_let "q " ~loc ~uloc:denv.uloc e1 res
626
  | Ptree.Eupdate (e1, fl) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
627
      let e1 = dexpr denv e1 in
628
      let e0 = mk_var "q " e1 in
629
      let fl = List.map (find_prog_field denv.uc) fl in
630 631
      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
632
        | Some e -> dexpr denv e
633
        | None ->
634
            let loc = Loc.dummy_position in
635 636
            let d, dvty = de_app loc (hidden_pl ~loc pj) [e0] in
            mk_dexpr d dvty loc Slab.empty in
637
      let res = de_app loc (hidden_pl ~loc cs) (List.map get_val pjl) in
638
      mk_let "q " ~loc ~uloc:denv.uloc e1 res
Andrei Paskevich's avatar
Andrei Paskevich committed
639
  | Ptree.Eassign (e1, q, e2) ->
640 641 642 643 644
      let fl = dexpr denv { expr_desc = Eident q; expr_loc = qloc q } in
      let pl = match fl.de_desc with
        | DEglobal_pl pl -> pl
        | _ -> Loc.errorm ~loc:(qloc q) "%a is not a field name" print_qualid q
      in
Andrei Paskevich's avatar
Andrei Paskevich committed
645 646
      let e1 = dexpr denv e1 in
      let e2 = dexpr denv e2 in
647 648
      let d, ty = de_app loc fl [e1] in
      let e0 = mk_dexpr d ty loc Slab.empty in
649
      let res = create_type_variable () in
650
      expected_type e0 res;
651
      expected_type_weak e2 res;
652
      DEassign (pl, e1, e2), ([], dity_unit)
653
  | Ptree.Econstant (Number.ConstInt _ as c) ->
654
      DEconstant c, ([], dity_int)
655
  | Ptree.Econstant (Number.ConstReal _ as c) ->
656
      DEconstant c, ([], dity_real)
657
  | Ptree.Enot e1 ->
Andrei Paskevich's avatar
Andrei Paskevich committed
658
      let e1 = dexpr denv e1 in
659
      expected_type e1 dity_bool;
660
      DEnot e1, ([], dity_bool)
661
  | Ptree.Elazy (op, e1, e2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
662 663
      let e1 = dexpr denv e1 in
      let e2 = dexpr denv e2 in
664 665
      expected_type e1 dity_bool;
      expected_type e2 dity_bool;
666
      DElazy (op, e1, e2), ([], dity_bool)
667
  | Ptree.Ematch (e1, bl) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
668
      let e1 = dexpr denv e1 in
669
      let ety = create_type_variable () in
670
      let res = create_type_variable () in
671
      expected_type e1 ety;
672
      let branch (pp,e) =
673
        let ppat, denv = dpattern denv pp ety in
Andrei Paskevich's avatar
Andrei Paskevich committed
674
        let e = dexpr denv e in
675 676
        expected_type e res;
        ppat, e in
677
      DEmatch (e1, List.map branch bl), ([], res)
Andrei Paskevich's avatar
Andrei Paskevich committed
678
  | Ptree.Eraise (q, e1) ->
679
      let xs = find_xsymbol denv.uc q in
Andrei Paskevich's avatar
Andrei Paskevich committed
680
      let e1 = match e1 with
Andrei Paskevich's avatar
Andrei Paskevich committed
681
        | Some e1 -> dexpr denv e1
682
        | None when ity_equal xs.xs_ity ity_unit -> de_unit ~loc
Andrei Paskevich's avatar
Andrei Paskevich committed
683
        | _ -> errorm ~loc "exception argument expected" in
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
684
      expected_type e1 (specialize_xsymbol xs);
685
      DEraise (xs, e1), ([], create_type_variable ())
Andrei Paskevich's avatar
Andrei Paskevich committed
686
  | Ptree.Etry (e1, cl) ->
687
      let res = create_type_variable () in
Andrei Paskevich's avatar
Andrei Paskevich committed
688
      let e1 = dexpr denv e1 in
689
      expected_type e1 res;
690
      let branch (q, pp, e) =
691
        let xs = find_xsymbol denv.uc q in
692
        let ety = specialize_xsymbol xs in
693
        let ppat, denv = dpattern denv pp ety in
694
        let e = dexpr denv e in
695
        expected_type e res;
696
        xs, ppat, e in
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
697
      DEtry (e1, List.map branch cl), e1.de_type
698
  | Ptree.Eabsurd ->
699
      DEabsurd, ([], create_type_variable ())
700
  | Ptree.Eassert (ak, lexpr) ->
701
      DEassert (ak, lexpr), ([], dity_unit)
Andrei Paskevich's avatar
Andrei Paskevich committed
702 703
  | Ptree.Emark (id, e1) ->
      let e1 = dexpr denv e1 in
704
      DEmark (id, e1), e1.de_type
705
  | Ptree.Eany tyc ->
706 707
      let tyc, dvty = dtype_c denv tyc in
      DEany tyc, dvty
708 709 710
  | Ptree.Eghost e1 ->
      let e1 = dexpr denv e1 in
      DEghost e1, e1.de_type
711
  | Ptree.Eabstract (e1, sp) ->
712
      let e1 = dexpr denv e1 in
713 714
      let sp = dspec denv.uc sp in
      DEabstract (e1, sp), e1.de_type
715 716 717 718
  | 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;
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
719
      DEloop (var, inv, e1), e1.de_type
720 721 722 723 724 725 726 727
  | 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;
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
728
      DEfor (id, efrom, dir, eto, inv, e1), e1.de_type
729

730
and dletrec denv fdl =
731
  (* add all functions into the environment *)
732
  let add_one denv (_,id,_,bl,_) =
733 734
    let argl = List.map (fun _ -> create_type_variable ()) bl in
    let dvty = argl, create_type_variable () in
735
    add_mono id dvty denv, dvty in
736
  let denv, dvtyl = Lists.map_fold_left add_one denv fdl in