From: Claudio Sacerdoti Coen Date: Fri, 11 Jul 2008 14:29:09 +0000 (+0000) Subject: Added new ternary layout \infrule premises conclusion name. X-Git-Tag: make_still_working~4942 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d063ddede0424eb1f47a4c9769eaefbb16d90700;p=helm.git 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 a0f9dc2f1..cfd8c8a30 100644 --- 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 7e06fa5e8..ff72f2a86 100644 --- 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 d4a55b353..25af9981e 100644 --- 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 8940c6614..aca53578b 100644 --- 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 728651acc..8ed430901 100644 --- 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 efb9e564b..1076338e6 100644 --- a/helm/software/matita/help/C/sec_usernotation.xml +++ b/helm/software/matita/help/C/sec_usernotation.xml @@ -316,6 +316,12 @@ \frac &layout; &layout; Fraction + + + | + \infrule &layout; &layout; &layout; + Inference rule (premises, conclusion, rule name) + |