From 81cf2dd18ed76a214ab610447d0c5861998b3d96 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 3 Aug 2011 21:39:10 +0000 Subject: [PATCH] the generation of the multiple conjunction is now supported! --- matita/components/binaries/xoa/ast.ml | 3 ++ matita/components/binaries/xoa/engine.ml | 49 +++++++++++++++++++++--- matita/components/binaries/xoa/xoa.ml | 4 ++ 3 files changed, 50 insertions(+), 6 deletions(-) diff --git a/matita/components/binaries/xoa/ast.ml b/matita/components/binaries/xoa/ast.ml index 4de0c1057..422855240 100644 --- a/matita/components/binaries/xoa/ast.ml +++ b/matita/components/binaries/xoa/ast.ml @@ -15,7 +15,10 @@ type subarity = int type directive = Exists of arity * subarity | Or of arity + | And of arity let mk_exists c v = Exists (c, v) let mk_or c = Or c + +let mk_and c = And c diff --git a/matita/components/binaries/xoa/engine.ml b/matita/components/binaries/xoa/engine.ml index bc9a8be5d..d650f07b5 100644 --- a/matita/components/binaries/xoa/engine.ml +++ b/matita/components/binaries/xoa/engine.ml @@ -30,8 +30,7 @@ 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 prec = "non associative with precedence 20\n" in let name s = P.sprintf "%s%u_%u" s c v in let o_name = name "ex" in let i_name = "'Ex" in @@ -81,14 +80,14 @@ 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 @@ -123,10 +122,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 diff --git a/matita/components/binaries/xoa/xoa.ml b/matita/components/binaries/xoa/xoa.ml index 92b473d79..de451f814 100644 --- a/matita/components/binaries/xoa/xoa.ml +++ b/matita/components/binaries/xoa/xoa.ml @@ -21,6 +21,9 @@ let unm_ex s = let unm_or s = Scanf.sscanf s "%u" A.mk_or +let unm_and s = + Scanf.sscanf s "%u" A.mk_and + let process conf = let preamble = L.get_preamble conf in let ooch = L.open_out preamble (R.get_string "xoa.objects") in @@ -28,6 +31,7 @@ let process conf = List.iter (L.out_include ooch) (R.get_list R.string "xoa.include"); 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 let _ = -- 2.39.2