From: Ferruccio Guidi Date: Wed, 3 Dec 2008 17:37:43 +0000 (+0000) Subject: log facility, initial environment for basic_rg X-Git-Tag: make_still_working~4463 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c45c77de154323feaf5bf6aee98c86b95361b9ae;p=helm.git log facility, initial environment for basic_rg --- diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt index a1019d0de..bfe5ffb87 100644 --- a/helm/software/lambda-delta/.depend.opt +++ b/helm/software/lambda-delta/.depend.opt @@ -1,25 +1,36 @@ lib/nUri.cmo: lib/nUri.cmi lib/nUri.cmx: lib/nUri.cmi +lib/log.cmo: lib/log.cmi +lib/log.cmx: lib/log.cmi +lib/time.cmo: lib/log.cmi +lib/time.cmx: lib/log.cmx automath/autOutput.cmi: automath/aut.cmx -automath/autOutput.cmo: lib/cps.cmx automath/aut.cmx automath/autOutput.cmi -automath/autOutput.cmx: lib/cps.cmx automath/aut.cmx automath/autOutput.cmi +automath/autOutput.cmo: lib/log.cmi lib/cps.cmx automath/aut.cmx \ + automath/autOutput.cmi +automath/autOutput.cmx: lib/log.cmx lib/cps.cmx automath/aut.cmx \ + automath/autOutput.cmi automath/autParser.cmi: automath/aut.cmx automath/autParser.cmo: automath/aut.cmx automath/autParser.cmi automath/autParser.cmx: automath/aut.cmx automath/autParser.cmi -automath/autLexer.cmo: automath/autParser.cmi -automath/autLexer.cmx: automath/autParser.cmx +automath/autLexer.cmo: lib/log.cmi automath/autParser.cmi +automath/autLexer.cmx: lib/log.cmx automath/autParser.cmx basic_rg/brg.cmo: lib/nUri.cmi automath/aut.cmx basic_rg/brg.cmx: lib/nUri.cmx automath/aut.cmx basic_rg/brgOutput.cmi: basic_rg/brg.cmx -basic_rg/brgOutput.cmo: basic_rg/brg.cmx basic_rg/brgOutput.cmi -basic_rg/brgOutput.cmx: basic_rg/brg.cmx basic_rg/brgOutput.cmi +basic_rg/brgOutput.cmo: lib/log.cmi basic_rg/brg.cmx basic_rg/brgOutput.cmi +basic_rg/brgOutput.cmx: lib/log.cmx basic_rg/brg.cmx basic_rg/brgOutput.cmi +basic_rg/brgEnvironment.cmi: lib/nUri.cmi basic_rg/brg.cmx +basic_rg/brgEnvironment.cmo: lib/nUri.cmi basic_rg/brg.cmx \ + basic_rg/brgEnvironment.cmi +basic_rg/brgEnvironment.cmx: lib/nUri.cmx basic_rg/brg.cmx \ + basic_rg/brgEnvironment.cmi toplevel/meta.cmo: lib/nUri.cmi automath/aut.cmx toplevel/meta.cmx: lib/nUri.cmx automath/aut.cmx toplevel/metaOutput.cmi: toplevel/meta.cmx -toplevel/metaOutput.cmo: lib/nUri.cmi toplevel/meta.cmx lib/cps.cmx \ - toplevel/metaOutput.cmi -toplevel/metaOutput.cmx: lib/nUri.cmx toplevel/meta.cmx lib/cps.cmx \ - toplevel/metaOutput.cmi +toplevel/metaOutput.cmo: lib/nUri.cmi toplevel/meta.cmx lib/log.cmi \ + lib/cps.cmx toplevel/metaOutput.cmi +toplevel/metaOutput.cmx: lib/nUri.cmx toplevel/meta.cmx lib/log.cmx \ + lib/cps.cmx toplevel/metaOutput.cmi toplevel/metaAut.cmi: toplevel/meta.cmx automath/aut.cmx toplevel/metaAut.cmo: lib/nUri.cmi toplevel/meta.cmx lib/cps.cmx \ automath/aut.cmx toplevel/metaAut.cmi @@ -31,8 +42,8 @@ toplevel/metaBrg.cmo: toplevel/meta.cmx lib/cps.cmx basic_rg/brg.cmx \ toplevel/metaBrg.cmx: toplevel/meta.cmx lib/cps.cmx basic_rg/brg.cmx \ toplevel/metaBrg.cmi toplevel/top.cmo: lib/time.cmx toplevel/metaOutput.cmi toplevel/metaBrg.cmi \ - toplevel/metaAut.cmi lib/cps.cmx basic_rg/brgOutput.cmi \ + toplevel/metaAut.cmi lib/log.cmi lib/cps.cmx basic_rg/brgOutput.cmi \ automath/autParser.cmi automath/autOutput.cmi automath/autLexer.cmx toplevel/top.cmx: lib/time.cmx toplevel/metaOutput.cmx toplevel/metaBrg.cmx \ - toplevel/metaAut.cmx lib/cps.cmx basic_rg/brgOutput.cmx \ + toplevel/metaAut.cmx lib/log.cmx lib/cps.cmx basic_rg/brgOutput.cmx \ automath/autParser.cmx automath/autOutput.cmx automath/autLexer.cmx diff --git a/helm/software/lambda-delta/Makefile b/helm/software/lambda-delta/Makefile index e7aa0ae76..2b218865e 100644 --- a/helm/software/lambda-delta/Makefile +++ b/helm/software/lambda-delta/Makefile @@ -10,6 +10,6 @@ CLEAN = log.txt include Makefile.common -test: opt +test: $(MAIN).opt @echo " HELENA automath/*.aut" $(H)./$(MAIN).opt -S 3 automath/*.aut > log.txt diff --git a/helm/software/lambda-delta/automath/autLexer.mll b/helm/software/lambda-delta/automath/autLexer.mll index f0ae1ae92..fa385bca4 100644 --- a/helm/software/lambda-delta/automath/autLexer.mll +++ b/helm/software/lambda-delta/automath/autLexer.mll @@ -1,33 +1,20 @@ -(* 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 L = Log module P = AutParser let debug = false - let out s = if debug then print_endline s else () + let out s = if debug then L.warn s else () } let LC = ['#' '%'] diff --git a/helm/software/lambda-delta/automath/autOutput.ml b/helm/software/lambda-delta/automath/autOutput.ml index 4ccb74b5c..3bda05f9e 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 = { @@ -78,18 +66,18 @@ let count_item f c = function 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: %6u" items); + L.warn (P.sprintf " Section items: %6u" c.sections); + L.warn (P.sprintf " Context items: %6u" c.contexts); + L.warn (P.sprintf " Block items: %6u" c.blocks); + L.warn (P.sprintf " Declaration items: %6u" c.decls); + L.warn (P.sprintf " Definition items: %6u" c.defs); + L.warn (P.sprintf " Total Parameter items: %6u" c.pars); + L.warn (P.sprintf " Application items: %6u" c.pars); + L.warn (P.sprintf " Total term items: %6u" terms); + L.warn (P.sprintf " Sort items: %6u" c.sorts); + L.warn (P.sprintf " Reference items: %6u" c.grefs); + L.warn (P.sprintf " Application items: %6u" c.appls); + L.warn (P.sprintf " Abstraction items: %6u" c.absts); + f () diff --git a/helm/software/lambda-delta/basic_rg/Make b/helm/software/lambda-delta/basic_rg/Make index bb05d5bb7..783502bdc 100644 --- a/helm/software/lambda-delta/basic_rg/Make +++ b/helm/software/lambda-delta/basic_rg/Make @@ -1 +1 @@ -brg brgOutput +brg brgOutput brgEnvironment diff --git a/helm/software/lambda-delta/basic_rg/brg.ml b/helm/software/lambda-delta/basic_rg/brg.ml index 09d2f247a..eaaeb6e60 100644 --- a/helm/software/lambda-delta/basic_rg/brg.ml +++ b/helm/software/lambda-delta/basic_rg/brg.ml @@ -21,6 +21,6 @@ type term = Sort of int (* hierarchy index *) | Appl of term * term (* argument, function *) | Bind of id * bind * term * term (* name, binder, content, scope *) -type entry = uri * bind * term (* uri, binder, contents *) +type obj = bind * term (* binder, contents *) -type item = entry option +type item = (obj * uri) option (* uri, object *) diff --git a/helm/software/lambda-delta/basic_rg/brgEnvironment.ml b/helm/software/lambda-delta/basic_rg/brgEnvironment.ml new file mode 100644 index 000000000..f1561516d --- /dev/null +++ b/helm/software/lambda-delta/basic_rg/brgEnvironment.ml @@ -0,0 +1,30 @@ +(* + ||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 U = NUri +module H = U.UriHash +module B = Brg + +exception ObjectNotFound of string Lazy.t + +let hsize = 7000 +let env = H.create hsize + +(* Internal functions *******************************************************) + +(* Interface functions ******************************************************) + +let set_obj f obj uri = + H.add env uri obj; f obj uri + +let get_obj f uri = + try f (H.find env uri) uri + with Not_found -> raise (ObjectNotFound (lazy (U.string_of_uri uri))) diff --git a/helm/software/lambda-delta/basic_rg/brgEnvironment.mli b/helm/software/lambda-delta/basic_rg/brgEnvironment.mli new file mode 100644 index 000000000..a6fec6db0 --- /dev/null +++ b/helm/software/lambda-delta/basic_rg/brgEnvironment.mli @@ -0,0 +1,16 @@ +(* + ||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_______________________________________________________________ *) + +exception ObjectNotFound of string Lazy.t + +val set_obj: (Brg.obj -> NUri.uri -> 'a) -> Brg.obj -> NUri.uri -> 'a + +val get_obj: (Brg.obj -> NUri.uri -> 'a) -> NUri.uri -> 'a diff --git a/helm/software/lambda-delta/basic_rg/brgOutput.ml b/helm/software/lambda-delta/basic_rg/brgOutput.ml index 741a2567d..dcefefa2e 100644 --- a/helm/software/lambda-delta/basic_rg/brgOutput.ml +++ b/helm/software/lambda-delta/basic_rg/brgOutput.ml @@ -9,6 +9,8 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) +module P = Printf +module L = Log module B = Brg type counters = { @@ -52,17 +54,17 @@ let rec count_term f c = function let f c = count_term f c t in count_term f c u -let count_entry_binder f c = function +let count_obj_binder f c = function | B.Abst -> f {c with eabsts = succ c.eabsts} | B.Abbr -> f {c with eabbrs = succ c.eabbrs} -let count_entry f c (_, b, t) = - let f c = count_entry_binder f c b in +let count_obj f c (b, t) = + let f c = count_obj_binder f c b in count_term f c t let count_item f c = function - | Some e -> count_entry f c e - | None -> f c + | Some (obj, _) -> count_obj f c obj + | None -> f c let print_counters f c = let terms = @@ -70,16 +72,16 @@ let print_counters f c = c.tabbrs in let items = c.eabsts + c.eabbrs in - Printf.printf " Kernel representation summary (basic_rg)\n"; - Printf.printf " Total entry items: %6u\n" items; - Printf.printf " Declaration items: %6u\n" c.eabsts; - Printf.printf " Definition items: %6u\n" c.eabbrs; - Printf.printf " Total term items: %6u\n" terms; - Printf.printf " Sort items: %6u\n" c.tsorts; - Printf.printf " Local reference items: %6u\n" c.tlrefs; - Printf.printf " Global reference items: %6u\n" c.tgrefs; - Printf.printf " Explicit Cast items: %6u\n" c.tcasts; - Printf.printf " Application items: %6u\n" c.tappls; - Printf.printf " Abstraction items: %6u\n" c.tabsts; - Printf.printf " Abbreviation items: %6u\n" c.tabbrs; - flush stdout; f () + L.warn (P.sprintf " Kernel representation summary (basic_rg)"); + L.warn (P.sprintf " Total entry items: %6u" items); + L.warn (P.sprintf " Declaration items: %6u" c.eabsts); + L.warn (P.sprintf " Definition items: %6u" c.eabbrs); + L.warn (P.sprintf " Total term items: %6u" terms); + L.warn (P.sprintf " Sort items: %6u" c.tsorts); + L.warn (P.sprintf " Local reference items: %6u" c.tlrefs); + L.warn (P.sprintf " Global reference items: %6u" c.tgrefs); + L.warn (P.sprintf " Explicit Cast items: %6u" c.tcasts); + L.warn (P.sprintf " Application items: %6u" c.tappls); + L.warn (P.sprintf " Abstraction items: %6u" c.tabsts); + L.warn (P.sprintf " Abbreviation items: %6u" c.tabbrs); + f () diff --git a/helm/software/lambda-delta/lib/Make b/helm/software/lambda-delta/lib/Make index 0d6e02e12..9a90150e8 100644 --- a/helm/software/lambda-delta/lib/Make +++ b/helm/software/lambda-delta/lib/Make @@ -1 +1 @@ -nUri cps time +nUri cps log time diff --git a/helm/software/lambda-delta/lib/log.ml b/helm/software/lambda-delta/lib/log.ml new file mode 100644 index 000000000..667fef534 --- /dev/null +++ b/helm/software/lambda-delta/lib/log.ml @@ -0,0 +1,21 @@ +(* + ||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 + +let init = + let started = ref false in + fun () -> + if !started then () else + begin P.printf "\n"; started := true end + +let warn msg = + init (); P.printf " %s\n" msg; flush stdout diff --git a/helm/software/lambda-delta/lib/log.mli b/helm/software/lambda-delta/lib/log.mli new file mode 100644 index 000000000..e32f6e0fd --- /dev/null +++ b/helm/software/lambda-delta/lib/log.mli @@ -0,0 +1,12 @@ +(* + ||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_______________________________________________________________ *) + +val warn: string -> unit diff --git a/helm/software/lambda-delta/lib/time.ml b/helm/software/lambda-delta/lib/time.ml index 2ea295a85..f139fdfbe 100644 --- a/helm/software/lambda-delta/lib/time.ml +++ b/helm/software/lambda-delta/lib/time.ml @@ -1,10 +1,24 @@ +(* + ||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 + let utime_stamp = let old = ref 0.0 in fun msg -> let times = Unix.times () in let stamp = times.Unix.tms_utime in let lap = stamp -. !old in - Printf.printf "UTIME STAMP (%s): %f (%f)\n" msg stamp lap; flush stdout; + L.warn (P.sprintf "UTIME STAMP (%s): %f (%f)" msg stamp lap); old := stamp let gmtime msg = @@ -15,6 +29,6 @@ let gmtime msg = let h = gmt.Unix.tm_hour in let m = gmt.Unix.tm_min in let s = gmt.Unix.tm_sec in - Printf.printf "UTC TIME STAMP (%s): %u/%u/%u %u:%u:%u\n" - msg yy mm dd h m s; - flush stdout + L.warn ( + P.sprintf "UTC TIME STAMP (%s): %u/%u/%u %u:%u:%u" msg yy mm dd h m s + ) diff --git a/helm/software/lambda-delta/toplevel/metaAut.ml b/helm/software/lambda-delta/toplevel/metaAut.ml index 71759f79a..59801dac7 100644 --- a/helm/software/lambda-delta/toplevel/metaAut.ml +++ b/helm/software/lambda-delta/toplevel/metaAut.ml @@ -33,7 +33,7 @@ type status = { type resolver = Local of int | Global of M.pars -let hsize = 11 (* hash tables initial size *) +let hsize = 7000 (* hash tables initial size *) (* Internal functions *******************************************************) diff --git a/helm/software/lambda-delta/toplevel/metaBrg.ml b/helm/software/lambda-delta/toplevel/metaBrg.ml index 4ca8e5c22..7c7adce7e 100644 --- a/helm/software/lambda-delta/toplevel/metaBrg.ml +++ b/helm/software/lambda-delta/toplevel/metaBrg.ml @@ -46,11 +46,11 @@ let xlate_pars f (id, w) = let xlate_entry f = function | _, pars, uri, u, None -> - let f u = f (uri, B.Abst, u) in + let f u = f ((B.Abst, u), uri) in let f pars = map_fold_left f xlate_term map_pars u pars in Cps.list_rev_map f xlate_pars pars | _, pars, uri, u, Some (_, t) -> - let f u t = f (uri, B.Abbr, (B.Cast (u, t))) in + let f u t = f ((B.Abbr, (B.Cast (u, t))), uri) in let f pars u = map_fold_left (f u) xlate_term map_pars t pars in let f pars = map_fold_left (f pars) xlate_term map_pars u pars in Cps.list_rev_map f xlate_pars pars diff --git a/helm/software/lambda-delta/toplevel/metaOutput.ml b/helm/software/lambda-delta/toplevel/metaOutput.ml index 04e15e4db..2d5bc3ad5 100644 --- a/helm/software/lambda-delta/toplevel/metaOutput.ml +++ b/helm/software/lambda-delta/toplevel/metaOutput.ml @@ -9,8 +9,10 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) +module P = Printf module F = Format module U = NUri +module L = Log module M = Meta type counters = { @@ -71,20 +73,20 @@ let print_counters f c = let terms = c.tsorts + c.tgrefs + c.tgrefs + c.tappls + c.tabsts in let pars = c.pabsts + c.pappls in let items = c.eabsts + c.eabbrs in - Printf.printf " Intermediate representation summary\n"; - Printf.printf " Total entry items: %6u\n" items; - Printf.printf " Declaration items: %6u\n" c.eabsts; - Printf.printf " Definition items: %6u\n" c.eabbrs; - Printf.printf " Total parameter items: %6u\n" pars; - Printf.printf " Application items: %6u\n" c.pappls; - Printf.printf " Abstraction items: %6u\n" c.pabsts; - Printf.printf " Total term items: %6u\n" terms; - Printf.printf " Sort items: %6u\n" c.tsorts; - Printf.printf " Local reference items: %6u\n" c.tlrefs; - Printf.printf " Global reference items: %6u\n" c.tgrefs; - Printf.printf " Application items: %6u\n" c.tappls; - Printf.printf " Abstraction items: %6u\n" c.tabsts; - flush stdout; f () + L.warn (P.sprintf " Intermediate representation summary"); + L.warn (P.sprintf " Total entry items: %6u" items); + L.warn (P.sprintf " Declaration items: %6u" c.eabsts); + L.warn (P.sprintf " Definition items: %6u" c.eabbrs); + L.warn (P.sprintf " Total parameter items: %6u" pars); + L.warn (P.sprintf " Application items: %6u" c.pappls); + L.warn (P.sprintf " Abstraction items: %6u" c.pabsts); + L.warn (P.sprintf " Total term items: %6u" terms); + L.warn (P.sprintf " Sort items: %6u" c.tsorts); + L.warn (P.sprintf " Local reference items: %6u" c.tlrefs); + L.warn (P.sprintf " Global reference items: %6u" c.tgrefs); + L.warn (P.sprintf " Application items: %6u" c.tappls); + L.warn (P.sprintf " Abstraction items: %6u" c.tabsts); + f () let string_of_sort = function | true -> "Type" diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml index 27f40026e..1442d7521 100644 --- a/helm/software/lambda-delta/toplevel/top.ml +++ b/helm/software/lambda-delta/toplevel/top.ml @@ -9,6 +9,8 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) +module P = Printf +module L = Log module AO = AutOutput module MA = MetaAut module MO = MetaOutput @@ -40,7 +42,7 @@ let main = let stage = ref 2 in let meta_file = ref None in let set_summary i = summary := i in - let print_version () = print_endline version_string; exit 0 in + let print_version () = L.warn version_string; exit 0 in let set_stage i = stage := i in let close = function | None -> () @@ -56,7 +58,7 @@ let main = let read_file name = if !summary > 0 then Time.gmtime version_string; if !summary > 1 then - Printf.printf "Processing file: %s\n" name; flush stdout; + L.warn (P.sprintf "Processing file: %s" name); if !summary > 0 then Time.utime_stamp "started"; let ich = open_in name in let lexbuf = Lexing.from_channel ich in