]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/toplevel/top.ml
we improved the data structures used in the translation to the intermediate
[helm.git] / helm / software / lambda-delta / toplevel / top.ml
index 823ce1a47cae6430c61c1d8616190b8c7eb5161e..f7839a6f9c939fa59c7b56d391b1e148bcb430dc 100644 (file)
  * 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 id _ = () in
    let summary = ref 0 in
+   let stage = ref 1 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 read_file name =
       if !summary > 0 then
          Printf.printf "Processing file: %s\n" name; flush stdout;
@@ -39,12 +42,19 @@ let main =
       let book = AutParser.book AutLexer.token lexbuf in
       close_in ich;
       if !summary > 1 then
-        AH.count (AH.print_counters id) AH.initial_counters book         
+        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
+      in
+      if !stage > 0 then MA.meta_of_aut f book
    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> ] <file> ..." in
+   let help_S = "<number>  Set summary level" in
    let help_V = " Show version information" 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)
+      ("-V", Arg.Unit print_version, help_V);
+      ("-s", Arg.Int set_stage, help_s);
    ] read_file help