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.
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_______________________________________________________________ *)
16 type uri_generator = string -> string
18 type kernel = V4 | V3 | V0
28 (* interface functions ******************************************************)
30 let version_string = "Helena 0.8.3 M (June 2015)"
32 let stage = ref 3 (* stage *)
34 let trace = ref 0 (* trace level *)
36 let ct = ref 0 (* current trace level *)
38 let summary = ref false (* log summary information *)
40 let export = ref false (* export entities to XML *)
42 let xdir = ref "" (* directory for XML output *)
44 let kernel = ref V3 (* kernel type *)
46 let si = ref false (* use sort inclusion *)
48 let cover = ref "" (* initial uri segment *)
50 let cc = ref false (* activate conversion constraints *)
52 let expand = ref false (* always expand global definitions *)
54 let indexes = ref false (* show de Bruijn indexes *)
56 let icm = ref 0 (* complexity measure of relocated terms *)
58 let unquote = ref false (* do not quote identifiers when lexing *)
60 let debug_parser = ref false (* output parser debug information *)
62 let debug_lexer = ref false (* output lexer debug information *)
64 let manager_dir = ref "" (* output directory for manager *)
66 let manager = ref Quiet (* manager *)
68 let preamble = ref "" (* preamble file for manager *)
70 let alpha = ref "" (* prefix of numeric identifiers *)
72 let first = ref 0 (* begin trace here *)
74 let last = ref max_int (* end trace here *)
76 let extended = ref false (* extended applications *)
78 let infinity = ref false (* use ∞-abstractions in contexts *)
80 let short = ref false (* short global constants *)
82 let set_current_trace n =
83 ct := if !first <= n && n <= !last then !trace else 0
86 let id = match !kernel with
88 | V3 -> "Environment_V3"
89 | V0 -> "Environment_V0"
91 let si = if !si then "_si" else "" in
92 let ext = if !extended then "_x" else "" in
96 String.concat "/" ["ld:"; kernel_id (); !cover; "" ]
99 let bu = get_baseuri () in
100 fun s -> KF.concat bu (s ^ ".ld")
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