Added new ternary layout \infrule premises conclusion name.

Very useful to render proof terms as trees.

diff --git a/helm/software/components/acic_content/cicNotationPp.ml b/helm/software/components/acic_content/cicNotationPp.ml
index a0f9dc2f12a8fb7e61ca82756e8f3c463a3519de..cfd8c8a308956cdef0466d57f5adc231c85e36ab 100644 (file)
--- a/helm/software/components/acic_content/cicNotationPp.ml
+++ b/helm/software/components/acic_content/cicNotationPp.ml
@@ -211,6 +211,7 @@ and pp_layout = function
   | Ast.Over (t1, t2) -> sprintf "[%s \\OVER %s]" (pp_term t1) (pp_term t2)
   | Ast.Atop (t1, t2) -> sprintf "[%s \\ATOP %s]" (pp_term t1) (pp_term t2)
   | Ast.Frac (t1, t2) -> sprintf "\\FRAC %s %s" (pp_term t1) (pp_term t2)
+  | Ast.InfRule (t1, t2, t3) -> sprintf "\\INFRULE %s %s %s" (pp_term t1) (pp_term t2) (pp_term t3)
   | Ast.Sqrt t -> sprintf "\\SQRT %s" (pp_term t)
   | Ast.Root (arg, index) ->
       sprintf "\\ROOT %s \\OF %s" (pp_term index) (pp_term arg)

diff --git a/helm/software/components/acic_content/cicNotationPt.ml b/helm/software/components/acic_content/cicNotationPt.ml
index 7e06fa5e82a722c990f0e021db87474f013bf528..ff72f2a86c9722cac3d24e2e8f17614c05af74a3 100644 (file)
--- a/helm/software/components/acic_content/cicNotationPt.ml
+++ b/helm/software/components/acic_content/cicNotationPt.ml
@@ -119,6 +119,7 @@ and layout_pattern =
   | Frac of term * term
   | Over of term * term
   | Atop of term * term
+  | InfRule of term * term * term
 (*   | array of term * literal option * literal option
       |+ column separator, row separator +| *)
   | Sqrt of term

diff --git a/helm/software/components/acic_content/cicNotationUtil.ml b/helm/software/components/acic_content/cicNotationUtil.ml
index d4a55b353adf41221cd44958e294c6ef38ee59a9..25af9981e7f5dff7131aba171dfdcf1fb5dadf8e 100644 (file)
--- a/helm/software/components/acic_content/cicNotationUtil.ml
+++ b/helm/software/components/acic_content/cicNotationUtil.ml
@@ -85,6 +85,7 @@ let visit_layout k = function
   | Ast.Over (t1, t2) -> Ast.Over (k t1, k t2)
   | Ast.Atop (t1, t2) -> Ast.Atop (k t1, k t2)
   | Ast.Frac (t1, t2) -> Ast.Frac (k t1, k t2)
+  | Ast.InfRule (t1, t2, t3) -> Ast.InfRule (k t1, k t2, k t3)
   | Ast.Sqrt t -> Ast.Sqrt (k t)
   | Ast.Root (arg, index) -> Ast.Root (k arg, k index)
   | Ast.Break -> Ast.Break

diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml
index 8940c6614ebafb0622fb6bc83f348e88eb40854b..aca53578b1fb9c7ca0beff072d14c2e7dbcaacf4 100644 (file)
--- a/helm/software/components/content_pres/cicNotationParser.ml
+++ b/helm/software/components/content_pres/cicNotationParser.ml
@@ -150,6 +150,7 @@ let extract_term_production pattern =
     | Ast.Below (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\below"] @ aux p2
     | Ast.Above (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\above"] @ aux p2
     | Ast.Frac (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\frac"] @ aux p2
+    | Ast.InfRule (p1, p2, p3) -> aux p1 @ [NoBinding, gram_symbol "\\infrule"] @ aux p2 @ aux p3
     | Ast.Atop (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\atop"] @ aux p2
     | Ast.Over (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\over"] @ aux p2
     | Ast.Root (p1, p2) ->
@@ -233,6 +234,7 @@ let check_l1_pattern level1_pattern level associativity =
     | Ast.Below (p1, p2) -> let p1 = aux p1 in let p2 = aux p2 in Ast.Below (p1, p2)
     | Ast.Above (p1, p2) -> let p1 = aux p1 in let p2 = aux p2 in Ast.Above (p1, p2)
     | Ast.Frac (p1, p2)  -> let p1 = aux p1 in let p2 = aux p2 in Ast.Frac (p1, p2)
+    | Ast.InfRule (p1, p2, p3)  -> let p1 = aux p1 in let p2 = aux p2 in let p3 = aux p3 in Ast.InfRule (p1, p2, p3)
     | Ast.Atop (p1, p2)  -> let p1 = aux p1 in let p2 = aux p2 in Ast.Atop (p1, p2)
     | Ast.Over (p1, p2)  -> let p1 = aux p1 in let p2 = aux p2 in Ast.Over (p1, p2)
     | Ast.Root (p1, p2)  -> let p1 = aux p1 in let p2 = aux p2 in Ast.Root (p1, p2)
@@ -426,6 +428,9 @@ EXTEND
       | SYMBOL "\\frac"; p1 = SELF; p2 = SELF ->
           return_term_of_level loc 
             (fun l -> Ast.Layout (Ast.Frac (p1 l, p2 l)))
+      | SYMBOL "\\infrule"; p1 = SELF; p2 = SELF; p3 = SELF ->
+          return_term_of_level loc 
+            (fun l -> Ast.Layout (Ast.InfRule (p1 l, p2 l, p3 l)))
       | SYMBOL "\\sqrt"; p = SELF -> 
           return_term_of_level loc (fun l -> Ast.Layout (Ast.Sqrt p l))
       | SYMBOL "\\root"; index = SELF; SYMBOL "\\of"; arg = SELF ->

diff --git a/helm/software/components/content_pres/cicNotationPres.ml b/helm/software/components/content_pres/cicNotationPres.ml
index 728651acc6f2be52523302352c46b0eaf81ec34f..8ed430901893a0d2cf8f268b34c6509428e30fbd 100644 (file)
--- a/helm/software/components/content_pres/cicNotationPres.ml
+++ b/helm/software/components/content_pres/cicNotationPres.ml
@@ -380,6 +380,12 @@ let render ids_to_uris ?(prec=(-1)) =
     | A.Atop (t1, t2) ->
         Mpres.Mfrac (atop_attributes @ attrs, invoke_reinit t1,
           invoke_reinit t2)
+    | A.InfRule (t1, t2, t3) ->
+       Mpres.Mrow (attrs,
+        [Mpres.Mfrac ([],
+           Mpres.Mstyle ([None,"scriptlevel","0"],invoke_reinit t1),
+           Mpres.Mstyle ([None,"scriptlevel","0"],invoke_reinit t2));
+         Mpres.Mstyle ([None,"scriptlevel","2"],invoke_reinit t3)])
     | A.Sqrt t -> Mpres.Msqrt (attrs, invoke_reinit t)
     | A.Root (t1, t2) ->
         Mpres.Mroot (attrs, invoke_reinit t1, invoke_reinit t2)

diff --git a/helm/software/matita/help/C/sec_usernotation.xml b/helm/software/matita/help/C/sec_usernotation.xml
index efb9e564bb187d87d895b705cb3959496f4310ca..1076338e6e06050d6702f29f3acb360e6c9873f8 100644 (file)
--- a/helm/software/matita/help/C/sec_usernotation.xml
+++ b/helm/software/matita/help/C/sec_usernotation.xml
@@ -316,6 +316,12 @@
         <entry><emphasis role="bold">\frac</emphasis> &layout; &layout;</entry>
         <entry>Fraction</entry>
        </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry><emphasis role="bold">\infrule</emphasis> &layout; &layout; &layout;</entry>
+        <entry>Inference rule (premises, conclusion, rule name)</entry>
+       </row>
        <row>
         <entry></entry>
         <entry>|</entry>