automath/autOutput.cmi: automath/aut.cmx
-automath/autOutput.cmo: cps/cps.cmx automath/aut.cmx automath/autOutput.cmi
-automath/autOutput.cmx: cps/cps.cmx automath/aut.cmx automath/autOutput.cmi
+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/autParser.cmi: automath/aut.cmx
automath/autParser.cmo: automath/aut.cmx automath/autParser.cmi
automath/autParser.cmx: automath/aut.cmx automath/autParser.cmi
toplevel/meta.cmo: automath/aut.cmx
toplevel/meta.cmx: automath/aut.cmx
toplevel/metaOutput.cmi: toplevel/meta.cmx
-toplevel/metaOutput.cmo: toplevel/meta.cmx cps/cps.cmx \
+toplevel/metaOutput.cmo: toplevel/meta.cmx lib/cps.cmx \
toplevel/metaOutput.cmi
-toplevel/metaOutput.cmx: toplevel/meta.cmx cps/cps.cmx \
+toplevel/metaOutput.cmx: toplevel/meta.cmx lib/cps.cmx \
toplevel/metaOutput.cmi
toplevel/metaAut.cmi: toplevel/meta.cmx automath/aut.cmx
-toplevel/metaAut.cmo: toplevel/meta.cmx cps/cps.cmx automath/aut.cmx \
+toplevel/metaAut.cmo: toplevel/meta.cmx lib/cps.cmx automath/aut.cmx \
toplevel/metaAut.cmi
-toplevel/metaAut.cmx: toplevel/meta.cmx cps/cps.cmx automath/aut.cmx \
+toplevel/metaAut.cmx: toplevel/meta.cmx lib/cps.cmx automath/aut.cmx \
toplevel/metaAut.cmi
-toplevel/top.cmo: toplevel/metaOutput.cmi toplevel/metaAut.cmi cps/cps.cmx \
- automath/autParser.cmi automath/autOutput.cmi automath/autLexer.cmx
-toplevel/top.cmx: toplevel/metaOutput.cmx toplevel/metaAut.cmx cps/cps.cmx \
- automath/autParser.cmx automath/autOutput.cmx automath/autLexer.cmx
+toplevel/top.cmo: lib/time.cmx toplevel/metaOutput.cmi toplevel/metaAut.cmi \
+ lib/cps.cmx automath/autParser.cmi automath/autOutput.cmi \
+ automath/autLexer.cmx
+toplevel/top.cmx: lib/time.cmx toplevel/metaOutput.cmx toplevel/metaAut.cmx \
+ lib/cps.cmx automath/autParser.cmx automath/autOutput.cmx \
+ automath/autLexer.cmx
MAIN = helena
-DIRECTORIES = cps automath toplevel
+DIRECTORIES = lib automath toplevel
-REQUIRES =
+REQUIRES = unix
KEEP = README automath/*.aut
test: opt
@echo " HELENA automath/*.aut"
- $(H)./$(MAIN).opt -S 2 automath/*.aut > log.txt
+ $(H)./$(MAIN).opt -S 3 automath/*.aut > log.txt
INCLUDES = $(DIRECTORIES:%=-I %)
OCAMLDEP = ocamlfind ocamldep -native $(INCLUDES)
-OCAMLOPT = ocamlfind opt -package "$(REQUIRES)" $(INCLUDES)
+OCAMLOPT = ocamlfind opt -linkpkg -package "$(REQUIRES)" $(INCLUDES)
OCAMLLEX = ocamllex
OCAMLYACC = ocamlyacc -v
TAR = tar -czf $(MAIN:%=%.tgz)
| Block of id * term (* block opener: name, type *)
| Decl of id * term (* declaration: name, type *)
| Def of id * term * bool * term (* definition: name, type, transparent?, body *)
-
-type book = item list (* book *)
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
val initial_counters: counters
-val count: (counters -> 'a) -> counters -> Aut.book -> 'a
+val count_item: (counters -> 'a) -> counters -> Aut.item -> 'a
val print_counters: (unit -> 'a) -> counters -> 'a
%token TYPE PROP DEF EB E PN EXIT
%start book
- %type <Aut.book> book
+ %type <Aut.item list> book
%%
path: MINUS {} | FS {} ;
oftype: CN {} | CM {} ;
+++ /dev/null
-(* 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/.
- *)
-
-let id _ = ()
-
-let rec list_sub_strict f l1 l2 = match l1, l2 with
- | _, [] -> f l1
- | _ :: tl1, _ :: tl2 -> list_sub_strict f tl1 tl2
- | _ -> assert false
-
-let rec list_fold_left f map a = function
- | [] -> f a
- | hd :: tl ->
- let f a = list_fold_left f map a tl in
- map f a hd
-
-let rec list_rev_map_append f map ~tail = function
- | [] -> f tail
- | hd :: tl ->
- let f hd = list_rev_map_append f map ~tail:(hd :: tail) tl in
- map f hd
-
-let list_rev_append f =
- list_rev_map_append f (fun f t -> f t)
-
-let list_rev_map =
- list_rev_map_append ~tail:[]
-
-let list_rev =
- list_rev_append ~tail:[]
-
-let list_map f =
- list_rev_map (list_rev f)
-
--- /dev/null
+(* 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/.
+ *)
+
+let id x = x
+
+let rec list_sub_strict f l1 l2 = match l1, l2 with
+ | _, [] -> f l1
+ | _ :: tl1, _ :: tl2 -> list_sub_strict f tl1 tl2
+ | _ -> assert false
+
+let rec list_fold_left f map a = function
+ | [] -> f a
+ | hd :: tl ->
+ let f a = list_fold_left f map a tl in
+ map f a hd
+
+let rec list_rev_map_append f map ~tail = function
+ | [] -> f tail
+ | hd :: tl ->
+ let f hd = list_rev_map_append f map ~tail:(hd :: tail) tl in
+ map f hd
+
+let list_rev_append f =
+ list_rev_map_append f (fun f t -> f t)
+
+let list_rev_map =
+ list_rev_map_append ~tail:[]
+
+let list_rev =
+ list_rev_append ~tail:[]
+
+let list_map f =
+ list_rev_map (list_rev f)
+
--- /dev/null
+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;
+ old := stamp
+
+let gmtime msg =
+ let gmt = Unix.gmtime (Unix.time ()) in
+ let yy = gmt.Unix.tm_year + 1900 in
+ let mm = gmt.Unix.tm_mon in
+ let dd = gmt.Unix.tm_mday in
+ 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
type pars = (qid * term) list (* parameter declarations: name, type *)
-(* environment: line number, parameters, name, type, (transparent?, body) *)
-type environment = (int * pars * qid * term * (bool * term) option) list
+(* entry: line number, parameters, name, type, (transparent?, body) *)
+type entry = int * pars * qid * term * (bool * term) option
+
+type item = entry option
type context_node = M.qid option (* context node: None = root *)
type status = {
- genv: M.environment; (* global environment *)
henv: environment; (* optimized global environment *)
path: M.id list; (* current section path *)
hcnt: environment; (* optimized context *)
let hsize = 11 (* hash tables initial size *)
+(* Internal functions *******************************************************)
+
let initial_status size = {
- genv = []; path = []; node = None; nodes = []; line = 1; explicit = true;
+ path = []; node = None; nodes = []; line = 1; explicit = true;
henv = H.create size; hcnt = H.create size
}
let xlate_item f st = function
| A.Section (Some name) ->
- f {st with path = name :: st.path; nodes = st.node :: st.nodes}
+ f {st with path = name :: st.path; nodes = st.node :: st.nodes} None
| A.Section None ->
begin match st.path, st.nodes with
| _ :: ptl, nhd :: ntl ->
- f {st with path = ptl; node = nhd; nodes = ntl}
+ f {st with path = ptl; node = nhd; nodes = ntl} None
| _ -> assert false
end
| A.Context None ->
- f {st with node = None}
+ f {st with node = None} None
| A.Context (Some name) ->
- let f name = f {st with node = Some name} in
- complete_qid f st name
+ let f name = f {st with node = Some name} None in
+ complete_qid f st name
| A.Block (name, w) ->
let f name =
let f pars =
let f ww =
H.add st.hcnt name ((name, ww) :: pars);
- f {st with node = Some name}
+ f {st with node = Some name} None
in
xlate_term f st pars w
in
let f ww =
let entry = (st.line, pars, name, ww, None) in
H.add st.henv name pars;
- f {st with genv = entry :: st.genv; line = succ st.line}
+ f {st with line = succ st.line} (Some entry)
in
xlate_term f st pars w
in
let f ww vv =
let entry = (st.line, pars, name, ww, Some (trans, vv)) in
H.add st.henv name pars;
- f {st with genv = entry :: st.genv; line = succ st.line}
+ f {st with line = succ st.line} (Some entry)
in
let f ww = xlate_term (f ww) st pars v in
xlate_term f st pars w
in
get_pars_relaxed f st
-let meta_of_aut f book =
- let f st = f st.genv in
- Cps.list_fold_left f xlate_item (initial_status hsize) book
+(* Interface functions ******************************************************)
+
+let initial_status = initial_status hsize
+
+let meta_of_aut = xlate_item
* http://cs.unibo.it/helm/.
*)
-val meta_of_aut: (Meta.environment -> 'a) -> Aut.book -> 'a
+type status
+
+val initial_status: status
+
+val meta_of_aut: (status -> Meta.item -> 'a) -> status -> Aut.item -> 'a
let count_par f c (_, w) = count_term f c w
-let count_item f c = function
+let count_entry f c = function
| _, pars, _, w, None ->
let c = {c with eabsts = succ c.eabsts} in
let c = {c with pabsts = c.pabsts + List.length pars} in
let f c = count_term f c w in
Cps.list_fold_left f count_par c pars
-let count f c b =
- Cps.list_fold_left f count_item c b
+let count_item 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
| Some (trans, t) ->
F.fprintf frm "%s%a" (string_of_transparent trans) pp_term t
-let pp_item frm (l, pars, qid, u, body) =
+let pp_entry frm (l, pars, qid, u, body) =
F.fprintf frm "@[%u@@%s%a%a:%a@]@\n%!"
l (string_of_qid qid) pp_pars pars pp_body body pp_term u
-let pp_environment f frm genv =
- List.iter (pp_item frm) genv; f ()
+let pp_item f frm = function
+ | Some entry -> pp_entry frm entry; f ()
+ | None -> f ()
val initial_counters: counters
-val count: (counters -> 'a) -> counters -> Meta.environment -> 'a
+val count_item: (counters -> 'a) -> counters -> Meta.item -> 'a
val print_counters: (unit -> 'a) -> counters -> 'a
-val pp_environment: (unit -> 'a) -> Format.formatter -> Meta.environment -> 'a
+val pp_item: (unit -> 'a) -> Format.formatter -> Meta.item -> 'a
module MO = MetaOutput
let main =
- let version_string = "Helena Checker 0.8.0 M (June 2008)" in
+ let version_string = "Helena Checker 0.8.0 M - November 2008" in
let summary = ref 0 in
let stage = ref 1 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 set_stage i = stage := i in
+ let close = function
+ | None -> ()
+ | Some (och, _) -> close_out och
+ in
+ let set_meta_file name =
+ close !meta_file;
+ let och = open_out name in
+ let frm = Format.formatter_of_out_channel och in
+ Format.pp_set_margin frm max_int;
+ meta_file := Some (och, frm)
+ in
let read_file name =
- if !summary > 0 then
+ if !summary > 0 then Time.gmtime version_string;
+ if !summary > 1 then
Printf.printf "Processing file: %s\n" name; flush stdout;
+ if !summary > 0 then Time.utime_stamp "started";
let ich = open_in name in
let lexbuf = Lexing.from_channel ich in
let book = AutParser.book AutLexer.token lexbuf in
close_in ich;
- if !summary > 1 then
- AO.count (AO.print_counters Cps.id) AO.initial_counters book;
- let f env =
- if !summary > 1 then
- MO.count (MO.print_counters Cps.id) MO.initial_counters env;
- let frm = Format.err_formatter in
- Format.pp_set_margin frm max_int;
- MO.pp_environment Cps.id frm (List.rev env)
+ if !summary > 0 then Time.utime_stamp "parsed";
+ let rec aux ac mc st = function
+ | [] -> ac, mc, st
+ | item :: tl ->
+ let ac = if !summary > 2 then AO.count_item Cps.id ac item else ac in
+ let f st item =
+ let mc = if !summary > 2 then MO.count_item Cps.id mc item else mc in
+ begin match !meta_file with
+ | None -> ()
+ | Some (_, frm) -> MO.pp_item Cps.id frm item
+ end;
+ st, mc
+ in
+ let st, mc = if !stage > 0 then MA.meta_of_aut f st item else st, mc in
+ aux ac mc st tl
+ in
+ let ac, mc, _st =
+ aux AO.initial_counters MO.initial_counters MA.initial_status book
in
- if !stage > 0 then MA.meta_of_aut f book
+ if !summary > 0 then Time.utime_stamp "processed";
+ if !summary > 2 then AO.print_counters Cps.id ac;
+ if !summary > 2 && !stage > 0 then MO.print_counters Cps.id mc;
in
- let help = "Usage: helena [ -V | -Ss <number> ] <file> ..." in
+ let help = "Usage: helena [ -V | -Ss <number> | -m <file> ] <file> ..." in
let help_S = "<number> Set summary level" in
let help_V = " Show version information" in
+ let help_m = "<file> output intermediate representation" in
let help_s = "<number> Set translation stage" in
Arg.parse [
("-S", Arg.Int set_summary, help_S);
("-V", Arg.Unit print_version, help_V);
+ ("-m", Arg.String set_meta_file, help_m);
("-s", Arg.Int set_stage, help_s);
- ] read_file help
+ ] read_file help;
+ if !summary > 0 then Time.utime_stamp "at exit"
projects / helm.git / commitdiff