(* ||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 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 - 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 () = 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 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 > 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 | -Ss | -m ] ..." in let help_S = " Set summary level" in let help_V = " Show version information" in let help_m = " output intermediate representation" in let help_s = " Set translation stage" in Arg.parse [ ("-S", Arg.Int set_summary, help_S); ("-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"