helm/software/helena/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 KF = Filename
  13 module KL = List
  14 module KP = Printf
  15 module KS = String
  16 module KT = String
  17
  18 module U  = NUri
  19 module C  = Cps
  20 module L  = Log
  21 module Y  = Time
  22 module P  = Marks
  23 module G  = Options
  24 module H  = Hierarchy
  25 module N  = Layer
  26 module E  = Entity
  27 module O  = Output
  28 module DO = CrgOutput
  29 module TD = TxtCrg
  30 module AA = AutProcess
  31 module AO = AutOutput
  32 module AD = AutCrg
  33 module XL = XmlLibrary
  34 module XD = XmlCrg
  35 module B  = Brg
  36 module BD = BrgCrg
  37 module BO = BrgOutput
  38 module BR = BrgReduction
  39 module BU = BrgUntrusted
  40 module BG = BrgGrafite
  41 module BA = BrgGallina
  42 module BP = BrgLP
  43 module ZD = BagCrg
  44 module ZO = BagOutput
  45 module ZT = BagType
  46 module ZU = BagUntrusted
  47
  48 type status = {
  49    kst: N.status;
  50    tst: TD.status;
  51    pst: AA.status;
  52    ast: AD.status;
  53    ac : AO.counters;
  54    dc : DO.counters;
  55    bc : BO.counters;
  56    zc : ZO.counters;
  57    mst: B.manager option;
  58 }
  59
  60 let level = 0
  61
  62 let bag_error st s msg =
  63    L.error st.kst ZO.specs (L.Warn s :: msg)
  64
  65 let brg_error st s msg =
  66    L.error st.kst BR.specs (L.Warn s :: msg)
  67
  68 let initial_status () = {
  69    kst = N.initial_status ();
  70    tst = TD.initial_status ();
  71    pst = AA.initial_status ();
  72    ast = AD.initial_status ();
  73    ac  = AO.initial_counters;
  74    dc  = DO.initial_counters;
  75    bc  = BO.initial_counters;
  76    zc  = ZO.initial_counters;
  77    mst = None;
  78 }
  79
  80 let refresh_status st = {st with
  81    kst = N.refresh_status st.kst;
  82    tst = TD.refresh_status st.tst;
  83    ast = AD.refresh_status st.ast;
  84 }
  85
  86 (* kernel related ***********************************************************)
  87
  88 type kernel_entity = BrgEntity of Brg.entity
  89                    | BagEntity of Bag.entity
  90                    | CrgEntity of Crg.entity
  91
  92 IFDEF SUMMARY THEN
  93
  94 let print_counters st = function
  95    | G.V4 -> DO.print_counters C.start st.dc
  96    | G.V3 -> BO.print_counters C.start st.bc
  97    | G.V0 -> ZO.print_counters C.start st.zc
  98
  99 END
 100
 101 IFDEF TRACE THEN
 102
 103 let pp_progress e =
 104    let f _ na u =
 105       let s = U.string_of_uri u in
 106       L.warn 2 (KP.sprintf "[%u] <%s>" na.E.n_apix s);
 107    in
 108    Y.utime_stamp "intermediate";
 109    match e with
 110       | CrgEntity e -> E.common f e
 111       | BrgEntity e -> E.common f e
 112       | BagEntity e -> E.common f e
 113
 114 END
 115
 116 IFDEF SUMMARY THEN
 117
 118 let count_entity st = function
 119    | BrgEntity e -> {st with bc = BO.count_entity C.start st.bc e}
 120    | BagEntity e -> {st with zc = ZO.count_entity C.start st.zc e}
 121    | CrgEntity e -> {st with dc = DO.count_entity C.start st.dc e}
 122
 123 END
 124
 125 IFDEF OBJECTS THEN
 126
 127 let export_entity st = function
 128    | CrgEntity e -> XL.export_entity (XD.export_term st.kst) e
 129    | BrgEntity e -> XL.export_entity (BO.export_term st.kst) e
 130    | BagEntity e -> XL.export_entity (ZO.export_term st.kst) e
 131
 132 END
 133
 134 IFDEF TYPE THEN
 135
 136 let type_check st k =
 137    let brg_err msg = brg_error st "Type Error" msg; failwith "Interrupted" in
 138    let bag_err msg = bag_error st "Type Error" msg; failwith "Interrupted" in
 139    let ok _ _ = st in
 140    match k with
 141       | BrgEntity entity -> BU.type_check brg_err ok st.kst entity
 142       | BagEntity entity -> ZU.type_check bag_err ok st.kst entity
 143       | CrgEntity _      -> st
 144
 145 END
 146
 147 IFDEF MANAGER THEN
 148
 149 let manager st output_entity = function
 150    | BrgEntity entity ->
 151       if output_entity st.kst entity then st else
 152       begin L.warn level "manager exportation stopped"; {st with mst = None} end
 153    | BagEntity _      -> st
 154    | CrgEntity _      -> st
 155
 156 END
 157
 158 let xlate_entity st entity = match !G.kernel, entity with
 159    | G.V3, CrgEntity e ->
 160       let f e = (BrgEntity e) in E.xlate f BD.brg_of_crg e
 161    | G.V0, CrgEntity e ->
 162       let f e = (BagEntity e) in E.xlate f (ZD.bag_of_crg st.kst) e
 163    | _, entity         -> entity
 164
 165 let validate st k =
 166    let brg_err msg = brg_error st "Validation Error" msg; failwith "Interrupted" in
 167    let ok _ = st in
 168    match k with
 169       | BrgEntity entity -> BU.validate brg_err ok st.kst entity
 170       | BagEntity _      -> st
 171       | CrgEntity _      -> st
 172
 173 (* extended lexer ***********************************************************)
 174
 175 type 'token lexer = {
 176    parse : Lexing.lexbuf -> 'token;
 177    mutable tokbuf: 'token option;
 178    mutable unget : bool
 179 }
 180
 181 let initial_lexer parse = {
 182    parse = parse; tokbuf = None; unget = false
 183 }
 184
 185 let token xl lexbuf = match xl.tokbuf with
 186    | Some token when xl.unget ->
 187       xl.unget <- false; token
 188    | _                        ->
 189       let token = xl.parse lexbuf in
 190       xl.tokbuf <- Some token; token
 191
 192 (* input related ************************************************************)
 193
 194 type input = Text | Automath
 195
 196 type input_entity = TxtEntity of Txt.command
 197                   | AutEntity of Aut.command
 198                   | NoEntity
 199
 200 let type_of_input name =
 201    if KF.check_suffix name ".hln" then Text
 202    else if KF.check_suffix name ".aut" then
 203       let _ = H.set_sorts 0 ["Set"; "Prop"] in
 204       assert (H.set_graph "Z2");
 205       Automath
 206    else begin
 207       L.warn level (KP.sprintf "Unknown file type: %s" name); exit 2
 208    end
 209
 210 let txt_xl = initial_lexer TxtLexer.token
 211
 212 let aut_xl = initial_lexer AutLexer.token
 213
 214 let parbuf = ref [] (* parser buffer *)
 215
 216 let gen_text command =
 217    parbuf := TxtEntity command :: !parbuf
 218
 219 let entity_of_input lexbuf i = match i, !parbuf with
 220    | Automath, _    ->
 221       begin match AutParser.entry (token aut_xl) lexbuf with
 222          | Some e -> aut_xl.unget <- true; AutEntity e
 223          | None   -> NoEntity
 224       end
 225    | Text, []       ->
 226       begin match TxtParser.entry (token txt_xl) lexbuf with
 227          | Some e -> txt_xl.unget <- true; TxtEntity e
 228          | None   -> NoEntity
 229       end
 230    | Text, hd :: tl ->
 231       parbuf := tl; hd
 232
 233 IFDEF PREPROCESS THEN
 234
 235 let process_input f st = function
 236    | AutEntity e     ->
 237       let f pst e = f {st with pst = pst} (AutEntity e) in
 238       AA.process_command f st.pst e
 239    | xe              -> f st xe
 240
 241 END
 242
 243 IFDEF SUMMARY THEN
 244
 245 let count_input st = function
 246    | AutEntity e -> {st with ac = AO.count_command C.start st.ac e}
 247    | xe          -> st
 248
 249 END
 250
 251 (****************************************************************************)
 252
 253 let st = ref (initial_status ())
 254 let streaming = ref false (* parsing style (temporary) *)
 255
 256 let process_2 st entity =
 257    let st =
 258 IFDEF SUMMARY THEN
 259       if !G.summary then count_entity st entity else st
 260 ELSE
 261       st
 262 END
 263    in
 264    let st =
 265 IFDEF STAGE THEN
 266       if !G.stage >= 3 then
 267 IFDEF TYPE THEN
 268          let f = if !G.validate then validate else type_check in f st entity
 269 ELSE
 270          validate st entity
 271 END
 272       else st
 273 ELSE
 274 IFDEF TYPE THEN
 275       let f = if !G.validate then validate else type_check in f st entity
 276 ELSE
 277       validate st entity
 278 END
 279 END
 280    in
 281 IFDEF OBJECTS THEN
 282    if !G.export then export_entity st entity
 283 ELSE () END;
 284 IFDEF MANAGER THEN
 285    match st.mst with
 286      | None                    -> st
 287      | Some (export_entity, _) -> manager st export_entity entity
 288 ELSE
 289      st
 290 END
 291
 292 let process_1 st entity =
 293 IFDEF TRACE THEN
 294    if !G.ct >= 3 then pp_progress entity;
 295 ELSE () END;
 296    let st =
 297 IFDEF SUMMARY THEN
 298       if !G.summary then count_entity st entity else st
 299 ELSE
 300       st
 301 END
 302    in
 303 IFDEF STAGE THEN
 304 IFDEF OBJECTS THEN
 305    if !G.export && !G.stage = 1 then export_entity st entity
 306 ELSE () END;
 307    if !G.stage >= 2 then process_2 st (xlate_entity st entity) else st
 308 ELSE
 309    process_2 st (xlate_entity st entity)
 310 END
 311
 312 let process_0 st entity =
 313    let f st entity =
 314 IFDEF STAGE THEN
 315       if !G.stage = 0 then st else
 316       match entity with
 317          | AutEntity e ->
 318             let err ast = {st with ast = ast} in
 319             let g ast e = process_1 {st with ast = ast} (CrgEntity e) in
 320             AD.crg_of_aut err g st.kst st.ast e
 321          | TxtEntity e ->
 322             let crr tst = {st with tst = tst} in
 323             let d tst e = process_1 {st with tst = tst} (CrgEntity e) in
 324             TD.crg_of_txt crr d gen_text st.tst e
 325          | NoEntity    -> assert false
 326 ELSE
 327       match entity with
 328          | AutEntity e ->
 329             let err ast = {st with ast = ast} in
 330             let g ast e = process_1 {st with ast = ast} (CrgEntity e) in
 331             AD.crg_of_aut err g st.kst st.ast e
 332          | TxtEntity e ->
 333             let crr tst = {st with tst = tst} in
 334             let d tst e = process_1 {st with tst = tst} (CrgEntity e) in
 335             TD.crg_of_txt crr d gen_text st.tst e
 336          | NoEntity    -> assert false
 337 END
 338    in
 339    let st =
 340 IFDEF SUMMARY THEN
 341       if !G.summary then count_input st entity else st
 342 ELSE
 343       st
 344 END
 345    in
 346 IFDEF PREPROCESS THEN
 347    if !G.preprocess then process_input f st entity else f st entity
 348 ELSE
 349    f st entity
 350 END
 351
 352 let process_nostreaming st lexbuf input =
 353    let id x = x in
 354    let rec aux1 book = match entity_of_input lexbuf input with
 355       | NoEntity -> List.rev book
 356       | e        -> aux1 (id e :: book)
 357    in
 358    let rec aux2 st = function
 359       | []           -> st
 360       | entity :: tl -> aux2 (process_0 st entity) tl
 361    in
 362    aux2 st (aux1 [])
 363
 364 let process_streaming st lexbuf input =
 365    let rec aux st = match entity_of_input lexbuf input with
 366       | NoEntity -> st
 367       | e        -> aux (process_0 st e)
 368    in
 369    aux st
 370
 371 (****************************************************************************)
 372
 373 IFDEF PREPROCESS THEN
 374
 375 let set_preprocess () =
 376    if !G.trace >= 2 then begin
 377       G.preprocess := true;
 378 IFDEF SUMMARY THEN
 379       G.summary := true
 380 ELSE () END
 381    end
 382
 383 END
 384
 385 IFDEF MANAGER THEN
 386
 387 let set_manager s = match KS.lowercase s with
 388    | "v8"  -> G.manager := G.Coq
 389    | "ma2" -> G.manager := G.Matita
 390    | "lp1" -> G.manager := G.LP1
 391    | "lp2" -> G.manager := G.LP2
 392    | "tj2" -> G.manager := G.TJ2
 393    | "tj3" -> G.manager := G.TJ3
 394    | s     -> L.warn level (KP.sprintf "Unknown manager: %s" s)
 395
 396 END
 397
 398 IFDEF SUMMARY THEN
 399
 400 let set_summary () =
 401    if !G.trace >= 2 then G.summary := true
 402
 403 END
 404
 405 let set_trace i =
 406    if !G.trace = 0 && i > 0 then Y.gmtime (G.version_string false);
 407    if !G.trace > 0 && i = 0 then Y.utime_stamp "at exit";
 408    G.trace := i;
 409 IFDEF SUMMARY THEN
 410    if i <= 1 then G.summary := false
 411 ELSE () END;
 412 IFDEF PREPROCESS THEN
 413    if i <= 1 then G.preprocess := false
 414 ELSE () END
 415
 416 let custom_exit () =
 417    if !G.trace >= 1 then Y.utime_stamp "at exit"
 418
 419 let process st name =
 420    let process = if !streaming then process_streaming else process_nostreaming in
 421    let input = type_of_input name in
 422    let ich = open_in name in
 423    let lexbuf = Lexing.from_channel ich in
 424    let st = process st lexbuf input in
 425    close_in ich;
 426    st, input
 427
 428 let main =
 429    let print_version () =
 430       let features = [
 431 (IFDEF LEXER THEN "LEXER" ELSE "" END);
 432 (IFDEF PARSER THEN "PARSER" ELSE "" END);
 433 (IFDEF TRACE THEN "TRACE" ELSE "" END);
 434 (IFDEF SUMMARY THEN "SUMMARY" ELSE "" END);
 435 (IFDEF EXPAND THEN "EXPAND" ELSE "" END);
 436 (IFDEF MANAGER THEN "MANAGER" ELSE "" END);
 437 (IFDEF OBJECTS THEN "OBJECTS" ELSE "" END);
 438 (IFDEF PREPROCESS THEN "PREPROCESS" ELSE "" END);
 439 (IFDEF QUOTE THEN "QUOTE" ELSE "" END);
 440 (IFDEF STAGE THEN "STAGE" ELSE "" END);
 441 (IFDEF TYPE THEN "TYPE" ELSE "" END);
 442 (IFDEF PROFV THEN "PROFV" ELSE "" END);
 443       ] in
 444       let map s = s <> "" in
 445       let features_string = KT.concat " " (KL.filter map features) in
 446       L.warn level (KP.sprintf "%s [%s]" (G.version_string true) features_string);
 447       exit 0
 448    in
 449    let set_hierarchy s =
 450       if H.set_graph s then () else
 451          L.warn level (KP.sprintf "Unknown type hierarchy: %s" s)
 452    in
 453    let set_kernel = function
 454       | "V3" -> G.kernel := G.V3
 455       | "V0" -> G.kernel := G.V0
 456       | s    -> L.warn level (KP.sprintf "Unknown kernel version: %s" s)
 457    in
 458    let clear_options () =
 459       G.clear (); H.clear ();
 460 IFDEF SUMMARY THEN
 461       O.clear_reductions ()
 462 ELSE () END;
 463       streaming := false;
 464    in
 465    let undefined opt () =
 466       L.warn level (KP.sprintf "%s was compiled without the support for option %s" (G.version_string true) opt);
 467       exit 0
 468    in
 469    let arg_undefined opt = Arg.Unit (undefined opt) in
 470    let process_file name =
 471       if !G.trace >= 2 then begin
 472          L.warn 1 (KP.sprintf "Processing file: %s" name);
 473          Y.utime_stamp "started"
 474       end;
 475       let base_name = Filename.chop_extension (Filename.basename name) in
 476       let cover = KF.concat !G.root base_name in
 477       G.cover := cover;
 478 IFDEF STAGE THEN
 479       if !G.stage <= 1 then G.kernel := G.V4;
 480 ELSE () END;
 481 IFDEF MANAGER THEN
 482       begin match !G.manager with
 483          | G.Coq    -> st := {!st with mst = Some (BA.open_out base_name)}
 484          | G.Matita -> st := {!st with mst = Some (BG.open_out base_name)}
 485          | G.LP1    -> st := {!st with mst = Some (BP.open_out_lp1 base_name)}
 486          | G.LP2    -> st := {!st with mst = Some (BP.open_out_lp2 base_name)}
 487          | G.TJ2    -> st := {!st with mst = Some (BP.open_out_tj2 base_name)}
 488          | G.TJ3    -> st := {!st with mst = Some (BP.open_out_tj3 base_name)}
 489          | G.Quiet  -> ()
 490       end
 491 ELSE () END;
 492       P.clear_marks ();
 493       let sst, input = process (refresh_status !st) name in
 494       st := begin match sst.mst with
 495          | None                -> sst
 496          | Some (_, close_out) -> close_out (); {sst with mst = None}
 497       end;
 498       if !G.trace >= 2 then Y.utime_stamp "processed";
 499 IFDEF SUMMARY THEN
 500       if !G.summary then begin
 501          AO.print_counters C.start !st.ac;
 502 IFDEF PREPROCESS THEN
 503          if !G.preprocess then AO.print_process_counters C.start !st.pst
 504 ELSE () END;
 505 IFDEF STAGE THEN
 506          if !G.stage >= 1 then print_counters !st G.V4;
 507          if !G.stage >= 2 then print_counters !st !G.kernel;
 508          if !G.stage >= 3 then O.print_reductions ()
 509 ELSE
 510          print_counters !st G.V4;
 511          print_counters !st !G.kernel;
 512          O.print_reductions ()
 513 END
 514       end
 515 ELSE () END
 516    in
 517    let help =
 518       "Usage: helena [ -LPVXdgilnoqtuxy01 | -Ts <number> | -MO <dir> | -p <file> | -ahkmr <string> | -be <age> ]* [ <file> ]*\n\n" ^
 519       "Trace levels: 0 just errors (default), 1 time stamps, 2 processed files, 3 processed objects,\n" ^
 520       "              4 typing information, 5 conversion information, 6 reduction information,\n" ^
 521       "              7 level disambiguation\n\n" ^
 522       "Stages: 0 parsing, 1 to intermediate, 2 to untrusted, 3 to trusted (default)\n\n" ^
 523       "Supported manages: \"ma2\" (Grafite NG), \"v8\" (Gallina 8), \"lp1\" \"lp2\" \"tj2\" (lambda-Prolog)\n"
 524    in
 525    let help_L = "         [lexer]     Show lexer debug information" in
 526    let help_M = "<dir>    [manager]   Set location of output directory (manager) to <dir> (default: current directory)" in
 527    let help_O = "<dir>    [output]    Set location of output directory (XML) to <dir> (default: current directory)" in
 528    let help_P = "         [parser]    Show parser debug information" in
 529    let help_T = "<number> [trace]     Set trace level (see above)" in
 530    let help_V = "         [version]   Show version information" in
 531    let help_X = "                     Clear options" in
 532
 533    let help_a = "<string> [alpha]     Set prefix of numeric identifiers (default: empty)" in
 534    let help_b = "<age>    [begin]     Begin trace at this global constant (default: first)" in
 535    let help_d = "         [data]      Show summary information (requires trace >= 2)" in
 536    let help_e = "<age>    [end]       End trace at this global constant (default: last)" in
 537    let help_g = "         [global]    Disable age-driven expansion of global definitions (default: enable)" in
 538    let help_h = "<string> [hierarchy] Set type hierarchy (default: \"Z1\")" in
 539    let help_i = "         [indexes]   Show local references by index" in
 540    let help_k = "<string> [kernel]    Set kernel version (default: \"V3\")" in
 541    let help_l = "         [layer]     Disambiguate binders layer (Automath)" in
 542    let help_m = "<string> [manager]   Export kernel entities for this manager (see above, default: no manager)" in
 543    let help_n = "         [names]     Show short constants (default: qualified constants)" in
 544    let help_o = "         [objects]   Export kernel entities (XML)" in
 545    let help_p = "<file>   [preamble]  Set preamble to this file (default: empty)" in
 546    let help_q = "         [quote]     Quote identifiers (default: disable)" in
 547    let help_r = "<string> [root]      Set initial segment of URI hierarchy (default: empty)" in
 548    let help_s = "<number> [stage]     Set translation stage (see above)" in
 549    let help_t = "         [type]      Type check (default: validate)" in
 550    let help_u = "         [upsilon]   Activate type comparison by sort inclusion (default: deactivate)" in
 551    let help_x = "         [extended]  Use extended applications (Automath)" in
 552    let help_y = "         [infinity]  Use ∞-abstractions in contexts" in
 553    let help_0 = "         [zero]      Preprocess source (Automath)" in
 554    let help_1 = "         [one]       parse files with streaming policy" in
 555    at_exit custom_exit;
 556    Arg.parse [
 557       ("-L", (IFDEF LEXER THEN Arg.Set G.debug_lexer ELSE arg_undefined "-L" END), help_L);
 558       ("-M", (IFDEF MANAGER THEN Arg.String ((:=) G.manager_dir) ELSE arg_undefined "-M" END), help_M);
 559       ("-O", (IFDEF OBJECTS THEN Arg.String ((:=) G.xdir) ELSE arg_undefined "-O" END), help_O);
 560       ("-P", (IFDEF PARSER THEN Arg.Set G.debug_parser ELSE arg_undefined "-P" END), help_P);
 561       ("-T", Arg.Int set_trace, help_T);
 562       ("-V", Arg.Unit print_version, help_V);
 563       ("-X", Arg.Unit clear_options, help_X);
 564       ("-a", Arg.String ((:=) G.alpha), help_a);
 565       ("-b", Arg.Int ((:=) G.first), help_b);
 566       ("-d", (IFDEF SUMMARY THEN Arg.Unit set_summary ELSE arg_undefined "-d" END), help_d);
 567       ("-e", Arg.Int ((:=) G.last), help_e);
 568       ("-g", (IFDEF EXPAND THEN Arg.Set G.expand ELSE arg_undefined "-g" END), help_g);
 569       ("-h", Arg.String set_hierarchy, help_h);
 570       ("-i", Arg.Set G.indexes, help_i);
 571       ("-k", Arg.String set_kernel, help_k);
 572       ("-l", Arg.Set G.cc, help_l);
 573       ("-m", (IFDEF MANAGER THEN Arg.String set_manager ELSE arg_undefined "-m" END), help_m);
 574       ("-n", Arg.Set G.short, help_n);
 575       ("-o", (IFDEF OBJECTS THEN Arg.Set G.export ELSE arg_undefined "-o" END), help_o);
 576       ("-p", (IFDEF MANAGER THEN Arg.String ((:=) G.preamble) ELSE arg_undefined "-p" END), help_p);
 577       ("-q", (IFDEF QUOTE THEN Arg.Set G.quote ELSE arg_undefined "-q" END), help_q);
 578       ("-r", Arg.String ((:=) G.root), help_r);
 579       ("-s", (IFDEF STAGE THEN Arg.Int ((:=) G.stage) ELSE arg_undefined "-s" END), help_s);
 580       ("-t", (IFDEF TYPE THEN Arg.Clear G.validate ELSE arg_undefined "-t" END), help_t);
 581       ("-u", Arg.Set G.si, help_u);
 582       ("-x", Arg.Set G.extended, help_x);
 583       ("-y", Arg.Set G.infinity, help_y);
 584       ("-0", (IFDEF PREPROCESS THEN Arg.Unit set_preprocess ELSE arg_undefined "-0" END), help_0);
 585       ("-1", Arg.Set streaming, help_1);
 586    ] process_file help