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