X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fautomath%2FautOutput.ml;h=668de746284d75241dc97711b4c76b487a2c6cd0;hb=e22808c929a9cebf5e4e2b7428ff0cbf89e1f92a;hp=1acb075b2b99ae3cf9b25784140d3c64cc68ecee;hpb=b00b8de85c5ae6c5fbb6f47dc559bf4cfcf2a5b6;p=helm.git diff --git a/helm/software/lambda-delta/automath/autOutput.ml b/helm/software/lambda-delta/automath/autOutput.ml index 1acb075b2..668de7462 100644 --- a/helm/software/lambda-delta/automath/autOutput.ml +++ b/helm/software/lambda-delta/automath/autOutput.ml @@ -1,29 +1,19 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM 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. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) +module P = Printf +module C = Cps +module L = Log module A = Aut +module R = AutProcess type counters = { sections: int; @@ -35,64 +25,76 @@ type counters = { grefs: int; appls: int; absts: int; - pars: int + pars: int; + xnodes: int } let initial_counters = { sections = 0; contexts = 0; blocks = 0; decls = 0; defs = 0; - sorts = 0; grefs = 0; appls = 0; absts = 0; pars = 0 + sorts = 0; grefs = 0; appls = 0; absts = 0; pars = 0; xnodes = 0 } let rec count_term f c = function | A.Sort _ -> - f {c with sorts = succ c.sorts} + f {c with sorts = succ c.sorts; xnodes = succ c.xnodes} | A.GRef (_, ts) -> let c = {c with grefs = succ c.grefs} in let c = {c with pars = c.pars + List.length ts} in - Cps.list_fold_left f count_term c ts + let c = {c with xnodes = succ c.xnodes + List.length ts} in + C.list_fold_left f count_term c ts | A.Appl (v, t) -> - let c = {c with appls = succ c.appls} in + let c = {c with appls = succ c.appls; xnodes = succ c.xnodes} in let f c = count_term f c t in count_term f c v | A.Abst (_, w, t) -> - let c = {c with absts = succ c.absts} in + let c = {c with absts = succ c.absts; xnodes = succ c.xnodes} in let f c = count_term f c t in count_term f c w -let count_item f c = function +let count_entity f c = function | A.Section _ -> f {c with sections = succ c.sections} | A.Context _ -> f {c with contexts = succ c.contexts} | A.Block (_, w) -> - let c = {c with blocks = succ c.blocks} in + let c = {c with blocks = succ c.blocks; xnodes = succ c.xnodes} in count_term f c w | A.Decl (_, w) -> - let c = {c with decls = succ c.decls} in + let c = {c with decls = succ c.decls; xnodes = succ c.xnodes} in count_term f c w | A.Def (_, w, _, t) -> - let c = {c with defs = succ c.defs} in + let c = {c with defs = succ c.defs; xnodes = succ c.xnodes} in let f c = count_term f c t in count_term f c w -let count f c b = - Cps.list_fold_left f count_item c b - let print_counters f c = let terms = c.sorts + c.grefs + c.appls + c.absts in - let items = c.sections + c.contexts + c.blocks + c.decls + c.defs in - Printf.printf " Automath representation summary\n"; - Printf.printf " Total book items: %6u\n" items; - Printf.printf " Section items: %6u\n" c.sections; - Printf.printf " Context items: %6u\n" c.contexts; - Printf.printf " Block items: %6u\n" c.blocks; - Printf.printf " Declaration items: %6u\n" c.decls; - Printf.printf " Definition items: %6u\n" c.defs; - Printf.printf " Total Parameter items: %6u\n" c.pars; - Printf.printf " Application items: %6u\n" c.pars; - Printf.printf " Total term items: %6u\n" terms; - Printf.printf " Sort items: %6u\n" c.sorts; - Printf.printf " Reference items: %6u\n" c.grefs; - Printf.printf " Application items: %6u\n" c.appls; - Printf.printf " Abstraction items: %6u\n" c.absts; - flush stdout; f () + let entities = c.sections + c.contexts + c.blocks + c.decls + c.defs in + L.warn (P.sprintf " Automath representation summary"); + L.warn (P.sprintf " Total book entities: %7u" entities); + L.warn (P.sprintf " Section entities: %7u" c.sections); + L.warn (P.sprintf " Context entities: %7u" c.contexts); + L.warn (P.sprintf " Block entities: %7u" c.blocks); + L.warn (P.sprintf " Declaration entities: %7u" c.decls); + L.warn (P.sprintf " Definition entities: %7u" c.defs); + L.warn (P.sprintf " Total Parameter items: %7u" c.pars); + L.warn (P.sprintf " Application items: %7u" c.pars); + L.warn (P.sprintf " Total term items: %7u" terms); + L.warn (P.sprintf " Sort items: %7u" c.sorts); + L.warn (P.sprintf " Reference items: %7u" c.grefs); + L.warn (P.sprintf " Application items: %7u" c.appls); + L.warn (P.sprintf " Abstraction items: %7u" c.absts); + L.warn (P.sprintf " Global Int. Complexity: unknown"); + L.warn (P.sprintf " + Abbreviation nodes: %7u" c.xnodes); + f () + +let print_process_counters f c = + let f iao iar iac iag = + L.warn (P.sprintf " Automath process summary"); + L.warn (P.sprintf " Implicit after opening: %7u" iao); + L.warn (P.sprintf " Implicit after reopening: %7u" iar); + L.warn (P.sprintf " Implicit after closing: %7u" iac); + L.warn (P.sprintf " Implicit after global: %7u" iag); + f () + in + R.get_counters f c