xoa updated

a dependence from matita removed
optional generation of separated objects (this should be the default)

diff --git a/matita/components/binaries/xoa/lib.ml b/matita/components/binaries/xoa/lib.ml
index e6e203e62738d111c253ac6c311afcd3cc8c13df..573e0ebfb14a8bb9d5125d199071e82d02897e47 100644 (file)
--- a/matita/components/binaries/xoa/lib.ml
+++ b/matita/components/binaries/xoa/lib.ml
@@ -35,7 +35,6 @@ let print_comment och =
 
 let open_out preamble name =
    let path = [
-      R.get_string "matita.rt_base_dir"; 
       R.get_string "xoa.output_dir"; 
       name
    ] in

diff --git a/matita/components/binaries/xoa/xoa.ml b/matita/components/binaries/xoa/xoa.ml
index e4e0e7c69f17bcbca0b0b6dd7b19f0d6711c6d46..d6f0bca0d49fa252af44a588ab51010c53176279 100644 (file)
--- a/matita/components/binaries/xoa/xoa.ml
+++ b/matita/components/binaries/xoa/xoa.ml
@@ -9,39 +9,70 @@
      \ /   This software is distributed as is, NO WARRANTY.     
       V_______________________________________________________________ *)
 
-module G = Arg
-
 module R = Helm_registry
 
 module L = Lib
 module A = Ast
-module E = Engine 
+module E = Engine
+
+let separate = ref false
+
+let clear () =
+   separate := false;
+   R.clear ()
 
 let unm_ex s =
    Scanf.sscanf s "%u %u" A.mk_exists
 
 let unm_or s =
-   Scanf.sscanf s "%u" A.mk_or 
+   Scanf.sscanf s "%u" A.mk_or
 
 let unm_and s =
-   Scanf.sscanf s "%u" A.mk_and 
+   Scanf.sscanf s "%u" A.mk_and
 
-let process conf =
+let process_centralized conf =
    let preamble = L.get_preamble conf in
    if R.has "xoa.objects" && R.has "xoa.notations" then begin
       let ooch = L.open_out preamble (R.get_string "xoa.objects") in
       let noch = L.open_out preamble (R.get_string "xoa.notations") in
-      List.iter (L.out_include ooch) (R.get_list R.string "xoa.include");   
-      L.out_include ooch (R.get_string "xoa.notations" ^ ".ma");      
+      List.iter (L.out_include ooch) (R.get_list R.string "xoa.include");
+      L.out_include ooch (R.get_string "xoa.notations" ^ ".ma");
       List.iter (E.generate ooch noch) (R.get_list unm_ex "xoa.ex");
       List.iter (E.generate ooch noch) (R.get_list unm_or "xoa.or");
       List.iter (E.generate ooch noch) (R.get_list unm_and "xoa.and");
       close_out noch; close_out ooch
    end
 
+let generate (p, o, n) = function
+   | A.Exists (c, v) as d ->
+      let oname = Printf.sprintf "%s/ex_%u_%u" o c v in
+      let nname = Printf.sprintf "%s/ex_%u_%u" n c v in
+      let ooch = L.open_out p oname in
+      let noch = L.open_out p nname in
+      List.iter (L.out_include ooch) (R.get_list R.string "xoa.include");
+      L.out_include ooch (nname ^ ".ma");
+      E.generate ooch noch d;
+      close_out noch; close_out ooch
+   | A.Or c          -> ()
+   | A.And c         -> ()
+
+let process_distributed conf =
+   let preamble = L.get_preamble conf in
+   if R.has "xoa.objects" && R.has "xoa.notations" then begin
+      let st = preamble, R.get_string "xoa.objects", R.get_string "xoa.notations" in
+      List.iter (generate st) (R.get_list unm_ex "xoa.ex");
+      List.iter (generate st) (R.get_list unm_or "xoa.or");
+      List.iter (generate st) (R.get_list unm_and "xoa.and");
+   end
+
+let process conf =
+   if !separate then process_distributed conf else process_centralized conf
+
 let _ =
-   let help = "Usage: xoa [ -X | <configuration file> ]*\n" in
-   let help_X  = " Clear configuration" in   
+   let help = "Usage: xoa [ -Xs | <configuration file> ]*\n" in
+   let help_X  = " Clear configuration" in
+   let help_s  = " Generate separate objects" in
    Arg.parse [
-      "-X" , G.Unit R.clear, help_X;
+      "-X", Arg.Unit clear, help_X;
+      "-s", Arg.Set separate, help_s;
    ] process help