- we now use a streaming architecture (run time gain: 11 secs)

[helm.git] / helm / software / lambda-delta / toplevel / metaOutput.ml

diff --git a/helm/software/lambda-delta/toplevel/metaOutput.ml b/helm/software/lambda-delta/toplevel/metaOutput.ml
index 4efee4a6833e511ba53428c3670cc2aec2e79082..7a15d07c250c5fa844958d63beeaab9a5b104384 100644 (file)
--- a/helm/software/lambda-delta/toplevel/metaOutput.ml
+++ b/helm/software/lambda-delta/toplevel/metaOutput.ml
@@ -63,7 +63,7 @@ let rec count_term f c = function
 
 let count_par f c (_, w) = count_term f c w
 
-let count_item f c = function
+let count_entry f c = function
    | _, pars, _, w, None        ->
       let c = {c with eabsts = succ c.eabsts} in
       let c = {c with pabsts = c.pabsts + List.length pars} in
@@ -76,8 +76,9 @@ let count_item f c = function
       let f c = count_term f c w in
       Cps.list_fold_left f count_par c pars
 
-let count f c b =
-   Cps.list_fold_left f count_item c b
+let count_item f c = function
+   | Some e -> count_entry f c e
+   | None   -> f c
 
 let print_counters f c =
    let terms = c.tsorts + c.tgrefs + c.tgrefs + c.tappls + c.tabsts in
@@ -142,9 +143,10 @@ let pp_body frm = function
    | Some (trans, t) ->
       F.fprintf frm "%s%a" (string_of_transparent trans) pp_term t
 
-let pp_item frm (l, pars, qid, u, body) =
+let pp_entry frm (l, pars, qid, u, body) =
    F.fprintf frm "@[%u@@%s%a%a:%a@]@\n%!" 
       l (string_of_qid qid) pp_pars pars pp_body body pp_term u
 
-let pp_environment f frm genv =
-   List.iter (pp_item frm) genv; f ()
+let pp_item f frm = function 
+   | Some entry -> pp_entry frm entry; f ()
+   | None       -> f ()