X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fbinaries%2Fxoa%2Fengine.ml;h=baf460c0929c8c0a49ed2d4dc5e188ed3b57da32;hb=040c8158f327a3091c45295e91aaed2dedc137cb;hp=bc9a8be5da1f3935bf175134251ce4b4cd45154a;hpb=4de2411d2cecf21630f6675f58e64f8ec6de9b60;p=helm.git diff --git a/matita/components/binaries/xoa/engine.ml b/matita/components/binaries/xoa/engine.ml index bc9a8be5d..baf460c09 100644 --- a/matita/components/binaries/xoa/engine.ml +++ b/matita/components/binaries/xoa/engine.ml @@ -30,47 +30,49 @@ let void_iter f n = let mk_exists ooch noch c v = let description = "multiple existental quantifier" in - let in_prec = "non associative with precedence 20\n" in -(* let out_prec = "right associative with precedence 20\n" in *) - let name s = P.sprintf "%s%u_%u" s c v in + let prec = "non associative with precedence 20\n" in + 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 - let i_name = "'Ex" in - + let i_name = + 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; @@ -81,29 +83,29 @@ let mk_exists ooch noch c v = P.fprintf noch "(* %s (%u, %u) *)\n\n" description c v; P.fprintf noch "notation > \"hvbox(∃∃ %s break . %s)\"\n %s for @{ %s %s }.\n\n" - id_list term_conj in_prec i_name (full_seq false); + id_list term_conj prec i_name (full_seq false); P.fprintf noch "notation < \"hvbox(∃∃ %s break . %s)\"\n %s for @{ %s %s }.\n\n" - id_list term_conj in_prec i_name (full_seq true) + id_list term_conj prec i_name (full_seq true) let mk_or ooch noch c = let description = "multiple disjunction connective" in - let in_prec = "non associative with precedence 30\n" in + let prec = "non associative with precedence 30\n" in let name s = P.sprintf "%s%u" s c in 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" @@ -112,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"; @@ -123,10 +125,48 @@ let mk_or ooch noch c = P.fprintf noch "(* %s (%u) *)\n\n" description c; P.fprintf noch "notation \"hvbox(∨∨ %s)\"\n %s for @{ %s %s }.\n\n" - term_disj in_prec i_name par_seq + term_disj prec i_name par_seq + +let mk_and ooch noch c = + let description = "multiple conjunction connective" in + let prec = "non associative with precedence 35\n" in + let name s = P.sprintf "%s%u" s c in + let o_name = name "and" in + let i_name = "'And" 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 qm n = "?" 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 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" + o_name pre_list; + P.fprintf ooch " | %s_intro: %s → %s %s\n.\n\n" + o_name pre_type o_name qm_pre; + + P.fprintf ooch "interpretation \"%s (%u)\" %s %s = (%s %s).\n\n" + description c i_name pre_seq o_name pre_seq; + + P.fprintf noch "(* %s (%u) *)\n\n" description c; + + P.fprintf noch "notation \"hvbox(∧∧ %s)\"\n %s for @{ %s %s }.\n\n" + term_conj prec i_name par_seq let generate ooch noch = function | A.Exists (c, v) -> if c > 0 && v > 0 then mk_exists ooch noch c v | A.Or c -> if c > 1 then mk_or ooch noch c + | A.And c -> + if c > 1 then mk_and ooch noch c