pgm_typing.ml 19.5 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, dpurify env c.dc_result_type
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
  | DEany c ->
      let c = type_c uc env c in
      Eany c
526

527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545
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

546
and triple uc env ((denvp, p), e, q) =
547
  let p = Typing.type_fmla denvp env p in
548
  let e = expr uc env e in
549
  let q = post env e.expr_type q in
550 551
  (p, e, q)

552 553
let type_expr uc e =
  let denv = create_denv uc in
554
  let e = dexpr denv e in
555
  expr uc Mstr.empty e
556

557 558 559 560 561
let type_type uc ty =
  let denv = create_denv uc in
  let dty = Typing.dty denv.denv ty in
  Denv.ty_of_dty dty

562 563 564 565 566 567 568 569
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
570
    errorm ?loc "clash with previous symbol %s" ls.ls_name.id_string
571
    
572 573 574 575 576
let file env uc dl =
  let uc, dl =
    List.fold_left
      (fun (uc, acc) d -> match d with
	 | Pgm_ptree.Dlogic dl -> 
577
	     let dl = logic_list0_decl dl in
578 579
	     List.fold_left (Typing.add_decl env Mnm.empty) uc dl, acc
	 | Pgm_ptree.Dlet (id, e) -> 
580 581
	     let e = type_expr uc e in
	     let tyl, ty = uncurrying uc e.expr_type in
582
	     let ls = create_lsymbol (id_user id.id id.id_loc) tyl (Some ty) in
583
	     let uc = add_decl uc ls in
584
	     uc, Dlet (ls, e) :: acc
585 586 587 588 589 590
	 | 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
591
	       let id = id_fresh v.vs_name.id_string in
592
	       let ls = create_lsymbol id tyl (Some ty) in
593
	       add_decl uc ls, (ls, r)
594 595 596
	     in
	     let uc, dl = map_fold_left one uc dl in
	     uc, Dletrec dl :: acc
597 598 599 600 601 602
	 | 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
603
	     let uc = add_decl uc ls in
604
	     uc, Dparam (ls, tyv) :: acc
605 606 607 608 609 610 611 612 613
	 | 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
614
      )
615 616 617
      (uc, []) dl
  in
  uc, List.rev dl
618 619 620 621 622 623

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

(* 
TODO:
627 628
- tuples

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

632
- ghost / effects
633
*)