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}.
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).
21 Open Scope string_scope.
22 Notation "a +++ b" := (append a b) (at level 100).
24 Context (emptyleaf:string).
26 Context (leaf:T -> string).
27 Fixpoint tree2latex' (j:Tree ??T) : string :=
29 | T_Leaf None => emptyleaf
30 | T_Leaf (Some j') => leaf j'
31 | T_Branch b1 b2 => "\left["+++tree2latex' b1+++
33 tree2latex' b2+++"\right]"
35 Definition tree2latex (j:Tree ??T) : string :=
37 | T_Leaf None => emptyleaf
38 | T_Leaf (Some j') => leaf j'
39 | T_Branch b1 b2 => tree2latex' b1+++
43 Fixpoint list2latex (sep:string)(l:list T) : string :=
47 | (a::b) => (leaf a)+++sep+++(list2latex sep b)
51 Definition judgments2latex (j:Tree ??Judgment) :=
52 list2latex " " judgment2latex " \\ " (leaves j).
54 (* invariant: each proof shall emit its hypotheses visibly, except nd_id0 *)
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).
60 Fixpoint SCND_toLatex {h}{c}(pns:SCND h c) : string :=
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
65 | scnd_comp ht ct c pns rule => if hideRule _ _ rule
67 else "\trfrac["+++rule2latex _ _ rule +++ "]{" +++ eol +++
68 SCND_toLatex pns +++ "}{" +++ eol +++
69 judgment2latex c +++ "}" +++ eol
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) :=
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