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
  17   (* the "user" must supply functions for latexifying judgments and rules *)
  18   Context (judgment2latex : Judgment -> string).
  19   Context (rule2latex     : forall h c, Rule h c -> string).
  20
  21   Open Scope string_scope.
  22   Notation "a +++ b" := (append a b) (at level 100).
  23   Section TreeToLatex.
  24     Context (emptyleaf:string).
  25     Context {T:Type}.
  26     Context (leaf:T -> string).
  27     Fixpoint tree2latex' (j:Tree ??T) : string :=
  28       match j with
  29         | T_Leaf   None      => emptyleaf
  30         | T_Leaf   (Some j') => leaf j'
  31         | T_Branch b1 b2     => "\left["+++tree2latex' b1+++
  32                                 "\text{\tt{,}}"+++
  33                                 tree2latex' b2+++"\right]"
  34       end.
  35     Definition tree2latex (j:Tree ??T) : string :=
  36       match j with
  37         | T_Leaf   None      => emptyleaf
  38         | T_Leaf   (Some j') => leaf j'
  39         | T_Branch b1 b2     => tree2latex' b1+++
  40                                 "\text{\tt{,}}"+++
  41                                 tree2latex' b2
  42       end.
  43     Fixpoint list2latex (sep:string)(l:list T) : string :=
  44       match l with
  45         | nil      => emptyleaf
  46         | (a::nil) => leaf a
  47         | (a::b)   => (leaf a)+++sep+++(list2latex sep b)
  48       end.
  49   End TreeToLatex.
  50
  51   Definition judgments2latex (j:Tree ??Judgment) :=
  52     list2latex " " judgment2latex " \\ " (leaves j).
  53
  54   (* invariant: each proof shall emit its hypotheses visibly, except nd_id0 *)
  55   Section SCND_toLatex.
  56
  57     (* indicates which rules should be hidden (omitted) from the rendered proof; useful for structural operations *)
  58     Context (hideRule : forall h c (r:Rule h c), bool).
  59
  60     Fixpoint SCND_toLatex {h}{c}(pns:SCND h c) : string :=
  61       match pns with
  62         | scnd_leaf   ht c pn            => SCND_toLatex pn
  63         | scnd_branch ht c1 c2 pns1 pns2 => SCND_toLatex pns1 +++ " \hspace{1cm} " +++ SCND_toLatex pns2
  64         | scnd_weak     c                => ""
  65         | scnd_comp ht ct c pns rule => if hideRule _ _ rule
  66                                       then SCND_toLatex pns
  67                                       else "\trfrac["+++rule2latex _ _ rule +++ "]{" +++ eol +++
  68                                              SCND_toLatex pns +++ "}{" +++ eol +++
  69                                              judgment2latex c +++ "}" +++ eol
  70       end.
  71   End SCND_toLatex.
  72
  73   (* this is a work-in-progress; please use SCND_toLatex for now *)
  74   Fixpoint nd_toLatex {h}{c}(nd:@ND _ Rule h c)(indent:string) :=
  75     match nd with
  76       | nd_id0                      => indent +++ "% nd_id0 " +++ eol
  77       | nd_id1  h'                  => indent +++ "% nd_id1 "+++ judgments2latex h +++ eol
  78       | nd_weak h'                  => indent +++ "\inferrule*[Left=ndWeak]{" +++ judgment2latex h' +++ "}{ }" +++ eol
  79       | nd_copy h'                  => indent +++ "\inferrule*[Left=ndCopy]{"+++judgments2latex h+++
  80                                                          "}{"+++judgments2latex c+++"}" +++ eol
  81       | nd_prod h1 h2 c1 c2 pf1 pf2 => indent +++ "% prod " +++ eol +++
  82                                        indent +++ "\begin{array}{c c}" +++ eol +++
  83                                        (nd_toLatex pf1 ("  "+++indent)) +++
  84                                        indent +++ " & " +++ eol +++
  85                                        (nd_toLatex pf2 ("  "+++indent)) +++
  86                                        indent +++ "\end{array}"
  87       | nd_comp h  m     c  pf1 pf2 => indent +++ "% comp " +++ eol +++
  88                                        indent +++ "\begin{array}{c}" +++ eol +++
  89                                        (nd_toLatex pf1 ("  "+++indent)) +++
  90                                        indent +++ " \\ " +++ eol +++
  91                                        (nd_toLatex pf2 ("  "+++indent)) +++
  92                                        indent +++ "\end{array}"
  93       | nd_cancell a                => indent +++ "% nd-cancell " +++ (judgments2latex a) +++ eol
  94       | nd_cancelr a                => indent +++ "% nd-cancelr " +++ (judgments2latex a) +++ eol
  95       | nd_llecnac a                => indent +++ "% nd-llecnac " +++ (judgments2latex a) +++ eol
  96       | nd_rlecnac a                => indent +++ "% nd-rlecnac " +++ (judgments2latex a) +++ eol
  97       | nd_assoc   a b c            => ""
  98       | nd_cossa   a b c            => ""
  99       | nd_rule    h c r            => rule2latex h c r
 100     end.
 101
 102 End ToLatex.