X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fautomath%2FautOutput.ml;h=ffbdfdb2096eeac175e3e86ee1af854c60fe100a;hb=a872dba2b03e27967d5b9b51e950e85967340e52;hp=4ccb74b5c3650531e906c6cfbe4b69d8d5373e8d;hpb=973b0b1fd5f44b96a3c367a9756f28b75b9fa30b;p=helm.git diff --git a/helm/software/lambda-delta/automath/autOutput.ml b/helm/software/lambda-delta/automath/autOutput.ml index 4ccb74b5c..ffbdfdb20 100644 --- a/helm/software/lambda-delta/automath/autOutput.ml +++ b/helm/software/lambda-delta/automath/autOutput.ml @@ -1,28 +1,16 @@ -(* 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 L = Log module A = Aut type counters = { @@ -35,27 +23,29 @@ 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 + let c = {c with xnodes = succ c.xnodes + List.length ts} in Cps.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 @@ -65,31 +55,33 @@ let count_item f c = function | 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 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 () + L.warn (P.sprintf " Automath representation summary"); + L.warn (P.sprintf " Total book items: %7u" items); + L.warn (P.sprintf " Section items: %7u" c.sections); + L.warn (P.sprintf " Context items: %7u" c.contexts); + L.warn (P.sprintf " Block items: %7u" c.blocks); + L.warn (P.sprintf " Declaration items: %7u" c.decls); + L.warn (P.sprintf " Definition items: %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 ()