pgm_typing.ml 19.4 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
(*    Francois Bobot                                                      *)
(*    Jean-Christophe Filliatre                                           *)
(*    Johannes Kanig                                                      *)
(*    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.                  *)
(*                                                                        *)
(**************************************************************************)

20
open Format
21
open Why
22
open Util
23
open Ident
24
open Ty
25
open Term
26
open Theory
27 28 29
open Denv
open Ptree
open Pgm_ttree
30

31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54
type error =
  | Message of string

exception Error of error

let error ?loc e = match loc with
  | None -> raise (Error e)
  | Some loc -> raise (Loc.Located (loc, Error e))

let errorm ?loc f =
  let buf = Buffer.create 512 in
  let fmt = Format.formatter_of_buffer buf in
  Format.kfprintf
    (fun _ ->
       Format.pp_print_flush fmt ();
       let s = Buffer.contents buf in
       Buffer.clear buf;
       error ?loc (Message s))
    fmt f

let report fmt = function
  | Message s ->
      fprintf fmt "%s" s

55 56
let id_result = "result"

57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72
(* parsing LOGIC strings using functions from src/parser/
   requires proper relocation *)

let reloc loc lb =
  lb.Lexing.lex_curr_p <- loc;
  lb.Lexing.lex_abs_pos <- loc.Lexing.pos_cnum
    
let parse_string f loc s =
  let lb = Lexing.from_string s in
  reloc loc lb;
  f lb
    
let logic_list0_decl (loc, s) = parse_string Lexer.parse_list0_decl loc s
  
let lexpr (loc, s) = parse_string Lexer.parse_lexpr loc s

73 74
(* environments *)

75
let ts_unit uc = ns_find_ts (get_namespace uc) ["unit"]
76
let ts_ref uc = ns_find_ts (get_namespace uc) ["ref"]
77
let ts_arrow uc = ns_find_ts (get_namespace uc) ["arrow"]
78 79 80 81 82 83 84
let ts_exn uc = ns_find_ts (get_namespace uc) ["exn"]

let ls_Unit uc = ns_find_ls (get_namespace uc) ["Unit"]

let dty_bool uc = Tyapp (ns_find_ts (get_namespace uc) ["bool"], [])
let dty_unit uc = Tyapp (ts_unit uc, [])
let dty_label uc = Tyapp (ns_find_ts (get_namespace uc) ["label"], [])
85

86
type denv = {
87
  uc   : theory_uc;
88 89 90
  denv : Typing.denv;
}

91 92 93
let create_denv uc = 
  { uc   = uc;
    denv = Typing.create_denv uc;
94
  }
95

96 97 98 99
let create_type_var loc =
  let tv = Ty.create_tvsymbol (id_user "a" loc) in
  Tyvar (create_ty_decl_var ~loc ~user:false tv)

100 101
let dcurrying uc tyl ty =
  let make_arrow_type ty1 ty2 = Tyapp (ts_arrow uc, [ty1; ty2]) in
102
  List.fold_right make_arrow_type tyl ty
103

104
let uncurrying uc ty =
105
  let rec uncurry acc ty = match ty.ty_node with
106
    | Ty.Tyapp (ts, [t1; t2]) when ts == ts_arrow uc -> uncurry (t1 :: acc) t2
107 108 109 110
    | _ -> List.rev acc, ty
  in
  uncurry [] ty

111
let expected_type e ty =
112 113
  if not (Denv.unify e.dexpr_type ty) then
    errorm ~loc:e.dexpr_loc 
114
      "this expression has type %a, but is expected to have type %a"
115
      print_dty e.dexpr_type print_dty ty
116

117 118
(* phase 1: typing programs (using destructive type inference) *)

119 120
let pure_type env = Typing.dty env.denv

121 122 123 124 125 126
let rec dpurify env = function
  | DTpure ty -> 
      ty
  | DTarrow (bl, c) -> 
      dcurrying env.uc (List.map (fun (_,ty) -> dpurify env ty) bl)
	(dpurify env c.dc_result_type)
127

128 129 130 131 132
let check_reference_type uc loc ty =
  let ty_ref =Tyapp (ts_ref uc, [create_type_var loc]) in
  if not (Denv.unify ty ty_ref) then
    errorm ~loc "this expression has type %a, but is expected to be a reference"
      print_dty ty
133 134 135 136 137
  
let dreference env id =
  if Typing.mem_var id.id env.denv then
    (* local variable *)
    let ty = Typing.find_var id.id env.denv in
138
    check_reference_type env.uc id.id_loc ty;
139 140 141
    DRlocal id.id
  else 
    let p = Qident id in
142 143
    let s, _, ty = Typing.specialize_fsymbol p env.uc in
    check_reference_type env.uc id.id_loc ty;
144 145
    DRglobal s

146 147 148 149 150 151 152 153 154
let dexception env id =
  let p = Qident id in
  let _, _, ty as r = Typing.specialize_fsymbol p env.uc in
  let ty_exn = Tyapp (ts_exn env.uc, []) in
  if not (Denv.unify ty ty_exn) then
    errorm ~loc:id.id_loc
      "this expression has type %a, but is expected to be an exception"
      print_dty ty;
  r
155 156 157 158

let deffect env e =
  { de_reads  = List.map (dreference env) e.Pgm_ptree.pe_reads;
    de_writes = List.map (dreference env) e.Pgm_ptree.pe_writes;
159 160 161
    de_raises = 
      List.map (fun id -> let ls,_,_ = dexception env id in ls) 
	e.Pgm_ptree.pe_raises; }
162

163 164 165 166 167 168 169 170 171 172 173 174 175
let dpost env ty (q, ql) =
  let dexn (id, l) =
    let s, tyl, _ = dexception env id in
    let denv = match tyl with
      | [] -> env.denv
      | [ty] -> Typing.add_var id_result ty env.denv
      | _ -> assert false
    in
    s, (denv, lexpr l)
  in
  let denv = Typing.add_var id_result ty env.denv in
  (denv, lexpr q), List.map dexn ql

176 177 178 179 180 181 182 183 184 185 186 187
let rec dtype_v env = function
  | Pgm_ptree.Tpure pt -> 
      DTpure (pure_type env pt)
  | Pgm_ptree.Tarrow (bl, c) -> 
      let env, bl = map_fold_left dbinder env bl in
      let c = dtype_c env c in
      DTarrow (bl, c) 

and dtype_c env c = 
  let ty = dtype_v env c.Pgm_ptree.pc_result_type in
  { dc_result_name = c.Pgm_ptree.pc_result_name.id;
    dc_result_type = ty;
188
    dc_effect      = deffect env c.Pgm_ptree.pc_effect;
189 190
    dc_pre         = env.denv, lexpr c.Pgm_ptree.pc_pre;
    dc_post        = dpost env (dpurify env ty) c.Pgm_ptree.pc_post;
191
  }
192

193
and dbinder env ({id=x; id_loc=loc}, v) =
194 195 196 197 198 199 200 201
  let v = match v with
    | Some v -> dtype_v env v 
    | None -> DTpure (create_type_var loc)
  in
  let ty = dpurify env v in
  let env = { env with denv = Typing.add_var x ty env.denv } in
  env, (x, v)

202 203 204 205
let dloop_annotation a =
  { dloop_invariant = option_map lexpr a.Pgm_ptree.loop_invariant;
    dloop_variant   = option_map lexpr a.Pgm_ptree.loop_variant; }

206
let rec dexpr env e = 
207
  let d, ty = dexpr_desc env e.Pgm_ptree.expr_loc e.Pgm_ptree.expr_desc in
208 209
  { dexpr_desc = d; dexpr_loc = e.Pgm_ptree.expr_loc;
    dexpr_denv = env.denv; dexpr_type = ty;  }
210

211
and dexpr_desc env loc = function
212
  | Pgm_ptree.Econstant (ConstInt _ as c) ->
213
      DEconstant c, Tyapp (Ty.ts_int, [])
214
  | Pgm_ptree.Econstant (ConstReal _ as c) ->
215 216
      DEconstant c, Tyapp (Ty.ts_real, [])
  | Pgm_ptree.Eident (Qident {id=x}) when Typing.mem_var x env.denv ->
217
      (* local variable *)
218 219
      let ty = Typing.find_var x env.denv in
      DElocal x, ty
220
  | Pgm_ptree.Eident p ->
221 222
      let s, tyl, ty = Typing.specialize_fsymbol p env.uc in
      DEglobal s, dcurrying env.uc tyl ty
223
  | Pgm_ptree.Eapply (e1, e2) ->
224 225
      let e1 = dexpr env e1 in
      let e2 = dexpr env e2 in
226
      let ty2 = create_type_var loc and ty = create_type_var loc in
227 228
      if not (Denv.unify e1.dexpr_type (Tyapp (ts_arrow env.uc, [ty2; ty]))) 
      then
229 230 231
	errorm ~loc:e1.dexpr_loc "this expression is not a function";
      expected_type e2 ty2;
      DEapply (e1, e2), ty
232 233 234 235
  | Pgm_ptree.Efun (bl, t) ->
      let env, bl = map_fold_left dbinder env bl in
      let (_,e,_) as t = dtriple env t in
      let tyl = List.map (fun (x,_) -> Typing.find_var x env.denv) bl in
236
      let ty = dcurrying env.uc tyl e.dexpr_type in
237
      DEfun (bl, t), ty
238
  | Pgm_ptree.Elet ({id=x}, e1, e2) ->
239 240 241 242 243
      let e1 = dexpr env e1 in
      let ty1 = e1.dexpr_type in
      let env = { env with denv = Typing.add_var x ty1 env.denv } in
      let e2 = dexpr env e2 in
      DElet (x, e1, e2), e2.dexpr_type
244 245 246 247
  | Pgm_ptree.Eletrec (dl, e1) ->
      let env, dl = dletrec env dl in
      let e1 = dexpr env e1 in
      DEletrec (dl, e1), e1.dexpr_type
248

249
  | Pgm_ptree.Esequence (e1, e2) ->
250
      let e1 = dexpr env e1 in
251
      expected_type e1 (dty_unit env.uc);
252 253
      let e2 = dexpr env e2 in
      DEsequence (e1, e2), e2.dexpr_type
254
  | Pgm_ptree.Eif (e1, e2, e3) ->
255
      let e1 = dexpr env e1 in
256
      expected_type e1 (dty_bool env.uc);
257 258 259 260
      let e2 = dexpr env e2 in
      let e3 = dexpr env e3 in
      expected_type e3 e2.dexpr_type;
      DEif (e1, e2, e3), e2.dexpr_type
261
  | Pgm_ptree.Ewhile (e1, a, e2) ->
262
      let e1 = dexpr env e1 in
263
      expected_type e1 (dty_bool env.uc);
264
      let e2 = dexpr env e2 in
265
      expected_type e2 (dty_unit env.uc);
266
      DEwhile (e1, dloop_annotation a, e2), (dty_unit env.uc)
267
  | Pgm_ptree.Elazy (op, e1, e2) ->
268
      let e1 = dexpr env e1 in
269
      expected_type e1 (dty_bool env.uc);
270
      let e2 = dexpr env e2 in
271 272
      expected_type e2 (dty_bool env.uc);
      DElazy (op, e1, e2), (dty_bool env.uc)
273 274 275 276 277 278 279 280 281 282 283 284 285
  | Pgm_ptree.Ematch (el, bl) ->
      let el = List.map (dexpr env) el in
      let tyl = List.map (fun e -> e.dexpr_type) el in
      let ty = create_type_var loc in (* the type of all branches *)
      let branch (pl, e) =
	let denv, pl = Typing.dpat_list env.denv tyl pl in
	let env = { env with denv = denv } in
	let e = dexpr env e in
	expected_type e ty;
	pl, e
      in
      let bl = List.map branch bl in
      DEmatch (el, bl), ty
286
  | Pgm_ptree.Eskip ->
287
      DEskip, (dty_unit env.uc)
288 289
  | Pgm_ptree.Eabsurd ->
      DEabsurd, create_type_var loc
290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307
  | Pgm_ptree.Eraise (id, e) ->
      let ls, tyl, _ = dexception env id in
      let e = match e, tyl with
	| None, [] ->  
	    None
	| Some _, [] ->
	    errorm ~loc "expection %s has no argument" id.id
	| None, [ty] ->
	    errorm ~loc "exception %s is expecting an argument of type %a"
	      id.id print_dty ty;
	| Some e, [ty] -> 
	    let e = dexpr env e in
	    expected_type e ty;
	    Some e
	| _ -> 
	    assert false
      in
      DEraise (ls, e), create_type_var loc
308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329
  | Pgm_ptree.Etry (e1, hl) ->
      let e1 = dexpr env e1 in
      let handler (id, x, h) =
	let ls, tyl, _ = dexception env id in
	let x, env = match x, tyl with
	  | Some _, [] -> 
	      errorm ~loc "expection %s has no argument" id.id
	  | None, [] -> 
	      None, env
	  | None, [ty] ->
	      errorm ~loc "exception %s is expecting an argument of type %a"
		id.id print_dty ty;
	  | Some x, [ty] -> 
	      Some x.id, { env with denv = Typing.add_var x.id ty env.denv } 
	  | _ ->
	      assert false
	in
	let h = dexpr env h in
	expected_type h e1.dexpr_type;
	(ls, x, h)
      in
      DEtry (e1, List.map handler hl), e1.dexpr_type
330 331

  | Pgm_ptree.Eassert (k, le) ->
332
      DEassert (k, lexpr le), (dty_unit env.uc) 
333 334 335 336
  | Pgm_ptree.Eghost e1 ->
      let e1 = dexpr env e1 in
      DEghost e1, e1.dexpr_type
  | Pgm_ptree.Elabel ({id=l}, e1) ->
337
      let ty = dty_label env.uc in
338
      let env = { env with denv = Typing.add_var l ty env.denv } in
339 340
      let e1 = dexpr env e1 in
      DElabel (l, e1), e1.dexpr_type
341 342 343 344 345
  | Pgm_ptree.Ecast (e1, ty) ->
      let e1 = dexpr env e1 in
      let ty = pure_type env ty in
      expected_type e1 ty;
      e1.dexpr_desc, ty
346 347 348
  | Pgm_ptree.Eany _c ->
      (* let c = dtype_c env c in *)
(*       DEany c, c.dc_result_type *)assert false (*TODO*)
349

350 351
and dletrec env dl =
  (* add all functions into environment *)
352
  let add_one env (id, bl, var, t) = 
353
    let ty = create_type_var id.id_loc in
354
    let env = { env with denv = Typing.add_var id.id ty env.denv } in
355
    env, ((id, ty), bl, option_map lexpr var, t)
356
  in
357
  let env, dl = map_fold_left add_one env dl in
358
  (* then type-check all of them and unify *)
359
  let type_one ((id, tyres), bl, v, t) = 
360 361 362 363 364 365 366 367
    let env, bl = map_fold_left dbinder env bl in
    let (_,e,_) as t = dtriple env t in
    let tyl = List.map (fun (x,_) -> Typing.find_var x env.denv) bl in
    let ty = dcurrying env.uc tyl e.dexpr_type in
    if not (Denv.unify ty tyres) then 
      errorm ~loc:id.id_loc
	"this expression has type %a, but is expected to have type %a"
	print_dty ty print_dty tyres;
368
    ((id.id, tyres), bl, v, t)
369 370 371
  in
  env, List.map type_one dl

372
and dtriple env (p, e, q) =     
373
  let p = env.denv, lexpr p in
374 375
  let e = dexpr env e in
  let ty = e.dexpr_type in
376
  let q = dpost env ty q in
377 378
  (p, e, q)

379 380
(* phase 2: typing annotations *)

381 382 383
let currying uc tyl ty =
  let make_arrow_type ty1 ty2 = Ty.ty_app (ts_arrow uc) [ty1; ty2] in
  List.fold_right make_arrow_type tyl ty
384

385 386 387 388
let purify uc = function
  | Tpure ty -> 
      ty
  | Tarrow (bl, c) -> 
389
      currying uc (List.map (fun (v,_) -> v.vs_ty) bl) c.c_result_name.vs_ty
390

391 392 393 394 395 396 397 398 399
let reference _uc env = function
  | DRlocal x -> Rlocal (Mstr.find x env)
  | DRglobal ls -> Rglobal ls

let effect uc env e =
  { e_reads  = List.map (reference uc env) e.de_reads;
    e_writes = List.map (reference uc env) e.de_writes;
    e_raises = e.de_raises; }

400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419
let pre env (denv, l) = Typing.type_fmla denv env l

let post env ty (q, ql) =
  let exn (ls, (denv, l)) =
    let env = match ls.ls_args with
      | [] -> 
	  env
      | [ty] -> 
	  let v_result = create_vsymbol (id_fresh id_result) ty in
	  Mstr.add id_result v_result env
      | _ -> 
	  assert false
    in
    (ls, Typing.type_fmla denv env l)
  in
  let denv, l = q in 
  let v_result = create_vsymbol (id_fresh id_result) ty in
  let env = Mstr.add id_result v_result env in
  Typing.type_fmla denv env l, List.map exn ql

420 421 422 423 424 425 426 427 428 429 430 431 432
let rec type_v uc env = function
  | DTpure ty -> 
      Tpure (Denv.ty_of_dty ty)
  | DTarrow (bl, c) -> 
      let env, bl = map_fold_left (binder uc) env bl in
      Tarrow (bl, type_c uc env c)

and type_c uc env c = 
  let tyv = type_v uc env c.dc_result_type in
  let ty = purify uc tyv in
  let v = create_vsymbol (id_fresh c.dc_result_name) ty in
  { c_result_name = v;
    c_result_type = tyv;
433
    c_effect      = effect uc env c.dc_effect;
434 435
    c_pre         = pre env c.dc_pre;
    c_post        = post env ty c.dc_post;
436 437 438 439 440
  }
    
and binder uc env (x, tyv) = 
  let tyv = type_v uc env tyv in
  let v = create_vsymbol (id_fresh x) (purify uc tyv) in
441 442 443
  let env = Mstr.add x v env in
  env, (v, tyv)

444 445
let rec expr uc env e =
  let d = expr_desc uc env e.dexpr_denv e.dexpr_desc in
446 447 448
  let ty = Denv.ty_of_dty e.dexpr_type in
  { expr_desc = d; expr_type = ty; expr_loc = e.dexpr_loc }

449
and expr_desc uc env denv = function
450 451 452
  | DEconstant c ->
      Econstant c
  | DElocal x ->
453
      Elocal (Mstr.find x env)
454 455 456
  | DEglobal ls ->
      Eglobal ls
  | DEapply (e1, e2) ->
457
      Eapply (expr uc env e1, expr uc env e2)
458
  | DEfun (bl, e1) ->
459 460
      let env, bl = map_fold_left (binder uc) env bl in
      Efun (bl, triple uc env e1)
461
  | DElet (x, e1, e2) ->
462
      let e1 = expr uc env e1 in
463 464
      let v = create_vsymbol (id_fresh x) e1.expr_type in
      let env = Mstr.add x v env in
465
      Elet (v, e1, expr uc env e2)
466 467 468 469
  | DEletrec (dl, e1) ->
      let env, dl = letrec uc env dl in
      let e1 = expr uc env e1 in
      Eletrec (dl, e1)
470 471

  | DEsequence (e1, e2) ->
472
      Esequence (expr uc env e1, expr uc env e2)
473
  | DEif (e1, e2, e3) ->
474
      Eif (expr uc env e1, expr uc env e2, expr uc env e3)
475
  | DEwhile (e1, la, e2) ->
476 477
      let la = 
	{ loop_invariant = 
478
	    option_map (Typing.type_fmla denv env) la.dloop_invariant;
479
	  loop_variant   = 
480
	    option_map (Typing.type_term denv env) la.dloop_variant; }
481
      in
482
      Ewhile (expr uc env e1, la, expr uc env e2)
483
  | DElazy (op, e1, e2) ->
484
      Elazy (op, expr uc env e1, expr uc env e2)
485 486 487 488 489 490 491 492
  | DEmatch (el, bl) ->
      let el = List.map (expr uc env) el in
      let branch (pl, e) = 
        let env, pl = map_fold_left Typing.pattern env pl in
        (pl, expr uc env e)
      in
      let bl = List.map branch bl in
      Ematch (el, bl)
493 494
  | DEskip ->
      Eskip
495 496
  | DEabsurd ->
      Eabsurd
497 498
  | DEraise (ls, e) ->
      Eraise (ls, option_map (expr uc env) e)
499 500 501 502 503 504 505 506 507 508 509 510 511
  | DEtry (e, hl) ->
      let handler (ls, x, h) =
	let x, env = match x with
	  | Some x -> 
	      let ty = match ls.ls_args with [ty] -> ty | _ -> assert false in
	      let v = create_vsymbol (id_fresh x) ty in
	      Some v, Mstr.add x v env 
	  | None ->
	      None, env
	in
	(ls, x, expr uc env h)
      in
      Etry (expr uc env e, List.map handler hl)
512 513

  | DEassert (k, f) ->
514
      let f = Typing.type_fmla denv env f in
515
      Eassert (k, f)
516
  | DEghost e1 -> 
517
      Eghost (expr uc env e1)
518
  | DElabel (s, e1) ->
519 520 521
      let ty = Denv.ty_of_dty (Typing.find_var s e1.dexpr_denv) in
      let v = create_vsymbol (id_fresh s) ty in
      let env = Mstr.add s v env in 
522
      Elabel (s, expr uc env e1)
523

524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542
and letrec uc env dl =
  (* add all functions into env, and compute local env *)
  let step1 env ((x, dty), bl, var, t) = 
    let ty = Denv.ty_of_dty dty in
    let v = create_vsymbol (id_fresh x) ty in
    let env = Mstr.add x v env in
    env, (v, bl, var, t)
  in
  let env, dl = map_fold_left step1 env dl in
  (* then translate variants and bodies *)
  let step2 (v, bl, var, (_,e,_ as t)) =
    let env, bl = map_fold_left (binder uc) env bl in
    let denv = e.dexpr_denv in
    let var = option_map (Typing.type_term denv env) var in
    let t = triple uc env t in
    (v, bl, var, t)
  in
  env, List.map step2 dl

543
and triple uc env ((denvp, p), e, q) =
544
  let p = Typing.type_fmla denvp env p in
545
  let e = expr uc env e in
546
  let q = post env e.expr_type q in
547 548
  (p, e, q)

549 550
let type_expr uc e =
  let denv = create_denv uc in
551
  let e = dexpr denv e in
552
  expr uc Mstr.empty e
553

554 555 556 557 558
let type_type uc ty =
  let denv = create_denv uc in
  let dty = Typing.dty denv.denv ty in
  Denv.ty_of_dty dty

559 560 561 562 563 564 565 566
let add_decl uc ls =
  try
    Theory.add_decl uc (Decl.create_logic_decl [ls, None])
  with Theory.ClashSymbol _ ->
    let loc = match ls.ls_name.id_origin with
      | User loc -> Some loc
      | _ -> None (* FIXME: loc for recursive functions *)
    in
567
    errorm ?loc "clash with previous symbol %s" ls.ls_name.id_string
568
    
569 570 571 572 573
let file env uc dl =
  let uc, dl =
    List.fold_left
      (fun (uc, acc) d -> match d with
	 | Pgm_ptree.Dlogic dl -> 
574
	     let dl = logic_list0_decl dl in
575 576
	     List.fold_left (Typing.add_decl env Mnm.empty) uc dl, acc
	 | Pgm_ptree.Dlet (id, e) -> 
577 578
	     let e = type_expr uc e in
	     let tyl, ty = uncurrying uc e.expr_type in
579
	     let ls = create_lsymbol (id_user id.id id.id_loc) tyl (Some ty) in
580
	     let uc = add_decl uc ls in
581
	     uc, Dlet (ls, e) :: acc
582 583 584 585 586 587
	 | Pgm_ptree.Dletrec dl -> 
	     let denv = create_denv uc in
	     let _, dl = dletrec denv dl in
	     let _, dl = letrec uc Mstr.empty dl in
	     let one uc (v,_,_,_ as r) =
	       let tyl, ty = uncurrying uc v.vs_ty in
588
	       let id = id_fresh v.vs_name.id_string in
589
	       let ls = create_lsymbol id tyl (Some ty) in
590
	       add_decl uc ls, (ls, r)
591 592 593
	     in
	     let uc, dl = map_fold_left one uc dl in
	     uc, Dletrec dl :: acc
594 595 596 597 598 599
	 | Pgm_ptree.Dparam (id, tyv) ->
	     let denv = create_denv uc in
	     let tyv = dtype_v denv tyv in
	     let tyv = type_v uc Mstr.empty tyv in
	     let tyl, ty = uncurrying uc (purify uc tyv) in
	     let ls = create_lsymbol (id_user id.id id.id_loc) tyl (Some ty) in
600
	     let uc = add_decl uc ls in
601
	     uc, Dparam (ls, tyv) :: acc
602 603 604 605 606 607 608 609 610
	 | Pgm_ptree.Dexn (id, ty) ->
	     let tyl = match ty with
	       | None -> []
	       | Some ty -> [type_type uc ty]
	     in
	     let exn = ty_app (ts_exn uc) [] in
	     let ls = create_lsymbol (id_user id.id id.id_loc) tyl (Some exn) in
	     let uc = add_decl uc ls in
	     uc, acc
611
      )
612 613 614
      (uc, []) dl
  in
  uc, List.rev dl
615 616 617 618 619 620

(*
Local Variables: 
compile-command: "unset LANG; make -C ../.. testl"
End: 
*)
621 622 623 624 625 626 627 628

(* 

TODO:
- mutually recursive functions: check variants are all present or all absent
- variant: check type int or relation order specified

*)