updated xoa and predefined virtuals

+ xoa: existing decentralized files are not overwritten by default
+ predefined virtuals: an addition for use in λδ

diff --git a/matita/components/binaries/xoa/ast.ml b/matita/components/binaries/xoa/ast.ml
index 42285524036073349c2ba7c1c67c93bba14304c7..42b4034c12174aa1553b9e42c0fc992b770f76e1 100644 (file)
--- a/matita/components/binaries/xoa/ast.ml
+++ b/matita/components/binaries/xoa/ast.ml
@@ -19,6 +19,6 @@ type directive = Exists of arity * subarity
 
 let mk_exists c v = Exists (c, v)
 
-let mk_or c = Or c 
+let mk_or c = Or c
 
-let mk_and c = And c 
+let mk_and c = And c

diff --git a/matita/components/binaries/xoa/engine.ml b/matita/components/binaries/xoa/engine.ml
index fa4b471fb69742fef505276f7760c90546483bba..baf460c0929c8c0a49ed2d4dc5e188ed3b57da32 100644 (file)
--- a/matita/components/binaries/xoa/engine.ml
+++ b/matita/components/binaries/xoa/engine.ml
@@ -31,7 +31,7 @@ let void_iter f n =
 let mk_exists ooch noch c v =
    let description = "multiple existental quantifier" in
    let prec = "non associative with precedence 20\n" in
-   let name s = 
+   let name s =
       if v = 1 then P.sprintf "%s%u" s c else P.sprintf "%s%u_%u" s c v
    in
    let o_name = name "ex" in
@@ -39,40 +39,40 @@ let mk_exists ooch noch c v =
       if v = 1 then "'Ex" else P.sprintf "'Ex%u" v
    in
    let set n      = P.sprintf "A%u" (v - n) in
-   let set_list   = string_iter "," set v in   
+   let set_list   = string_iter "," set v in
    let set_type   = string_iter "→" set v in
-      
+
    let ele n      = P.sprintf "x%u" (v - n) in
    let ele_list   = string_iter "," ele v in
    let ele_seq    = string_iter " " ele v in
-   
-   let pre n      = P.sprintf "P%u" (c - n) in   
+
+   let pre n      = P.sprintf "P%u" (c - n) in
    let pre_list   = string_iter "," pre c in
-   let pre_seq    = string_iter " " pre c in 
-   let pre_appl n = P.sprintf "%s %s" (pre n) ele_seq in 
+   let pre_seq    = string_iter " " pre c in
+   let pre_appl n = P.sprintf "%s %s" (pre n) ele_seq in
    let pre_type   = string_iter " → " pre_appl c in
 
    let qm n       = "?" in
-   let qm_set     = string_iter " " qm v in 
-   let qm_pre     = string_iter " " qm c in 
+   let qm_set     = string_iter " " qm v in
+   let qm_pre     = string_iter " " qm c in
 
    let id n       = P.sprintf "ident x%u" (v - n) in
-   let id_list    = string_iter " , " id v in 
+   let id_list    = string_iter " , " id v in
 
    let term n     = P.sprintf "term 19 P%u" (c - n) in
-   let term_conj  = string_iter " break & " term c in 
+   let term_conj  = string_iter " break & " term c in
 
    let abst b n   = let xty = if b then P.sprintf ":$T%u" (v - n) else "" in
                     P.sprintf "λ${ident x%u}%s" (v - n) xty in
 
-   let abst_clo b = string_iter "." (abst b) v in 
+   let abst_clo b = string_iter "." (abst b) v in
 
-   let full b n   = P.sprintf "(%s.$P%u)" (abst_clo b) (c - n) in 
+   let full b n   = P.sprintf "(%s.$P%u)" (abst_clo b) (c - n) in
    let full_seq b = string_iter " " (full b) c in
 
    P.fprintf ooch "(* %s (%u, %u) *)\n\n" description c v;
 
-   P.fprintf ooch "inductive %s (%s:Type[0]) (%s:%s→Prop) : Prop ≝\n" 
+   P.fprintf ooch "inductive %s (%s:Type[0]) (%s:%s→Prop) : Prop ≝\n"
       o_name set_list pre_list set_type;
    P.fprintf ooch "   | %s_intro: ∀%s. %s → %s %s %s\n.\n\n"
       o_name ele_list pre_type o_name qm_set qm_pre;
@@ -95,17 +95,17 @@ let mk_or ooch noch c =
    let o_name = name "or" in
    let i_name = "'Or" in
 
-   let pre n      = P.sprintf "P%u" (c - n) in   
+   let pre n      = P.sprintf "P%u" (c - n) in
    let pre_list   = string_iter "," pre c in
-   let pre_seq    = string_iter " " pre c in 
+   let pre_seq    = string_iter " " pre c in
 
    let qm n       = "?" in
-   let qm_pre     = string_iter " " qm c in 
+   let qm_pre     = string_iter " " qm c in
 
    let term n     = P.sprintf "term 29 P%u" (c - n) in
-   let term_disj  = string_iter " break | " term c in 
+   let term_disj  = string_iter " break | " term c in
 
-   let par n     = P.sprintf "$P%u" (c - n) in 
+   let par n     = P.sprintf "$P%u" (c - n) in
    let par_seq   = string_iter " " par c in
 
    let mk_con n   = P.fprintf ooch "   | %s_intro%u: %s → %s %s\n"
@@ -114,7 +114,7 @@ let mk_or ooch noch c =
 
    P.fprintf ooch "(* %s (%u) *)\n\n" description c;
 
-   P.fprintf ooch "inductive %s (%s:Prop) : Prop ≝\n" 
+   P.fprintf ooch "inductive %s (%s:Prop) : Prop ≝\n"
       o_name pre_list;
    void_iter mk_con c;
    P.fprintf ooch ".\n\n";
@@ -134,23 +134,23 @@ let mk_and ooch noch c =
    let o_name = name "and" in
    let i_name = "'And" in
 
-   let pre n      = P.sprintf "P%u" (c - n) in   
+   let pre n      = P.sprintf "P%u" (c - n) in
    let pre_list   = string_iter "," pre c in
-   let pre_type   = string_iter " → " pre c in   
-   let pre_seq    = string_iter " " pre c in 
+   let pre_type   = string_iter " → " pre c in
+   let pre_seq    = string_iter " " pre c in
 
    let qm n       = "?" in
-   let qm_pre     = string_iter " " qm c in 
+   let qm_pre     = string_iter " " qm c in
 
    let term n     = P.sprintf "term 34 P%u" (c - n) in
-   let term_conj  = string_iter " break & " term c in 
+   let term_conj  = string_iter " break & " term c in
 
-   let par n     = P.sprintf "$P%u" (c - n) in 
+   let par n     = P.sprintf "$P%u" (c - n) in
    let par_seq   = string_iter " " par c in
 
    P.fprintf ooch "(* %s (%u) *)\n\n" description c;
 
-   P.fprintf ooch "inductive %s (%s:Prop) : Prop ≝\n" 
+   P.fprintf ooch "inductive %s (%s:Prop) : Prop ≝\n"
       o_name pre_list;
    P.fprintf ooch "   | %s_intro: %s → %s %s\n.\n\n"
       o_name pre_type o_name qm_pre;

diff --git a/matita/components/binaries/xoa/lib.ml b/matita/components/binaries/xoa/lib.ml
index 573e0ebfb14a8bb9d5125d199071e82d02897e47..ec9ec81d2910ad1c57e15e2d7413411892ef7176 100644 (file)
--- a/matita/components/binaries/xoa/lib.ml
+++ b/matita/components/binaries/xoa/lib.ml
@@ -9,9 +9,10 @@
      \ /   This software is distributed as is, NO WARRANTY.     
       V_______________________________________________________________ *)
 
-module F   = Filename
+module F = Filename
+module K = Sys
 
-module R   = Helm_registry
+module R = Helm_registry
 
 let template = "matita.ma.templ"
 
@@ -33,12 +34,20 @@ let print_comment och =
    let stars = String.make (30 - String.length myself) '*' in
    Printf.fprintf och "(* This file was generated by %s: do not edit %s*)\n\n" myself stars
 
+let exists_out name =
+   let path = [
+      R.get_string "xoa.output_dir";
+      name
+   ] in
+   let name = List.fold_left F.concat "" path in
+   K.file_exists (name ^ ".ma")
+
 let open_out preamble name =
    let path = [
-      R.get_string "xoa.output_dir"; 
+      R.get_string "xoa.output_dir";
       name
    ] in
-   let name = List.fold_left F.concat "" path in 
+   let name = List.fold_left F.concat "" path in
    let och = open_out (name ^ ".ma") in
    copy_preamble preamble och; print_comment och;
    och

diff --git a/matita/components/binaries/xoa/lib.mli b/matita/components/binaries/xoa/lib.mli
index 756d7478c9c50be5fa6a7920484dae6052f0438c..0c81d24253c3a2784366d39de43a37070cfcc23b 100644 (file)
--- a/matita/components/binaries/xoa/lib.mli
+++ b/matita/components/binaries/xoa/lib.mli
@@ -11,6 +11,8 @@
 
 val get_preamble: string -> string
 
+val exists_out: string -> bool
+
 val open_out: string -> string -> out_channel
 
 val out_include: out_channel -> string -> unit

diff --git a/matita/components/binaries/xoa/xoa.ml b/matita/components/binaries/xoa/xoa.ml
index d6f0bca0d49fa252af44a588ab51010c53176279..219b906605327240452fba5c3638e34e2dc482b1 100644 (file)
--- a/matita/components/binaries/xoa/xoa.ml
+++ b/matita/components/binaries/xoa/xoa.ml
@@ -15,9 +15,11 @@ module L = Lib
 module A = Ast
 module E = Engine
 
+let incremental = ref true
 let separate = ref false
 
 let clear () =
+   incremental := true;
    separate := false;
    R.clear ()
 
@@ -47,12 +49,15 @@ 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
+      if !incremental && L.exists_out oname && L.exists_out nname then () else
+      begin
+         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
+      end
    | A.Or c          -> ()
    | A.And c         -> ()
 
@@ -72,7 +77,9 @@ let _ =
    let help = "Usage: xoa [ -Xs | <configuration file> ]*\n" in
    let help_X  = " Clear configuration" in
    let help_s  = " Generate separate objects" in
+   let help_u  = " Update existing separate files" in
    Arg.parse [
       "-X", Arg.Unit clear, help_X;
       "-s", Arg.Set separate, help_s;
+      "-u", Arg.Clear incremental, help_u;
    ] process help

diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml
index 9c1715d39135b5c26eb5522aeb4f286f1ca6c401..6dd729c310f5a8453e6dec587a97736424387ea6 100644 (file)
--- a/matita/matita/predefined_virtuals.ml
+++ b/matita/matita/predefined_virtuals.ml
@@ -1515,7 +1515,7 @@ let predefined_classes = [
  ["="; "≝"; "≡"; "≘"; "≗"; "≐"; "≑"; "≛"; "≚"; "≙"; "⌆"; "⧦"; "⊜"; "≋"; "⩳"; "≅"; "⩬"; "≂"; "≃"; "≈"; ];  
  ["→"; "↦"; "⇝"; "⤞"; "⇾"; "⤍"; "⤏"; "⤳"; ] ;
  ["⇒"; "⤇"; "➾"; "⇨"; "➡"; "⬈"; "➤"; "➸"; "⇉"; "⥰"; ] ;
- ["^"; "↑"; ] ;
+ ["^"; "↑"; "⇡"; ] ;
  ["⇑"; "⇧"; "⬆"; ] ; 
  ["⇓"; "⇩"; "⬇"; "⬊"; "➷"; ] ;
  ["⇕"; "⇳"; "⬍"; "↕"; ];