mlw_typing.ml 46.3 KB
Newer Older
1 2
(**************************************************************************)
(*                                                                        *)
MARCHE Claude's avatar
MARCHE Claude committed
3
(*  Copyright (C) 2010-2012                                               *)
4 5 6
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
MARCHE Claude's avatar
MARCHE Claude committed
7
(*    Guillaume Melquiond                                                 *)
8 9 10 11 12 13 14 15 16 17 18 19 20 21 22
(*    Andrei Paskevich                                                    *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)

open Why3
open Util
23
open Ident
24 25 26
open Ty
open Term
open Decl
27 28 29
open Theory
open Env
open Ptree
30
open Mlw_dtree
31
open Mlw_ty
32
open Mlw_ty.T
33 34
open Mlw_expr
open Mlw_decl
35
open Mlw_pretty
36
open Mlw_module
Andrei Paskevich's avatar
Andrei Paskevich committed
37
open Mlw_wp
38
open Mlw_dty
39

40 41
(** errors *)

42
exception DuplicateProgVar of string
43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64
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

let rec print_qualid fmt = function
  | Qident s -> Format.fprintf fmt "%s" s.id
  | Qdot (m, s) -> Format.fprintf fmt "%a.%s" print_qualid m s.id

let () = Exn_printer.register (fun fmt e -> match e with
  | DuplicateTypeVar s ->
65 66 67
      Format.fprintf fmt "Type parameter %s is used twice" s
  | DuplicateProgVar s ->
      Format.fprintf fmt "Parameter %s is used twice" s
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 93
(*
  | 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 *)

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

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

108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128
(** 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 ->
          let loc = Typing.qloc p in
          errorm ~loc "unbound symbol %a" Typing.print_qualid p
      end
  | Ptree.PPTtuple pl ->
      ts_app (ts_tuple (List.length pl)) (List.map (dity_of_pty ~user denv) pl)
129 130 131

(** Typing program expressions *)

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

138 139
let expected_type ?(weak=false) e dity =
  unify ~weak e.dexpr_type dity
140

141 142 143 144 145 146 147 148
let rec extract_labels labs loc e = match e.Ptree.expr_desc with
  | Ptree.Enamed (Ptree.Lstr s, e) -> extract_labels (s :: labs) loc e
  | 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)
  | e -> List.rev labs, loc, e

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

153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176
(* 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

let find_field ~loc uc (p,e) =
  let x = Typing.string_list_of_qualid [] p in
  try match ns_find_ps (get_namespace uc) x with
    | PL pl -> (pl,e)
177
    | _ -> errorm ~loc "bad record field %a" Typing.print_qualid p
178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213
  with Not_found -> errorm ~loc "unbound symbol %a" Typing.print_qualid p

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

let pure_record ~loc uc = function
  | [] -> error ~loc Decl.EmptyRecord
  | (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 =
  { dexpr_desc = DEglobal_pl pl;
    dexpr_type = specialize_plsymbol pl;
    dexpr_loc  = loc; dexpr_lab = [] }

let hidden_ls ~loc ls =
  { dexpr_desc = DEglobal_ls ls;
    dexpr_type = specialize_lsymbol ls;
    dexpr_loc  = loc; dexpr_lab = [] }

(* helper functions for let-expansion *)
let test_var e = match e.dexpr_desc with
  | DElocal _ | DEglobal_pv _ -> true
  | _ -> false

let mk_var e =
  if test_var e then e else
  { dexpr_desc = DElocal "q";
    dexpr_type = e.dexpr_type;
    dexpr_loc  = e.dexpr_loc;
    dexpr_lab  = [] }

214 215 216 217 218 219
let mk_id s loc =
  { id = s; id_loc = loc; id_lab = [] }

let mk_dexpr desc dity loc labs =
  { dexpr_desc = desc; dexpr_type = dity; dexpr_loc = loc; dexpr_lab = labs }

Andrei Paskevich's avatar
Andrei Paskevich committed
220
let mk_let ~loc ~uloc e (desc,dity) =
221
  if test_var e then desc, dity else
Andrei Paskevich's avatar
Andrei Paskevich committed
222
  let loc = def_option loc uloc in
223 224
  let e1 = mk_dexpr desc dity loc [] in
  DElet (mk_id "q" loc, e, e1), dity
225

226 227 228 229 230 231 232 233 234 235 236 237 238
(* 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 }

let specialize_qualid ~loc uc p =
  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
239
    | PX xs -> errorm ~loc "unexpected exception symbol %a" print_xs xs
240 241 242 243 244 245
  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 ->
    errorm ~loc "unbound symbol %a" Typing.print_qualid p

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

254 255 256 257 258 259 260 261 262 263 264
let find_variant_ls ~loc uc p =
  let x = Typing.string_list_of_qualid [] p in
  try match ns_find_ps (get_namespace uc) x with
    | _ -> errorm ~loc "%a is not a binary relation" Typing.print_qualid p
  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
      | ls -> errorm ~loc "%a is not a binary relation" Pretty.print_ls ls
  with Not_found ->
    errorm ~loc "unbound symbol %a" Typing.print_qualid p

265 266 267 268 269
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
270
      PPvar (Denv.create_user_id id), dity, add_var id dity denv
271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296
  | Ptree.PPpapp (q,ppl) ->
      let sym, dity = specialize_qualid ~loc denv.uc q in
      dpat_app denv (mk_dexpr sym dity loc []) ppl
  | Ptree.PPprec fl when pure_record ~loc denv.uc fl ->
      let kn = Theory.get_known (get_theory denv.uc) in
      let fl = List.map (find_pure_field ~loc denv.uc) fl in
      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 ->
      let fl = List.map (find_field ~loc denv.uc) fl in
      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
297
      PPas (pp, Denv.create_user_id id), dity, add_var id dity denv
298 299 300 301 302 303 304 305

and dpat_app denv ({ dexpr_loc = loc } as de) ppl =
  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
  let pp = match de.dexpr_desc with
    | DEglobal_pl pl -> Mlw_expr.PPpapp (pl, ppl)
    | DEglobal_ls ls -> PPlapp (ls, ppl)
306 307
    | 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
308 309 310 311 312 313
    | _ -> assert false
  in
  let res = create_type_variable () in
  Loc.try2 loc unify de.dexpr_type (make_arrow_type tyl res);
  pp, res, denv

314 315 316 317 318 319 320 321 322 323
(*
let deff_of_peff ~loc denv pe =
  { deff_reads  = pe.pe_reads;
    deff_writes = pe.pe_writes;
    deff_raises =
      List.map (fun q -> false, find_xsymbol ~loc denv.uc q) pe.pe_raises; }
*)

let dexpr_unit ~loc = hidden_ls ~loc (fs_tuple 0)

324 325 326 327 328 329
let dexpr_app e el =
  let res = create_type_variable () in
  let tyl = List.map (fun a -> a.dexpr_type) el in
  expected_type e (make_arrow_type tyl res);
  DEapply (e, el), res

Andrei Paskevich's avatar
Andrei Paskevich committed
330
let rec dexpr denv e =
331
  let loc = e.Ptree.expr_loc in
Andrei Paskevich's avatar
Andrei Paskevich committed
332 333 334 335
  let labs, uloc, d = extract_labels [] denv.uloc e in
  let denv = { denv with uloc = uloc } in
  let d, ty = dexpr_desc denv loc d in
  let loc = def_option loc uloc in
336
  mk_dexpr d ty loc labs
337

Andrei Paskevich's avatar
Andrei Paskevich committed
338
and dexpr_desc denv loc = function
339 340
  | Ptree.Eident (Qident {id=x}) when Mstr.mem x denv.locals ->
      (* local variable *)
341 342 343
      let tvs, dity = Mstr.find x denv.locals in
      let dity = specialize_scheme tvs dity in
      DElocal x, dity
344
  | Ptree.Eident p ->
345
      specialize_qualid ~loc denv.uc p
346 347
  | Ptree.Eapply (e1, e2) ->
      let e, el = decompose_app [e2] e1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
348 349
      let el = List.map (dexpr denv) el in
      dexpr_app (dexpr denv e) el
350
  | Ptree.Elet (id, e1, e2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
351
      let e1 = dexpr denv e1 in
352
      let dity = e1.dexpr_type in
Andrei Paskevich's avatar
Andrei Paskevich committed
353 354 355
      let tvars = match e1.dexpr_desc with
        | DEfun _ -> denv.tvars
        | _ -> add_tvars denv.tvars dity in
356 357
      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
358
      let e2 = dexpr denv e2 in
359
      DElet (id, e1, e2), e2.dexpr_type
Andrei Paskevich's avatar
Andrei Paskevich committed
360
  | Ptree.Eletrec (rdl, e1) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
361
      let rdl = dletrec denv rdl in
362
      let add_one denv ({ id = id }, dity, _) =
363 364
        { 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
365
      let e1 = dexpr denv e1 in
366
      DEletrec (rdl, e1), e1.dexpr_type
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
367
  | Ptree.Efun (bl, tr) ->
368 369
      let lam, dity = dlambda ~loc denv bl None tr in
      DEfun lam, dity
370
  | Ptree.Ecast (e1, pty) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
371
      let e1 = dexpr denv e1 in
372
      expected_type e1 (dity_of_pty ~user:false denv pty);
373 374 375
      e1.dexpr_desc, e1.dexpr_type
  | Ptree.Enamed _ ->
      assert false
376
  | Ptree.Esequence (e1, e2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
377
      let e1 = dexpr denv e1 in
378
      expected_type e1 dity_unit;
Andrei Paskevich's avatar
Andrei Paskevich committed
379
      let e2 = dexpr denv e2 in
380
      DElet (mk_id "_" loc, e1, e2), e2.dexpr_type
381
  | Ptree.Eif (e1, e2, e3) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
382
      let e1 = dexpr denv e1 in
383
      expected_type e1 dity_bool;
Andrei Paskevich's avatar
Andrei Paskevich committed
384 385
      let e2 = dexpr denv e2 in
      let e3 = dexpr denv e3 in
386 387 388 389
      expected_type e3 e2.dexpr_type;
      DEif (e1, e2, e3), e2.dexpr_type
  | Ptree.Etuple el ->
      let ls = fs_tuple (List.length el) in
Andrei Paskevich's avatar
Andrei Paskevich committed
390
      let el = List.map (dexpr denv) el in
391 392 393 394 395 396
      dexpr_app (hidden_ls ~loc ls) el
  | Ptree.Erecord fl when pure_record ~loc denv.uc fl ->
      let kn = Theory.get_known (get_theory denv.uc) in
      let fl = List.map (find_pure_field ~loc denv.uc) fl in
      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
397
        | Some e -> dexpr denv e
398 399 400 401 402 403
        | None -> error ~loc (Decl.RecordFieldMissing (cs,pj)) in
      dexpr_app (hidden_ls ~loc cs) (List.map get_val pjl)
  | Ptree.Erecord fl ->
      let fl = List.map (find_field ~loc denv.uc) fl in
      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
404
        | Some e -> dexpr denv e
405 406 407
        | None -> error ~loc (Decl.RecordFieldMissing (cs.pl_ls,pj.pl_ls)) in
      dexpr_app (hidden_pl ~loc cs) (List.map get_val pjl)
  | Ptree.Eupdate (e1, fl) when pure_record ~loc denv.uc fl ->
Andrei Paskevich's avatar
Andrei Paskevich committed
408
      let e1 = dexpr denv e1 in
409 410 411 412 413
      let e0 = mk_var e1 in
      let kn = Theory.get_known (get_theory denv.uc) in
      let fl = List.map (find_pure_field ~loc denv.uc) fl in
      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
414
        | Some e -> dexpr denv e
415
        | None ->
416 417
            let d, dity = dexpr_app (hidden_ls ~loc pj) [e0] in
            mk_dexpr d dity loc [] in
418
      let res = dexpr_app (hidden_ls ~loc cs) (List.map get_val pjl) in
Andrei Paskevich's avatar
Andrei Paskevich committed
419
      mk_let ~loc ~uloc:denv.uloc e1 res
420
  | Ptree.Eupdate (e1, fl) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
421
      let e1 = dexpr denv e1 in
422 423 424 425
      let e0 = mk_var e1 in
      let fl = List.map (find_field ~loc denv.uc) fl in
      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
426
        | Some e -> dexpr denv e
427
        | None ->
428 429
            let d, dity = dexpr_app (hidden_pl ~loc pj) [e0] in
            mk_dexpr d dity loc [] in
430
      let res = dexpr_app (hidden_pl ~loc cs) (List.map get_val pjl) in
Andrei Paskevich's avatar
Andrei Paskevich committed
431
      mk_let ~loc ~uloc:denv.uloc e1 res
Andrei Paskevich's avatar
Andrei Paskevich committed
432
  | Ptree.Eassign (e1, q, e2) ->
433 434
      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
435 436
      let e1 = dexpr denv e1 in
      let e2 = dexpr denv e2 in
437
      expected_type ~weak:true e2 e1.dexpr_type;
Andrei Paskevich's avatar
Andrei Paskevich committed
438
      DEassign (e1, e2), dity_unit
439 440 441 442 443
  | 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
444
      let e1 = dexpr denv e1 in
445 446 447
      expected_type e1 dity_bool;
      DEnot e1, dity_bool
  | Ptree.Elazy (op, e1, e2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
448 449
      let e1 = dexpr denv e1 in
      let e2 = dexpr denv e2 in
450 451 452
      expected_type e1 dity_bool;
      expected_type e2 dity_bool;
      DElazy (op, e1, e2), dity_bool
453
  | Ptree.Ematch (e1, bl) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
454
      let e1 = dexpr denv e1 in
455 456 457
      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
458
        let e = dexpr denv e in
459 460 461 462
        Loc.try2 pp.pat_loc unify dity e1.dexpr_type;
        expected_type e res;
        ppat, e in
      DEmatch (e1, List.map branch bl), res
Andrei Paskevich's avatar
Andrei Paskevich committed
463 464
  | Ptree.Eraise (q, e1) ->
      let res = create_type_variable () in
465 466
      let xs = find_xsymbol ~loc denv.uc q in
      let dity = specialize_xsymbol xs in
Andrei Paskevich's avatar
Andrei Paskevich committed
467
      let e1 = match e1 with
Andrei Paskevich's avatar
Andrei Paskevich committed
468
        | Some e1 -> dexpr denv e1
469
        | None when ity_equal xs.xs_ity ity_unit -> dexpr_unit ~loc
Andrei Paskevich's avatar
Andrei Paskevich committed
470 471 472 473
        | _ -> 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
474
      let e1 = dexpr denv e1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
475
      let branch (q, id, e) =
476 477
        let xs = find_xsymbol ~loc denv.uc q in
        let dity = specialize_xsymbol xs in
Andrei Paskevich's avatar
Andrei Paskevich committed
478 479
        let id, denv = match id with
          | Some id -> id, add_var id dity denv
480
          | None -> mk_id "void" loc, denv in
Andrei Paskevich's avatar
Andrei Paskevich committed
481
        xs, id, dexpr denv e
Andrei Paskevich's avatar
Andrei Paskevich committed
482 483 484
      in
      let cl = List.map branch cl in
      DEtry (e1, cl), e1.dexpr_type
485
  | Ptree.Eabsurd ->
486
      DEabsurd, create_type_variable ()
487 488
  | Ptree.Eassert (ak, lexpr) ->
      DEassert (ak, lexpr), dity_unit
Andrei Paskevich's avatar
Andrei Paskevich committed
489 490 491
  | Ptree.Emark (id, e1) ->
      let e1 = dexpr denv e1 in
      DEmark (id, e1), e1.dexpr_type
492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516
  | Ptree.Eany _ ->
      errorm ~loc "\"any\" expressions are not supported"
(*
  | Ptree.Eany { pc_result_type = Tpure pty;
                 pc_effect      = pe;
                 pc_pre         = { pp_desc = PPtrue };
                 pc_post        = { pp_desc = PPtrue },[]; } ->
      let dity = dity_of_pty ~user:true denv pty in
      DEany (deff_of_peff pe), dity
  | Ptree.Eany { pc_result_type = Tarrow (bl,tyc);
                 pc_effect      = pe;
                 pc_pre         = { pp_desc = PPtrue };
                 pc_post        = { pp_desc = PPtrue },[]; } ->
      let e1 = mk_dexpr (DEany (deff_of_peff pe)) dity_unit loc [] in
      let e2 = { pp_desc = Ptree.Eany tyc; pp_loc = loc } in
      let d2 = Ptree.Efun (bl,(tyc.pc_pre,e2,tyc.pc_post)) in
      let e2 = dexpr denv { pp_desc = d2; pp_loc = loc } in
      DElet (mk_id "_" loc, e1, e2), e2.dexpr_type
  | Ptree.Eany tyc ->
      let bl = [mk_id "_" loc, None] in
      let e = dtype_v tyc.pc_effect tyc.pc_result_type in
      let lam,dity = dlambda ~loc denv bl None (tyc.pc_pre, e, tyc.pc_post) in
      let fn = mk_dexpr (DEfun lam) dity loc [] in
      dexpr_app fn [dexpr_unit ~loc]
*)
517
  | Ptree.Eloop (_ann, _e1) ->
518 519 520 521
      assert false (*TODO*)
  | Ptree.Efor (_id, _e1, _dir, _e2, _lexpr_opt, _e3) ->
      assert false (*TODO*)
  | Ptree.Eabstract (_e1, _post) ->
522 523
      assert false (*TODO*)

Andrei Paskevich's avatar
Andrei Paskevich committed
524
and dletrec denv rdl =
Andrei Paskevich's avatar
Andrei Paskevich committed
525 526 527
  (* add all functions into environment *)
  let add_one denv (id, bl, var, tr) =
    let res = create_type_variable () in
Andrei Paskevich's avatar
Andrei Paskevich committed
528
    add_var id res denv, (id, res, bl, var, tr) in
Andrei Paskevich's avatar
Andrei Paskevich committed
529 530 531
  let denv, rdl = Util.map_fold_left add_one denv rdl in
  (* then type-check all of them and unify *)
  let type_one (id, res, bl, var, tr) =
532
    let lam, dity = dlambda ~loc:id.id_loc denv bl var tr in
Andrei Paskevich's avatar
Andrei Paskevich committed
533
    Loc.try2 id.id_loc unify dity res;
534
    id, dity, lam in
535
  List.map type_one rdl
Andrei Paskevich's avatar
Andrei Paskevich committed
536

537
and dlambda ~loc denv bl var (p, e, (q, xq)) =
Andrei Paskevich's avatar
Andrei Paskevich committed
538 539
  let dbinder denv (id, pty) =
    let dity = match pty with
Andrei Paskevich's avatar
Andrei Paskevich committed
540
      | Some pty -> dity_of_pty ~user:true denv pty
Andrei Paskevich's avatar
Andrei Paskevich committed
541 542 543 544
      | None -> create_type_variable () in
    add_var id dity denv, (id, false, dity) in
  let denv, bl = Util.map_fold_left dbinder denv bl in
  let tyl = List.map (fun (_,_,d) -> d) bl in
Andrei Paskevich's avatar
Andrei Paskevich committed
545
  let e = dexpr denv e in
546 547 548 549 550 551 552 553 554 555 556
  let var = match var with
    | Some (le, Some q) -> [le, Some (find_variant_ls ~loc denv.uc q)]
    | Some (le, None) -> [le, None]
    | None -> [] in
(* TODO: accept a list of variants in the surface language
  let var = List.map (fun (le,q) ->
    le, Util.option_map (find_variant_ls ~loc denv.uc) q) var in
*)
  let xq = List.map
    (fun (q,f) -> find_xsymbol ~loc:f.pp_loc denv.uc q, f) xq in
  (bl, var, p, e, q, xq), make_arrow_type tyl e.dexpr_type
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
557

558 559 560 561 562 563 564 565 566 567 568 569 570 571
(*
and dtype_v ~loc denv = function
  | Ptree.Tpure pty ->
      let dity = dity_of_pty ~user:true denv pty in
      let deff = { deff_reads = []; deff_writes = []; deff_raises = [] } in
      DEany deff, dity
  | Ptree.Tarrow (bl, tyc) ->
      let pptrue = { pp_desc = PPtrue ; pp_loc = loc } in
      let d = Ptree.Eany { tyc with pc_pre = pptrue; pc_post = pptrue,[] } in
      let tr = tyc.pc_pre, { expr_desc = d; expr_loc = loc }, tyc.pc_post in
      let lam, dity = dlambda ~loc denv bl None tr in
      DEfun lam, dity
*)

Andrei Paskevich's avatar
Andrei Paskevich committed
572 573 574 575 576
type lenv = {
  mod_uc   : module_uc;
  let_vars : let_var Mstr.t;
  log_vars : vsymbol Mstr.t;
  log_denv : Typing.denv;
577 578
}

Andrei Paskevich's avatar
Andrei Paskevich committed
579 580
let create_lenv uc = {
  mod_uc   = uc;
581 582 583 584 585 586 587 588 589 590 591
  let_vars = Mstr.empty;
  log_vars = Mstr.empty;
  log_denv = Typing.denv_empty;
}

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)

592 593 594 595
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
Andrei Paskevich's avatar
Andrei Paskevich committed
596 597 598 599
  (* FIXME? We could add th_mark in create_lenv, but then at/old
     would be available in preconditions, variants, etc... *)
  let th = Theory.use_export (get_theory lenv.mod_uc) Mlw_wp.th_mark in
  create_post res (Typing.type_fmla th log_denv log_vars f)
600 601 602 603

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

Andrei Paskevich's avatar
Andrei Paskevich committed
604
let add_local x lv lenv = match lv with
605
  | LetA _ ->
Andrei Paskevich's avatar
Andrei Paskevich committed
606
      { lenv with let_vars = Mstr.add x lv lenv.let_vars }
607 608
  | LetV pv ->
      let dty = dty_of_ty pv.pv_vs.vs_ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
609 610 611 612
      { 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 }
613

614 615
exception DuplicateException of xsymbol

Andrei Paskevich's avatar
Andrei Paskevich committed
616
let rec expr lenv de = match de.dexpr_desc with
617
  | DElocal x ->
Andrei Paskevich's avatar
Andrei Paskevich committed
618 619
      assert (Mstr.mem x lenv.let_vars);
      begin match Mstr.find x lenv.let_vars with
620 621
      | LetV pv -> e_value pv
      | LetA ps -> e_cast ps (vty_of_dity de.dexpr_type)
622
      end
623 624 625
  | DElet (x, { dexpr_desc = DEfun lam }, de2) ->
      let def = expr_fun lenv x lam in
      let lenv = add_local x.id (LetA def.rec_ps) lenv in
Andrei Paskevich's avatar
Andrei Paskevich committed
626
      let e2 = expr lenv de2 in
627 628
      e_rec [def] e2
  | DEfun lam ->
629
      let x = mk_id "fn" de.dexpr_loc in
630
      let def = expr_fun lenv x lam in
631 632 633
      let e2 = e_cast def.rec_ps (VTarrow def.rec_ps.ps_vta) in
      e_rec [def] e2
  | DElet (x, de1, de2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
634
      let e1 = expr lenv de1 in
635
      let def1 = create_let_defn (Denv.create_user_id x) e1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
636 637
      let lenv = add_local x.id def1.let_var lenv in
      let e2 = expr lenv de2 in
638
      e_let def1 e2
Andrei Paskevich's avatar
Andrei Paskevich committed
639
  | DEletrec (rdl, de1) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
640
      let rdl = expr_rec lenv rdl in
641
      let add_rd { rec_ps = ps } = add_local ps.ps_name.id_string (LetA ps) in
Andrei Paskevich's avatar
Andrei Paskevich committed
642
      let e1 = expr (List.fold_right add_rd rdl lenv) de1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
643
      e_rec rdl e1
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
644
  | DEapply (de1, del) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
645
      let el = List.map (expr lenv) del in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
646 647 648
      begin match de1.dexpr_desc with
        | DEglobal_pl pls -> e_plapp pls el (ity_of_dity de.dexpr_type)
        | DEglobal_ls ls  -> e_lapp  ls  el (ity_of_dity de.dexpr_type)
Andrei Paskevich's avatar
Andrei Paskevich committed
649
        | _               -> e_app (expr lenv de1) el
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
650
      end
651 652 653 654
  | DEglobal_pv pv ->
      e_value pv
  | DEglobal_ps ps ->
      e_cast ps (vty_of_dity de.dexpr_type)
Andrei Paskevich's avatar
Andrei Paskevich committed
655 656 657
  | DEglobal_pl pl ->
      assert (pl.pl_ls.ls_args = []);
      e_plapp pl [] (ity_of_dity de.dexpr_type)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
658
  | DEglobal_ls ls ->
Andrei Paskevich's avatar
Andrei Paskevich committed
659
      assert (ls.ls_args = []);
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
660
      e_lapp ls [] (ity_of_dity de.dexpr_type)
661
  | DEif (de1, de2, de3) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
662
      e_if (expr lenv de1) (expr lenv de2) (expr lenv de3)
Andrei Paskevich's avatar
Andrei Paskevich committed
663
  | DEassign (de1, de2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
664
      e_assign (expr lenv de1) (expr lenv de2)
665 666 667
  | DEconstant c ->
      e_const c
  | DElazy (LazyAnd, de1, de2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
668
      e_lazy_and (expr lenv de1) (expr lenv de2)
669
  | DElazy (LazyOr, de1, de2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
670
      e_lazy_or (expr lenv de1) (expr lenv de2)
671
  | DEnot de1 ->
Andrei Paskevich's avatar
Andrei Paskevich committed
672
      e_not (expr lenv de1)
673
  | DEmatch (de1, bl) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
674
      let e1 = expr lenv de1 in
675 676 677
      let vtv = vtv_of_expr e1 in
      let branch (pp,de) =
        let vm, pp = make_ppattern pp vtv in
Andrei Paskevich's avatar
Andrei Paskevich committed
678 679
        let lenv = Mstr.fold (fun s pv -> add_local s (LetV pv)) vm lenv in
        pp, expr lenv de in
680
      e_case e1 (List.map branch bl)
Andrei Paskevich's avatar
Andrei Paskevich committed
681 682 683 684 685
  | DEassert (ak, f) ->
      let ak = match ak with
        | Ptree.Aassert -> Aassert
        | Ptree.Aassume -> Aassume
        | Ptree.Acheck  -> Acheck in
686
      e_assert ak (create_pre lenv f)
687 688
  | DEabsurd ->
      e_absurd (ity_of_dity de.dexpr_type)
Andrei Paskevich's avatar
Andrei Paskevich committed
689
  | DEraise (xs, de1) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
690
      e_raise xs (expr lenv de1) (ity_of_dity de.dexpr_type)
Andrei Paskevich's avatar
Andrei Paskevich committed
691
  | DEtry (de1, bl) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
692
      let e1 = expr lenv de1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
693 694 695
      let branch (xs,id,de) =
        let vtv = vty_value xs.xs_ity in
        let pv = create_pvsymbol (Denv.create_user_id id) vtv in
Andrei Paskevich's avatar
Andrei Paskevich committed
696 697
        let lenv = add_local id.id (LetV pv) lenv in
        xs, pv, expr lenv de in
Andrei Paskevich's avatar
Andrei Paskevich committed
698
      e_try e1 (List.map branch bl)
Andrei Paskevich's avatar
Andrei Paskevich committed
699 700 701 702
  | DEmark (x, de1) ->
      let ld = create_let_defn (Denv.create_user_id x) e_setmark in
      let lenv = add_local x.id ld.let_var lenv in
      e_let ld (expr lenv de1)
703 704 705 706 707 708 709 710 711 712
(*
  | DEany deff ->
      let aeff = {
        aeff_reads  = List.map (expr lenv) deff.deff_reads;
        aeff_writes = List.map (expr lenv) deff.deff_writes;
        aeff_raises = deff.deff_raises } in
      e_any aeff (ity_of_dity de.dexpr_type)
*)
  | DEghost de1 ->
      e_ghost (expr lenv de1)
713 714 715
  | _ ->
      assert false (*TODO*)

Andrei Paskevich's avatar
Andrei Paskevich committed
716
and expr_rec lenv rdl =
717
  let step1 lenv (id, dity, lam) =
Andrei Paskevich's avatar
Andrei Paskevich committed
718 719 720
    let vta = match vty_of_dity dity with
      | VTarrow vta -> vta
      | VTvalue _ -> assert false in
721
    let ps = create_psymbol (Denv.create_user_id id) vta vars_empty in
722
    add_local id.id (LetA ps) lenv, (ps, lam)
Andrei Paskevich's avatar
Andrei Paskevich committed
723
  in
Andrei Paskevich's avatar
Andrei Paskevich committed
724
  let lenv, rdl = Util.map_fold_left step1 lenv rdl in
725
  let step2 (ps, lam) = ps, expr_lam lenv lam in
Andrei Paskevich's avatar
Andrei Paskevich committed
726 727
  create_rec_defn (List.map step2 rdl)

728 729
and expr_fun lenv x lam =
  let lam = expr_lam lenv lam in
730
  create_fun_defn (Denv.create_user_id x) lam
Andrei Paskevich's avatar
Andrei Paskevich committed
731

732
and expr_lam lenv (bl, var, p, e, q, xq) =
733 734
  let binder (id, ghost, dity) =
    let vtv = vty_value ~ghost (ity_of_dity dity) in
735
    create_pvsymbol (Denv.create_user_id id) vtv in
736
  let pvl = List.map binder bl in
737
  let add_binder pv = add_local pv.pv_vs.vs_name.id_string (LetV pv) in
Andrei Paskevich's avatar
Andrei Paskevich committed
738 739
  let lenv = List.fold_right add_binder pvl lenv in
  let e = expr lenv e in
Andrei Paskevich's avatar
Andrei Paskevich committed
740
  let ty = match e.e_vty with
Andrei Paskevich's avatar
Andrei Paskevich committed
741
    | VTarrow _ -> ty_unit
742
    | VTvalue vtv -> ty_of_ity vtv.vtv_ity in
743 744 745 746
  let mk_variant (t,r) = { v_term = create_pre lenv t; v_rel = r } in
  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
Andrei Paskevich's avatar
Andrei Paskevich committed
747
  { l_args = pvl;
748 749
    l_variant = List.map mk_variant var;
    l_pre = create_pre lenv p;
Andrei Paskevich's avatar
Andrei Paskevich committed
750
    l_expr = e;
751 752
    l_post = create_post lenv "result" ty q;
    l_xpost = List.fold_left add_exn Mexn.empty xq;
Andrei Paskevich's avatar
Andrei Paskevich committed
753
  }
754

755 756
(** Type declaration *)

757
type tys = ProgTS of itysymbol | PureTS of tysymbol
758 759 760 761 762 763 764 765 766

let find_tysymbol q uc =
  let loc = Typing.qloc q in
  let sl = Typing.string_list_of_qualid [] q in
  try ProgTS (ns_find_it (get_namespace uc) sl)
  with Not_found ->
  try PureTS (ns_find_ts (Theory.get_namespace (get_theory uc)) sl)
  with Not_found -> error ~loc (UnboundSymbol sl)

767 768 769
let look_for_loc tdl s =
  let look_id loc id = if id.id = s then Some id.id_loc else loc in
  let look_pj loc (id,_) = option_fold look_id loc id in
770 771 772
  let look_cs loc (csloc,id,pjl) =
    let loc = if id.id = s then Some csloc else loc in
    List.fold_left look_pj loc pjl in
773 774 775 776 777 778 779 780 781 782
  let look_fl loc f = look_id loc f.f_ident in
  let look loc d =
    let loc = look_id loc d.td_ident in
    match d.td_def with
      | TDabstract | TDalias _ -> loc
      | TDalgebraic csl -> List.fold_left look_cs loc csl
      | TDrecord fl -> List.fold_left look_fl loc fl
  in
  List.fold_left look None tdl

783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 854
let add_types uc tdl =
  let add m d =
    let id = d.td_ident.id in
    Mstr.add_new (Loc.Located (d.td_loc, ClashSymbol id)) id d m in
  let def = List.fold_left add Mstr.empty tdl in

  (* detect cycles *)

  let rec cyc_visit x d seen = match Mstr.find_opt x seen with
    | Some true -> seen
    | Some false -> errorm ~loc:d.td_loc "Cyclic type definition"
    | None ->
        let ts_seen seen = function
          | Qident { id = x } ->
              begin try cyc_visit x (Mstr.find x def) seen
              with Not_found -> seen end
          | _ -> seen in
        let rec check seen = function
          | PPTtyvar _ -> seen
          | PPTtyapp (tyl,q) -> List.fold_left check (ts_seen seen q) tyl
          | PPTtuple tyl -> List.fold_left check seen tyl in
        let seen = match d.td_def with
          | TDabstract | TDalgebraic _ | TDrecord _ -> seen
          | TDalias ty -> check (Mstr.add x false seen) ty in
        Mstr.add x true seen in
  ignore (Mstr.fold cyc_visit def Mstr.empty);

  (* detect mutable types *)

  let mutables = Hashtbl.create 5 in
  let rec mut_visit x =
    try Hashtbl.find mutables x
    with Not_found ->
      let ts_mut = function
        | Qident { id = x } when Mstr.mem x def -> mut_visit x
        | q ->
            begin match find_tysymbol q uc with
              | ProgTS s -> s.its_regs <> []
              | PureTS _ -> false end in
      let rec check = function
        | PPTtyvar _ -> false
        | PPTtyapp (tyl,q) -> ts_mut q || List.exists check tyl
        | PPTtuple tyl -> List.exists check tyl in
      Hashtbl.replace mutables x false;
      let mut = match (Mstr.find x def).td_def with
        | TDabstract -> false
        | TDalias ty -> check ty
        | TDalgebraic csl ->
            let proj (_,pty) = check pty in
            List.exists (fun (_,_,l) -> List.exists proj l) csl
        | TDrecord fl ->
            let field f = f.f_mutable || check f.f_pty in
            List.exists field fl in
      Hashtbl.replace mutables x mut;
      mut
  in
  Mstr.iter (fun x _ -> ignore (mut_visit x)) def;

  (* create type symbols and predefinitions for mutable types *)

  let tysymbols = Hashtbl.create 5 in
  let predefs = Hashtbl.create 5 in
  let rec its_visit x =
    try match Hashtbl.find tysymbols x with
      | Some ts -> ts
      | None ->
          let loc = (Mstr.find x def).td_loc in
          errorm ~loc "Mutable type in a recursive type definition"
    with Not_found ->
      let d = Mstr.find x def in
      let add_tv acc id =
        let e = Loc.Located (id.id_loc, DuplicateTypeVar id.id) in
855
        let tv = create_tvsymbol (Denv.create_user_id id) in
856 857 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873 874 875 876 877
        Mstr.add_new e id.id tv acc in
      let vars = List.fold_left add_tv Mstr.empty d.td_params in
      let vl = List.map (fun id -> Mstr.find id.id vars) d.td_params in
      let id = Denv.create_user_id d.td_ident in
      let abst = d.td_vis = Abstract in
      let priv = d.td_vis = Private in
      Hashtbl.add tysymbols x None;
      let get_ts = function
        | Qident { id = x } when Mstr.mem x def -> ProgTS (its_visit x)
        | q -> find_tysymbol q uc
      in
      let rec parse = function
        | PPTtyvar { id = v ; id_loc = loc } ->
            let e = Loc.Located (loc, UnboundTypeVar v) in
            ity_var (Mstr.find_exn e v vars)
        | PPTtyapp (tyl,q) ->
            let tyl = List.map parse tyl in
            begin match get_ts q with
              | PureTS ts -> Loc.try2 (Typing.qloc q) ity_pur ts tyl
              | ProgTS ts -> Loc.try2 (Typing.qloc q) ity_app_fresh ts tyl
            end
        | PPTtuple tyl ->
878
            let ts = ts_tuple (List.length tyl) in
879 880 881 882 883
            ity_pur ts (List.map parse tyl)
      in
      let ts = match d.td_def with
        | TDalias ty ->
            let def = parse ty in
884 885
            let rl = Sreg.elements def.ity_vars.vars_reg in
            create_itysymbol id ~abst ~priv vl rl (Some def)
886
        | TDalgebraic csl when Hashtbl.find mutables x ->
887 888 889 890 891 892
            let projs = Hashtbl.create 5 in
            (* to check projections' types we must fix the tyvars *)
            let add s v = let t = ity_var v in ity_match s t t in
            let sbs = List.fold_left add ity_subst_empty vl in
            let mk_proj s (id,pty) =
              let ity = parse pty in
893
              let vtv = vty_value ity in
894 895
              match id with
                | None ->
896
                    let pv = create_pvsymbol (id_fresh "pj") vtv in
897
                    Sreg.union s ity.ity_vars.vars_reg, (pv, false)
898 899 900
                | Some id ->
                    try
                      let pv = Hashtbl.find projs id.id in
901
                      let ty = pv.pv_vtv.vtv_ity in
902 903
                      (* once we have ghost/mutable fields in algebraics,
                         don't forget to check here that they coincide, too *)
904
                      ignore (Loc.try3 id.id_loc ity_match sbs ty ity);
905 906
                      s, (pv, true)
                    with Not_found ->
907
                      let pv = create_pvsymbol (Denv.create_user_id id) vtv in
908
                      Hashtbl.replace projs id.id pv;
909
                      Sreg.union s ity.ity_vars.vars_reg, (pv, true)
910 911 912 913 914 915
            in
            let mk_constr s (_loc,cid,pjl) =
              let s,pjl = Util.map_fold_left mk_proj s pjl in
              s, (Denv.create_user_id cid, pjl)
            in
            let s,def = Util.map_fold_left mk_constr Sreg.empty csl in
916
            Hashtbl.replace predefs x def;
917
            create_itysymbol id ~abst ~priv vl (Sreg.elements s) None
918
        | TDrecord fl when Hashtbl.find mutables x ->
919 920 921 922 923
            let mk_field s f =
              let ghost = f.f_ghost in
              let ity = parse f.f_pty in
              let fid = Denv.create_user_id f.f_ident in
              let s,mut = if f.f_mutable then
924
                let r = create_region fid ity in
925 926
                Sreg.add r s, Some r
              else
927
                Sreg.union s ity.ity_vars.vars_reg, None
928
              in
929 930
              let vtv = vty_value ?mut ~ghost ity in
              s, (create_pvsymbol fid vtv, true)
931 932 933
            in
            let s,pjl = Util.map_fold_left mk_field Sreg.empty fl in
            let cid = { d.td_ident with id = "mk " ^ d.td_ident.id } in
934
            Hashtbl.replace predefs x [Denv.create_user_id cid, pjl];
935 936 937 938 939 940 941 942 943 944 945
            create_itysymbol id ~abst ~priv vl (Sreg.elements s) None
        | TDalgebraic _ | TDrecord _ | TDabstract ->
            create_itysymbol id ~abst ~priv vl [] None
      in
      Hashtbl.add tysymbols x (Some ts);
      ts
  in
  Mstr.iter (fun x _ -> ignore (its_visit x)) def;

  (* create predefinitions for immutable types *)

946
  let def_visit d (abstr,algeb,alias) =
947 948 949 950 951 952 953 954 955 956 957 958 959 960 961 962 963 964 965 966
    let x = d.td_ident.id in
    let ts = Util.of_option (Hashtbl.find tysymbols x) in