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 C = Cps
  13
  14 type uri_generator = string -> string
  15
  16 type kernel = Crg | Brg | Bag
  17
  18 (* interface functions ******************************************************)
  19
  20 let xdir = ref ""
  21
  22 let kernel = ref Brg
  23
  24 let si = ref false           (* use sort inclusion *)
  25
  26 let cover = ref ""           (* initial uri segment *)
  27
  28 let cc = ref false           (* activate conversion constraints *)
  29
  30 let expand = ref false       (* always expand global definitions *)
  31
  32 let indexes = ref false      (* show de Bruijn indexes *)
  33
  34 let icm = ref 0              (* complexity measure of relocated terms *)
  35
  36 let unquote = ref false      (* do not quote identifiers when lexing *)
  37
  38 let debug_parser = ref false (* output parser debug information *)
  39
  40 let debug_lexer = ref false  (* output lexer debug information *)
  41
  42 let kernel_id () =
  43    let id = match !kernel with
  44       | Crg -> "crg"
  45       | Brg -> "brg"
  46       | Bag -> "bag"
  47    in
  48    let si = if !si then "-si" else "" in
  49    id ^ si
  50
  51 let get_baseuri () =
  52    String.concat "/" ["ld:"; kernel_id (); !cover ]
  53
  54 let get_mk_uri () =
  55    let bu = get_baseuri () in
  56    fun s -> bu ^ "/" ^ s ^ ".ld"
  57
  58 let clear () =
  59    xdir := ""; kernel := Brg; si := false; cover := "";
  60    expand := false; indexes := false; icm := 0; unquote := false;
  61    debug_parser := false; debug_lexer := false