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 type manager = Quiet
  21              | Coq
  22              | Matita
  23              | LP1    (* newelpi *)
  24              | LP2    (* newelpi *)
  25              | TJ2    (* teyjus  *)
  26              | TJ3    (* teyjus  *)
  27
  28 (* interface functions ******************************************************)
  29
  30 let version_string = "Helena 0.8.3 M (June 2015)"
  31
  32 let stage = ref 3            (* stage *)
  33
  34 let trace = ref 0            (* trace level *)
  35
  36 let ct = ref 0               (* current trace level *)
  37
  38 let summary = ref false      (* log summary information *)
  39
  40 let export = ref false       (* export entities to XML *)
  41
  42 let xdir = ref ""            (* directory for XML output *)
  43
  44 let kernel = ref V3          (* kernel type *)
  45
  46 let si = ref false           (* use sort inclusion *)
  47
  48 let cover = ref ""           (* initial uri segment *)
  49
  50 let cc = ref false           (* activate conversion constraints *)
  51
  52 let expand = ref false       (* always expand global definitions *)
  53
  54 let indexes = ref false      (* show de Bruijn indexes *)
  55
  56 let icm = ref 0              (* complexity measure of relocated terms *)
  57
  58 let unquote = ref false      (* do not quote identifiers when lexing *)
  59
  60 let debug_parser = ref false (* output parser debug information *)
  61
  62 let debug_lexer = ref false  (* output lexer debug information *)
  63
  64 let manager_dir = ref ""     (* output directory for manager *)
  65
  66 let manager = ref Quiet      (* manager *)
  67
  68 let preamble = ref ""        (* preamble file for manager *)
  69
  70 let alpha = ref ""           (* prefix of numeric identifiers *)
  71
  72 let first = ref 0            (* begin trace here *)
  73
  74 let last = ref max_int       (* end trace here *)
  75
  76 let extended = ref false     (* extended applications *)
  77
  78 let infinity = ref false     (* use ∞-abstractions in contexts *)
  79
  80 let short = ref false        (* short global constants *)
  81
  82 let set_current_trace n =
  83    ct := if !first <= n && n <= !last then !trace else 0
  84
  85 let kernel_id () =
  86    let id = match !kernel with
  87       | V4 -> "Environment"
  88       | V3 -> "Environment_V3"
  89       | V0 -> "Environment_V0"
  90    in
  91    let si = if !si then "_si" else "" in
  92    let ext = if !extended then "_x" else "" in
  93    id ^ si ^ ext
  94
  95 let get_baseuri () =
  96    String.concat "/" ["ld:"; kernel_id (); !cover; "" ]
  97
  98 let get_mk_uri () =
  99    let bu = get_baseuri () in
 100    fun s -> KF.concat bu (s ^ ".ld")
 101
 102 let clear () =
 103    stage := 3; trace := 0; summary := false; export := false; first := 0; last := max_int;
 104    xdir := ""; kernel := V3; si := false; extended := false; infinity := false; cover := "";
 105    expand := false; indexes := false; icm := 0; unquote := false; short := false;
 106    debug_parser := false; debug_lexer := false;
 107    manager_dir := ""; manager := Quiet