helm/software/lambda-delta/src/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 F  = Filename
  13 module P  = Printf
  14 module U  = NUri
  15 module C  = Cps
  16 module L  = Log
  17 module Y  = Time
  18 module G  = Options
  19 module H  = Hierarchy
  20 module O  = Output
  21 module E  = Entity
  22 module S  = Status
  23 module DO = CrgOutput
  24 module TD = TxtCrg
  25 module AA = AutProcess
  26 module AO = AutOutput
  27 module AD = AutCrg
  28 module XL = XmlLibrary
  29 module XD = XmlCrg
  30 module BD = BrgCrg
  31 module BO = BrgOutput
  32 module BR = BrgReduction
  33 module BU = BrgUntrusted
  34 module ZO = BagOutput
  35 module ZT = BagType
  36 module ZU = BagUntrusted
  37
  38 type status = {
  39    kst: S.status;
  40    tst: TD.status;
  41    pst: AA.status;
  42    ast: AD.status;
  43    ac : AO.counters;
  44    dc : DO.counters;
  45    bc : BO.counters;
  46    zc : ZO.counters;
  47 }
  48
  49 let flush_all () = L.flush 0; L.flush_err ()
  50
  51 let bag_error s msg =
  52    L.error ZO.specs (L.Warn s :: L.Loc :: msg); flush_all ()
  53
  54 let brg_error s msg =
  55    L.error BR.specs (L.Warn s :: L.Loc :: msg); flush_all ()
  56
  57 let initial_status () = {
  58    kst = S.initial_status ();
  59    tst = TD.initial_status ();
  60    pst = AA.initial_status ();
  61    ast = AD.initial_status ();
  62    ac  = AO.initial_counters;
  63    dc  = DO.initial_counters;
  64    bc  = BO.initial_counters;
  65    zc  = ZO.initial_counters;
  66 }
  67
  68 let refresh_status st = {st with
  69    kst = S.refresh_status st.kst;
  70    tst = TD.refresh_status st.tst;
  71    ast = AD.refresh_status st.ast;
  72 }
  73
  74 (* kernel related ***********************************************************)
  75
  76 type kernel_entity = BrgEntity of Brg.entity
  77                    | BagEntity of Bag.entity
  78                    | CrgEntity of Crg.entity
  79
  80 let print_counters st = function
  81    | G.Crg -> DO.print_counters C.start st.dc
  82    | G.Brg -> BO.print_counters C.start st.bc
  83    | G.Bag -> ZO.print_counters C.start st.zc
  84
  85 let xlate_entity entity = match !G.kernel, entity with
  86    | G.Brg, CrgEntity e ->
  87       let f e = (BrgEntity e) in E.xlate f BD.brg_of_crg e
  88    | _, entity          -> entity
  89
  90 let pp_progress e =
  91    let f a u =
  92       let s = U.string_of_uri u in
  93       let err () = L.warn (P.sprintf "%s" s) in
  94       let f i = L.warn (P.sprintf "[%u] %s" i s) in
  95       E.mark err f a
  96    in
  97    match e with
  98       | CrgEntity e -> E.common f e
  99       | BrgEntity e -> E.common f e
 100       | BagEntity e -> E.common f e
 101
 102 let count_entity st = function
 103    | BrgEntity e -> {st with bc = BO.count_entity C.start st.bc e}
 104    | BagEntity e -> {st with zc = ZO.count_entity C.start st.zc e}
 105    | CrgEntity e -> {st with dc = DO.count_entity C.start st.dc e}
 106
 107 let export_entity = function
 108    | CrgEntity e -> XL.export_entity XD.export_term e
 109    | BrgEntity e -> XL.export_entity BO.export_term e
 110    | BagEntity _ -> ()
 111
 112 let type_check st k =
 113    let brg_err msg = brg_error "Type Error" msg; failwith "Interrupted" in
 114    let ok _ _ = st in
 115    match k with
 116       | BrgEntity entity -> BU.type_check brg_err ok st.kst entity
 117       | BagEntity entity -> ZU.type_check ok st.kst entity
 118       | CrgEntity _      -> st
 119
 120 (* extended lexer ***********************************************************)
 121
 122 type 'token lexer = {
 123    parse : Lexing.lexbuf -> 'token;
 124    mutable tokbuf: 'token option;
 125    mutable unget : bool
 126 }
 127
 128 let initial_lexer parse = {
 129    parse = parse; tokbuf = None; unget = false
 130 }
 131
 132 let token xl lexbuf = match xl.tokbuf with
 133    | Some token when xl.unget ->
 134       xl.unget <- false; token
 135    | _                        ->
 136       let token = xl.parse lexbuf in
 137       xl.tokbuf <- Some token; token
 138
 139 (* input related ************************************************************)
 140
 141 type input = Text | Automath
 142
 143 type input_entity = TxtEntity of Txt.command
 144                   | AutEntity of Aut.command
 145                   | NoEntity
 146
 147 let type_of_input name =
 148    if F.check_suffix name ".hln" then Text
 149    else if F.check_suffix name ".aut" then
 150       let _ = H.set_sorts 0 ["Set"; "Prop"] in
 151       assert (H.set_graph "Z2");
 152       Automath
 153    else begin
 154       L.warn (P.sprintf "Unknown file type: %s" name); exit 2
 155    end
 156
 157 let txt_xl = initial_lexer TxtLexer.token
 158
 159 let aut_xl = initial_lexer AutLexer.token
 160
 161 let parbuf = ref [] (* parser buffer *)
 162
 163 let gen_text command =
 164    parbuf := TxtEntity command :: !parbuf
 165
 166 let entity_of_input lexbuf i = match i, !parbuf with
 167    | Automath, _    ->
 168       begin match AutParser.entry (token aut_xl) lexbuf with
 169          | Some e -> aut_xl.unget <- true; AutEntity e
 170          | None   -> NoEntity
 171       end
 172    | Text, []       ->
 173       begin match TxtParser.entry (token txt_xl) lexbuf with
 174          | Some e -> txt_xl.unget <- true; TxtEntity e
 175          | None   -> NoEntity
 176       end
 177    | Text, hd :: tl ->
 178       parbuf := tl; hd
 179
 180 let process_input f st = function
 181    | AutEntity e     ->
 182       let f pst e = f {st with pst = pst} (AutEntity e) in
 183       AA.process_command f st.pst e
 184    | xe              -> f st xe
 185
 186 let count_input st = function
 187    | AutEntity e -> {st with ac = AO.count_command C.start st.ac e}
 188    | xe          -> st
 189
 190 (****************************************************************************)
 191
 192 let stage = ref 3
 193 let progress = ref false
 194 let preprocess = ref false
 195 let root = ref ""
 196 let export = ref false
 197 let st = ref (initial_status ())
 198 let streaming = ref false (* parsing style (temporary) *)
 199
 200 let process_2 st entity =
 201    let st = if !L.level > 2 then count_entity st entity else st in
 202    if !export then export_entity entity;
 203    if !stage > 2 then type_check st entity else st
 204
 205 let process_1 st entity =
 206    if !progress then pp_progress entity;
 207    let st = if !L.level > 2 then count_entity st entity else st in
 208    if !export && !stage = 1 then export_entity entity;
 209    if !stage > 1 then process_2 st (xlate_entity entity) else st
 210
 211 let process_0 st entity =
 212    let f st entity =
 213       if !stage = 0 then st else
 214       match entity with
 215          | AutEntity e ->
 216             let err ast = {st with ast = ast} in
 217             let g ast e = process_1 {st with ast = ast} (CrgEntity e) in
 218             AD.crg_of_aut err g st.ast e
 219          | TxtEntity e ->
 220             let crr tst = {st with tst = tst} in
 221             let d tst e = process_1 {st with tst = tst} (CrgEntity e) in
 222             TD.crg_of_txt crr d gen_text st.tst e
 223          | NoEntity    -> assert false
 224    in
 225    let st = if !L.level > 2 then count_input st entity else st in
 226    if !preprocess then process_input f st entity else f st entity
 227
 228 let process_nostreaming st lexbuf input =
 229    let id x = x in
 230    let rec aux1 book = match entity_of_input lexbuf input with
 231       | NoEntity -> List.rev book
 232       | e        -> aux1 (id e :: book)
 233    in
 234    let rec aux2 st = function
 235       | []           -> st
 236       | entity :: tl -> aux2 (process_0 st entity) tl
 237    in
 238    aux2 st (aux1 [])
 239
 240 let process_streaming st lexbuf input =
 241    let rec aux st = match entity_of_input lexbuf input with
 242       | NoEntity -> st
 243       | e        -> aux (process_0 st e)
 244    in
 245    aux st
 246
 247 (****************************************************************************)
 248
 249 let process st name =
 250    let process = if !streaming then process_streaming else process_nostreaming in
 251    let input = type_of_input name in
 252    let ich = open_in name in
 253    let lexbuf = Lexing.from_channel ich in
 254    let st = process st lexbuf input in
 255    close_in ich;
 256    if !stage > 2 && !G.cc && !G.si then XL.export_csys st.kst.S.cc;
 257    st, input
 258
 259 let main =
 260 try
 261    let version_string = "Helena 0.8.1 M - November 2010" in
 262    let print_version () = L.warn (version_string ^ "\n"); exit 0 in
 263    let set_hierarchy s =
 264       if H.set_graph s then () else
 265          L.warn (P.sprintf "Unknown type hierarchy: %s" s)
 266    in
 267    let set_kernel = function
 268       | "brg" -> G.kernel := G.Brg
 269       | "bag" -> G.kernel := G.Bag
 270       | s     -> L.warn (P.sprintf "Unknown kernel version: %s" s)
 271    in
 272    let set_summary i = L.level := i in
 273    let set_stage i = stage := i in
 274    let set_xdir s = G.xdir := s in
 275    let set_root s = root := s in
 276    let clear_options () =
 277       progress := false; export := false; preprocess := false;
 278       stage := 3; root := "";
 279       st := initial_status ();
 280       L.clear (); G.clear (); H.clear (); O.clear_reductions ();
 281       streaming := false;
 282    in
 283    let process_file name =
 284       if !L.level > 0 then Y.gmtime version_string;
 285       if !L.level > 1 then
 286          L.warn (P.sprintf "Processing file: %s" name);
 287       if !L.level > 0 then Y.utime_stamp "started";
 288       let base_name = Filename.chop_extension (Filename.basename name) in
 289       let cover = F.concat !root base_name in
 290       if !stage < 2 then G.kernel := G.Crg;
 291       G.cover := cover;
 292       let sst, input = process (refresh_status !st) name in
 293       st := sst;
 294       if !L.level > 0 then Y.utime_stamp "processed";
 295       if !L.level > 2 then begin
 296          AO.print_counters C.start !st.ac;
 297          if !preprocess then AO.print_process_counters C.start !st.pst;
 298          if !stage > 0 then print_counters !st G.Crg;
 299          if !stage > 1 then print_counters !st !G.kernel;
 300          if !stage > 2 then O.print_reductions ()
 301       end
 302    in
 303    let exit () =
 304       if !L.level > 0 then Y.utime_stamp "at exit";
 305       flush_all ()
 306    in
 307    let help =
 308       "Usage: helena [ -LPVXcgijopqx1 | -Ss <number> | -O <dir> | -hkr <string> ]* [ <file> ]*\n\n" ^
 309       "Summary levels: 0 just errors (default), 1 time stamps, 2 processed file names, \
 310        3 data information, 4 typing information, 5 reduction information\n\n" ^
 311        "Stages: 0 parsing, 1 to intermediate, 2 to untrusted, 3 to trusted (default)\n"
 312    in
 313    let help_L = " show lexer debug information" in
 314    let help_O = "<dir>  set location of output directory (XML) to <dir> (default: current directory)" in
 315    let help_P = " show parser debug information" in
 316    let help_S = "<number>  set summary level (see above)" in
 317    let help_V = " show version information" in
 318    let help_X = " clear options" in
 319
 320    let help_c = " read/write conversion constraints" in
 321    let help_g = " always expand global definitions" in
 322    let help_h = "<string>  set type hierarchy (default: \"Z1\")" in
 323    let help_i = " show local references by index" in
 324    let help_j = " show URI of processed kernel objects" in
 325    let help_k = "<string>  set kernel version (default: \"brg\")" in
 326    let help_o = " activate sort inclusion" in
 327    let help_p = " preprocess source" in
 328    let help_q = " disable quotation of identifiers" in
 329    let help_r = "<string>  set initial segment of URI hierarchy (default: empty)" in
 330    let help_s = "<number>  set translation stage (see above)" in
 331    let help_x = " export kernel entities (XML)" in
 332
 333    let help_1 = " parse files with streaming policy" in
 334    L.box 0; L.box_err ();
 335    at_exit exit;
 336    Arg.parse [
 337       ("-L", Arg.Set G.debug_lexer, help_L);
 338       ("-O", Arg.String set_xdir, help_O);
 339       ("-P", Arg.Set G.debug_parser, help_P);
 340       ("-S", Arg.Int set_summary, help_S);
 341       ("-V", Arg.Unit print_version, help_V);
 342       ("-X", Arg.Unit clear_options, help_X);
 343       ("-c", Arg.Set G.cc, help_c);
 344       ("-g", Arg.Set G.expand, help_g);
 345       ("-h", Arg.String set_hierarchy, help_h);
 346       ("-i", Arg.Set G.indexes, help_i);
 347       ("-j", Arg.Set progress, help_j);
 348       ("-k", Arg.String set_kernel, help_k);
 349       ("-o", Arg.Set G.si, help_o);
 350       ("-p", Arg.Set preprocess, help_p);
 351       ("-q", Arg.Set G.unquote, help_q);
 352       ("-r", Arg.String set_root, help_r);
 353       ("-s", Arg.Int set_stage, help_s);
 354       ("-x", Arg.Set export, help_x);
 355       ("-1", Arg.Set streaming, help_1);
 356    ] process_file help;
 357 with ZT.TypeError msg -> bag_error "Type Error" msg