we are optimizing the code by conditional compilation.

[helm.git] / helm / software / helena / src / common / options.ml

diff --git a/helm/software/helena/src/common/options.ml b/helm/software/helena/src/common/options.ml
index b2dc972925ac4e16a8c9ced43ec60bcd759b1120..415d0b02ab292207223363f988a146a642a97831 100644 (file)
--- a/helm/software/helena/src/common/options.ml
+++ b/helm/software/helena/src/common/options.ml
@@ -49,8 +49,6 @@ let cover = ref ""           (* initial uri segment *)
 
 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 *)
@@ -61,12 +59,6 @@ let debug_parser = ref false (* output parser debug information *)
 
 let debug_lexer = ref false  (* output lexer debug information *)
 
-let manager_dir = ref ""     (* output directory for manager *)
-
-let manager = ref Quiet      (* manager *)
-
-let preamble = ref ""        (* preamble file for manager *)
-
 let alpha = ref ""           (* prefix of numeric identifiers *)
 
 let first = ref 0            (* begin trace here *)
@@ -79,6 +71,20 @@ let infinity = ref false     (* use ∞-abstractions in contexts *)
 
 let short = ref false        (* short global constants *) 
 
+IFDEF EXPAND THEN
+let expand = ref false       (* always expand global definitions *)
+END
+
+IFDEF PREPROCESS THEN
+let preprocess = ref false   (* preprocess source *)
+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 set_current_trace n =
    ct := if !first <= n && n <= !last then !trace else 0
 
@@ -102,6 +108,8 @@ let get_mk_uri () =
 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;
+   indexes := false; icm := 0; unquote := false; short := false;
    debug_parser := false; debug_lexer := false;
-   manager_dir := ""; manager := Quiet
+   IFDEF EXPAND THEN expand := false ELSE () END;
+   IFDEF MANAGER THEN manager_dir := ""; manager := Quiet; preamble := "" ELSE () END;
+   IFDEF PREPROCESS THEN preprocess := false ELSE () END