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     Context (hideRule : forall h c (r:Rule h c), bool).
  61
  62     Fixpoint SCND_toLatex {h}{c}(pns:SCND h c) : string :=
  63       match pns with
  64         | scnd_leaf   ht c pn            => SCND_toLatex pn
  65         | scnd_branch ht c1 c2 pns1 pns2 => SCND_toLatex pns1 +++ " \hspace{1cm} " +++ SCND_toLatex pns2
  66         | scnd_weak     c                => ""
  67         | scnd_axiom c               => judgment2latex c +++ eol
  68         | scnd_comp ht ct c pns rule => if hideRule _ _ rule
  69                                       then SCND_toLatex pns
  70                                       else "\trfrac["+++rule2latex _ _ rule +++ "]{" +++ eol +++
  71                                              SCND_toLatex pns +++ "}{" +++ eol +++
  72                                              judgment2latex c +++ "}" +++ eol
  73       end.
  74   End SCND_toLatex.
  75
  76   (* FIXME: this doesn't actually work properly (but SCND_toLatex does!) *)
  77   Fixpoint nd_toLatex {h}{c}(nd:@ND _ Rule h c)(indent:string) :=
  78     match nd with
  79       | nd_id0                      => indent +++ "% nd_id0 " +++ eol
  80       | nd_id1  h'                  => indent +++ "% nd_id1 "+++ judgments2latex h +++ eol
  81       | nd_weak h'                  => indent +++ "\inferrule*[Left=ndWeak]{" +++ judgment2latex h' +++ "}{ }" +++ eol
  82       | nd_copy h'                  => indent +++ "\inferrule*[Left=ndCopy]{"+++judgments2latex h+++
  83                                                          "}{"+++judgments2latex c+++"}" +++ eol
  84       | nd_prod h1 h2 c1 c2 pf1 pf2 => indent +++ "% prod " +++ eol +++
  85                                        indent +++ "\begin{array}{c c}" +++ eol +++
  86                                        (nd_toLatex pf1 ("  "+++indent)) +++
  87                                        indent +++ " & " +++ eol +++
  88                                        (nd_toLatex pf2 ("  "+++indent)) +++
  89                                        indent +++ "\end{array}"
  90       | nd_comp h  m     c  pf1 pf2 => indent +++ "% comp " +++ eol +++
  91                                        indent +++ "\begin{array}{c}" +++ eol +++
  92                                        (nd_toLatex pf1 ("  "+++indent)) +++
  93                                        indent +++ " \\ " +++ eol +++
  94                                        (nd_toLatex pf2 ("  "+++indent)) +++
  95                                        indent +++ "\end{array}"
  96       | nd_cancell a                => indent +++ "% nd-cancell " +++ (judgments2latex a) +++ eol
  97       | nd_cancelr a                => indent +++ "% nd-cancelr " +++ (judgments2latex a) +++ eol
  98       | nd_llecnac a                => indent +++ "% nd-llecnac " +++ (judgments2latex a) +++ eol
  99       | nd_rlecnac a                => indent +++ "% nd-rlecnac " +++ (judgments2latex a) +++ eol
 100       | nd_assoc   a b c            => ""
 101       | nd_cossa   a b c            => ""
 102       | nd_rule    h c r            => rule2latex h c r
 103     end.
 104
 105 End ToLatex.