1 (*********************************************************************************************************************************)
2 (* NaturalDeductionToLatex: rendering natural deduction proofs as LaTeX code *)
3 (*********************************************************************************************************************************)
5 Generalizable All Variables.
6 Require Import Preamble.
7 Require Import General.
8 Require Import Coq.Strings.Ascii.
9 Require Import Coq.Strings.String.
10 Require Import NaturalDeduction.
14 Context {Judgment : Type}.
15 Context {Rule : forall (hypotheses:Tree ??Judgment)(conclusion:Tree ??Judgment), Type}.
16 Context {JudgmentToLatexMath : ToLatexMath Judgment}.
17 Context {RuleToLatexMath : forall h c, ToLatexMath (Rule h c)}.
19 Open Scope string_scope.
21 Definition judgments2latex (j:Tree ??Judgment) := treeToLatexMath (mapOptionTree toLatexMath j).
23 Definition eolL : LatexMath := rawLatexMath eol.
25 (* invariant: each proof shall emit its hypotheses visibly, except nd_id0 *)
28 (* indicates which rules should be hidden (omitted) from the rendered proof; useful for structural operations *)
29 Context (hideRule : forall h c (r:Rule h c), bool).
31 Fixpoint SCND_toLatexMath {h}{c}(pns:SCND(Rule:=Rule) h c) : LatexMath :=
33 | scnd_leaf ht c pn => SCND_toLatexMath pn
34 | scnd_branch ht c1 c2 pns1 pns2 => SCND_toLatexMath pns1 +++ rawLatexMath " \hspace{1cm} " +++ SCND_toLatexMath pns2
35 | scnd_weak c => rawLatexMath ""
36 | scnd_comp ht ct c pns rule => if hideRule _ _ rule
37 then SCND_toLatexMath pns
38 else rawLatexMath "\trfrac["+++ toLatexMath rule +++ rawLatexMath "]{" +++ eolL +++
39 SCND_toLatexMath pns +++ rawLatexMath "}{" +++ eolL +++
40 toLatexMath c +++ rawLatexMath "}" +++ eolL
44 (* this is a work-in-progress; please use SCND_toLatexMath for now *)
45 Fixpoint nd_toLatexMath {h}{c}(nd:@ND _ Rule h c)(indent:string) :=
47 | nd_id0 => rawLatexMath indent +++
48 rawLatexMath "% nd_id0 " +++ eolL
49 | nd_id1 h' => rawLatexMath indent +++
50 rawLatexMath "% nd_id1 "+++ judgments2latex h +++ eolL
51 | nd_weak h' => rawLatexMath indent +++
52 rawLatexMath "\inferrule*[Left=ndWeak]{" +++ toLatexMath h' +++ rawLatexMath "}{ }" +++ eolL
53 | nd_copy h' => rawLatexMath indent +++
54 rawLatexMath "\inferrule*[Left=ndCopy]{"+++judgments2latex h+++
55 rawLatexMath "}{"+++judgments2latex c+++rawLatexMath "}" +++ eolL
56 | nd_prod h1 h2 c1 c2 pf1 pf2 => rawLatexMath indent +++
57 rawLatexMath "% prod " +++ eolL +++
58 rawLatexMath indent +++
59 rawLatexMath "\begin{array}{c c}" +++ eolL +++
60 (nd_toLatexMath pf1 (" "+++indent)) +++
61 rawLatexMath indent +++
62 rawLatexMath " & " +++ eolL +++
63 (nd_toLatexMath pf2 (" "+++indent)) +++
64 rawLatexMath indent +++
65 rawLatexMath "\end{array}"
66 | nd_comp h m c pf1 pf2 => rawLatexMath indent +++
67 rawLatexMath "% comp " +++ eolL +++
68 rawLatexMath indent +++
69 rawLatexMath "\begin{array}{c}" +++ eolL +++
70 (nd_toLatexMath pf1 (" "+++indent)) +++
71 rawLatexMath indent +++
72 rawLatexMath " \\ " +++ eolL +++
73 (nd_toLatexMath pf2 (" "+++indent)) +++
74 rawLatexMath indent +++
75 rawLatexMath "\end{array}"
76 | nd_cancell a => rawLatexMath indent +++
77 rawLatexMath "% nd-cancell " +++ (judgments2latex a) +++ eolL
78 | nd_cancelr a => rawLatexMath indent +++
79 rawLatexMath "% nd-cancelr " +++ (judgments2latex a) +++ eolL
80 | nd_llecnac a => rawLatexMath indent +++
81 rawLatexMath "% nd-llecnac " +++ (judgments2latex a) +++ eolL
82 | nd_rlecnac a => rawLatexMath indent +++
83 rawLatexMath "% nd-rlecnac " +++ (judgments2latex a) +++ eolL
84 | nd_assoc a b c => rawLatexMath ""
85 | nd_cossa a b c => rawLatexMath ""
86 | nd_rule h c r => toLatexMath r