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