X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Ftoplevel%2Ftop.ml;h=27f40026e543dc3db1d83fcf3a1b327ea2d57816;hb=e86383ae4805a526b3acca2ef3c936b3f22daaad;hp=bb6dcd8433a5536377c26e41a64d82f9f4dafafd;hpb=51870ae9cdf98c4f58ebf223be4c85c40d49ec85;p=helm.git

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 <number> | -m <file> ] <file> ..." in
    let help_S = "<number>  Set summary level" in