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.
13 Variable eol : string.
14 Extract Constant eol => "'\n':[]".
18 Context {Judgment : Type}.
19 Context {Rule : forall (hypotheses:Tree ??Judgment)(conclusion:Tree ??Judgment), Type}.
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).
25 Open Scope string_scope.
26 Notation "a +++ b" := (append a b) (at level 100).
28 Context (emptyleaf:string).
30 Context (leaf:T -> string).
31 Fixpoint tree2latex' (j:Tree ??T) : string :=
33 | T_Leaf None => emptyleaf
34 | T_Leaf (Some j') => leaf j'
35 | T_Branch b1 b2 => "\left["+++tree2latex' b1+++
37 tree2latex' b2+++"\right]"
39 Definition tree2latex (j:Tree ??T) : string :=
41 | T_Leaf None => emptyleaf
42 | T_Leaf (Some j') => leaf j'
43 | T_Branch b1 b2 => tree2latex' b1+++
47 Fixpoint list2latex (sep:string)(l:list T) : string :=
51 | (a::b) => (leaf a)+++sep+++(list2latex sep b)
55 Definition judgments2latex (j:Tree ??Judgment) :=
56 list2latex " " judgment2latex " \\ " (leaves j).
58 (* invariant: each proof shall emit its hypotheses visibly, except nd_id0 *)
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).
64 Fixpoint SCND_toLatex {h}{c}(pns:SCND h c) : string :=
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
69 | scnd_comp ht ct c pns rule => if hideRule _ _ rule
71 else "\trfrac["+++rule2latex _ _ rule +++ "]{" +++ eol +++
72 SCND_toLatex pns +++ "}{" +++ eol +++
73 judgment2latex c +++ "}" +++ eol
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) :=
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