when sort inclusion is enabled, we can produce conversion constraints in xml

[helm.git] / helm / software / lambda-delta / src / common / options.ml

diff --git a/helm/software/lambda-delta/src/common/options.ml b/helm/software/lambda-delta/src/common/options.ml
index d9783c76623a62fcfa28d2f8b738c03d433df709..c133bed7c1ece2954816935b5c2bf63ae485ee51 100644 (file)
--- a/helm/software/lambda-delta/src/common/options.ml
+++ b/helm/software/lambda-delta/src/common/options.ml
@@ -13,30 +13,49 @@ module C = Cps
 
 type uri_generator = string -> string
 
+type kernel = Crg | Brg | Bag
+
 (* interface functions ******************************************************)
 
-let indexes = ref false      (* show de Bruijn indexes *)
+let xdir = ref ""
 
-let expand = ref false       (* always expand global definitions *)
+let kernel = ref Brg
 
 let si = ref false           (* use sort inclusion *)
 
-let unquote = ref false      (* do not quote identifiers when lexing *)
+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 *)
 
-let cover = ref ""           (* initial uri segment *)
+let unquote = ref false      (* do not quote identifiers when lexing *)
 
 let debug_parser = ref false (* output parser debug information *)
 
 let debug_lexer = ref false  (* output lexer debug information *)
 
-let mk_uri = ref (fun _ _ -> C.err : bool -> string -> uri_generator) 
+let kernel_id () = 
+   let id = match !kernel with
+      | Crg -> "crg"
+      | Brg -> "brg"
+      | Bag -> "bag"
+   in
+   let si = if !si then "-si" else "" in
+   id ^ si
+
+let get_baseuri () =
+   String.concat "/" ["ld:"; kernel_id (); !cover ]
 
 let get_mk_uri () =
-   !mk_uri !si !cover
+   let bu = get_baseuri () in
+   fun s -> bu ^ "/" ^ s ^ ".ld"
 
 let clear () =
-   expand := false; si := false; cover := ""; indexes := false; icm := 0;
-   debug_parser := false; debug_lexer := false;
-   mk_uri := fun _ _ -> C.err 
+   xdir := ""; kernel := Brg; si := false; cover := ""; 
+   expand := false; indexes := false; icm := 0; unquote := false;
+   debug_parser := false; debug_lexer := false