X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Ftoplevel%2Ftop.ml;h=dc2bfee9334bc4966ed8f2661e22dbcbb05af290;hb=299f571083fa9cc38060c0d6b2ec81eefeaa1050;hp=823ce1a47cae6430c61c1d8616190b8c7eb5161e;hpb=9b4286fdc2d88b0d8018e5718ef055804f5cf7ac;p=helm.git diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml index 823ce1a47..dc2bfee93 100644 --- a/helm/software/lambda-delta/toplevel/top.ml +++ b/helm/software/lambda-delta/toplevel/top.ml @@ -23,14 +23,17 @@ * 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,22 @@ 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; + let frm = Format.err_formatter in + Format.pp_set_margin frm max_int; + MO.pp_environment Cps.id frm (List.rev env) + in + if !stage > 0 then MA.meta_of_aut f book in - let help = "Usage: helena [ -V | -S ] ..." in - let help_S = " Set summary level" in + let help = "Usage: helena [ -V | -Ss ] ..." in + let help_S = " Set summary level" in let help_V = " Show version information" in + let help_s = " 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