From: Ferruccio Guidi Date: Tue, 2 Dec 2008 19:31:31 +0000 (+0000) Subject: - we updated some preambles to match that of nUri.ml X-Git-Tag: make_still_working~4464 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e86383ae4805a526b3acca2ef3c936b3f22daaad;p=helm.git - we updated some preambles to match that of nUri.ml - the transformation to from "meta" to "basic_rg" is now working --- diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt index 4ad04534d..a1019d0de 100644 --- a/helm/software/lambda-delta/.depend.opt +++ b/helm/software/lambda-delta/.depend.opt @@ -10,6 +10,9 @@ automath/autLexer.cmo: automath/autParser.cmi automath/autLexer.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 toplevel/meta.cmo: lib/nUri.cmi automath/aut.cmx toplevel/meta.cmx: lib/nUri.cmx automath/aut.cmx toplevel/metaOutput.cmi: toplevel/meta.cmx @@ -22,9 +25,14 @@ toplevel/metaAut.cmo: lib/nUri.cmi toplevel/meta.cmx lib/cps.cmx \ automath/aut.cmx toplevel/metaAut.cmi toplevel/metaAut.cmx: lib/nUri.cmx toplevel/meta.cmx lib/cps.cmx \ automath/aut.cmx toplevel/metaAut.cmi -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 +toplevel/metaBrg.cmi: toplevel/meta.cmx basic_rg/brg.cmx +toplevel/metaBrg.cmo: toplevel/meta.cmx lib/cps.cmx basic_rg/brg.cmx \ + toplevel/metaBrg.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 \ + 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 \ + automath/autParser.cmx automath/autOutput.cmx automath/autLexer.cmx diff --git a/helm/software/lambda-delta/basic_rg/Make b/helm/software/lambda-delta/basic_rg/Make index be843055b..bb05d5bb7 100644 --- a/helm/software/lambda-delta/basic_rg/Make +++ b/helm/software/lambda-delta/basic_rg/Make @@ -1 +1 @@ -brg +brg brgOutput diff --git a/helm/software/lambda-delta/basic_rg/brg.ml b/helm/software/lambda-delta/basic_rg/brg.ml index a3a32f8d0..09d2f247a 100644 --- a/helm/software/lambda-delta/basic_rg/brg.ml +++ b/helm/software/lambda-delta/basic_rg/brg.ml @@ -1,15 +1,26 @@ -module U = NUri -module A = Aut +(* + ||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_______________________________________________________________ *) -type uri = U.uri -type id = A.id +type uri = NUri.uri +type id = Aut.id -type binder = Abst | Abbr +type bind = Abst | Abbr (* abstraction, abbreviation *) -type term = Sort of int - | LRef of int - | GRef of uri - | Cast of term * term - | Appl of term * term - | Bind of id * binder * term * term - +type term = Sort of int (* hierarchy index *) + | LRef of int (* reverse de Bruijn index *) + | GRef of uri (* reference *) + | Cast of term * term (* type, term *) + | 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 item = entry option diff --git a/helm/software/lambda-delta/basic_rg/brgOutput.ml b/helm/software/lambda-delta/basic_rg/brgOutput.ml new file mode 100644 index 000000000..741a2567d --- /dev/null +++ b/helm/software/lambda-delta/basic_rg/brgOutput.ml @@ -0,0 +1,85 @@ +(* + ||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 B = Brg + +type counters = { + eabsts: int; + eabbrs: int; + tsorts: int; + tlrefs: int; + tgrefs: int; + tcasts: int; + tappls: int; + tabsts: int; + tabbrs: int +} + +let initial_counters = { + eabsts = 0; eabbrs = 0; tsorts = 0; tlrefs = 0; tgrefs = 0; + tcasts = 0; tappls = 0; tabsts = 0; tabbrs = 0 +} + +let count_term_binder f c = function + | B.Abst -> f {c with tabsts = succ c.tabsts} + | B.Abbr -> f {c with tabbrs = succ c.tabbrs} + +let rec count_term f c = function + | B.Sort _ -> + f {c with tsorts = succ c.tsorts} + | B.LRef _ -> + f {c with tlrefs = succ c.tlrefs} + | B.GRef _ -> + f {c with tgrefs = succ c.tgrefs} + | B.Cast (v, t) -> + let c = {c with tcasts = succ c.tcasts} in + let f c = count_term f c t in + count_term f c v + | B.Appl (v, t) -> + let c = {c with tappls = succ c.tappls} in + let f c = count_term f c t in + count_term f c v + | B.Bind (_, b, u, t) -> + let f c = count_term_binder f c b in + let f c = count_term f c t in + count_term f c u + +let count_entry_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 + count_term f c t + +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.tcasts + c.tappls + c.tabsts + + 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 () diff --git a/helm/software/lambda-delta/basic_rg/brgOutput.mli b/helm/software/lambda-delta/basic_rg/brgOutput.mli new file mode 100644 index 000000000..49b5064d1 --- /dev/null +++ b/helm/software/lambda-delta/basic_rg/brgOutput.mli @@ -0,0 +1,18 @@ +(* + ||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_______________________________________________________________ *) + +type counters + +val initial_counters: counters + +val count_item: (counters -> 'a) -> counters -> Brg.item -> 'a + +val print_counters: (unit -> 'a) -> counters -> 'a diff --git a/helm/software/lambda-delta/lib/cps.ml b/helm/software/lambda-delta/lib/cps.ml index 199a786cd..14b9d4a2c 100644 --- a/helm/software/lambda-delta/lib/cps.ml +++ b/helm/software/lambda-delta/lib/cps.ml @@ -1,29 +1,17 @@ -(* 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 +(* + ||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_______________________________________________________________ *) + +let start x = x + +let id f x = f x let rec list_sub_strict f l1 l2 = match l1, l2 with | _, [] -> f l1 diff --git a/helm/software/lambda-delta/toplevel/Make b/helm/software/lambda-delta/toplevel/Make index 33afbe36e..7b8610821 100644 --- a/helm/software/lambda-delta/toplevel/Make +++ b/helm/software/lambda-delta/toplevel/Make @@ -1 +1 @@ -meta metaOutput metaAut top +meta metaOutput metaAut metaBrg top diff --git a/helm/software/lambda-delta/toplevel/meta.ml b/helm/software/lambda-delta/toplevel/meta.ml index af3f9b0af..5b3895e79 100644 --- a/helm/software/lambda-delta/toplevel/meta.ml +++ b/helm/software/lambda-delta/toplevel/meta.ml @@ -1,27 +1,13 @@ -(* 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_______________________________________________________________ *) type uri = NUri.uri @@ -31,7 +17,7 @@ type term = Sort of bool (* sorts: true = TYPE, false = PROP *) | LRef of int * int (* local reference: context length, de bruijn index *) | GRef of int * uri * term list (* global reference: context length, name, arguments *) | Appl of term * term (* application: argument, function *) - | Abst of id * term * term (* abstraction: name, type, body *) + | Abst of id * term * term (* abstraction: name, type, scope *) type pars = (id * term) list (* parameter declarations: name, type *) diff --git a/helm/software/lambda-delta/toplevel/metaAut.ml b/helm/software/lambda-delta/toplevel/metaAut.ml index 767a44afb..71759f79a 100644 --- a/helm/software/lambda-delta/toplevel/metaAut.ml +++ b/helm/software/lambda-delta/toplevel/metaAut.ml @@ -1,27 +1,13 @@ -(* 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 H = Hashtbl module U = NUri diff --git a/helm/software/lambda-delta/toplevel/metaBrg.ml b/helm/software/lambda-delta/toplevel/metaBrg.ml new file mode 100644 index 000000000..4ca8e5c22 --- /dev/null +++ b/helm/software/lambda-delta/toplevel/metaBrg.ml @@ -0,0 +1,64 @@ +(* + ||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 B = Brg +module M = Meta + +(* Internal functions *******************************************************) + +let map_fold_left f map1 map2 a l = + let f a = Cps.list_fold_left f map2 a l in + map1 f a + +let map_args f t v = f (B.Appl (v, t)) + +let map_pars f t (id, w) = f (B.Bind (id, B.Abst, w, t)) + +let rec xlate_term f = function + | M.Sort s -> + let f h = f (B.Sort h) in + if s then f 0 else f 1 + | M.LRef (l, i) -> + f (B.LRef (l - i)) + | M.GRef (_, uri, vs) -> + let f vs = map_fold_left f Cps.id map_args (B.GRef uri) vs in + Cps.list_rev_map f xlate_term vs + | M.Appl (v, t) -> + let f v t = f (B.Appl (v, t)) in + let f v = xlate_term (f v) t in + xlate_term f v + | M.Abst (id, w, t) -> + let f w t = f (B.Bind (id, B.Abst, w, t)) in + let f w = xlate_term (f w) t in + xlate_term f w + +let xlate_pars f (id, w) = + let f w = f (id, w) in + xlate_term f w + +let xlate_entry f = function + | _, pars, uri, u, None -> + let f u = f (uri, B.Abst, u) 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 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 + +let xlate_item f = function + | None -> f None + | Some e -> let f e = f (Some e) in xlate_entry f e + +(* Interface functions ******************************************************) + +let brg_of_meta = xlate_item diff --git a/helm/software/lambda-delta/toplevel/metaBrg.mli b/helm/software/lambda-delta/toplevel/metaBrg.mli new file mode 100644 index 000000000..cb47bc9c1 --- /dev/null +++ b/helm/software/lambda-delta/toplevel/metaBrg.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 brg_of_meta: (Brg.item -> 'a) -> Meta.item -> 'a diff --git a/helm/software/lambda-delta/toplevel/metaOutput.ml b/helm/software/lambda-delta/toplevel/metaOutput.ml index a12818ee3..04e15e4db 100644 --- a/helm/software/lambda-delta/toplevel/metaOutput.ml +++ b/helm/software/lambda-delta/toplevel/metaOutput.ml @@ -1,27 +1,13 @@ -(* 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 F = Format module U = NUri diff --git a/helm/software/lambda-delta/toplevel/metaOutput.mli b/helm/software/lambda-delta/toplevel/metaOutput.mli index 2095e2677..aefb43bef 100644 --- a/helm/software/lambda-delta/toplevel/metaOutput.mli +++ b/helm/software/lambda-delta/toplevel/metaOutput.mli @@ -1,27 +1,13 @@ -(* 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_______________________________________________________________ *) type counters diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml index bb6dcd843..27f40026e 100644 --- a/helm/software/lambda-delta/toplevel/top.ml +++ b/helm/software/lambda-delta/toplevel/top.ml @@ -1,36 +1,43 @@ -(* 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 AO = AutOutput -module MA = MetaAut -module MO = MetaOutput +module AO = AutOutput +module MA = MetaAut +module MO = MetaOutput +module MBrg = MetaBrg +module BrgO = BrgOutput + +type status = { + summary: int; + mst : MA.status; + ac : AO.counters; + mc : MO.counters; + brgc: BrgO.counters +} + +let initial_status summary = { + summary = summary; + ac = AO.initial_counters; + mc = MO.initial_counters; + brgc= BrgO.initial_counters; + mst = MA.initial_status +} + +let count st count_fun c item = + if st.summary > 2 then count_fun Cps.start c item else c let main = - let version_string = "Helena Checker 0.8.0 M - November 2008" in + let version_string = "Helena Checker 0.8.0 M - December 2008" in let summary = ref 0 in - let stage = ref 1 in + 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 @@ -56,27 +63,33 @@ let main = let book = AutParser.book AutLexer.token lexbuf in close_in ich; 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 + let rec aux st = function + | [] -> st + | item :: tl -> + let st = {st with ac = count st AO.count_item st.ac item} in + let f st item = + {st with brgc = count st BrgO.count_item st.brgc item} + in + let f mst item = + let st = {st with + mst = mst; mc = count st MO.count_item st.mc item + } in begin match !meta_file with | None -> () - | Some (_, frm) -> MO.pp_item Cps.id frm item + | Some (_, frm) -> MO.pp_item Cps.start frm item end; - st, mc + if !stage > 1 then MBrg.brg_of_meta (f st) item else st + in + let st = + if !stage > 0 then MA.meta_of_aut f st.mst item else st in - let st, mc = if !stage > 0 then MA.meta_of_aut f st item else st, mc in - aux ac mc st tl + aux st tl in - let ac, mc, _st = - aux AO.initial_counters MO.initial_counters MA.initial_status book - in + let st = aux (initial_status !summary) book in 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; + if !summary > 2 then AO.print_counters Cps.start st.ac; + if !summary > 2 && !stage > 0 then MO.print_counters Cps.start st.mc; + if !summary > 2 && !stage > 1 then BrgO.print_counters Cps.start st.brgc; in let help = "Usage: helena [ -V | -Ss | -m ] ..." in let help_S = " Set summary level" in