Initial release

sliminality · Jun 28, 2019 · 0b98945 · 0b98945
1 parent 062646c
commit 0b98945
Show file tree

Hide file tree

Showing 19 changed files with 644 additions and 205 deletions.
diff --git a/.gitignore b/.gitignore
@@ -1,3 +1,6 @@
 .stack-work/
 pandoc-theorem.cabal
 *~
+examples/*.pdf
+examples/*.tex
+!examples/header.tex
diff --git a/Makefile b/Makefile
@@ -0,0 +1,35 @@
+# Run the test suite during development.
+dev:
+	stack test --fast --haddock-deps --file-watch
+
+# Autoformat code using Brittany.
+format:
+	brittany --indent=4 --write-mode=inplace ./**/*.hs
+
+# Copy binaries to $HOME/.local/bin.
+install:
+	stack install
+
+# Build PDF and write to disk.
+%.pdf: %.md
+	pandoc --filter pandoc-theorem-exe $< -H examples/header.tex -o $@
+
+# Output LaTeX to stdout.
+%.tex: %.md
+	pandoc --filter pandoc-theorem-exe $< -H examples/header.tex -t latex
+
+# Output the Pandoc AST to stdout.
+%.ast: %.md
+	pandoc --filter pandoc-theorem-exe $< -H examples/header.tex -t native
+
+# Build PDF without filter, and write to disk.
+%.clean.pdf: %.md
+	pandoc $< -o $@
+
+# Output LaTeX to stdout, compiling without the filter.
+%.clean.tex: %.md
+	pandoc $< -t latex
+
+# Output the Pandoc AST to stdout, compiling without the filter.
+%.clean.ast: %.md
+	pandoc $< -t native
diff --git a/README.md b/README.md
@@ -1 +1,217 @@
 # pandoc-theorem
+
+A [Pandoc](https://pandoc.org/) filter to convert [definition lists](https://pandoc.org/MANUAL.html#definition-lists) into [amsthm](https://www.ctan.org/pkg/amsthm) theorem environments, for compiling to PDF and LaTeX.
+
+The extension supports the following theorem environments:
+
+<a name="identifiers">
+
+| Supported environment | Supported Markdown identifiers |
+|-|-|
+| `definition` | `Definition`, `Def` |
+| `theorem` | `Theorem`, `Thm` |
+| `lemma` | `Lemma` |
+| `proof` | `Proof`, `Pf` |
+
+Note that compilation targets other than PDF and LaTeX have not been tested. Notably, this includes HTML.
+
+## Example
+
+Given the following Markdown:
+
+```markdown
+Lemma (Pumping Lemma). \label{pumping}
+
+:   Let $L$ be a regular language. Then there exists an integer $p \geq 1$ called the "pumping length" which depends only on $L$, such that every string $w \in L$ of length at least $p$ can be divided into three substrings $w = xyz$ such that the following conditions hold:
+
+    - $|y| \geq 1$
+    - $|xy| \leq p$
+    - $xy^n z \in L$, for all $n \geq 0$.
+
+    That is, the non-empty substring $y$ occurring within the first $p$ characters of $w$ can be "pumped" any number of times, and the resulting string is always in $L$.
+```
+
+we transform it into this PDF output:
+
+![LaTeX compilation output](examples/example-block.png)
+
+equivalent to this LaTeX:
+
+```latex
+\begin{lemma}[Pumping Lemma] \label{lem}
+
+Let \(L\) be a regular language. Then there exists an integer
+\(p \geq 1\) called the ``pumping length'' which depends only on \(L\),
+such that every string \(w \in L\) of length at least \(p\) can be
+divided into three substrings \(w = xyz\) such that the following
+conditions hold:
+
+\begin{itemize}
+\tightlist
+\item
+  \(|y| \geq 1\)
+\item
+  \(|xy| \leq p\)
+\item
+  \(xy^n z \in L\), for all \(n \geq 0\).
+\end{itemize}
+
+That is, the non-empty substring \(y\) occurring within the first \(p\)
+characters of \(w\) can be ``pumped'' any number of times, and the
+resulting string is always in \(L\).
+
+\end{lemma}
+```
+
+## Usage
+
+### Installation
+
+You must have Pandoc installed and available in your PATH.
+
+Clone and `stack install` this repository, which copies the `pandoc-theorem-exe` binary to your global Stack install location. Now `pandoc-theorem-exe` should be in your PATH as well.
+
+```
+$ which pandoc-theorem-exe
+/Users/slim/.local/bin/pandoc-theorem-exe
+```
+
+### Syntax
+
+pandoc-theorem repurposes the syntax for [definition lists](https://pandoc.org/MANUAL.html#definition-lists), checking for [recognized identifiers](#identifiers).
+
+```markdown
+Theorem (Fermat's Little).
+
+:    If $p$ is a prime number, then for any integer $a$, the number $$a^p - a$$ is an integer multiple of $p$.
+```
+
+In general, the format looks like this:
+
+```markdown
+<term>
+
+:    <body>
+```
+where `<body>` is standard Pandoc Markdown (with inline or block formatting), and `<term>` is one of the following:
+```
+<term> ::= <identifier>.
+        |  <identifier> (<name>).
+        |  <identifier> (<name>). <additional text>
+```
+
+That is, a `<term>` consists of:
+
+- A supported environment identifier (required), followed by either
+    - A period (`.`) if the environment has no name, or
+    - A name in parentheses `()` which will be passed to the LaTeX environment
+- Optional additional Pandoc Markdown (e.g. for LaTeX `\labels`)
+
+Supported `<identifier>` values are [documented](#identifiers).
+
+Confused about indentation, line spacing, or the `:` characters? Consult the documentated syntax for Pandoc [definition lists](https://pandoc.org/MANUAL.html#definition-lists).
+
+More examples can be found in the [Examples](#examples) section below.
+
+### Compilation
+
+To use, pass the `pandoc-theorem-exe` executable as a filter to [Pandoc](https://pandoc.org/):
+
+```sh
+# Compile to PDF.
+pandoc --filter pandoc-theorem-exe input.md -H header.tex -o output.pdf
+
+# Output LaTeX.
+pandoc --filter pandoc-theorem-exe input.md -H header.tex -t latex
+```
+
+Note that you will always need to include the following header file using Pandoc's `-H` flag:
+
+```latex
+% examples/header.tex
+\usepackage{amsthm}
+\newtheorem{definition}{Definition}
+\newtheorem{lemma}{Lemma}
+\newtheorem{theorem}{Theorem}
+```
+
+## Examples
+
+This repository includes an example Markdown file in `examples/kitchen-sink.md`. You can explore its output using the following command:
+
+```sh
+pandoc --filter pandoc-theorem-exe examples/kitchen-sink.md -H examples/header.tex -o examples/kitchen-sink.pdf
+```
+
+### Simple block-level theorem
+
+```markdown
+Theorem (Hedberg).
+
+:   Any type with decidable equality is a set.
+```
+
+![Compiled LaTeX PDF for simple block-level theorem](examples/example-block.png)
+
+### Complex block-level theorem
+
+```markdown
+Lemma (Pumping Lemma). \label{lem}
+
+:   Let $L$ be a regular language. Then there exists an integer $p \geq 1$ called the "pumping length" which depends only on $L$, such that every string $w \in L$ of length at least $p$ can be divided into three substrings $w = xyz$ such that the following conditions hold:
+
+    - $|y| \geq 1$
+    - $|xy| \leq p$
+    - $xy^n z \in L$, for all $n \geq 0$.
+
+    That is, the non-empty substring $y$ occurring within the first $p$ characters of $w$ can be "pumped" any number of times, and the resulting string is always in $L$.
+```
+
+![Compiled LaTeX PDF for complex block-level theorem](examples/example-block.png)
+
+### Single inline theorem
+
+```markdown
+Proof. 
+: By induction on the structure of the typing judgment.
+```
+
+![Compiled LaTeX PDF for inline theorem](examples/example-inline.png)
+
+### Multiple inline theorems
+
+```markdown
+Def (Agda).
+:   A dependently-typed programming language often used for interactive theorem proving.
+:   A video game that doesn't mean you understand the underlying theory, according to Bob.
+```
+
+![Compiled LaTeX PDF for multiple inline theorems](examples/example-multiple-inline.png)
+
+### Regular definition lists still work
+
+If you do not use 
+
+```markdown
+Groceries
+: Bananas
+: Lenses
+: Barbed wire
+```
+
+```markdown
+Programming language checklist
+
+:     *Strictures:* Does the language have sufficiently many restrictions? It is always easier to relax strictures later on.
+
+:     *Affordances:* Actually, these don't really matter.
+```
+
+![Compiled LaTeX PDF for regular Pandoc definition lists](examples/example-regular-definitions.png)
+
+## Acknowledgements
+
+In addition to [John MacFarlane](https://www.johnmacfarlane.net/)'s incredible work on Pandoc itself, this filter benefited from the following prior efforts:
+
+- [pandoc-moreblock-filter](https://github.com/NMarkgraf/pandoc-moreblock-filter/blob/master/moreblocks.hs) and [npfc](https://github.com/NMarkgraf/npfc/blob/master/moreblocks.py) by [Norman Markgraf](https://github.com/NMarkgraf)
+- [defenv.py](https://github.com/01mf02/pandocfilters/blob/master/defenv.py) by [Michael Färber](https://github.com/01mf02), documented in [Pandoc filters for scientific writing](http://gedenkt.at/blog/scientific-pandoc/) and the earlier [Theorems in Pandoc](http://gedenkt.at/blog/theorems-in-pandoc/)
diff --git a/app/Main.hs b/app/Main.hs
@@ -1,7 +1,8 @@
 module Main where
 
+import Text.Pandoc.Builder (toList)
 import Text.Pandoc.JSON (toJSONFilter)
 import Env (convertBlock)
 
 main :: IO ()
-main = toJSONFilter convertBlock
+main = toJSONFilter $ toList . convertBlock
diff --git a/examples/example-block.png b/examples/example-block.png
diff --git a/examples/example-inline.png b/examples/example-inline.png
diff --git a/examples/example-multiple-inline.png b/examples/example-multiple-inline.png
diff --git a/examples/example-regular-definitions.png b/examples/example-regular-definitions.png
diff --git a/examples/example-simple.png b/examples/example-simple.png
diff --git a/header.tex → examples/header.tex b/header.tex → examples/header.tex
@@ -1,5 +1,5 @@
+% examples/header.tex
 \usepackage{amsthm}
 \newtheorem{definition}{Definition}
 \newtheorem{lemma}{Lemma}
 \newtheorem{theorem}{Theorem}
-
diff --git a/examples/kitchen-sink.md b/examples/kitchen-sink.md
@@ -0,0 +1,42 @@
+## Simple block-level theorem
+
+Theorem (Hedberg).
+
+:   Any type with decidable equality is a set.
+
+## Complex block-level theorem
+
+Lemma (Pumping Lemma). \label{lem}
+
+:   Let $L$ be a regular language. Then there exists an integer $p \geq 1$ called the "pumping length" which depends only on $L$, such that every string $w \in L$ of length at least $p$ can be divided into three substrings $w = xyz$ such that the following conditions hold:
+
+    - $|y| \geq 1$
+    - $|xy| \leq p$
+    - $xy^n z \in L$, for all $n \geq 0$.
+
+    That is, the non-empty substring $y$ occurring within the first $p$ characters of $w$ can be "pumped" any number of times, and the resulting string is always in $L$.
+
+## Single inline theorem
+
+Proof. 
+: By induction on the structure of the typing judgment.
+
+## Multiple inline theorems
+
+Def (Agda).
+:   A dependently-typed programming language often used for interactive theorem proving.
+:   A video game that doesn't mean you understand the underlying theory, according to Bob.
+
+## Regular definition lists still work
+
+Groceries
+: Bananas
+: Lenses
+: Barbed wire
+
+Programming language checklist
+
+:     *Strictures:* Does the language have sufficiently many restrictions? It is always easier to relax strictures later on.
+
+:     *Affordances:* Actually, these don't really matter.
+
diff --git a/native b/native
@@ -0,0 +1,33 @@
+<!DOCTYPE html>
+<html xmlns="http://www.w3.org/1999/xhtml" lang="" xml:lang="">
+<head>
+  <meta charset="utf-8" />
+  <meta name="generator" content="pandoc" />
+  <meta name="viewport" content="width=device-width, initial-scale=1.0, user-scalable=yes" />
+  <title>test</title>
+  <style>
+      code{white-space: pre-wrap;}
+      span.smallcaps{font-variant: small-caps;}
+      span.underline{text-decoration: underline;}
+      div.column{display: inline-block; vertical-align: top; width: 50%;}
+  </style>
+  <!--[if lt IE 9]>
+    <script src="//cdnjs.cloudflare.com/ajax/libs/html5shiv/3.7.3/html5shiv-printshiv.min.js"></script>
+  <![endif]-->
+  \usepackage{amsthm}
+  \newtheorem{definition}{Definition}
+  \newtheorem{lemma}{Lemma}
+  \newtheorem{theorem}{Theorem}
+</head>
+<body>
+ Lemma). 
+<p>Let <span class="math inline"><em>L</em></span> be a regular language. Then there exists an integer <span class="math inline"><em>p</em> ≥ 1</span> called the “pumping length” which depends only on <span class="math inline"><em>L</em></span>, such that every string <span class="math inline"><em>w</em> ∈ <em>L</em></span> of length at least <span class="math inline"><em>p</em></span> can be divided into three substrings <span class="math inline"><em>w</em> = <em>x</em><em>y</em><em>z</em></span> such that the following conditions hold:</p>
+<ul>
+<li><span class="math inline">|<em>y</em>| ≥ 1</span></li>
+<li><span class="math inline">|<em>x</em><em>y</em>| ≤ <em>p</em></span></li>
+<li><span class="math inline"><em>x</em><em>y</em><sup><em>n</em></sup><em>z</em> ∈ <em>L</em></span>, for all <span class="math inline"><em>n</em> ≥ 0</span>.</li>
+</ul>
+<p>That is, the non-empty substring <span class="math inline"><em>y</em></span> occurring within the first <span class="math inline"><em>p</em></span> characters of <span class="math inline"><em>w</em></span> can be “pumped” any number of times, and the resulting string is always in <span class="math inline"><em>L</em></span>.</p>
+ Lemma).
+</body>
+</html>
diff --git a/package.yaml b/package.yaml
@@ -24,6 +24,7 @@ dependencies:
 - pandoc
 - pandoc-types
 - text
+- containers
 
 library:
   source-dirs: src
@@ -49,3 +50,4 @@ tests:
     - -with-rtsopts=-N
     dependencies:
     - pandoc-theorem
+    - hspec