X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FNaturalDeductionToLatex.v;h=ddf6e8c94cee0d160da8a236d8ae1da08ef9a2f4;hp=2d6fb553fd8c0b9e5cb963d8565c8bc95bc66da8;hb=97552c1a6dfb32098d4491951929ab1d4aca96a0;hpb=92e148ed7a7b0068cf2029537b019a88a7b07d43 diff --git a/src/NaturalDeductionToLatex.v b/src/NaturalDeductionToLatex.v index 2d6fb55..ddf6e8c 100644 --- a/src/NaturalDeductionToLatex.v +++ b/src/NaturalDeductionToLatex.v @@ -13,43 +13,14 @@ Section ToLatex. Context {Judgment : Type}. Context {Rule : forall (hypotheses:Tree ??Judgment)(conclusion:Tree ??Judgment), Type}. - - (* the "user" must supply functions for latexifying judgments and rules *) - Context (judgment2latex : Judgment -> string). - Context (rule2latex : forall h c, Rule h c -> string). + Context {JudgmentToLatexMath : ToLatexMath Judgment}. + Context {RuleToLatexMath : forall h c, ToLatexMath (Rule h c)}. Open Scope string_scope. - Notation "a +++ b" := (append a b) (at level 100). - Section TreeToLatex. - Context (emptyleaf:string). - Context {T:Type}. - Context (leaf:T -> string). - Fixpoint tree2latex' (j:Tree ??T) : string := - match j with - | T_Leaf None => emptyleaf - | T_Leaf (Some j') => leaf j' - | T_Branch b1 b2 => "\left["+++tree2latex' b1+++ - "\text{\tt{,}}"+++ - tree2latex' b2+++"\right]" - end. - Definition tree2latex (j:Tree ??T) : string := - match j with - | T_Leaf None => emptyleaf - | T_Leaf (Some j') => leaf j' - | T_Branch b1 b2 => tree2latex' b1+++ - "\text{\tt{,}}"+++ - tree2latex' b2 - end. - Fixpoint list2latex (sep:string)(l:list T) : string := - match l with - | nil => emptyleaf - | (a::nil) => leaf a - | (a::b) => (leaf a)+++sep+++(list2latex sep b) - end. - End TreeToLatex. - Definition judgments2latex (j:Tree ??Judgment) := - list2latex " " judgment2latex " \\ " (leaves j). + Definition judgments2latex (j:Tree ??Judgment) := treeToLatexMath (mapOptionTree toLatexMath j). + + Definition eolL : LatexMath := rawLatexMath eol. (* invariant: each proof shall emit its hypotheses visibly, except nd_id0 *) Section SCND_toLatex. @@ -57,46 +28,62 @@ Section ToLatex. (* indicates which rules should be hidden (omitted) from the rendered proof; useful for structural operations *) Context (hideRule : forall h c (r:Rule h c), bool). - Fixpoint SCND_toLatex {h}{c}(pns:SCND h c) : string := + Fixpoint SCND_toLatexMath {h}{c}(pns:SCND(Rule:=Rule) h c) : LatexMath := match pns with - | scnd_leaf ht c pn => SCND_toLatex pn - | scnd_branch ht c1 c2 pns1 pns2 => SCND_toLatex pns1 +++ " \hspace{1cm} " +++ SCND_toLatex pns2 - | scnd_weak c => "" - | scnd_comp ht ct c pns rule => if hideRule _ _ rule - then SCND_toLatex pns - else "\trfrac["+++rule2latex _ _ rule +++ "]{" +++ eol +++ - SCND_toLatex pns +++ "}{" +++ eol +++ - judgment2latex c +++ "}" +++ eol + | scnd_leaf ht c pn => SCND_toLatexMath pn + | scnd_branch ht c1 c2 pns1 pns2 => SCND_toLatexMath pns1 +++ rawLatexMath " \hspace{1cm} " +++ SCND_toLatexMath pns2 + | scnd_weak c => rawLatexMath "" + | scnd_comp ht ct c pns rule => if hideRule _ _ rule + then SCND_toLatexMath pns + else rawLatexMath "\trfrac["+++ toLatexMath rule +++ rawLatexMath "]{" +++ eolL +++ + SCND_toLatexMath pns +++ rawLatexMath "}{" +++ eolL +++ + toLatexMath c +++ rawLatexMath "}" +++ eolL end. End SCND_toLatex. - (* this is a work-in-progress; please use SCND_toLatex for now *) - Fixpoint nd_toLatex {h}{c}(nd:@ND _ Rule h c)(indent:string) := + (* this is a work-in-progress; please use SCND_toLatexMath for now *) + Fixpoint nd_toLatexMath {h}{c}(nd:@ND _ Rule h c)(indent:string) := match nd with - | nd_id0 => indent +++ "% nd_id0 " +++ eol - | nd_id1 h' => indent +++ "% nd_id1 "+++ judgments2latex h +++ eol - | nd_weak h' => indent +++ "\inferrule*[Left=ndWeak]{" +++ judgment2latex h' +++ "}{ }" +++ eol - | nd_copy h' => indent +++ "\inferrule*[Left=ndCopy]{"+++judgments2latex h+++ - "}{"+++judgments2latex c+++"}" +++ eol - | nd_prod h1 h2 c1 c2 pf1 pf2 => indent +++ "% prod " +++ eol +++ - indent +++ "\begin{array}{c c}" +++ eol +++ - (nd_toLatex pf1 (" "+++indent)) +++ - indent +++ " & " +++ eol +++ - (nd_toLatex pf2 (" "+++indent)) +++ - indent +++ "\end{array}" - | nd_comp h m c pf1 pf2 => indent +++ "% comp " +++ eol +++ - indent +++ "\begin{array}{c}" +++ eol +++ - (nd_toLatex pf1 (" "+++indent)) +++ - indent +++ " \\ " +++ eol +++ - (nd_toLatex pf2 (" "+++indent)) +++ - indent +++ "\end{array}" - | nd_cancell a => indent +++ "% nd-cancell " +++ (judgments2latex a) +++ eol - | nd_cancelr a => indent +++ "% nd-cancelr " +++ (judgments2latex a) +++ eol - | nd_llecnac a => indent +++ "% nd-llecnac " +++ (judgments2latex a) +++ eol - | nd_rlecnac a => indent +++ "% nd-rlecnac " +++ (judgments2latex a) +++ eol - | nd_assoc a b c => "" - | nd_cossa a b c => "" - | nd_rule h c r => rule2latex h c r + | nd_id0 => rawLatexMath indent +++ + rawLatexMath "% nd_id0 " +++ eolL + | nd_id1 h' => rawLatexMath indent +++ + rawLatexMath "% nd_id1 "+++ judgments2latex h +++ eolL + | nd_weak h' => rawLatexMath indent +++ + rawLatexMath "\inferrule*[Left=ndWeak]{" +++ toLatexMath h' +++ rawLatexMath "}{ }" +++ eolL + | nd_copy h' => rawLatexMath indent +++ + rawLatexMath "\inferrule*[Left=ndCopy]{"+++judgments2latex h+++ + rawLatexMath "}{"+++judgments2latex c+++rawLatexMath "}" +++ eolL + | nd_prod h1 h2 c1 c2 pf1 pf2 => rawLatexMath indent +++ + rawLatexMath "% prod " +++ eolL +++ + rawLatexMath indent +++ + rawLatexMath "\begin{array}{c c}" +++ eolL +++ + (nd_toLatexMath pf1 (" "+++indent)) +++ + rawLatexMath indent +++ + rawLatexMath " & " +++ eolL +++ + (nd_toLatexMath pf2 (" "+++indent)) +++ + rawLatexMath indent +++ + rawLatexMath "\end{array}" + | nd_comp h m c pf1 pf2 => rawLatexMath indent +++ + rawLatexMath "% comp " +++ eolL +++ + rawLatexMath indent +++ + rawLatexMath "\begin{array}{c}" +++ eolL +++ + (nd_toLatexMath pf1 (" "+++indent)) +++ + rawLatexMath indent +++ + rawLatexMath " \\ " +++ eolL +++ + (nd_toLatexMath pf2 (" "+++indent)) +++ + rawLatexMath indent +++ + rawLatexMath "\end{array}" + | nd_cancell a => rawLatexMath indent +++ + rawLatexMath "% nd-cancell " +++ (judgments2latex a) +++ eolL + | nd_cancelr a => rawLatexMath indent +++ + rawLatexMath "% nd-cancelr " +++ (judgments2latex a) +++ eolL + | nd_llecnac a => rawLatexMath indent +++ + rawLatexMath "% nd-llecnac " +++ (judgments2latex a) +++ eolL + | nd_rlecnac a => rawLatexMath indent +++ + rawLatexMath "% nd-rlecnac " +++ (judgments2latex a) +++ eolL + | nd_assoc a b c => rawLatexMath "" + | nd_cossa a b c => rawLatexMath "" + | nd_rule h c r => toLatexMath r end. End ToLatex.