From: Ferruccio Guidi Date: Tue, 11 Nov 2008 17:05:12 +0000 (+0000) Subject: - we now use a streaming architecture (run time gain: 11 secs) X-Git-Tag: make_still_working~4575 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=973b0b1fd5f44b96a3c367a9756f28b75b9fa30b;p=helm.git - we now use a streaming architecture (run time gain: 11 secs) - we added some time stamp support --- diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt index 144dab5e6..f5f529ef7 100644 --- a/helm/software/lambda-delta/.depend.opt +++ b/helm/software/lambda-delta/.depend.opt @@ -1,6 +1,6 @@ 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 @@ -9,16 +9,18 @@ automath/autLexer.cmx: automath/autParser.cmx 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 diff --git a/helm/software/lambda-delta/Makefile b/helm/software/lambda-delta/Makefile index e62fb5dfc..50f1a83b6 100644 --- a/helm/software/lambda-delta/Makefile +++ b/helm/software/lambda-delta/Makefile @@ -1,8 +1,8 @@ MAIN = helena -DIRECTORIES = cps automath toplevel +DIRECTORIES = lib automath toplevel -REQUIRES = +REQUIRES = unix KEEP = README automath/*.aut @@ -12,4 +12,4 @@ include Makefile.common test: opt @echo " HELENA automath/*.aut" - $(H)./$(MAIN).opt -S 2 automath/*.aut > log.txt + $(H)./$(MAIN).opt -S 3 automath/*.aut > log.txt diff --git a/helm/software/lambda-delta/Makefile.common b/helm/software/lambda-delta/Makefile.common index b6e08f89e..0adedde84 100644 --- a/helm/software/lambda-delta/Makefile.common +++ b/helm/software/lambda-delta/Makefile.common @@ -3,7 +3,7 @@ H=@ 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) diff --git a/helm/software/lambda-delta/automath/aut.ml b/helm/software/lambda-delta/automath/aut.ml index c95d20a7e..66c252d5e 100644 --- a/helm/software/lambda-delta/automath/aut.ml +++ b/helm/software/lambda-delta/automath/aut.ml @@ -37,5 +37,3 @@ type item = Section of id option (* section: Some = open/reopen, None | 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 *) diff --git a/helm/software/lambda-delta/automath/autOutput.ml b/helm/software/lambda-delta/automath/autOutput.ml index 1acb075b2..4ccb74b5c 100644 --- a/helm/software/lambda-delta/automath/autOutput.ml +++ b/helm/software/lambda-delta/automath/autOutput.ml @@ -75,9 +75,6 @@ let count_item f c = function 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 diff --git a/helm/software/lambda-delta/automath/autOutput.mli b/helm/software/lambda-delta/automath/autOutput.mli index 6ff94387b..a73697418 100644 --- a/helm/software/lambda-delta/automath/autOutput.mli +++ b/helm/software/lambda-delta/automath/autOutput.mli @@ -27,6 +27,6 @@ type counters 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 diff --git a/helm/software/lambda-delta/automath/autParser.mly b/helm/software/lambda-delta/automath/autParser.mly index 2f7c06349..3bf5f3d00 100644 --- a/helm/software/lambda-delta/automath/autParser.mly +++ b/helm/software/lambda-delta/automath/autParser.mly @@ -32,7 +32,7 @@ %token TYPE PROP DEF EB E PN EXIT %start book - %type book + %type book %% path: MINUS {} | FS {} ; oftype: CN {} | CM {} ; diff --git a/helm/software/lambda-delta/cps/Make b/helm/software/lambda-delta/cps/Make deleted file mode 100644 index 0e120998d..000000000 --- a/helm/software/lambda-delta/cps/Make +++ /dev/null @@ -1 +0,0 @@ -cps diff --git a/helm/software/lambda-delta/cps/cps.ml b/helm/software/lambda-delta/cps/cps.ml deleted file mode 100644 index 83570aa2e..000000000 --- a/helm/software/lambda-delta/cps/cps.ml +++ /dev/null @@ -1,56 +0,0 @@ -(* 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) - diff --git a/helm/software/lambda-delta/lib/Make b/helm/software/lambda-delta/lib/Make new file mode 100644 index 000000000..60114a82c --- /dev/null +++ b/helm/software/lambda-delta/lib/Make @@ -0,0 +1 @@ +cps time diff --git a/helm/software/lambda-delta/lib/cps.ml b/helm/software/lambda-delta/lib/cps.ml new file mode 100644 index 000000000..199a786cd --- /dev/null +++ b/helm/software/lambda-delta/lib/cps.ml @@ -0,0 +1,56 @@ +(* 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) + diff --git a/helm/software/lambda-delta/lib/time.ml b/helm/software/lambda-delta/lib/time.ml new file mode 100644 index 000000000..2ea295a85 --- /dev/null +++ b/helm/software/lambda-delta/lib/time.ml @@ -0,0 +1,20 @@ +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 diff --git a/helm/software/lambda-delta/toplevel/meta.ml b/helm/software/lambda-delta/toplevel/meta.ml index 23f8f52f5..4b04e3af8 100644 --- a/helm/software/lambda-delta/toplevel/meta.ml +++ b/helm/software/lambda-delta/toplevel/meta.ml @@ -35,5 +35,7 @@ type term = Sort of bool (* sorts: true = TYPE, false = PROP *) 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 diff --git a/helm/software/lambda-delta/toplevel/metaAut.ml b/helm/software/lambda-delta/toplevel/metaAut.ml index 5b85e46cb..031e74cf2 100644 --- a/helm/software/lambda-delta/toplevel/metaAut.ml +++ b/helm/software/lambda-delta/toplevel/metaAut.ml @@ -33,7 +33,6 @@ type environment = (M.qid, M.pars) H.t 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 *) @@ -48,8 +47,10 @@ type resolver = Local of int 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 } @@ -149,24 +150,24 @@ let rec xlate_term f st lenv = function 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 @@ -179,7 +180,7 @@ let xlate_item f st = function 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 @@ -192,7 +193,7 @@ let xlate_item f st = function 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 @@ -201,6 +202,8 @@ let xlate_item f st = function 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 diff --git a/helm/software/lambda-delta/toplevel/metaAut.mli b/helm/software/lambda-delta/toplevel/metaAut.mli index 1172424c7..128215cc4 100644 --- a/helm/software/lambda-delta/toplevel/metaAut.mli +++ b/helm/software/lambda-delta/toplevel/metaAut.mli @@ -23,4 +23,8 @@ * 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 diff --git a/helm/software/lambda-delta/toplevel/metaOutput.ml b/helm/software/lambda-delta/toplevel/metaOutput.ml index 4efee4a68..7a15d07c2 100644 --- a/helm/software/lambda-delta/toplevel/metaOutput.ml +++ b/helm/software/lambda-delta/toplevel/metaOutput.ml @@ -63,7 +63,7 @@ let rec count_term f c = function 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 @@ -76,8 +76,9 @@ let count_item f c = function 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 @@ -142,9 +143,10 @@ let pp_body frm = function | 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 () diff --git a/helm/software/lambda-delta/toplevel/metaOutput.mli b/helm/software/lambda-delta/toplevel/metaOutput.mli index 83da0591e..2095e2677 100644 --- a/helm/software/lambda-delta/toplevel/metaOutput.mli +++ b/helm/software/lambda-delta/toplevel/metaOutput.mli @@ -27,8 +27,8 @@ type counters 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 diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml index dc2bfee93..bb6dcd843 100644 --- a/helm/software/lambda-delta/toplevel/top.ml +++ b/helm/software/lambda-delta/toplevel/top.ml @@ -28,36 +28,65 @@ module MA = MetaAut 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 ] ..." in + let help = "Usage: helena [ -V | -Ss | -m ] ..." in let help_S = " Set summary level" in let help_V = " Show version information" in + let help_m = " output intermediate representation" in let help_s = " 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"