the generation of the multiple conjunction is now supported!

diff --git a/matita/components/binaries/xoa/ast.ml b/matita/components/binaries/xoa/ast.ml
index 4de0c10579e07b5c66947796eeef8a23983f3325..42285524036073349c2ba7c1c67c93bba14304c7 100644 (file)
--- 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 bc9a8be5da1f3935bf175134251ce4b4cd45154a..d650f07b518dee5507fe4d6616315061cb8761d6 100644 (file)
--- 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 92b473d7965cc4682769eb41982caff1d4ba0d93..de451f8148f9e17c0a64cd12dc3fdbc6e19d29f1 100644 (file)
--- 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 _ =