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
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
include Makefile.common
-test: opt
+test: $(MAIN).opt
@echo " HELENA automath/*.aut"
$(H)./$(MAIN).opt -S 3 automath/*.aut > log.txt
-(* 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 = ['#' '%']
-(* 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 = {
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 ()
-brg brgOutput
+brg brgOutput brgEnvironment
| 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 *)
--- /dev/null
+(*
+ ||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)))
--- /dev/null
+(*
+ ||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
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
+module P = Printf
+module L = Log
module B = Brg
type counters = {
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 =
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 ()
-nUri cps time
+nUri cps log time
--- /dev/null
+(*
+ ||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
--- /dev/null
+(*
+ ||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
+(*
+ ||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 =
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
+ )
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 *******************************************************)
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
\ / 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 = {
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"
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
+module P = Printf
+module L = Log
module AO = AutOutput
module MA = MetaAut
module MO = MetaOutput
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 -> ()
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
projects / helm.git / commitdiff