pgm_wp.ml 16.3 KB
Newer Older
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
1 2 3
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
MARCHE Claude's avatar
MARCHE Claude committed
4 5 6
(*    François Bobot                                                     *)
(*    Jean-Christophe Filliâtre                                          *)
(*    Claude Marché                                                      *)
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
7 8 9 10 11 12 13 14 15 16 17 18
(*    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.                  *)
(*                                                                        *)
(**************************************************************************)
19

20
open Format
21
open Why
22
open Util
23
open Ident
24
open Ty
25 26 27
open Term
open Decl
open Theory
28
open Pretty
29
open Pgm_ttree
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
30
open Pgm_types
31
open Pgm_types.T
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
32
open Pgm_module
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
33

34
let debug = Debug.register_flag "program_wp"
35

36 37
(* phase 4: weakest preconditions *******************************************)

38 39 40
(* smart constructors for building WPs
   TODO: use simp forms / tag with label "WP" *)

41
let wp_and ?(sym=false) f1 f2 =
42 43
(*   if sym then f_and_simp f1 f2 else f_and_simp f1 (f_implies_simp f1 f2)  *)
  let f = f_and_simp f1 f2 in
44 45 46
  match f.f_node with
    | Fbinop (Fand, _, _) when not sym -> f_label_add Split_goal.asym_split f
    | _ -> f
47

48 49 50
let wp_ands ?(sym=false) fl =
  List.fold_left (wp_and ~sym) f_true fl

51 52 53
let wp_implies f1 f2 = match f2.f_node with
  | Ffalse -> f_implies f1 f2
  | _ -> f_implies_simp f1 f2
54

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
55 56
let find_ts uc s = ns_find_ts (get_namespace (theory_uc uc)) [s]
let find_ls uc s = ns_find_ls (get_namespace (theory_uc uc)) [s]
57

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
58 59
let is_arrow_ty ty = match ty.ty_node with
  | Tyapp (ts, _) -> ts_equal ts ts_arrow
60 61
  | _ -> false

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
62 63
let wp_forall v f =
  if is_arrow_ty v.vs_ty then f else match f.f_node with
64 65 66 67 68 69 70
    | Fbinop (Fimplies, {f_node = Fapp (s,[{t_node = Tvar u};r])},h)
      when ls_equal s ps_equ && vs_equal u v && not (t_occurs_single v r) ->
        f_subst_single v r h
    | Fbinop (Fimplies, {f_node = Fbinop (Fand, g,
                        {f_node = Fapp (s,[{t_node = Tvar u};r])})},h)
      when ls_equal s ps_equ && vs_equal u v && not (t_occurs_single v r) ->
        f_subst_single v r (f_implies_simp g h)
Andrei Paskevich's avatar
Andrei Paskevich committed
71 72 73 74
    | _ when f_occurs_single v f ->
        f_forall_close_simp [v] [] f
    | _ ->
        f
75 76

(* utility functions for building WPs *)
77

78
let fresh_label env =
79
  let ty = ty_app (find_ts env "label_") [] in
80
  create_vsymbol (id_fresh "label") ty
81

82 83
let wp_binder x f = match x.pv_tv with
  | Tpure _ -> wp_forall x.pv_vs f
84 85
  | Tarrow _ -> f

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
86
let wp_binders = List.fold_right wp_binder
87

88 89 90
(* replace old(t) with at(t,lab) everywhere in formula f *)
let rec old_label env lab f =
  f_map (old_label_term env lab) (old_label env lab) f
91

92
and old_label_term env lab t = match t.t_node with
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
93
  | Tapp (ls, [t]) when ls_equal ls (find_ls env "old") ->
94
      let t = old_label_term env lab t in (* NECESSARY? *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
95
      t_app (find_ls env "at") [t; t_var lab] t.t_ty
96 97 98 99 100
  | _ ->
      t_map (old_label_term env lab) (old_label env lab) t

(* replace at(t,lab) with t everywhere in formula f *)
let rec erase_label env lab f =
101
  f_map (erase_label_term env lab) (erase_label env lab) f
102 103

and erase_label_term env lab t = match t.t_node with
104
  | Tapp (ls, [t; {t_node = Tvar l}])
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
105
    when ls_equal ls (find_ls env "at") && vs_equal l lab ->
106 107 108 109 110 111 112
      erase_label_term env lab t
  | _ ->
      t_map (erase_label_term env lab) (erase_label env lab) t

let rec unref env r v f =
  f_map (unref_term env r v) (unref env r v) f

113 114 115 116 117 118
and unref_term env r v t = match r, t.t_node with
  | R.Rglobal {p_ls=ls1}, Tapp (ls2, _) when ls_equal ls1 ls2 ->
      t_var v
  | R.Rlocal {pv_vs=vs1}, Tvar vs2 when vs_equal vs1 vs2 ->
      t_var v
  | _, Tapp (ls, _) when ls_equal ls (find_ls env "old") ->
119
      assert false
120
  | _, Tapp (ls, _) when ls_equal ls (find_ls env "at") -> 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
121
      (* do not recurse in at(...) *)
122
      t
123 124 125 126
  | _ ->
      t_map (unref_term env r v) (unref env r v) t

(* quantify over all references in ef *)
127
let quantify ?(all=false) env ef f =
128
  (* eprintf "quantify: ef=%a f=%a@." E.print ef Pretty.print_fmla f; *)
129
  let quantify1 r f =
130
    let ty = R.type_of r in
131
    let v = create_vsymbol (id_clone (R.name_of r)) ty in
132
    let f = unref env r v f in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
133
    wp_forall v f
134
  in
135
  let s = ef.E.writes in
136 137
  let s = if all then Sref.union ef.E.reads s else s in
  Sref.fold quantify1 s f
138

139 140
let abstract_wp env ef (q',ql') (q,ql) =
  assert (List.length ql' = List.length ql);
141
  let quantify_res f' f res =
142
    let f = wp_implies f' f in
143
    let f = match res with
144
      (* | Some v when is_mutable_ty v.vs_ty -> *)
145 146
      (* 	  let v' = create_vsymbol (id_clone v.vs_name) (unref_ty env v.vs_ty) in *)
      (* 	  wp_forall v' (unref env (R.Rlocal v) v' f) *)
147
      | Some v ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
148
	  wp_forall v f
149 150
      | None ->
	  f
151
    in
152 153 154 155 156
    quantify env ef f
  in
  let quantify_h (e',(x',f')) (e,(x,f)) =
    assert (ls_equal e' e);
    let res, f' = match x', x with
157
      | Some v', Some v -> Some v, f_subst (subst1 v' (t_var v)) f'
158 159 160
      | None, None -> None, f'
      | _ -> assert false
    in
161
    quantify_res f' f res
162
  in
163
  let f =
164
    let res, f = q and res', f' = q' in
165
    let f' = f_subst (subst1 res' (t_var res)) f' in
166
    quantify_res f' f (Some res)
167 168 169
  in
  wp_ands (f :: List.map2 quantify_h ql' ql)

170
let opaque_wp env ef q' q =
171 172 173 174 175
  let lab = fresh_label env in
  let q' = post_map (old_label env lab) q' in
  let f = abstract_wp env ef q' q in
  erase_label env lab f

176 177 178 179
(*s [filter_post k q] removes exc. postconditions from [q] which do not
    appear in effect [ef] *)

let filter_post ef (q, ql) =
180
  let keep (ls, _) = Sexn.mem ls ef.E.raises in
181 182 183 184 185 186 187 188 189 190
  q, List.filter keep ql

let rec ls_assoc ls = function
  | [] -> raise Not_found
  | (ls', x) :: _ when ls_equal ls ls' -> x
  | _ :: r -> ls_assoc ls r

let default_exn_post ls = ls, (exn_v_result ls, f_true)

let default_post ty ef =
191
  (v_result ty, f_true),
192
  List.map default_exn_post (Sexn.elements ef.E.raises)
193

194
let rec assoc_handler x = function
195
  | [] -> raise Not_found
196 197 198
  | (y, h) :: _ when ls_equal x y -> h
  | _ :: hl -> assoc_handler x hl

199 200 201
(*s [saturate_post ef f q] makes a postcondition for a program of effect [ef]
    out of a normal postcondition [f] and the exc. postconditions from [q] *)

202
let saturate_post ef q (_, ql) =
203
  let set_post x = try x, ls_assoc x ql with Not_found -> default_exn_post x in
204
  let xs = Sexn.elements ef.E.raises in
205
  (q, List.map set_post xs)
206

207 208 209 210 211 212 213 214 215 216
(* maximum *)

let is_default_post = f_equal f_true

let sup ((q, ql) : post) (_, ql') =
  assert (List.length ql = List.length ql');
  let supx (x, (_,fa) as a) (x', _ as a') =
    assert (ls_equal x x');
    if is_default_post fa then a' else a
  in
217
  q, List.map2 supx ql ql'
218 219 220 221

(* post-condition for a loop body *)

let default_exns_post ef =
222
  let xs = Sexn.elements ef.E.raises in
223
  List.map default_exn_post xs
224

225
let term_at env lab t =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
226
  t_app (find_ls env "at") [t; t_var lab] t.t_ty
227

228
let while_post_block env inv var lab e =
229
  let decphi = match var with
230
    | None ->
231
	f_true
232 233 234 235 236 237
    | Some (phi, None) ->
	let old_phi = term_at env lab phi in
	(* 0 <= old_phi and phi < old_phi *)
	wp_and (f_app (find_ls env "infix <=") [t_int_const "0"; old_phi])
	       (f_app (find_ls env "infix <")  [phi; old_phi])
    | Some (phi, Some r) ->
238 239 240 241 242
	f_app r [phi; term_at env lab phi]
  in
  let ql = default_exns_post e.expr_effect in
  let res = v_result e.expr_type in
  match inv with
243
    | None ->
244
	(res, decphi), ql
245
    | Some i ->
246 247 248 249 250 251 252
	(res, wp_and i decphi), ql

let well_founded_rel = function
  | None -> f_true
  | Some (_,_r) -> f_true (* TODO: Papp (well_founded, [Tvar r], []) *)


253 254
(* Recursive computation of the weakest precondition *)

255 256 257
let propose_label l f =
  if f.f_label = [] then f_label [l] f else f

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
258 259 260
let t_True env =
  t_app (find_ls env "True") [] (ty_app (find_ts env "bool") [])

261
let rec wp_expr env e q =
262 263 264
  let lab = fresh_label env in
  let q = post_map (old_label env lab) q in
  let f = wp_desc env e q in
265
  let f = erase_label env lab f in
266
  let f = propose_label (label ~loc:e.expr_loc "WP") f in
267 268 269 270 271
  if Debug.test_flag debug then begin
    eprintf "@[--------@\n@[<hov 2>e = %a@]@\n" Pgm_pretty.print_expr e;
    eprintf "@[<hov 2>q = %a@]@\n" Pretty.print_fmla (snd (fst q));
    eprintf "@[<hov 2>f = %a@]@\n----@]@\n" Pretty.print_fmla f;
  end;
272
  f
273 274

and wp_desc env e q = match e.expr_desc with
275
  | Elogic t ->
276
      let (v, q), _ = q in
Andrei Paskevich's avatar
Andrei Paskevich committed
277
      f_subst_single v t q
278 279
  | Elocal v ->
      let (res, q), _ = q in
280
      f_subst (subst1 res (t_var v.pv_vs)) q
281
  | Eglobal _ ->
282
      let (_, q), _ = q in q
283
  | Efun (bl, t) ->
284
      let (_, q), _ = q in
285
      let f = wp_triple env t in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
286
      wp_and q (wp_binders bl f)
287 288
  | Elet (x, e1, e2) ->
      let w2 = wp_expr env e2 (filter_post e2.expr_effect q) in
289
      let v1 = v_result x.pv_vs.vs_ty in
290
      let t1 = t_label_add (label ~loc:e1.expr_loc "let") (t_var v1) in
291
      let q1 = v1, f_subst (subst1 x.pv_vs t1) w2 in
292 293
      let q1 = saturate_post e1.expr_effect q1 q in
      wp_expr env e1 q1
294 295
  | Eletrec (dl, e1) ->
      let w1 = wp_expr env e1 q in
296
      let wl = List.map (wp_recfun env) dl in
297
      wp_ands ~sym:true (w1 :: wl)
298

299 300 301 302 303 304
  | Eif (e1, e2, e3) ->
      let w2 = wp_expr env e2 (filter_post e2.expr_effect q) in
      let w3 = wp_expr env e3 (filter_post e3.expr_effect q) in
      let q1 = (* if result=True then w2 else w3 *)
	let res = v_result e1.expr_type in
	let test = f_equ (t_var res) (t_True env) in
305
	let test = f_label_add (label ~loc:e1.expr_loc "WP") test in
306 307 308 309
	let q1 = f_if test w2 w3 in
	saturate_post e1.expr_effect (res, q1) q
      in
      wp_expr env e1 q1
310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326
  | Eloop ({ loop_invariant = inv; loop_variant = var }, e1) ->
      let wfr = well_founded_rel var in
      let lab = fresh_label env in
      let q1 = while_post_block env inv var lab e1 in
      let q1 = sup q1 q in (* exc. posts taken from [q] *)
      let we = wp_expr env e1 q1 in
      let we = erase_label env lab we in
      let w = match inv with
	| None ->
	    wp_and wfr (quantify env e.expr_effect we)
	| Some i ->
	    wp_and wfr
	      (wp_and ~sym:true
		 i
		 (quantify env e.expr_effect (wp_implies i we)))
	in
	w
327
  (* optimization for the particular case let _ = y in e *)
328
  | Ematch (_, [{ppat_pat = {pat_node = Term.Pwild}}, e]) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
329
      wp_expr env e (filter_post e.expr_effect q)
Andrei Paskevich's avatar
Andrei Paskevich committed
330
  | Ematch (x, bl) ->
331
      let branch (p, e) =
332
        f_close_branch p.ppat_pat (wp_expr env e (filter_post e.expr_effect q))
333
      in
334
      let t = t_var x.pv_vs in
Andrei Paskevich's avatar
Andrei Paskevich committed
335
      f_case t (List.map branch bl)
336
  | Eabsurd ->
337 338 339 340 341 342 343 344 345
      f_false
  | Eraise (x, None) ->
      (* $wp(raise E, _, R) = R$ *)
      let _, ql = q in
      let _, f = assoc_handler x ql in f
  | Eraise (x, Some e1) ->
      (* $wp(raise (E e1), _, R) = wp(e1, R, R)$ *)
      let _, ql = q in
      let q1 = match assoc_handler x ql with
346
	| Some v, r -> (v, r), ql
347 348 349 350 351 352
	| None, _ -> assert false
      in
      let q1 = filter_post e1.expr_effect q1 in
      wp_expr env e1 q1
  | Etry (e1, hl) ->
      (* $wp(try e1 with E -> e2, Q, R) = wp(e1, Q, wp(e2, Q, R))$ *)
353 354 355
      let hwl =
	List.map
	  (fun (x, v, h) ->
356
	     let w = wp_expr env h (filter_post h.expr_effect q) in
357
	     let v = option_map (fun v -> v.pv_vs) v in
358
	     x, (v, w))
359
	  hl
360 361 362 363 364 365 366 367 368 369
      in
      let make_post (q, ql) =
	let hpost (x, r) =
	  x, try assoc_handler x hwl with Not_found -> r
	in
	q, List.map hpost ql
      in
      let q1 = saturate_post e1.expr_effect (fst q) q in
      let q1 = filter_post e1.expr_effect (make_post q1) in
      wp_expr env e1 q1
370
  | Efor (x, v1, d, v2, inv, e1) ->
371 372 373
      (* wp(for x = v1 to v2 do inv { I(x) } e1, Q, R) =
             v1 > v2  -> Q
         and v1 <= v2 ->     I(v1)
374
                         and forall S. forall i. v1 <= i <= v2 ->
375 376 377
                                                 I(i) -> wp(e1, I(i+1), R)
	                               and I(v2+1) -> Q                    *)
      let (res, q1), _ = q in
378
      let gt, le, incr = match d with
379
	| Ptree.To     -> 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
380
	    find_ls env "infix >", find_ls env "infix <=", t_int_const  "1"
381
	| Ptree.Downto -> 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
382
	    find_ls env "infix <", find_ls env "infix >=", t_int_const "-1"
383
      in
384 385
      let v1_gt_v2 = f_app gt [t_var v1.pv_vs; t_var v2.pv_vs] in
      let v1_le_v2 = f_app le [t_var v1.pv_vs; t_var v2.pv_vs] in
386
      let inv = match inv with Some inv -> inv | None -> f_true in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
387
      let add = find_ls env "infix +" in
388
      let wp1 =
389 390
	let xp1 = t_app add [t_var x.pv_vs; incr] ty_int in
	let post = f_subst (subst1 x.pv_vs xp1) inv in
391 392 393 394
	let q1 = saturate_post e1.expr_effect (res, post) q in
	wp_expr env e1 q1
      in
      let f = wp_and ~sym:true
395
	(f_subst (subst1 x.pv_vs (t_var v1.pv_vs)) inv)
396 397
	(quantify env e.expr_effect
	   (wp_and ~sym:true
398 399 400 401
	      (wp_forall x.pv_vs
	         (wp_implies 
		    (wp_and (f_app le [t_var v1.pv_vs; t_var x.pv_vs])
		            (f_app le [t_var x.pv_vs;  t_var v2.pv_vs]))
402
                 (wp_implies inv wp1)))
403 404
	      (let sv2 = t_app add [t_var v2.pv_vs; incr] ty_int in
	       wp_implies (f_subst (subst1 x.pv_vs sv2) inv) q1)))
405 406
      in
      wp_and ~sym:true (wp_implies v1_gt_v2 q1) (wp_implies v1_le_v2 f)
407

408
  | Eassert (Ptree.Aassert, f) ->
409 410
      let (_, q), _ = q in
      wp_and f q
411
  | Eassert (Ptree.Acheck, f) ->
412
      let (_, q), _ = q in
413
      wp_and ~sym:true f q
414
  | Eassert (Ptree.Aassume, f) ->
415 416 417 418 419
      let (_, q), _ = q in
      wp_implies f q
  | Elabel (lab, e1) ->
      let w1 = wp_expr env e1 q in
      erase_label env lab w1
420
  | Eany c ->
421
      (* TODO: propagate call labels into c.c_post *)
422
      let w = opaque_wp env c.c_effect c.c_post q in
423 424
      let p = f_label_add (label ~loc:e.expr_loc "call pre") c.c_pre in
      wp_and p w
425 426 427 428

and wp_triple env (p, e, q) =
  let f = wp_expr env e q in
  let f = wp_implies p f in
429
  quantify ~all:true env e.expr_effect f
430

431 432
and wp_recfun env (_, bl, _var, t) =
  let f = wp_triple env t in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
433
  wp_binders bl f
434

435
let wp env e =
436
  wp_expr env e (default_post e.expr_type e.expr_effect)
437

438 439 440
let rec t_btop env t = match t.t_node with
  | Tif (f,t1,t2) -> let f = f_btop env f in
      f_label t.t_label (f_if_simp f (t_btop env t1) (t_btop env t2))
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
441
  | Tapp (ls, [t1;t2]) when ls_equal ls (find_ls env "andb") ->
442
      f_label t.t_label (f_and_simp (t_btop env t1) (t_btop env t2))
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
443
  | Tapp (ls, [t1;t2]) when ls_equal ls (find_ls env "orb") ->
444
      f_label t.t_label (f_or_simp (t_btop env t1) (t_btop env t2))
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
445
  | Tapp (ls, [t1]) when ls_equal ls (find_ls env "notb") ->
446
      f_label t.t_label (f_not_simp (t_btop env t1))
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
447
  | Tapp (ls, []) when ls_equal ls (find_ls env "True") ->
448
      f_label t.t_label f_true
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
449
  | Tapp (ls, []) when ls_equal ls (find_ls env "False") ->
450 451 452 453 454 455
      f_label t.t_label f_false
  | _ ->
      f_equ t (t_True env)

and f_btop env f = match f.f_node with
  | Fapp (ls, [{t_ty = {ty_node = Tyapp (ts, [])}} as l; r])
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
456
  when ls_equal ls ps_equ && ts_equal ts (find_ts env "bool") ->
457 458 459
      f_label_copy f (f_iff_simp (t_btop env l) (t_btop env r))
  | _ -> f_map (fun t -> t) (f_btop env) f

460 461 462
let add_wp_decl ps f uc =
  let s = "WP_" ^ ps.p_name.id_string in
  let id = match id_from_user ps.p_name with
MARCHE Claude's avatar
MARCHE Claude committed
463 464 465
    | None -> id_fresh s
    | Some loc -> id_user s loc
  in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
466
  let f = f_btop uc f in
467
  (* printf "wp: f=%a@." print_fmla f; *)
MARCHE Claude's avatar
MARCHE Claude committed
468
  let pr = create_prsymbol id in
469
  let d = create_prop_decl Pgoal pr f in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
470
  add_logic_decl d uc
471

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
472
let decl uc = function
473 474 475
  | Pgm_ttree.Dlet ({ p_name = n } as ps, e) ->
      Debug.dprintf debug "@[--effect %s-----@\n  %a@]@\n----------------@."
	  n.id_string print_type_v e.expr_type_v;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
476
      let f = wp uc e in
477
      Debug.dprintf debug "wp = %a@\n----------------@." Pretty.print_fmla f;
478
      add_wp_decl ps f uc
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
479
  | Pgm_ttree.Dletrec dl ->
480
      let add_one uc ({ p_name = n } as ps, def) =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
481
	let f = wp_recfun uc def in
482 483 484
	Debug.dprintf debug "wp %s = %a@\n----------------@."
	   n.id_string Pretty.print_fmla f;
	add_wp_decl ps f uc
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
485
      in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
486
      List.fold_left add_one uc dl
487
  | Pgm_ttree.Dparam _ ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
488
      uc
489

490
(*
491
Local Variables:
492
compile-command: "unset LANG; make -C ../.. testl"
493
End:
494
*)