\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-module F = Filename
+module KF = Filename
module C = Cps
type uri_generator = string -> string
-type kernel = Crg | Brg | Bag
+type kernel = V4 | V3 | V0
-(* interface functions ******************************************************)
+IFDEF MANAGER THEN
-let version_string = "Helena 0.8.2 M - December 2014"
+type manager = Quiet
+ | Coq
+ | Matita
+ | LP1 (* elpi helena *)
+ | LP2 (* elpi helena *)
+ | TJ2 (* teyjus helena *)
+ | TJ3 (* teyjus helena *)
+ | PTS (* elpi pts *)
+ | LYP (* elpi lyp *)
-let stage = ref 3 (* stage *)
+END
-let trace = ref 0 (* trace level *)
-
-let summary = ref false (* log summary information *)
+(* interface functions ******************************************************)
-let xdir = ref "" (* directory for XML output *)
+let version_string b =
+ if b then "Helena 0.8.3 M (December 2017)"
+ else "Helena 0.8.3 M - December 2017"
-let kernel = ref Brg (* kernel type *)
+let kernel = ref V3 (* kernel type *)
let si = ref false (* use sort inclusion *)
let cc = ref false (* activate conversion constraints *)
-let expand = ref false (* always expand global definitions *)
-
let indexes = ref false (* show de Bruijn indexes *)
-let icm = ref 0 (* complexity measure of relocated terms *)
+let alpha = ref "" (* prefix of numeric identifiers *)
-let unquote = ref false (* do not quote identifiers when lexing *)
+let first = ref 0 (* begin trace here *)
-let debug_parser = ref false (* output parser debug information *)
+let last = ref max_int (* end trace here *)
+
+let restricted = ref true (* restricted applications *)
+
+let infinity = ref false (* use ∞-abstractions in contexts *)
+
+let short = ref false (* short global constants *)
+
+let cast = ref false (* anticipate cast *)
+
+let root = ref "" (* initial segment of URI hierarchy *)
+let trace = ref 0 (* trace level *)
+
+IFDEF LEXER THEN
let debug_lexer = ref false (* output lexer debug information *)
+END
-let ma_dir = ref "" (* directory for grafite output *)
+IFDEF PARSER THEN
+let debug_parser = ref false (* output parser debug information *)
+END
-let ma_preamble = ref "" (* location of grafite preamble file *)
+IFDEF TRACE THEN
+let ct = ref 0 (* current trace level *)
+END
-let alpha = ref "" (* prefix of numeric identifiers *)
+IFDEF SUMMARY THEN
+let summary = ref false (* log summary information *)
+END
+
+IFDEF EXPAND THEN
+let expand = ref false (* always expand global definitions *)
+END
+
+IFDEF MANAGER THEN
+let manager_dir = ref "" (* output directory for manager *)
+let manager = ref Quiet (* manager *)
+let preamble = ref "" (* preamble file for manager *)
+END
+
+IFDEF STAGE THEN
+let stage = ref 3 (* stage *)
+END
+
+IFDEF OBJECTS THEN
+let export = ref false (* export entities to XML *)
+let xdir = ref "" (* directory for XML output *)
+END
+
+IFDEF PREPROCESS THEN
+let preprocess = ref false (* preprocess source *)
+END
+
+IFDEF QUOTE THEN
+let quote = ref false (* quote identifiers when lexing *)
+END
+
+IFDEF TYPE THEN
+let validate = ref true (* validate vs. typecheck *)
+let icm = ref 0 (* complexity measure of relocated terms *)
+END
let kernel_id () =
let id = match !kernel with
- | Crg -> "crg"
- | Brg -> "brg"
- | Bag -> "bag"
+ | V4 -> "Environment"
+ | V3 -> "Environment_V3"
+ | V0 -> "Environment_V0"
in
let si = if !si then "_si" else "" in
- id ^ si
+ let rest = if !restricted then "" else "_x" in
+ id ^ si ^ rest
let get_baseuri () =
String.concat "/" ["ld:"; kernel_id (); !cover; "" ]
let get_mk_uri () =
let bu = get_baseuri () in
- fun s -> F.concat bu (s ^ ".ld")
+ fun s -> KF.concat bu (s ^ ".ld")
+
+IFDEF TRACE THEN
+let set_current_trace n =
+ ct := if !first <= n && n <= !last then !trace else 0
+END
let clear () =
- stage := 3; trace := 0; summary := false;
- xdir := ""; kernel := Brg; si := false; cover := "";
- expand := false; indexes := false; icm := 0; unquote := false;
- debug_parser := false; debug_lexer := false;
- ma_dir := ""; ma_preamble := ""
+ root := ""; first := 0; last := max_int;
+ kernel := V3; si := false; restricted := true; infinity := false; cast := false; cover := "";
+ indexes := false; short := false; trace := 0;
+ IFDEF LEXER THEN debug_lexer := false ELSE () END;
+ IFDEF PARSER THEN debug_parser := false ELSE () END;
+ IFDEF SUMMARY THEN summary := false ELSE () END;
+ IFDEF EXPAND THEN expand := false ELSE () END;
+ IFDEF MANAGER THEN manager_dir := ""; manager := Quiet; preamble := "" ELSE () END;
+ IFDEF STAGE THEN stage := 3 ELSE () END;
+ IFDEF OBJECTS THEN export := false; xdir := "" ELSE () END;
+ IFDEF PREPROCESS THEN preprocess := false ELSE () END;
+ IFDEF QUOTE THEN quote := false ELSE () END;
+ IFDEF TYPE THEN validate := true; icm := 0 ELSE () END