X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Ftoplevel%2Ftop.ml;h=bb6dcd8433a5536377c26e41a64d82f9f4dafafd;hb=973b0b1fd5f44b96a3c367a9756f28b75b9fa30b;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..bb6dcd843 100644
--- a/helm/software/lambda-delta/toplevel/top.ml
+++ b/helm/software/lambda-delta/toplevel/top.ml
@@ -23,27 +23,70 @@
  * http://cs.unibo.it/helm/.
  *)
 
-module AH = AutHelpers
+module AO = AutOutput
+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
-	 AH.count (AH.print_counters Cps.id) AH.initial_counters book         
+      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 !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 | -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"