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 F = Filename
  13 module C = Cps
  14
  15 type uri_generator = string -> string
  16
  17 type kernel = Crg | Brg | Bag
  18
  19 (* interface functions ******************************************************)
  20
  21 let version_string = "Helena 0.8.2 M - November 2014"
  22
  23 let stage = ref 3            (* stage *)
  24
  25 let trace = ref 0            (* trace level *)
  26
  27 let summary = ref false      (* log summary information *)
  28
  29 let xdir = ref ""            (* directory for XML output *)
  30
  31 let kernel = ref Brg         (* kernel type *)
  32
  33 let si = ref false           (* use sort inclusion *)
  34
  35 let cover = ref ""           (* initial uri segment *)
  36
  37 let cc = ref false           (* activate conversion constraints *)
  38
  39 let expand = ref false       (* always expand global definitions *)
  40
  41 let indexes = ref false      (* show de Bruijn indexes *)
  42
  43 let icm = ref 0              (* complexity measure of relocated terms *)
  44
  45 let unquote = ref false      (* do not quote identifiers when lexing *)
  46
  47 let debug_parser = ref false (* output parser debug information *)
  48
  49 let debug_lexer = ref false  (* output lexer debug information *)
  50
  51 let ma_preamble = ref ""     (* location of Matita preamble file *)
  52
  53 let kernel_id () =
  54    let id = match !kernel with
  55       | Crg -> "crg"
  56       | Brg -> "brg"
  57       | Bag -> "bag"
  58    in
  59    let si = if !si then "_si" else "" in
  60    id ^ si
  61
  62 let get_baseuri () =
  63    String.concat "/" ["ld:"; kernel_id (); !cover; "" ]
  64
  65 let get_mk_uri () =
  66    let bu = get_baseuri () in
  67    fun s -> F.concat bu (s ^ ".ld")
  68
  69 let clear () =
  70    stage := 3; trace := 0; summary := false;
  71    xdir := ""; kernel := Brg; si := false; cover := "";
  72    expand := false; indexes := false; icm := 0; unquote := false;
  73    debug_parser := false; debug_lexer := false;
  74    ma_preamble := ""