X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Ftoplevel%2Ftop.ml;h=1442d7521e2584546076ecb8d590a23e25a0e5f3;hb=c45c77de154323feaf5bf6aee98c86b95361b9ae;hp=1fd2b718c7ce0674438f802d5c2f3a4065d3e8f6;hpb=cbdccfa38c3e05d697318cfbb9903a451e4e80d6;p=helm.git

diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml
index 1fd2b718c..1442d7521 100644
--- a/helm/software/lambda-delta/toplevel/top.ml
+++ b/helm/software/lambda-delta/toplevel/top.ml
@@ -1,49 +1,107 @@
-(* 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 AH = AutHelpers
+module P    = Printf
+module L    = Log
+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 (June 2008)" in
+   let version_string = "Helena Checker 0.8.0 M - December 2008" in
    let summary = ref 0 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
+   let print_version () = L.warn 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
-         Printf.printf "Processing file: %s\n" name; flush stdout;
+      if !summary > 0 then Time.gmtime version_string;      
+      if !summary > 1 then
+         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
       let book = AutParser.book AutLexer.token lexbuf in
       close_in ich;
-      if !summary > 1 then
-	 AH.count (AH.print_counters Cps.id) AH.initial_counters book         
+      if !summary > 0 then Time.utime_stamp "parsed";
+      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.start frm item
+	       end;
+	       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
+	    aux st tl
+      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.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 | -S <number> ] <file> ..." in
-   let help_S = "<number>  Set summary level" 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)
-   ] read_file help
+      ("-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;
+   if !summary > 0 then Time.utime_stamp "at exit"