lots of cleanup

[coq-hetmet.git] / src / NaturalDeductionToLatex.v

diff --git a/src/NaturalDeductionToLatex.v b/src/NaturalDeductionToLatex.v
deleted file mode 100644 (file)
index 1f6f32a..0000000
--- a/src/NaturalDeductionToLatex.v
+++ /dev/null
@@ -1,88 +0,0 @@
-(*********************************************************************************************************************************)
-(* NaturalDeductionToLatex: rendering natural deduction proofs as LaTeX code                                                     *)
-(*********************************************************************************************************************************)
-
-Generalizable All Variables.
-Require Import Preamble.
-Require Import General.
-Require Import Coq.Strings.Ascii.
-Require Import Coq.Strings.String.
-Require Import NaturalDeduction.
-
-Section ToLatex.
-
-  Context {Judgment : Type}.
-  Context {Rule     : forall (hypotheses:Tree ??Judgment)(conclusion:Tree ??Judgment), Type}.
-  Context {JudgmentToLatexMath : ToLatexMath Judgment}.
-  Context {RuleToLatexMath     : forall h c, ToLatexMath (Rule h c)}.
-  
-  Open Scope string_scope.
-
-  Definition judgments2latex (j:Tree ??Judgment) := treeToLatexMath (mapOptionTree toLatexMath j).
-
-  Definition eolL : LatexMath := rawLatexMath eol.
-
-  (* invariant: each proof shall emit its hypotheses visibly, except nd_id0 *)
-  Section SCND_toLatex.
-
-    (* indicates which rules should be hidden (omitted) from the rendered proof; useful for structural operations *)
-    Context (hideRule : forall h c (r:Rule h c), bool).
-
-    Fixpoint SCND_toLatexMath {h}{c}(pns:SCND(Rule:=Rule) h c) : LatexMath :=
-      match pns with
-        | scnd_branch ht c1 c2 pns1 pns2 => SCND_toLatexMath pns1 +++ rawLatexMath " \hspace{1cm} " +++ SCND_toLatexMath pns2
-        | scnd_weak     c                => rawLatexMath ""
-        | scnd_comp ht ct c pns rule     => if hideRule _ _ rule
-                                            then SCND_toLatexMath pns
-                                            else rawLatexMath "\trfrac["+++ toLatexMath rule +++ rawLatexMath "]{" +++ eolL +++
-                                              SCND_toLatexMath pns +++ rawLatexMath "}{" +++ eolL +++
-                                              toLatexMath c +++ rawLatexMath "}" +++ eolL
-      end.
-  End SCND_toLatex.
-
-  (* this is a work-in-progress; please use SCND_toLatexMath for now *)
-  Fixpoint nd_toLatexMath {h}{c}(nd:@ND _ Rule h c)(indent:string) :=
-    match nd with
-      | nd_id0                      => rawLatexMath indent +++
-                                       rawLatexMath "% nd_id0 " +++ eolL
-      | nd_id1  h'                  => rawLatexMath indent +++
-                                       rawLatexMath "% nd_id1 "+++ judgments2latex h +++ eolL
-      | nd_weak h'                  => rawLatexMath indent +++
-                                       rawLatexMath "\inferrule*[Left=ndWeak]{" +++ toLatexMath h' +++ rawLatexMath "}{ }" +++ eolL
-      | nd_copy h'                  => rawLatexMath indent +++
-                                       rawLatexMath "\inferrule*[Left=ndCopy]{"+++judgments2latex h+++
-                                                         rawLatexMath "}{"+++judgments2latex c+++rawLatexMath "}" +++ eolL
-      | nd_prod h1 h2 c1 c2 pf1 pf2 => rawLatexMath indent +++
-                                       rawLatexMath "% prod " +++ eolL +++
-                                       rawLatexMath indent +++
-                                       rawLatexMath "\begin{array}{c c}" +++ eolL +++
-                                       (nd_toLatexMath pf1 ("  "+++indent)) +++
-                                       rawLatexMath indent +++
-                                       rawLatexMath " & " +++ eolL +++
-                                       (nd_toLatexMath pf2 ("  "+++indent)) +++
-                                       rawLatexMath indent +++
-                                       rawLatexMath "\end{array}"
-      | nd_comp h  m     c  pf1 pf2 => rawLatexMath indent +++
-                                       rawLatexMath "% comp " +++ eolL +++
-                                       rawLatexMath indent +++
-                                       rawLatexMath "\begin{array}{c}" +++ eolL +++
-                                       (nd_toLatexMath pf1 ("  "+++indent)) +++
-                                       rawLatexMath indent +++
-                                       rawLatexMath " \\ " +++ eolL +++
-                                       (nd_toLatexMath pf2 ("  "+++indent)) +++
-                                       rawLatexMath indent +++
-                                       rawLatexMath "\end{array}"
-      | nd_cancell a                => rawLatexMath indent +++
-                                       rawLatexMath "% nd-cancell " +++ (judgments2latex a) +++ eolL
-      | nd_cancelr a                => rawLatexMath indent +++
-                                       rawLatexMath "% nd-cancelr " +++ (judgments2latex a) +++ eolL
-      | nd_llecnac a                => rawLatexMath indent +++
-                                       rawLatexMath "% nd-llecnac " +++ (judgments2latex a) +++ eolL
-      | nd_rlecnac a                => rawLatexMath indent +++
-                                       rawLatexMath "% nd-rlecnac " +++ (judgments2latex a) +++ eolL
-      | nd_assoc   a b c            => rawLatexMath ""
-      | nd_cossa   a b c            => rawLatexMath ""
-      | nd_rule    h c r            => toLatexMath r
-    end.
-
-End ToLatex.