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

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

39 40
(** errors *)

41
exception DuplicateProgVar of string
42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63
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 ->
64 65 66
      Format.fprintf fmt "Type parameter %s is used twice" s
  | DuplicateProgVar s ->
      Format.fprintf fmt "Parameter %s is used twice" s
67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92
(*
  | PredicateExpected ->
      Format.fprintf fmt "syntax error: predicate expected"
  | TermExpected ->
      Format.fprintf fmt "syntax error: term expected"
  | FSymExpected ls ->
      Format.fprintf fmt "%a is not a function symbol" Pretty.print_ls ls
  | PSymExpected ls ->
      Format.fprintf fmt "%a is not a predicate symbol" Pretty.print_ls ls
  | ClashTheory s ->
      Format.fprintf fmt "Clash with previous theory %s" s
  | UnboundTheory q ->
      Format.fprintf fmt "unbound theory %a" print_qualid q
  | UnboundType sl ->
      Format.fprintf fmt "Unbound type '%a'"
        (Pp.print_list Pp.dot Pp.pp_print_string) sl
*)
  | UnboundTypeVar s ->
      Format.fprintf fmt "unbound type variable '%s" s
  | UnboundSymbol sl ->
      Format.fprintf fmt "Unbound symbol '%a'"
        (Pp.print_list Pp.dot Format.pp_print_string) sl
  | _ -> raise e)

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

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

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

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

(** Typing program expressions *)

131 132
let dity_int  = ts_app ts_int []
let dity_real = ts_app ts_real []
133
let dity_bool = ts_app ts_bool []
134
let dity_unit = ts_app (ts_tuple 0) []
135 136 137 138

let expected_type e dity =
  unify e.dexpr_type dity

139 140 141 142 143 144 145 146
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

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 171 172 173 174
(* 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)
175
    | _ -> errorm ~loc "bad record field %a" Typing.print_qualid p
176 177 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
  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  = [] }

Andrei Paskevich's avatar
Andrei Paskevich committed
212
let mk_let ~loc ~uloc e (desc,dity) =
213
  if test_var e then desc, dity else
Andrei Paskevich's avatar
Andrei Paskevich committed
214
  let loc = def_option loc uloc in
215 216 217 218
  let e1 = {
    dexpr_desc = desc; dexpr_type = dity; dexpr_loc = loc; dexpr_lab = [] } in
  DElet ({ id = "q"; id_lab = []; id_loc = loc }, e, e1), dity

219 220 221 222 223 224 225 226 227 228 229 230 231
(* 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
232
    | PX xs -> errorm ~loc "unexpected exception symbol %a" print_xs xs
233 234 235 236 237 238
  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

Andrei Paskevich's avatar
Andrei Paskevich committed
239 240 241 242 243 244 245 246
let specialize_exception ~loc uc p =
  let x = Typing.string_list_of_qualid [] p in
  try match ns_find_ps (get_namespace uc) x with
    | PX xs -> xs, specialize_xsymbol xs
    | _ -> errorm ~loc "exception symbol expected"
  with Not_found ->
    errorm ~loc "unbound symbol %a" Typing.print_qualid p

247 248 249 250 251 252 253 254
let mk_dexpr desc dity loc labs =
  { dexpr_desc = desc; dexpr_type = dity; dexpr_loc = loc; dexpr_lab = labs }

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
255
      PPvar (Denv.create_user_id id), dity, add_var id dity denv
256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281
  | 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
282
      PPas (pp, Denv.create_user_id id), dity, add_var id dity denv
283 284 285 286 287 288 289 290

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)
291 292
    | 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
293 294 295 296 297 298
    | _ -> assert false
  in
  let res = create_type_variable () in
  Loc.try2 loc unify de.dexpr_type (make_arrow_type tyl res);
  pp, res, denv

299 300 301 302 303
(* value restriction *)
let rec is_fun e = match e.dexpr_desc with
  | DEfun _ -> true
  | DEmark (_, e) -> is_fun e
  | _ -> false
304

305 306 307 308 309 310
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
311
let rec dexpr denv e =
312
  let loc = e.Ptree.expr_loc in
Andrei Paskevich's avatar
Andrei Paskevich committed
313 314 315 316
  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
317
  mk_dexpr d ty loc labs
318

Andrei Paskevich's avatar
Andrei Paskevich committed
319
and dexpr_desc denv loc = function
320 321
  | Ptree.Eident (Qident {id=x}) when Mstr.mem x denv.locals ->
      (* local variable *)
322 323 324
      let tvs, dity = Mstr.find x denv.locals in
      let dity = specialize_scheme tvs dity in
      DElocal x, dity
325
  | Ptree.Eident p ->
326
      specialize_qualid ~loc denv.uc p
327 328
  | Ptree.Eapply (e1, e2) ->
      let e, el = decompose_app [e2] e1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
329 330
      let el = List.map (dexpr denv) el in
      dexpr_app (dexpr denv e) el
331
  | Ptree.Elet (id, e1, e2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
332
      let e1 = dexpr denv e1 in
333 334 335 336
      let dity = e1.dexpr_type in
      let tvars = if is_fun e1 then denv.tvars else add_tvars denv.tvars dity in
      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
337
      let e2 = dexpr denv e2 in
338
      DElet (id, e1, e2), e2.dexpr_type
Andrei Paskevich's avatar
Andrei Paskevich committed
339
  | Ptree.Eletrec (rdl, e1) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
340
      let rdl = dletrec denv rdl in
341 342 343
      let add_one denv ({ id = id }, dity, _, _, _) =
        { 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
344
      let e1 = dexpr denv e1 in
345
      DEletrec (rdl, e1), e1.dexpr_type
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
346
  | Ptree.Efun (bl, tr) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
347
      let bl, _, tr, dity = dlambda denv bl None tr in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
348
      DEfun (bl, tr), dity
349
  | Ptree.Ecast (e1, pty) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
350
      let e1 = dexpr denv e1 in
351
      expected_type e1 (dity_of_pty ~user:false denv pty);
352 353 354
      e1.dexpr_desc, e1.dexpr_type
  | Ptree.Enamed _ ->
      assert false
355
  | Ptree.Esequence (e1, e2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
356
      let e1 = dexpr denv e1 in
357
      expected_type e1 dity_unit;
Andrei Paskevich's avatar
Andrei Paskevich committed
358
      let e2 = dexpr denv e2 in
359 360
      DElet ({ id = "_"; id_lab = []; id_loc = loc }, e1, e2), e2.dexpr_type
  | Ptree.Eif (e1, e2, e3) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
361
      let e1 = dexpr denv e1 in
362
      expected_type e1 dity_bool;
Andrei Paskevich's avatar
Andrei Paskevich committed
363 364
      let e2 = dexpr denv e2 in
      let e3 = dexpr denv e3 in
365 366 367 368
      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
369
      let el = List.map (dexpr denv) el in
370 371 372 373 374 375
      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
376
        | Some e -> dexpr denv e
377 378 379 380 381 382
        | 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
383
        | Some e -> dexpr denv e
384 385 386
        | 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
387
      let e1 = dexpr denv e1 in
388 389 390 391 392
      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
393
        | Some e -> dexpr denv e
394
        | None ->
395 396
            let d, dity = dexpr_app (hidden_ls ~loc pj) [e0] in
            mk_dexpr d dity loc [] in
397
      let res = dexpr_app (hidden_ls ~loc cs) (List.map get_val pjl) in
Andrei Paskevich's avatar
Andrei Paskevich committed
398
      mk_let ~loc ~uloc:denv.uloc e1 res
399
  | Ptree.Eupdate (e1, fl) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
400
      let e1 = dexpr denv e1 in
401 402 403 404
      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
405
        | Some e -> dexpr denv e
406
        | None ->
407 408
            let d, dity = dexpr_app (hidden_pl ~loc pj) [e0] in
            mk_dexpr d dity loc [] in
409
      let res = dexpr_app (hidden_pl ~loc cs) (List.map get_val pjl) in
Andrei Paskevich's avatar
Andrei Paskevich committed
410
      mk_let ~loc ~uloc:denv.uloc e1 res
Andrei Paskevich's avatar
Andrei Paskevich committed
411
  | Ptree.Eassign (e1, q, e2) ->
412 413
      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
414 415
      let e1 = dexpr denv e1 in
      let e2 = dexpr denv e2 in
Andrei Paskevich's avatar
Andrei Paskevich committed
416 417
      expected_type e2 e1.dexpr_type;
      DEassign (e1, e2), dity_unit
418 419 420 421 422
  | 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
423
      let e1 = dexpr denv e1 in
424 425 426
      expected_type e1 dity_bool;
      DEnot e1, dity_bool
  | Ptree.Elazy (op, e1, e2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
427 428
      let e1 = dexpr denv e1 in
      let e2 = dexpr denv e2 in
429 430 431
      expected_type e1 dity_bool;
      expected_type e2 dity_bool;
      DElazy (op, e1, e2), dity_bool
432
  | Ptree.Ematch (e1, bl) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
433
      let e1 = dexpr denv e1 in
434 435 436
      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
437
        let e = dexpr denv e in
438 439 440 441
        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
442 443 444 445
  | Ptree.Eraise (q, e1) ->
      let res = create_type_variable () in
      let xs, dity = specialize_exception ~loc denv.uc q in
      let e1 = match e1 with
Andrei Paskevich's avatar
Andrei Paskevich committed
446
        | Some e1 -> dexpr denv e1
Andrei Paskevich's avatar
Andrei Paskevich committed
447 448 449 450 451
        | None when ity_equal xs.xs_ity ity_unit -> hidden_ls ~loc (fs_tuple 0)
        | _ -> 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
452
      let e1 = dexpr denv e1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
453 454 455 456 457
      let branch (q, id, e) =
        let xs, dity = specialize_exception ~loc denv.uc q in
        let id, denv = match id with
          | Some id -> id, add_var id dity denv
          | None -> { id = "void" ; id_loc = loc ; id_lab = [] }, denv in
Andrei Paskevich's avatar
Andrei Paskevich committed
458
        xs, id, dexpr denv e
Andrei Paskevich's avatar
Andrei Paskevich committed
459 460 461
      in
      let cl = List.map branch cl in
      DEtry (e1, cl), e1.dexpr_type
462
  | Ptree.Eabsurd ->
463 464 465 466
      DEabsurd, create_type_variable ()
  | Ptree.Eassert (ass, lexpr) ->
      DEassert (ass, lexpr), dity_unit
  | Ptree.Eloop (_ann, _e1) ->
467 468 469 470 471 472 473 474
      assert false (*TODO*)
  | Ptree.Efor (_id, _e1, _dir, _e2, _lexpr_opt, _e3) ->
      assert false (*TODO*)
  | Ptree.Emark (_id, _e1) ->
      assert false (*TODO*)
  | Ptree.Eany (_type_c) ->
      assert false (*TODO*)
  | Ptree.Eabstract (_e1, _post) ->
475 476
      assert false (*TODO*)

Andrei Paskevich's avatar
Andrei Paskevich committed
477
and dletrec denv rdl =
Andrei Paskevich's avatar
Andrei Paskevich committed
478 479 480
  (* 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
481
    add_var id res denv, (id, res, bl, var, tr) in
Andrei Paskevich's avatar
Andrei Paskevich committed
482 483 484
  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) =
Andrei Paskevich's avatar
Andrei Paskevich committed
485
    let bl, var, tr, dity = dlambda denv bl var tr in
Andrei Paskevich's avatar
Andrei Paskevich committed
486 487
    Loc.try2 id.id_loc unify dity res;
    id, dity, bl, var, tr in
488
  List.map type_one rdl
Andrei Paskevich's avatar
Andrei Paskevich committed
489

Andrei Paskevich's avatar
Andrei Paskevich committed
490
and dlambda denv bl _var (p, e, q) =
Andrei Paskevich's avatar
Andrei Paskevich committed
491 492
  let dbinder denv (id, pty) =
    let dity = match pty with
Andrei Paskevich's avatar
Andrei Paskevich committed
493
      | Some pty -> dity_of_pty ~user:true denv pty
Andrei Paskevich's avatar
Andrei Paskevich committed
494 495 496 497
      | 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
498
  let e = dexpr denv e in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
499
  let q = dpost denv q in
Andrei Paskevich's avatar
Andrei Paskevich committed
500
  bl, [], (p, e, q), make_arrow_type tyl e.dexpr_type
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
501 502 503 504

and dpost _denv (q, _ql) =
  q, [] (* TODO *)

Andrei Paskevich's avatar
Andrei Paskevich committed
505 506 507 508 509
type lenv = {
  mod_uc   : module_uc;
  let_vars : let_var Mstr.t;
  log_vars : vsymbol Mstr.t;
  log_denv : Typing.denv;
510 511
}

Andrei Paskevich's avatar
Andrei Paskevich committed
512 513
let create_lenv uc = {
  mod_uc   = uc;
514 515 516 517 518 519 520 521 522 523 524
  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)

Andrei Paskevich's avatar
Andrei Paskevich committed
525
let add_local x lv lenv = match lv with
526
  | LetA _ ->
Andrei Paskevich's avatar
Andrei Paskevich committed
527
      { lenv with let_vars = Mstr.add x lv lenv.let_vars }
528 529
  | LetV pv ->
      let dty = dty_of_ty pv.pv_vs.vs_ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
530 531 532 533
      { 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 }
534

Andrei Paskevich's avatar
Andrei Paskevich committed
535
let rec expr lenv de = match de.dexpr_desc with
536
  | DElocal x ->
Andrei Paskevich's avatar
Andrei Paskevich committed
537 538
      assert (Mstr.mem x lenv.let_vars);
      begin match Mstr.find x lenv.let_vars with
539 540
      | LetV pv -> e_value pv
      | LetA ps -> e_cast ps (vty_of_dity de.dexpr_type)
541
      end
542
  | DElet (x, { dexpr_desc = DEfun (bl, tr) }, de2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
543 544 545
      let def1 = expr_fun lenv x bl tr in
      let lenv = add_local x.id (LetA def1.rec_ps) lenv in
      let e2 = expr lenv de2 in
546 547
      e_rec [def1] e2
  | DEfun (bl, tr) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
548
      let x = { id = "fn"; id_loc = de.dexpr_loc; id_lab = [] } in
Andrei Paskevich's avatar
Andrei Paskevich committed
549
      let def = expr_fun lenv x bl tr in
550 551 552
      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
553
      let e1 = expr lenv de1 in
554
      let def1 = create_let_defn (Denv.create_user_id x) e1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
555 556
      let lenv = add_local x.id def1.let_var lenv in
      let e2 = expr lenv de2 in
557
      e_let def1 e2
Andrei Paskevich's avatar
Andrei Paskevich committed
558
  | DEletrec (rdl, de1) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
559
      let rdl = expr_rec lenv rdl in
560
      let add_rd { rec_ps = ps } = add_local ps.ps_name.id_string (LetA ps) in
Andrei Paskevich's avatar
Andrei Paskevich committed
561
      let e1 = expr (List.fold_right add_rd rdl lenv) de1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
562
      e_rec rdl e1
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
563
  | DEapply (de1, del) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
564
      let el = List.map (expr lenv) del in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
565 566 567
      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
568
        | _               -> e_app (expr lenv de1) el
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
569
      end
570 571 572 573
  | 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
574 575 576
  | 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
577
  | DEglobal_ls ls ->
Andrei Paskevich's avatar
Andrei Paskevich committed
578
      assert (ls.ls_args = []);
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
579
      e_lapp ls [] (ity_of_dity de.dexpr_type)
580
  | DEif (de1, de2, de3) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
581
      e_if (expr lenv de1) (expr lenv de2) (expr lenv de3)
Andrei Paskevich's avatar
Andrei Paskevich committed
582
  | DEassign (de1, de2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
583
      e_assign (expr lenv de1) (expr lenv de2)
584 585 586
  | DEconstant c ->
      e_const c
  | DElazy (LazyAnd, de1, de2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
587
      e_lazy_and (expr lenv de1) (expr lenv de2)
588
  | DElazy (LazyOr, de1, de2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
589
      e_lazy_or (expr lenv de1) (expr lenv de2)
590
  | DEnot de1 ->
Andrei Paskevich's avatar
Andrei Paskevich committed
591
      e_not (expr lenv de1)
592
  | DEmatch (de1, bl) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
593
      let e1 = expr lenv de1 in
594 595 596
      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
597 598
        let lenv = Mstr.fold (fun s pv -> add_local s (LetV pv)) vm lenv in
        pp, expr lenv de in
599
      e_case e1 (List.map branch bl)
Andrei Paskevich's avatar
Andrei Paskevich committed
600
  | DEassert (ak, f) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
601 602
      let th = get_theory lenv.mod_uc in
      let f = Typing.type_fmla th lenv.log_denv lenv.log_vars f in
Andrei Paskevich's avatar
Andrei Paskevich committed
603 604 605 606 607
      let ak = match ak with
        | Ptree.Aassert -> Aassert
        | Ptree.Aassume -> Aassume
        | Ptree.Acheck  -> Acheck in
      e_assert ak f
608 609
  | DEabsurd ->
      e_absurd (ity_of_dity de.dexpr_type)
Andrei Paskevich's avatar
Andrei Paskevich committed
610
  | DEraise (xs, de1) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
611
      e_raise xs (expr lenv de1) (ity_of_dity de.dexpr_type)
Andrei Paskevich's avatar
Andrei Paskevich committed
612
  | DEtry (de1, bl) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
613
      let e1 = expr lenv de1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
614 615 616
      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
617 618
        let lenv = add_local id.id (LetV pv) lenv in
        xs, pv, expr lenv de in
Andrei Paskevich's avatar
Andrei Paskevich committed
619
      e_try e1 (List.map branch bl)
620 621 622
  | _ ->
      assert false (*TODO*)

Andrei Paskevich's avatar
Andrei Paskevich committed
623 624
and expr_rec lenv rdl =
  let step1 lenv (id, dity, bl, var, tr) =
Andrei Paskevich's avatar
Andrei Paskevich committed
625 626 627
    let vta = match vty_of_dity dity with
      | VTarrow vta -> vta
      | VTvalue _ -> assert false in
628
    let ps = create_psymbol (Denv.create_user_id id) vta vars_empty in
Andrei Paskevich's avatar
Andrei Paskevich committed
629
    add_local id.id (LetA ps) lenv, (ps, bl, var, tr)
Andrei Paskevich's avatar
Andrei Paskevich committed
630
  in
Andrei Paskevich's avatar
Andrei Paskevich committed
631 632
  let lenv, rdl = Util.map_fold_left step1 lenv rdl in
  let step2 (ps, bl, var, tr) = ps, expr_lam lenv bl var tr in
Andrei Paskevich's avatar
Andrei Paskevich committed
633 634
  create_rec_defn (List.map step2 rdl)

Andrei Paskevich's avatar
Andrei Paskevich committed
635 636
and expr_fun lenv x bl tr =
  let lam = expr_lam lenv bl [] tr in
637
  create_fun_defn (Denv.create_user_id x) lam
Andrei Paskevich's avatar
Andrei Paskevich committed
638

Andrei Paskevich's avatar
Andrei Paskevich committed
639
and expr_lam lenv bl _var (_, e, _) =
640 641
  let binder (id, ghost, dity) =
    let vtv = vty_value ~ghost (ity_of_dity dity) in
642
    create_pvsymbol (Denv.create_user_id id) vtv in
643
  let pvl = List.map binder bl in
644
  let add_binder pv = add_local pv.pv_vs.vs_name.id_string (LetV pv) in
Andrei Paskevich's avatar
Andrei Paskevich committed
645 646
  let lenv = List.fold_right add_binder pvl lenv in
  let e = expr lenv e in
Andrei Paskevich's avatar
Andrei Paskevich committed
647
  let ty = match e.e_vty with
648 649
    | VTarrow _ -> ty_tuple []
    | VTvalue vtv -> ty_of_ity vtv.vtv_ity in
Andrei Paskevich's avatar
Andrei Paskevich committed
650 651 652
  let res = create_vsymbol (id_fresh "result") ty in
  { l_args = pvl;
    l_variant = [];                   (* TODO *)
653
    l_pre = t_true;                   (* TODO *)
Andrei Paskevich's avatar
Andrei Paskevich committed
654 655
    l_expr = e;
    l_post = create_post res t_true;  (* TODO *)
656
    l_xpost = Mexn.empty;             (* TODO *)
Andrei Paskevich's avatar
Andrei Paskevich committed
657
  }
658

659 660
(** Type declaration *)

661
type tys = ProgTS of itysymbol | PureTS of tysymbol
662 663 664 665 666 667 668 669 670

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)

671 672 673
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
674 675 676
  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
677 678 679 680 681 682 683 684 685 686
  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

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 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758
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
759
        let tv = create_tvsymbol (Denv.create_user_id id) in
760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781
        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 ->
782
            let ts = ts_tuple (List.length tyl) in
783 784 785 786 787
            ity_pur ts (List.map parse tyl)
      in
      let ts = match d.td_def with
        | TDalias ty ->
            let def = parse ty in
788 789
            let rl = Sreg.elements def.ity_vars.vars_reg in
            create_itysymbol id ~abst ~priv vl rl (Some def)
790
        | TDalgebraic csl when Hashtbl.find mutables x ->
791 792 793 794 795 796
            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
797
              let vtv = vty_value ity in
798 799
              match id with
                | None ->
800
                    let pv = create_pvsymbol (id_fresh "pj") vtv in
801
                    Sreg.union s ity.ity_vars.vars_reg, (pv, false)
802 803 804
                | Some id ->
                    try
                      let pv = Hashtbl.find projs id.id in
805
                      let ty = pv.pv_vtv.vtv_ity in
806 807
                      (* once we have ghost/mutable fields in algebraics,
                         don't forget to check here that they coincide, too *)
808
                      ignore (Loc.try3 id.id_loc ity_match sbs ty ity);
809 810
                      s, (pv, true)
                    with Not_found ->
811
                      let pv = create_pvsymbol (Denv.create_user_id id) vtv in
812
                      Hashtbl.replace projs id.id pv;
813
                      Sreg.union s ity.ity_vars.vars_reg, (pv, true)
814 815 816 817 818 819
            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
820
            Hashtbl.replace predefs x def;
821
            create_itysymbol id ~abst ~priv vl (Sreg.elements s) None
822
        | TDrecord fl when Hashtbl.find mutables x ->
823 824 825 826 827
            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
828
                let r = create_region fid ity in
829 830
                Sreg.add r s, Some r
              else
831
                Sreg.union s ity.ity_vars.vars_reg, None
832
              in
833 834
              let vtv = vty_value ?mut ~ghost ity in
              s, (create_pvsymbol fid vtv, true)
835 836 837
            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
838
            Hashtbl.replace predefs x [Denv.create_user_id cid, pjl];
839 840 841 842 843 844 845 846 847 848 849
            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 *)

850
  let def_visit d (abstr,algeb,alias) =
851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866 867 868 869 870
    let x = d.td_ident.id in
    let ts = Util.of_option (Hashtbl.find tysymbols x) in
    let add_tv s x v = Mstr.add x.id v s in
    let vars = List.fold_left2 add_tv Mstr.empty d.td_params ts.its_args in
    let get_ts = function
      | Qident { id = x } when Mstr.mem x def ->
          ProgTS (Util.of_option (Hashtbl.find tysymbols 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.try3 (Typing.qloc q) ity_app ts tyl []
          end
      | PPTtuple tyl ->
871
          let ts = ts_tuple (List.length tyl) in
872 873 874
          ity_pur ts (List.map parse tyl)
    in
    match d.td_def with
875 876 877 878
      | TDabstract ->
          ts :: abstr, algeb, alias
      | TDalias _ ->
          abstr, algeb, ts :: alias
879
      | (TDalgebraic _ | TDrecord _) when Hashtbl.find mutables x ->
880
          abstr, (ts, Hashtbl.find predefs x) :: algeb, alias
881 882 883 884
      | TDalgebraic csl ->
          let projs = Hashtbl.create 5 in
          let mk_proj (id,pty) =
            let ity = parse pty in
885
            let vtv = vty_value ity in
886 887
            match id with
              | None ->
888
                  create_pvsymbol (id_fresh "pj") vtv, false
889 890 891
              | Some id ->
                  try
                    let pv = Hashtbl.find projs id.id in
892
                    let ty = pv.pv_vtv.vtv_ity in
893 894
                    (* once we have ghost/mutable fields in algebraics,
                       don't forget to check here that they coincide, too *)
895
                    Loc.try2 id.id_loc ity_equal_check ty ity;
896 897
                    pv, true
                  with Not_found ->
898
                    let pv = create_pvsymbol (Denv.create_user_id id) vtv in
899 900 901 902 903
                    Hashtbl.replace projs id.id pv;
                    pv, true
          in
          let mk_constr (_loc,cid,pjl) =
            Denv.create_user_id cid, List.map mk_proj pjl in
904
          abstr, (ts, List.map mk_constr csl) :: algeb, alias
905 906 907
      | TDrecord fl ->
          let mk_field f =
            let fid = Denv.create_user_id f.f_ident in
908 909
            let vtv = vty_value ~ghost:f.f_ghost (parse f.f_pty) in
            create_pvsymbol fid vtv, true in
910
          let cid = { d.td_ident with id = "mk " ^ d.td_ident.id } in
911 912
          let csl = [Denv.create_user_id cid, List.map mk_field fl] in
          abstr, (ts, csl) :: algeb, alias
913
  in
914
  let abstr,algeb,alias = List.fold_right def_visit tdl ([],[],[]) in
915 916

  (* detect pure type declarations *)
917

918 919 920
  let kn = get_known uc in
  let check its = Mid.mem its.its_pure.ts_name kn in
  let check ity = ity_s_any check Util.ffalse ity in
921
  let is_impure_type ts =
922
    ts.its_abst || ts.its_priv || ts.its_regs <> [] ||
923
    option_apply false check ts.its_def
924
  in
925
  let check (pv,_) =
926
    let vtv = pv.pv_vtv in
927
    vtv.vtv_ghost || vtv.vtv_mut <> None || check vtv.vtv_ity in
928 929 930
  let is_impure_data (ts,csl) =
    is_impure_type ts ||
    List.exists (fun (_,l) -> List.exists check l) csl
931
  in