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 AO   = AutOutput
  13 module MA   = MetaAut
  14 module MO   = MetaOutput
  15 module MBrg = MetaBrg
  16 module BrgO = BrgOutput
  17
  18 type status = {
  19    summary: int;
  20    mst : MA.status;
  21    ac  : AO.counters;
  22    mc  : MO.counters;
  23    brgc: BrgO.counters
  24 }
  25
  26 let initial_status summary = {
  27    summary = summary;
  28    ac = AO.initial_counters;
  29    mc = MO.initial_counters;
  30    brgc= BrgO.initial_counters;
  31    mst = MA.initial_status
  32 }
  33
  34 let count st count_fun c item =
  35    if st.summary > 2 then count_fun Cps.start c item else c
  36
  37 let main =
  38    let version_string = "Helena Checker 0.8.0 M - December 2008" in
  39    let summary = ref 0 in
  40    let stage = ref 2 in
  41    let meta_file = ref None in
  42    let set_summary i = summary := i in
  43    let print_version () = print_endline version_string; exit 0 in
  44    let set_stage i = stage := i in
  45    let close = function
  46       | None          -> ()
  47       | Some (och, _) -> close_out och
  48    in
  49    let set_meta_file name =
  50       close !meta_file;
  51       let och = open_out name in
  52       let frm = Format.formatter_of_out_channel och in
  53       Format.pp_set_margin frm max_int;
  54       meta_file := Some (och, frm)
  55    in
  56    let read_file name =
  57       if !summary > 0 then Time.gmtime version_string;
  58       if !summary > 1 then
  59          Printf.printf "Processing file: %s\n" name; flush stdout;
  60       if !summary > 0 then Time.utime_stamp "started";
  61       let ich = open_in name in
  62       let lexbuf = Lexing.from_channel ich in
  63       let book = AutParser.book AutLexer.token lexbuf in
  64       close_in ich;
  65       if !summary > 0 then Time.utime_stamp "parsed";
  66       let rec aux st = function
  67          | []         -> st
  68          | item :: tl ->
  69             let st = {st with ac = count st AO.count_item st.ac item} in
  70             let f st item =
  71                {st with brgc = count st BrgO.count_item st.brgc item}
  72             in
  73             let f mst item =
  74                let st = {st with
  75                   mst = mst; mc = count st MO.count_item st.mc item
  76                } in
  77                begin match !meta_file with
  78                   | None          -> ()
  79                   | Some (_, frm) -> MO.pp_item Cps.start frm item
  80                end;
  81                if !stage > 1 then MBrg.brg_of_meta (f st) item else st
  82             in
  83             let st =
  84                if !stage > 0 then MA.meta_of_aut f st.mst item else st
  85             in
  86             aux st tl
  87       in
  88       let st = aux (initial_status !summary) book in
  89       if !summary > 0 then Time.utime_stamp "processed";
  90       if !summary > 2 then AO.print_counters Cps.start st.ac;
  91       if !summary > 2 && !stage > 0 then MO.print_counters Cps.start st.mc;
  92       if !summary > 2 && !stage > 1 then BrgO.print_counters Cps.start st.brgc;
  93    in
  94    let help = "Usage: helena [ -V | -Ss <number> | -m <file> ] <file> ..." in
  95    let help_S = "<number>  Set summary level" in
  96    let help_V = " Show version information" in
  97    let help_m = "<file>  output intermediate representation" in
  98    let help_s = "<number>  Set translation stage" in
  99    Arg.parse [
 100       ("-S", Arg.Int set_summary, help_S);
 101       ("-V", Arg.Unit print_version, help_V);
 102       ("-m", Arg.String set_meta_file, help_m);
 103       ("-s", Arg.Int set_stage, help_s);
 104    ] read_file help;
 105    if !summary > 0 then Time.utime_stamp "at exit"