helm/software/lambda-delta/toplevel/top.ml

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department, University of Bologna, Italy.
   5     ||I||
   6     ||T||  HELM is free software; you can redistribute it and/or
   7     ||A||  modify it under the terms of the GNU General Public License
   8     \   /  version 2 or (at your option) any later version.
   9      \ /   This software is distributed as is, NO WARRANTY.
  10       V_______________________________________________________________ *)
  11
  12 module P    = Printf
  13 module L    = Log
  14 module AO   = AutOutput
  15 module MA   = MetaAut
  16 module MO   = MetaOutput
  17 module MBrg = MetaBrg
  18 module BrgO = BrgOutput
  19
  20 type status = {
  21    summary: int;
  22    mst : MA.status;
  23    ac  : AO.counters;
  24    mc  : MO.counters;
  25    brgc: BrgO.counters
  26 }
  27
  28 let initial_status summary = {
  29    summary = summary;
  30    ac = AO.initial_counters;
  31    mc = MO.initial_counters;
  32    brgc= BrgO.initial_counters;
  33    mst = MA.initial_status
  34 }
  35
  36 let count st count_fun c item =
  37    if st.summary > 2 then count_fun Cps.start c item else c
  38
  39 let main =
  40    let version_string = "Helena Checker 0.8.0 M - December 2008" in
  41    let summary = ref 0 in
  42    let stage = ref 2 in
  43    let meta_file = ref None in
  44    let set_summary i = summary := i in
  45    let print_version () = L.warn version_string; exit 0 in
  46    let set_stage i = stage := i in
  47    let close = function
  48       | None          -> ()
  49       | Some (och, _) -> close_out och
  50    in
  51    let set_meta_file name =
  52       close !meta_file;
  53       let och = open_out name in
  54       let frm = Format.formatter_of_out_channel och in
  55       Format.pp_set_margin frm max_int;
  56       meta_file := Some (och, frm)
  57    in
  58    let read_file name =
  59       if !summary > 0 then Time.gmtime version_string;
  60       if !summary > 1 then
  61          L.warn (P.sprintf "Processing file: %s" name);
  62       if !summary > 0 then Time.utime_stamp "started";
  63       let ich = open_in name in
  64       let lexbuf = Lexing.from_channel ich in
  65       let book = AutParser.book AutLexer.token lexbuf in
  66       close_in ich;
  67       if !summary > 0 then Time.utime_stamp "parsed";
  68       let rec aux st = function
  69          | []         -> st
  70          | item :: tl ->
  71             let st = {st with ac = count st AO.count_item st.ac item} in
  72             let f st item =
  73                {st with brgc = count st BrgO.count_item st.brgc item}
  74             in
  75             let f mst item =
  76                let st = {st with
  77                   mst = mst; mc = count st MO.count_item st.mc item
  78                } in
  79                begin match !meta_file with
  80                   | None          -> ()
  81                   | Some (_, frm) -> MO.pp_item Cps.start frm item
  82                end;
  83                if !stage > 1 then MBrg.brg_of_meta (f st) item else st
  84             in
  85             let st =
  86                if !stage > 0 then MA.meta_of_aut f st.mst item else st
  87             in
  88             aux st tl
  89       in
  90       let st = aux (initial_status !summary) book in
  91       if !summary > 0 then Time.utime_stamp "processed";
  92       if !summary > 2 then AO.print_counters Cps.start st.ac;
  93       if !summary > 2 && !stage > 0 then MO.print_counters Cps.start st.mc;
  94       if !summary > 2 && !stage > 1 then BrgO.print_counters Cps.start st.brgc;
  95    in
  96    let help = "Usage: helena [ -V | -Ss <number> | -m <file> ] <file> ..." in
  97    let help_S = "<number>  Set summary level" in
  98    let help_V = " Show version information" in
  99    let help_m = "<file>  output intermediate representation" in
 100    let help_s = "<number>  Set translation stage" in
 101    Arg.parse [
 102       ("-S", Arg.Int set_summary, help_S);
 103       ("-V", Arg.Unit print_version, help_V);
 104       ("-m", Arg.String set_meta_file, help_m);
 105       ("-s", Arg.Int set_stage, help_s);
 106    ] read_file help;
 107    if !summary > 0 then Time.utime_stamp "at exit"