helm/software/helena/src/common/options.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
  14 module C = Cps
  15
  16 type uri_generator = string -> string
  17
  18 type kernel = V4 | V3 | V0
  19
  20 IFDEF MANAGER THEN
  21
  22 type manager = Quiet
  23              | Coq
  24              | Matita
  25              | LP1    (* elpi helena *)
  26              | LP2    (* elpi helena *)
  27              | TJ2    (* teyjus helena *)
  28              | TJ3    (* teyjus helena *)
  29 (*
  30              | CC0    (* elpi cic *)
  31 *)
  32              | LYP    (* elpi lyp *)
  33
  34 END
  35
  36 (* interface functions ******************************************************)
  37
  38 let version_string b =
  39    if b then "Helena 0.8.3 M (December 2017)"
  40    else "Helena 0.8.3 M - December 2017"
  41
  42 let kernel = ref V3          (* kernel type *)
  43
  44 let si = ref false           (* use sort inclusion *)
  45
  46 let cover = ref ""           (* initial uri segment *)
  47
  48 let cc = ref false           (* activate conversion constraints *)
  49
  50 let indexes = ref false      (* show de Bruijn indexes *)
  51
  52 let alpha = ref ""           (* prefix of numeric identifiers *)
  53
  54 let first = ref 0            (* begin trace here *)
  55
  56 let last = ref max_int       (* end trace here *)
  57
  58 let restricted = ref true    (* restricted applications *)
  59
  60 let infinity = ref false     (* use ∞-abstractions in contexts *)
  61
  62 let short = ref false        (* short global constants *)
  63
  64 let cast = ref false         (* anticipate cast *)
  65
  66 let root = ref ""            (* initial segment of URI hierarchy *)
  67
  68 let trace = ref 0            (* trace level *)
  69
  70 IFDEF LEXER THEN
  71 let debug_lexer = ref false  (* output lexer debug information *)
  72 END
  73
  74 IFDEF PARSER THEN
  75 let debug_parser = ref false (* output parser debug information *)
  76 END
  77
  78 IFDEF TRACE THEN
  79 let ct = ref 0               (* current trace level *)
  80 END
  81
  82 IFDEF SUMMARY THEN
  83 let summary = ref false      (* log summary information *)
  84 END
  85
  86 IFDEF EXPAND THEN
  87 let expand = ref false       (* always expand global definitions *)
  88 END
  89
  90 IFDEF MANAGER THEN
  91 let manager_dir = ref ""     (* output directory for manager *)
  92 let manager = ref Quiet      (* manager *)
  93 let preamble = ref ""        (* preamble file for manager *)
  94 END
  95
  96 IFDEF STAGE THEN
  97 let stage = ref 3            (* stage *)
  98 END
  99
 100 IFDEF OBJECTS THEN
 101 let export = ref false       (* export entities to XML *)
 102 let xdir = ref ""            (* directory for XML output *)
 103 END
 104
 105 IFDEF PREPROCESS THEN
 106 let preprocess = ref false   (* preprocess source *)
 107 END
 108
 109 IFDEF QUOTE THEN
 110 let quote = ref false        (* quote identifiers when lexing *)
 111 END
 112
 113 IFDEF TYPE THEN
 114 let validate = ref true      (* validate vs. typecheck *)
 115 let icm = ref 0              (* complexity measure of relocated terms *)
 116 END
 117
 118 let kernel_id () =
 119    let id = match !kernel with
 120       | V4 -> "Environment"
 121       | V3 -> "Environment_V3"
 122       | V0 -> "Environment_V0"
 123    in
 124    let si = if !si then "_si" else "" in
 125    let rest = if !restricted then "" else "_x" in
 126    id ^ si ^ rest
 127
 128 let get_baseuri () =
 129    String.concat "/" ["ld:"; kernel_id (); !cover; "" ]
 130
 131 let get_mk_uri () =
 132    let bu = get_baseuri () in
 133    fun s -> KF.concat bu (s ^ ".ld")
 134
 135 IFDEF TRACE THEN
 136 let set_current_trace n =
 137    ct := if !first <= n && n <= !last then !trace else 0
 138 END
 139
 140 let clear () =
 141    root := ""; first := 0; last := max_int;
 142    kernel := V3; si := false; restricted := true; infinity := false; cast := false; cover := "";
 143    indexes := false; short := false; trace := 0;
 144    IFDEF LEXER THEN debug_lexer := false ELSE () END;
 145    IFDEF PARSER THEN debug_parser := false ELSE () END;
 146    IFDEF SUMMARY THEN summary := false ELSE () END;
 147    IFDEF EXPAND THEN expand := false ELSE () END;
 148    IFDEF MANAGER THEN manager_dir := ""; manager := Quiet; preamble := "" ELSE () END;
 149    IFDEF STAGE THEN stage := 3 ELSE () END;
 150    IFDEF OBJECTS THEN export := false; xdir := "" ELSE () END;
 151    IFDEF PREPROCESS THEN preprocess := false ELSE () END;
 152    IFDEF QUOTE THEN quote := false ELSE () END;
 153    IFDEF TYPE THEN validate := true; icm := 0 ELSE () END