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.
(* 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.
projects / coq-hetmet.git / blobdiff