X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fcommon%2Foptions.ml;h=71e55ececb796ea00dbfe30c05d5b51a696ee5e4;hb=88977b2d546e547e23b046792fe2ad8f6ff192a4;hp=ffef0796ee9292150124e438027f16fe467a00ac;hpb=67686e04702688cc822e809e5168f765bf69d7cb;p=helm.git

diff --git a/helm/software/helena/src/common/options.ml b/helm/software/helena/src/common/options.ml
index ffef0796e..71e55ecec 100644
--- a/helm/software/helena/src/common/options.ml
+++ b/helm/software/helena/src/common/options.ml
@@ -17,62 +17,101 @@ type uri_generator = string -> string
 
 type kernel = V4 | V3 | V0
 
+IFDEF MANAGER THEN
+
 type manager = Quiet
              | Coq
              | Matita
-             | ELPI1
-             | ELPI2
+             | LP1    (* elpi helena *)
+             | LP2    (* elpi helena *)
+             | TJ2    (* teyjus helena *)
+             | TJ3    (* teyjus helena *)
+             | CC0    (* elpi cic *)
+             | LYP    (* elpi lyp *)
+
+END
 
 (* interface functions ******************************************************)
 
-let version_string = "Helena 0.8.2 M (June 2015)"
+let version_string b =
+   if b then "Helena 0.8.3 M (December 2017)"
+   else "Helena 0.8.3 M - December 2017"
 
-let stage = ref 3            (* stage *)
+let kernel = ref V3          (* kernel type *)
 
-let trace = ref 0            (* trace level *)
+let si = ref false           (* use sort inclusion *)
 
-let ct = ref 0               (* current trace level *)
+let cover = ref ""           (* initial uri segment *)
 
-let summary = ref false      (* log summary information *)
+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
 
+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
 
-let alpha = ref ""           (* prefix of numeric identifiers *)
+IFDEF STAGE THEN
+let stage = ref 3            (* stage *)
+END
 
-let first = ref 0            (* begin trace here *)
+IFDEF OBJECTS THEN
+let export = ref false       (* export entities to XML *)
+let xdir = ref ""            (* directory for XML output *)
+END
 
-let last = ref max_int       (* end trace here *) 
+IFDEF PREPROCESS THEN
+let preprocess = ref false   (* preprocess source *)
+END
 
-let extended = ref false     (* extended applications *) 
+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
@@ -81,8 +120,8 @@ let kernel_id () =
       | 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; "" ]
@@ -91,9 +130,22 @@ let get_mk_uri () =
    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; first := 0; last := max_int;
-   xdir := ""; kernel := V3; si := false; extended := false; cover := ""; 
-   expand := false; indexes := false; icm := 0; unquote := 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