type kernel = V4 | V3 | V0
+IFDEF MANAGER THEN
+
type manager = Quiet
| Coq
| Matita
- | LP1 (* newelpi *)
- | LP2 (* newelpi *)
- | TJ2 (* teyjus *)
- | TJ3 (* teyjus *)
+ | LP1 (* elpi helena *)
+ | LP2 (* elpi helena *)
+ | TJ2 (* teyjus helena *)
+ | TJ3 (* teyjus helena *)
+ | PTS (* elpi pts *)
+ | LYP (* elpi lyp *)
-(* interface functions ******************************************************)
+END
-let version_string = "Helena 0.8.3 M (June 2015)"
+(* interface functions ******************************************************)
-let stage = ref 3 (* stage *)
+let version_string b =
+ if b then "Helena 0.8.3 M (December 2017)"
+ else "Helena 0.8.3 M - December 2017"
-let trace = ref 0 (* trace level *)
+let kernel = ref V3 (* kernel type *)
-let ct = ref 0 (* current trace level *)
+let si = ref false (* use sort inclusion *)
-let summary = ref false (* log summary information *)
+let cover = ref "" (* initial uri segment *)
-let export = ref false (* export entities to XML *)
+let cc = ref false (* activate conversion constraints *)
-let xdir = ref "" (* directory for XML output *)
+let indexes = ref false (* show de Bruijn indexes *)
-let kernel = ref V3 (* kernel type *)
+let alpha = ref "" (* prefix of numeric identifiers *)
-let si = ref false (* use sort inclusion *)
+let first = ref 0 (* begin trace here *)
-let cover = ref "" (* initial uri segment *)
+let last = ref max_int (* end trace here *)
-let cc = ref false (* activate conversion constraints *)
+let restricted = ref true (* restricted applications *)
-let expand = ref false (* always expand global definitions *)
+let infinity = ref false (* use ∞-abstractions in contexts *)
-let indexes = ref false (* show de Bruijn indexes *)
+let short = ref false (* short global constants *)
-let icm = ref 0 (* complexity measure of relocated terms *)
+let cast = ref false (* anticipate cast *)
-let unquote = ref false (* do not quote identifiers when lexing *)
+let root = ref "" (* initial segment of URI hierarchy *)
-let debug_parser = ref false (* output parser debug information *)
+let trace = ref 0 (* trace level *)
+IFDEF LEXER THEN
let debug_lexer = ref false (* output lexer debug information *)
+END
-let manager_dir = ref "" (* output directory for manager *)
+IFDEF PARSER THEN
+let debug_parser = ref false (* output parser debug information *)
+END
-let manager = ref Quiet (* manager *)
+IFDEF TRACE THEN
+let ct = ref 0 (* current trace level *)
+END
-let preamble = ref "" (* preamble file for manager *)
+IFDEF SUMMARY THEN
+let summary = ref false (* log summary information *)
+END
-let alpha = ref "" (* prefix of numeric identifiers *)
+IFDEF EXPAND THEN
+let expand = ref false (* always expand global definitions *)
+END
-let first = ref 0 (* begin trace here *)
+IFDEF MANAGER THEN
+let manager_dir = ref "" (* output directory for manager *)
+let manager = ref Quiet (* manager *)
+let preamble = ref "" (* preamble file for manager *)
+END
-let last = ref max_int (* end trace here *)
+IFDEF STAGE THEN
+let stage = ref 3 (* stage *)
+END
-let extended = ref false (* extended applications *)
+IFDEF OBJECTS THEN
+let export = ref false (* export entities to XML *)
+let xdir = ref "" (* directory for XML output *)
+END
-let infinity = ref false (* use ∞-abstractions in contexts *)
+IFDEF PREPROCESS THEN
+let preprocess = ref false (* preprocess source *)
+END
-let short = ref false (* short global constants *)
+IFDEF QUOTE THEN
+let quote = ref false (* quote identifiers when lexing *)
+END
-let set_current_trace n =
- ct := if !first <= n && n <= !last then !trace else 0
+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
| V0 -> "Environment_V0"
in
let si = if !si then "_si" else "" in
- let ext = if !extended then "_x" else "" in
- id ^ si ^ ext
+ let rest = if !restricted then "" else "_x" in
+ id ^ si ^ rest
let get_baseuri () =
String.concat "/" ["ld:"; kernel_id (); !cover; "" ]
let bu = get_baseuri () in
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; export := false; first := 0; last := max_int;
- xdir := ""; kernel := V3; si := false; extended := false; infinity := false; cover := "";
- expand := false; indexes := false; icm := 0; unquote := false; short := false;
- debug_parser := false; debug_lexer := false;
- manager_dir := ""; manager := Quiet
+ 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