src/NaturalDeductionToLatex.v

   1 (*********************************************************************************************************************************)
   2 (* NaturalDeductionToLatex: rendering natural deduction proofs as LaTeX code                                                     *)
   3 (*********************************************************************************************************************************)
   4
   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.
  11
  12 Section ToLatex.
  13
  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)}.
  18
  19   Open Scope string_scope.
  20
  21   Definition judgments2latex (j:Tree ??Judgment) := treeToLatexMath (mapOptionTree toLatexMath j).
  22
  23   Definition eolL : LatexMath := rawLatexMath eol.
  24
  25   (* invariant: each proof shall emit its hypotheses visibly, except nd_id0 *)
  26   Section SCND_toLatex.
  27
  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).
  30
  31     Fixpoint SCND_toLatexMath {h}{c}(pns:SCND(Rule:=Rule) h c) : LatexMath :=
  32       match pns with
  33         | scnd_branch ht c1 c2 pns1 pns2 => SCND_toLatexMath pns1 +++ rawLatexMath " \hspace{1cm} " +++ SCND_toLatexMath pns2
  34         | scnd_weak     c                => rawLatexMath ""
  35         | scnd_comp ht ct c pns rule     => if hideRule _ _ rule
  36                                             then SCND_toLatexMath pns
  37                                             else rawLatexMath "\trfrac["+++ toLatexMath rule +++ rawLatexMath "]{" +++ eolL +++
  38                                               SCND_toLatexMath pns +++ rawLatexMath "}{" +++ eolL +++
  39                                               toLatexMath c +++ rawLatexMath "}" +++ eolL
  40       end.
  41   End SCND_toLatex.
  42
  43   (* this is a work-in-progress; please use SCND_toLatexMath for now *)
  44   Fixpoint nd_toLatexMath {h}{c}(nd:@ND _ Rule h c)(indent:string) :=
  45     match nd with
  46       | nd_id0                      => rawLatexMath indent +++
  47                                        rawLatexMath "% nd_id0 " +++ eolL
  48       | nd_id1  h'                  => rawLatexMath indent +++
  49                                        rawLatexMath "% nd_id1 "+++ judgments2latex h +++ eolL
  50       | nd_weak h'                  => rawLatexMath indent +++
  51                                        rawLatexMath "\inferrule*[Left=ndWeak]{" +++ toLatexMath h' +++ rawLatexMath "}{ }" +++ eolL
  52       | nd_copy h'                  => rawLatexMath indent +++
  53                                        rawLatexMath "\inferrule*[Left=ndCopy]{"+++judgments2latex h+++
  54                                                          rawLatexMath "}{"+++judgments2latex c+++rawLatexMath "}" +++ eolL
  55       | nd_prod h1 h2 c1 c2 pf1 pf2 => rawLatexMath indent +++
  56                                        rawLatexMath "% prod " +++ eolL +++
  57                                        rawLatexMath indent +++
  58                                        rawLatexMath "\begin{array}{c c}" +++ eolL +++
  59                                        (nd_toLatexMath pf1 ("  "+++indent)) +++
  60                                        rawLatexMath indent +++
  61                                        rawLatexMath " & " +++ eolL +++
  62                                        (nd_toLatexMath pf2 ("  "+++indent)) +++
  63                                        rawLatexMath indent +++
  64                                        rawLatexMath "\end{array}"
  65       | nd_comp h  m     c  pf1 pf2 => rawLatexMath indent +++
  66                                        rawLatexMath "% comp " +++ eolL +++
  67                                        rawLatexMath indent +++
  68                                        rawLatexMath "\begin{array}{c}" +++ eolL +++
  69                                        (nd_toLatexMath pf1 ("  "+++indent)) +++
  70                                        rawLatexMath indent +++
  71                                        rawLatexMath " \\ " +++ eolL +++
  72                                        (nd_toLatexMath pf2 ("  "+++indent)) +++
  73                                        rawLatexMath indent +++
  74                                        rawLatexMath "\end{array}"
  75       | nd_cancell a                => rawLatexMath indent +++
  76                                        rawLatexMath "% nd-cancell " +++ (judgments2latex a) +++ eolL
  77       | nd_cancelr a                => rawLatexMath indent +++
  78                                        rawLatexMath "% nd-cancelr " +++ (judgments2latex a) +++ eolL
  79       | nd_llecnac a                => rawLatexMath indent +++
  80                                        rawLatexMath "% nd-llecnac " +++ (judgments2latex a) +++ eolL
  81       | nd_rlecnac a                => rawLatexMath indent +++
  82                                        rawLatexMath "% nd-rlecnac " +++ (judgments2latex a) +++ eolL
  83       | nd_assoc   a b c            => rawLatexMath ""
  84       | nd_cossa   a b c            => rawLatexMath ""
  85       | nd_rule    h c r            => toLatexMath r
  86     end.
  87
  88 End ToLatex.