From 040c8158f327a3091c45295e91aaed2dedc137cb Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 14 Jul 2018 20:34:18 +0200 Subject: [PATCH] updated xoa and predefined virtuals MIME-Version: 1.0 Content-Type: text/plain; charset=utf8 Content-Transfer-Encoding: 8bit + xoa: existing decentralized files are not overwritten by default + predefined virtuals: an addition for use in λδ --- matita/components/binaries/xoa/ast.ml | 4 +- matita/components/binaries/xoa/engine.ml | 54 ++++++++++++------------ matita/components/binaries/xoa/lib.ml | 17 ++++++-- matita/components/binaries/xoa/lib.mli | 2 + matita/components/binaries/xoa/xoa.ml | 19 ++++++--- matita/matita/predefined_virtuals.ml | 2 +- 6 files changed, 58 insertions(+), 40 deletions(-) diff --git a/matita/components/binaries/xoa/ast.ml b/matita/components/binaries/xoa/ast.ml index 422855240..42b4034c1 100644 --- 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 fa4b471fb..baf460c09 100644 --- 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 573e0ebfb..ec9ec81d2 100644 --- 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 756d7478c..0c81d2425 100644 --- 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 d6f0bca0d..219b90660 100644 --- 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 | ]*\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 9c1715d39..6dd729c31 100644 --- a/matita/matita/predefined_virtuals.ml +++ b/matita/matita/predefined_virtuals.ml @@ -1515,7 +1515,7 @@ let predefined_classes = [ ["="; "≝"; "≡"; "≘"; "≗"; "≐"; "≑"; "≛"; "≚"; "≙"; "⌆"; "⧦"; "⊜"; "≋"; "⩳"; "≅"; "⩬"; "≂"; "≃"; "≈"; ]; ["→"; "↦"; "⇝"; "⤞"; "⇾"; "⤍"; "⤏"; "⤳"; ] ; ["⇒"; "⤇"; "➾"; "⇨"; "➡"; "⬈"; "➤"; "➸"; "⇉"; "⥰"; ] ; - ["^"; "↑"; ] ; + ["^"; "↑"; "⇡"; ] ; ["⇑"; "⇧"; "⬆"; ] ; ["⇓"; "⇩"; "⬇"; "⬊"; "➷"; ] ; ["⇕"; "⇳"; "⬍"; "↕"; ]; -- 2.39.2