X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Ftoplevel%2FmetaOutput.ml;h=7f62c8abc0c71a6e6646e9bdb44fa5140cf9d1ba;hb=b183713e0e33245a4e58b433a930a94224d1f629;hp=7349fa573d9cbca4ee41e456c2c17304d361dbef;hpb=960ed22a5a6c415e2cf0ec9e8f5680d75c3ca0cd;p=helm.git diff --git a/helm/software/lambda-delta/toplevel/metaOutput.ml b/helm/software/lambda-delta/toplevel/metaOutput.ml index 7349fa573..7f62c8abc 100644 --- a/helm/software/lambda-delta/toplevel/metaOutput.ml +++ b/helm/software/lambda-delta/toplevel/metaOutput.ml @@ -60,9 +60,7 @@ let rec count_term f c = function let f c = count_term f c t in count_term f c w -let count_par f c (_, w) = - let c = {c with nodes = succ c.nodes} in - count_term f c w +let count_par f c (_, w) = count_term f c w let count_entry f c = function | _, pars, u, w, None -> @@ -79,17 +77,17 @@ let count_entry f c = function let f c = count_term f c w in Cps.list_fold_left f count_par c pars -let count_item f c = function +let count_entity 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 + let terms = c.tsorts + c.tlrefs + c.tgrefs + c.tappls + c.tabsts in let pars = c.pabsts + c.pappls in - let items = c.eabsts + c.eabbrs in + let entries = c.eabsts + c.eabbrs in let nodes = c.nodes + c.xnodes in L.warn (P.sprintf " Intermediate representation summary"); - L.warn (P.sprintf " Total entry items: %7u" items); + L.warn (P.sprintf " Total entries: %7u" entries); L.warn (P.sprintf " Declaration items: %7u" c.eabsts); L.warn (P.sprintf " Definition items: %7u" c.eabbrs); L.warn (P.sprintf " Total parameter items: %7u" pars); @@ -152,6 +150,6 @@ let pp_entry frm (l, pars, uri, u, body) = F.fprintf frm "@[%u@@%s%a%a:%a@]@\n%!" l (U.string_of_uri uri) pp_pars pars pp_body body pp_term u -let pp_item f frm = function +let pp_entity f frm = function | Some entry -> pp_entry frm entry; f () | None -> f ()