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

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

40
41
(** errors *)

42
exception DuplicateProgVar of string
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
exception DuplicateTypeVar of string
(*
exception PredicateExpected
exception TermExpected
exception FSymExpected of lsymbol
exception PSymExpected of lsymbol
exception ClashTheory of string
exception UnboundTheory of qualid
exception UnboundType of string list
*)
exception UnboundTypeVar of string
exception UnboundSymbol of string list

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

59
60
let qloc = Typing.qloc
let print_qualid = Typing.print_qualid
61
62
63

let () = Exn_printer.register (fun fmt e -> match e with
  | DuplicateTypeVar s ->
64
65
66
      Format.fprintf fmt "Type parameter %s is used twice" s
  | DuplicateProgVar s ->
      Format.fprintf fmt "Parameter %s is used twice" s
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
(*
  | PredicateExpected ->
      Format.fprintf fmt "syntax error: predicate expected"
  | TermExpected ->
      Format.fprintf fmt "syntax error: term expected"
  | FSymExpected ls ->
      Format.fprintf fmt "%a is not a function symbol" Pretty.print_ls ls
  | PSymExpected ls ->
      Format.fprintf fmt "%a is not a predicate symbol" Pretty.print_ls ls
  | ClashTheory s ->
      Format.fprintf fmt "Clash with previous theory %s" s
  | UnboundTheory q ->
      Format.fprintf fmt "unbound theory %a" print_qualid q
  | UnboundType sl ->
      Format.fprintf fmt "Unbound type '%a'"
        (Pp.print_list Pp.dot Pp.pp_print_string) sl
*)
  | UnboundTypeVar s ->
      Format.fprintf fmt "unbound type variable '%s" s
  | UnboundSymbol sl ->
      Format.fprintf fmt "Unbound symbol '%a'"
        (Pp.print_list Pp.dot Format.pp_print_string) sl
  | _ -> raise e)

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

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

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

107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
(** Typing type expressions *)

let rec dity_of_pty ~user denv = function
  | Ptree.PPTtyvar id ->
      create_user_type_variable id
  | Ptree.PPTtyapp (pl, p) ->
      let dl = List.map (dity_of_pty ~user denv) pl in
      let x = Typing.string_list_of_qualid [] p in
      begin
        try
          let its = ns_find_it (get_namespace denv.uc) x in
          its_app ~user its dl
        with Not_found -> try
          let ts = ns_find_ts (Theory.get_namespace (get_theory denv.uc)) x in
          ts_app ts dl
        with Not_found ->
123
          errorm ~loc:(qloc p) "unbound symbol %a" print_qualid p
124
125
126
      end
  | Ptree.PPTtuple pl ->
      ts_app (ts_tuple (List.length pl)) (List.map (dity_of_pty ~user denv) pl)
127
128
129

(** Typing program expressions *)

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

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

139
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
(* record parsing *)

let parse_record uc fll =
  let pl = match fll with
    | [] -> raise EmptyRecord
    | (pl,_)::_ -> pl in
  let its = match pl.pl_args with
    | [{ vtv_ity = { ity_node = Ityapp (its,_,_) }}] -> its
    | _ -> raise (BadRecordField pl.pl_ls) in
  let cs, pjl = match find_constructors (get_known uc) its with
    | [cs,pjl] -> cs, List.map (exn_option (BadRecordField pl.pl_ls)) pjl
    | _ -> raise (BadRecordField pl.pl_ls) in
  let pjs = List.fold_left (fun s pj -> Sls.add pj.pl_ls s) Sls.empty pjl in
  let flm = List.fold_left (fun m (pj,v) -> let pj = pj.pl_ls in
    if not (Sls.mem pj pjs) then raise (BadRecordField pj) else
      Mls.add_new (DuplicateRecordField (cs.pl_ls,pj)) pj v m)
    Mls.empty fll
  in
  cs,pjl,flm

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

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

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

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

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

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

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

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

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

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

224
225
226
227
228
229
230
(* patterns *)

let add_var id dity denv =
  let tvars = add_tvars denv.tvars dity in
  let locals = Mstr.add id.id (tvars,dity) denv.locals in
  { denv with locals = locals; tvars = tvars }

231
let specialize_qualid uc p =
232
233
234
235
236
  let x = Typing.string_list_of_qualid [] p in
  try match ns_find_ps (get_namespace uc) x with
    | PV pv -> DEglobal_pv pv, specialize_pvsymbol pv
    | PS ps -> DEglobal_ps ps, specialize_psymbol  ps
    | PL pl -> DEglobal_pl pl, specialize_plsymbol pl
237
238
    | PX xs ->
        errorm ~loc:(qloc p) "unexpected exception symbol %a" print_xs xs
239
240
241
242
  with Not_found -> try
    let ls = ns_find_ls (Theory.get_namespace (get_theory uc)) x in
    DEglobal_ls ls, specialize_lsymbol ls
  with Not_found ->
243
    errorm ~loc:(qloc p) "unbound symbol %a" print_qualid p
244

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

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

265
266
267
268
269
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
  | Ptree.PPpapp (q,ppl) ->
272
      let sym, dity = specialize_qualid denv.uc q in
273
      dpat_app denv (mk_dexpr sym dity loc []) ppl
274
  | Ptree.PPprec fl when pure_record denv.uc fl ->
275
      let kn = Theory.get_known (get_theory denv.uc) in
276
      let fl = List.map (find_pure_field denv.uc) fl in
277
278
279
280
281
      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 ->
282
      let fl = List.map (find_field denv.uc) fl in
283
284
285
286
287
288
289
290
291
292
293
294
295
296
      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
and dpat_app denv ({ de_loc = loc } as de) ppl =
300
301
302
  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
303
  let pp = match de.de_desc with
304
305
    | 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
    | _ -> assert false
  in
  let res = create_type_variable () in
311
  Loc.try2 loc unify de.de_type (make_arrow_type tyl res);
312
313
  pp, res, denv

314
315
(* specifications *)

316
317
318
319
320
321
322
323
let dbinders denv bl =
  let dbinder (id,pty) (denv,bl,tyl) =
    let dity = match pty with
      | Some pty -> dity_of_pty ~user:true denv pty
      | None -> create_type_variable () in
    add_var id dity denv, (id,false,dity)::bl, dity::tyl
  in
  List.fold_right dbinder bl (denv,[],[])
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343

let deff_of_peff uc pe =
  { deff_reads  = List.map (fun le -> false, le) pe.pe_reads;
    deff_writes = List.map (fun le -> false, le) pe.pe_writes;
    deff_raises = List.map (fun q -> false, find_xsymbol uc q) pe.pe_raises; }

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

let rec dtype_c denv tyc =
  let tyv, dity = dtype_v denv tyc.pc_result_type in
  { dc_result = tyv;
    dc_effect = deff_of_peff denv.uc tyc.pc_effect;
    dc_pre    = tyc.pc_pre;
    dc_post   = fst tyc.pc_post;
    dc_xpost  = dxpost denv.uc (snd tyc.pc_post); },
  dity

and dtype_v denv = function
  | Tpure pty ->
      let dity = dity_of_pty ~user:true denv pty in
344
      DSpecV (false,dity), dity
345
346
347
348
  | Tarrow (bl,tyc) ->
      let denv,bl,tyl = dbinders denv bl in
      let tyc,dity = dtype_c denv tyc in
      DSpecA (bl,tyc), make_arrow_type tyl dity
349

350
(* expressions *)
351

352
353
354
let de_unit ~loc = hidden_ls ~loc (fs_tuple 0)

let de_app e el =
355
  let res = create_type_variable () in
356
  let tyl = List.map (fun a -> a.de_type) el in
357
358
359
  expected_type e (make_arrow_type tyl res);
  DEapply (e, el), res

Andrei Paskevich's avatar
Andrei Paskevich committed
360
let rec dexpr denv e =
361
  let loc = e.Ptree.expr_loc in
Andrei Paskevich's avatar
Andrei Paskevich committed
362
363
  let labs, uloc, d = extract_labels [] denv.uloc e in
  let denv = { denv with uloc = uloc } in
364
  let d, ty = de_desc denv loc d in
Andrei Paskevich's avatar
Andrei Paskevich committed
365
  let loc = def_option loc uloc in
366
  mk_dexpr d ty loc labs
367

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

Andrei Paskevich's avatar
Andrei Paskevich committed
532
and dletrec denv rdl =
Andrei Paskevich's avatar
Andrei Paskevich committed
533
534
535
  (* 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
536
    add_var id res denv, (id, res, bl, var, tr) in
Andrei Paskevich's avatar
Andrei Paskevich committed
537
538
539
  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) =
540
    let lam, dity = dlambda denv bl var tr in
Andrei Paskevich's avatar
Andrei Paskevich committed
541
    Loc.try2 id.id_loc unify dity res;
542
    id, dity, lam in
543
  List.map type_one rdl
Andrei Paskevich's avatar
Andrei Paskevich committed
544

545
546
and dlambda denv bl var (p, e, (q, xq)) =
  let denv,bl,tyl = dbinders denv bl in
Andrei Paskevich's avatar
Andrei Paskevich committed
547
  let e = dexpr denv e in
548
  let var = match var with
549
    | Some (le, Some q) -> [le, Some (find_variant_ls denv.uc q)]
550
551
552
553
    | Some (le, None) -> [le, None]
    | None -> [] in
(* TODO: accept a list of variants in the surface language
  let var = List.map (fun (le,q) ->
554
    le, Util.option_map (find_variant_ls denv.uc) q) var in
555
*)
556
  (bl, var, p, e, q, dxpost denv.uc xq), make_arrow_type tyl e.de_type
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
557

558
(** stage 2 *)
559

Andrei Paskevich's avatar
Andrei Paskevich committed
560
561
562
563
564
type lenv = {
  mod_uc   : module_uc;
  let_vars : let_var Mstr.t;
  log_vars : vsymbol Mstr.t;
  log_denv : Typing.denv;
565
566
}

Andrei Paskevich's avatar
Andrei Paskevich committed
567
let create_lenv uc = {
568
  mod_uc   = use_export_theory uc Mlw_wp.th_mark;
569
570
571
572
573
574
575
576
577
578
579
  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)

580
581
582
583
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
584
585
  let f = Typing.type_fmla (get_theory lenv.mod_uc) log_denv log_vars f in
  create_post res f
586
587
588
589

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
590
591
592
let create_variant lenv t =
  Typing.type_term (get_theory lenv.mod_uc) lenv.log_denv lenv.log_vars t

Andrei Paskevich's avatar
Andrei Paskevich committed
593
let add_local x lv lenv = match lv with
594
  | LetA _ ->
Andrei Paskevich's avatar
Andrei Paskevich committed
595
      { lenv with let_vars = Mstr.add x lv lenv.let_vars }
596
597
  | LetV pv ->
      let dty = dty_of_ty pv.pv_vs.vs_ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
598
599
600
601
      { 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 }
602

603
604
exception DuplicateException of xsymbol

605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
let binders lenv bl =
  let binder lenv (id, ghost, dity) =
    let vtv = vty_value ~ghost (ity_of_dity dity) in
    let pv = create_pvsymbol (Denv.create_user_id id) vtv in
    add_local id.id (LetV pv) lenv, pv in
  Util.map_fold_left binder lenv bl

let xpost lenv xq =
  let add_exn m (xs,f) =
    let f = create_post lenv "result" (ty_of_ity xs.xs_ity) f in
    Mexn.add_new (DuplicateException xs) xs f m in
  List.fold_left add_exn Mexn.empty xq

let eff_of_deff _lenv _deff = eff_empty (* TODO *)

let rec type_c lenv dtyc =
  let result = type_v lenv dtyc.dc_result in
  let ty = match result with
    | SpecV v -> ty_of_ity v.vtv_ity
    | SpecA _ -> ty_unit in
  { c_pre    = create_pre lenv dtyc.dc_pre;
    c_effect = eff_of_deff lenv dtyc.dc_effect;
    c_result = result;
    c_post   = create_post lenv "result" ty dtyc.dc_post;
    c_xpost  = xpost lenv dtyc.dc_xpost; }

and type_v lenv = function
  | DSpecV (ghost,v) ->
      SpecV (vty_value ~ghost (ity_of_dity v))
  | DSpecA (bl,tyc) ->
      let lenv, pvl = binders lenv bl in
      SpecA (pvl, type_c lenv tyc)

(* expressions *)

640
let rec expr lenv de = match de.de_desc with
641
  | DElocal x ->
Andrei Paskevich's avatar
Andrei Paskevich committed
642
643
      assert (Mstr.mem x lenv.let_vars);
      begin match Mstr.find x lenv.let_vars with
644
      | LetV pv -> e_value pv
645
      | LetA ps -> e_cast ps (vty_of_dity de.de_type)
646
      end
647
  | DElet (x, { de_desc = DEfun lam }, de2) ->
648
649
      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
650
      let e2 = expr lenv de2 in
651
652
      e_rec [def] e2
  | DEfun lam ->
653
      let x = mk_id "fn" de.de_loc in
654
      let def = expr_fun lenv x lam in
655
656
657
      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
658
      let e1 = expr lenv de1 in
659
      let def1 = create_let_defn (Denv.create_user_id x) e1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
660
661
      let lenv = add_local x.id def1.let_var lenv in
      let e2 = expr lenv de2 in
662
      e_let def1 e2
Andrei Paskevich's avatar
Andrei Paskevich committed
663
  | DEletrec (rdl, de1) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
664
      let rdl = expr_rec lenv rdl in
665
      let add_rd { rec_ps = ps } = add_local ps.ps_name.id_string (LetA ps) in
Andrei Paskevich's avatar
Andrei Paskevich committed
666
      let e1 = expr (List.fold_right add_rd rdl lenv) de1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
667
      e_rec rdl e1
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
668
  | DEapply (de1, del) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
669
      let el = List.map (expr lenv) del in
670
671
672
      begin match de1.de_desc with
        | DEglobal_pl pls -> e_plapp pls el (ity_of_dity de.de_type)
        | DEglobal_ls ls  -> e_lapp  ls  el (ity_of_dity de.de_type)
Andrei Paskevich's avatar
Andrei Paskevich committed
673
        | _               -> e_app (expr lenv de1) el
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
674
      end
675
676
677
  | DEglobal_pv pv ->
      e_value pv
  | DEglobal_ps ps ->
678
      e_cast ps (vty_of_dity de.de_type)
Andrei Paskevich's avatar
Andrei Paskevich committed
679
680
  | DEglobal_pl pl ->
      assert (pl.pl_ls.ls_args = []);
681
      e_plapp pl [] (ity_of_dity de.de_type)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
682
  | DEglobal_ls ls ->
Andrei Paskevich's avatar
Andrei Paskevich committed
683
      assert (ls.ls_args = []);
684
      e_lapp ls [] (ity_of_dity de.de_type)
685
  | DEif (de1, de2, de3) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
686
      e_if (expr lenv de1) (expr lenv de2) (expr lenv de3)
Andrei Paskevich's avatar
Andrei Paskevich committed
687
  | DEassign (de1, de2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
688
      e_assign (expr lenv de1) (expr lenv de2)
689
690
691
  | DEconstant c ->
      e_const c
  | DElazy (LazyAnd, de1, de2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
692
      e_lazy_and (expr lenv de1) (expr lenv de2)
693
  | DElazy (LazyOr, de1, de2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
694
      e_lazy_or (expr lenv de1) (expr lenv de2)
695
  | DEnot de1 ->
Andrei Paskevich's avatar
Andrei Paskevich committed
696
      e_not (expr lenv de1)
697
  | DEmatch (de1, bl) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
698
      let e1 = expr lenv de1 in
699
700
701
      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
702
703
        let lenv = Mstr.fold (fun s pv -> add_local s (LetV pv)) vm lenv in
        pp, expr lenv de in
704
      e_case e1 (List.map branch bl)
Andrei Paskevich's avatar
Andrei Paskevich committed
705
706
707
708
709
  | DEassert (ak, f) ->
      let ak = match ak with
        | Ptree.Aassert -> Aassert
        | Ptree.Aassume -> Aassume
        | Ptree.Acheck  -> Acheck in
710
      e_assert ak (create_pre lenv f)
711
  | DEabsurd ->
712
      e_absurd (ity_of_dity de.de_type)
Andrei Paskevich's avatar
Andrei Paskevich committed
713
  | DEraise (xs, de1) ->
714
      e_raise xs (expr lenv de1) (ity_of_dity de.de_type)
Andrei Paskevich's avatar
Andrei Paskevich committed
715
  | DEtry (de1, bl) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
716
      let e1 = expr lenv de1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
717
718
719
      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
720
721
        let lenv = add_local id.id (LetV pv) lenv in
        xs, pv, expr lenv de in
Andrei Paskevich's avatar
Andrei Paskevich committed
722
      e_try e1 (List.map branch bl)
Andrei Paskevich's avatar
Andrei Paskevich committed
723
724
725
726
  | 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)
727
728
  | DEany dtyc ->
      e_any (type_c lenv dtyc)
729
730
  | DEghost de1 ->
      e_ghost (expr lenv de1)
731
732
733
  | _ ->
      assert false (*TODO*)

Andrei Paskevich's avatar
Andrei Paskevich committed
734
and expr_rec lenv rdl =
735
  let step1 lenv (id, dity, lam) =
Andrei Paskevich's avatar
Andrei Paskevich committed
736
737
738
    let vta = match vty_of_dity dity with
      | VTarrow vta -> vta
      | VTvalue _ -> assert false in
739
    let ps = create_psymbol (Denv.create_user_id id) vta vars_empty in
740
    add_local id.id (LetA ps) lenv, (ps, lam) in
Andrei Paskevich's avatar
Andrei Paskevich committed
741
  let lenv, rdl = Util.map_fold_left step1 lenv rdl in
742
  let step2 (ps, lam) = ps, expr_lam lenv lam in
Andrei Paskevich's avatar
Andrei Paskevich committed
743
744
  create_rec_defn (List.map step2 rdl)

745
746
and expr_fun lenv x lam =
  let lam = expr_lam lenv lam in
747
  create_fun_defn (Denv.create_user_id x) lam
Andrei Paskevich's avatar
Andrei Paskevich committed
748

749
and expr_lam lenv (bl, var, p, e, q, xq) =
750
  let lenv, pvl = binders lenv bl in
Andrei Paskevich's avatar
Andrei Paskevich committed
751
  let e = expr lenv e in
Andrei Paskevich's avatar
Andrei Paskevich committed
752
  let ty = match e.e_vty with
Andrei Paskevich's avatar
Andrei Paskevich committed
753
    | VTarrow _ -> ty_unit
754
    | VTvalue vtv -> ty_of_ity vtv.vtv_ity in
Andrei Paskevich's avatar
Andrei Paskevich committed
755
  let mk_variant (t,r) = { v_term = create_variant lenv t; v_rel = r } in
Andrei Paskevich's avatar
Andrei Paskevich committed
756
  { l_args = pvl;
757
758
    l_variant = List.map mk_variant var;
    l_pre = create_pre lenv p;
Andrei Paskevich's avatar
Andrei Paskevich committed
759
    l_expr = e;
760
    l_post = create_post lenv "result" ty q;
761
    l_xpost = xpost lenv xq; }
762

763
764
(** Type declaration *)

765
type tys = ProgTS of itysymbol | PureTS of tysymbol
766
767
768
769
770
771
772
773
774

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)

775
776
777
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
778
779
780
  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
781
782
783
784
785
786
787
788
789
790
  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

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
855
856
857
858
859
860
861
862
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
863
        let tv = create_tvsymbol (Denv.create_user_id id) in
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
        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 ->
886
            let ts = ts_tuple (List.length tyl) in
887
888
889
890
891
            ity_pur ts (List.map parse tyl)
      in
      let ts = match d.td_def with
        | TDalias ty ->
            let def = parse ty in
892
893
            let rl = Sreg.elements def.ity_vars.vars_reg in
            create_itysymbol id ~abst ~priv vl rl (Some def)
894
        | TDalgebraic csl when Hashtbl.find mutables x ->
895
896
897
898
899
900
            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
901
              let vtv = vty_value ity in
902
903
              match id with
                | None ->
904
                    let pv = create_pvsymbol (id_fresh "pj") vtv in
905
                    Sreg.union s ity.ity_vars.vars_reg, (pv, false)
906
907
908
                | Some id ->
                    try
                      let pv = Hashtbl.find projs id.id in
909
                      let ty = pv.pv_vtv.vtv_ity in
910
911
                      (* once we have ghost/mutable fields in algebraics,
                         don't forget to check here that they coincide, too *)
912
                      ignore (Loc.try3 id.id_loc ity_match sbs ty ity);
913
914
                      s, (pv, true)
                    with Not_found ->
915
                      let pv = create_pvsymbol (Denv.create_user_id id) vtv in
916
                      Hashtbl.replace projs id.id pv;
917
                      Sreg.union s ity.ity_vars.vars_reg, (pv, true)
918
919
920
921
922
923
            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
924
            Hashtbl.replace predefs x def;
925
            create_itysymbol id ~abst ~priv vl (Sreg.elements s) None
926
        | TDrecord fl when Hashtbl.find mutables x ->
927
928
929
930
931
            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
932
                let r = create_region fid ity in
933
934
                Sreg.add r s, Some r
              else
935
                Sreg.union s ity.ity_vars.vars_reg, None