Add a generator for theorems

They are specifically defined in such a way in the front end as to allow
nesting of other Markdown elements inside their description. This makes
it more natural to have theorems not only consisting of math blocks
while allowing the natural nesting of them.

examples/functionality/theorem.md

@@ -0,0 +1,20 @@
+# Theorems
+
+{definition}
+> A natural number `$ n` is called prime if it has exactly two divisors.
+
+{lemma, title="Euclid"}
+> If `$ p` is prime and divides `$ ab` then it divides `$ a` or `$ b`.
+
+{corollary, title="Prime factorization"}
+> Each number has a canonical decomposition into prime factors.
+
+{theorem, title="The main theorem"}
+> There is an infinite number of prime numbers.
+
+{proof}
+> Assume `$ p` to be the largest prime number. Define
+> ```$$
+> P' = 1+ \prod^p_{i=0, i prime} i
+> ```
+> Then `$ P'` is not divisible by any prime. But it has at least two divisors, one and itself, so there must a prime divisor larger than `$ p`. This is a contradiction.

src/backend/latex/complex/mod.rs

@@ -12,6 +12,7 @@ mod math;
 mod paragraph;
 mod rule;
 mod table;
+mod proof;
 
 pub use self::blockquote::BlockQuoteGen;
 pub use self::codeblock::CodeBlockGen;
@@ -25,5 +26,6 @@ pub use self::link::{InterLinkWithContentGen, UrlWithContentGen};
 pub use self::list::{EnumerateGen, ItemGen, ListGen};
 pub use self::math::{InlineMathGen, MathBlockGen};
 pub use self::paragraph::ParagraphGen;
+pub use self::proof::ProofGen;
 pub use self::rule::{RuleGen, BeamerRuleGen};
 pub use self::table::{TableCellGen, TableGen, TableHeadGen, TableRowGen};

src/backend/latex/complex/proof.rs

@@ -0,0 +1,57 @@
+use std::io::Write;
+
+use crate::backend::{Backend, CodeGenUnit};
+use crate::config::Config;
+use crate::error::Result;
+use crate::frontend::range::WithRange;
+use crate::generator::event::{Event, Proof, ProofKind};
+use crate::generator::Generator;
+
+trait ContextName {
+    fn context_name(&self) -> &'static str;
+}
+
+impl ContextName for ProofKind {
+    fn context_name(&self) -> &'static str {
+        match self {
+            ProofKind::Corollary => "amsthm-corollary",
+            ProofKind::Definition => "amsthm-definition",
+            ProofKind::Lemma => "amsthm-lemma",
+            ProofKind::Proof => "proof",
+            ProofKind::Theorem=> "amsthm-theorem",
+        }
+    }
+}
+
+#[derive(Debug)]
+pub struct ProofGen {
+    kind: ProofKind,
+}
+
+impl<'a> CodeGenUnit<'a, Proof<'a>> for ProofGen {
+    fn new(
+        _cfg: &'a Config, proof: WithRange<Proof<'a>>,
+        gen: &mut Generator<'a, impl Backend<'a>, impl Write>,
+    ) -> Result<Self> {
+        let WithRange(element, _range) = proof;
+        let out = gen.get_out();
+        write!(out, "\\begin{{{}}}", element.kind.context_name())?;
+        if let Some(WithRange(title, _)) = element.title {
+            write!(out, "[{}]", title)?;
+        }
+        if let Some(WithRange(label, _)) = element.label {
+            write!(out, "\\label{{{}}}", label)?;
+        }
+        Ok(ProofGen {
+            kind: element.kind,
+        })
+    }
+
+    fn finish(
+        self, gen: &mut Generator<'a, impl Backend<'a>, impl Write>,
+        _peek: Option<WithRange<&Event<'a>>>,
+    ) -> Result<()> {
+        write!(gen.get_out(), "\\end{{{}}}", self.kind.context_name())?;
+        Ok(())
+    }
+}

src/backend/latex/document/article.rs

@@ -59,6 +59,7 @@ impl<'a> Backend<'a> for Article {
 
     type MathBlock = latex::MathBlockGen<'a>;
     type Graphviz = latex::GraphvizGen<'a>;
+    type Proof = latex::ProofGen;
 
     fn new() -> Self {
         Article

src/backend/latex/document/beamer.rs

@@ -136,6 +136,7 @@ impl<'a> Backend<'a> for Beamer {
 
     type MathBlock = latex::MathBlockGen<'a>;
     type Graphviz = latex::GraphvizGen<'a>;
+    type Proof = latex::ProofGen;
 
     fn new() -> Self {
         Beamer {

src/backend/latex/document/report.rs

@@ -59,6 +59,7 @@ impl<'a> Backend<'a> for Report {
 
     type MathBlock = latex::MathBlockGen<'a>;
     type Graphviz = latex::GraphvizGen<'a>;
+    type Proof = latex::ProofGen;
 
     fn new() -> Self {
         Report

src/backend/latex/document/thesis.rs

@@ -67,6 +67,7 @@ impl<'a> Backend<'a> for Thesis {
 
     type MathBlock = latex::MathBlockGen<'a>;
     type Graphviz = latex::GraphvizGen<'a>;
+    type Proof = latex::ProofGen;
 
     fn new() -> Self {
         Thesis

src/backend/latex/mod.rs

@@ -54,6 +54,7 @@ use self::complex::{
     ListGen,
     MathBlockGen,
     ParagraphGen,
+    ProofGen,
     RuleGen,
     BeamerRuleGen,
     TableCellGen,

src/backend/latex/preamble.rs

@@ -64,6 +64,7 @@ pub fn write_packages(cfg: &Config, out: &mut impl Write) -> Result<()> {
     writeln!(out, "\\usepackage{{environ}}")?;
     writeln!(out, "\\usepackage{{amssymb}}")?;
     writeln!(out, "\\usepackage{{amsmath}}")?;
+    writeln!(out, "\\usepackage{{amsthm}}")?;
     writeln!(out, "\\usepackage{{stmaryrd}}")?;
     writeln!(out, "\\usepackage[gen]{{eurosym}}")?;
     writeln!(out, "\\usepackage[normalem]{{ulem}}")?;
@@ -100,6 +101,7 @@ pub fn write_fixes(cfg: &Config, out: &mut impl Write) -> Result<()> {
     writeln!(out, "{}", IMAGE_WITH_TEXT)?;
     writeln!(out, "{}", SCALE_TIKZ_PICTURE_TO_WIDTH)?;
     writeln!(out, "{}", TABULARX)?;
+    writeln!(out, "{}", AMSTHM_DEFAULTS)?;
     // TODO: figures inline? https://tex.stackexchange.com/a/11342 last codeblock
     // with package float and `[H]`
 
@@ -524,3 +526,14 @@ pub const TABULARX: &str = r#"
 \newcolumntype{R}{>{\raggedleft\let\newline\\\arraybackslash\hspace{0pt}}X}
 \renewcommand\tabularxcolumn[1]{m{#1}}
 "#;
+
+// TODO: i18n? How to interact with this smartly?
+pub const AMSTHM_DEFAULTS: &str = r#"
+\newcounter{common-thm-ctr}
+\theoremstyle{plain}
+\newtheorem{amsthm-theorem}[common-thm-ctr]{Theorem}
+\newtheorem{amsthm-lemma}[common-thm-ctr]{Lemma}
+\newtheorem{amsthm-corollary}[common-thm-ctr]{Corollary}
+\theoremstyle{amsthm-definition}
+\newtheorem{amsthm-definition}[common-thm-ctr]{Definition}
+"#;

src/backend/mod.rs

@@ -28,6 +28,7 @@ use crate::generator::event::{
     Table,
     TaskListMarker,
     Url,
+    Proof,
 };
 use crate::generator::{Generator, Stack};
 
@@ -94,6 +95,7 @@ pub trait Backend<'a>: Sized + Debug {
 
     type MathBlock: StatefulCodeGenUnit<'a, Self, MathBlock<'a>>;
     type Graphviz: StatefulCodeGenUnit<'a, Self, Graphviz<'a>>;
+    type Proof: StatefulCodeGenUnit<'a, Self, Proof<'a>>;
 
     fn new() -> Self;
     fn gen_preamble(&mut self, cfg: &Config, out: &mut impl Write, diagnostics: &Diagnostics<'a>) -> FatalResult<()>;

src/cskvp.rs

@@ -160,6 +160,14 @@ impl<'a> Cskvp<'a> {
         self.double.remove(key)
     }
 
+    pub fn take_single(&mut self) -> Option<WithRange<Cow<'a, str>>> {
+        if self.single.is_empty() {
+            None
+        } else {
+            Some(self.single.remove(0))
+        }
+    }
+
     /// Removes all elements from `self`.
     ///
     /// This can be used before dropping `Cskvp` to omit all "unused attribute" warnings.

src/frontend/event.rs

@@ -95,6 +95,7 @@ pub enum Tag<'a> {
 
     MathBlock(MathBlock<'a>),
     Graphviz(Graphviz<'a>),
+    Proof(Proof<'a>),
 }
 
 #[derive(Debug, Clone)]
@@ -167,3 +168,19 @@ pub struct Graphviz<'a> {
     pub width: Option<WithRange<Cow<'a, str>>>,
     pub height: Option<WithRange<Cow<'a, str>>>,
 }
+
+#[derive(Debug, Clone)]
+pub struct Proof<'a> {
+    pub kind: ProofKind,
+    pub label: Option<WithRange<Cow<'a, str>>>,
+    pub title: Option<WithRange<Cow<'a, str>>>,
+}
+
+#[derive(Debug, Clone)]
+pub enum ProofKind {
+    Corollary,
+    Definition,
+    Theorem,
+    Lemma,
+    Proof,
+}

src/frontend/mod.rs

@@ -503,6 +503,7 @@ impl<'a> Frontend<'a> {
         // otherwise create label event
         match self.parser.peek().unwrap() {
             WithRange(CmarkEvent::Start(CmarkTag::Header(_)), _)
+            | WithRange(CmarkEvent::Start(CmarkTag::BlockQuote), _)
             | WithRange(CmarkEvent::Start(CmarkTag::CodeBlock(_)), _)
             | WithRange(CmarkEvent::Start(CmarkTag::Table(_)), _)
             | WithRange(CmarkEvent::Start(CmarkTag::Image(..)), _) => {
@@ -560,6 +561,9 @@ impl<'a> Frontend<'a> {
             CmarkEvent::Start(CmarkTag::Header(label)) => {
                 self.convert_header(WithRange(label, next_range), Some(cskvp))
             },
+            CmarkEvent::Start(CmarkTag::BlockQuote) => {
+                self.convert_block_quote(next_range, cskvp)
+            },
             CmarkEvent::Start(CmarkTag::CodeBlock(lang)) => {
                 self.convert_code_block(WithRange(lang, next_range), Some(cskvp))
             },
@@ -656,6 +660,45 @@ impl<'a> Frontend<'a> {
         self.buffer.push_back(WithRange(Event::End(tag), range));
     }
 
+    fn convert_block_quote(&mut self, range: SourceRange, mut cskvp: Cskvp<'a>) {
+        let prefix = cskvp.take_single();
+
+        let kind = if let Some(prefix) = prefix {
+            match prefix.as_ref().element().as_ref() {
+                "corollary" => ProofKind::Corollary,
+                "definition" => ProofKind::Definition,
+                "lemma" => ProofKind::Lemma,
+                "proof" => ProofKind::Proof,
+                "theorem" => ProofKind::Theorem,
+                other => {
+                    self.diagnostics
+                        .error(format!("unknown quote environment {:?}", other))
+                        .with_error_section(prefix.range(), "type defined here")
+                        .emit();
+                    return;
+                }
+            }
+        } else {
+            self.diagnostics
+                .error("quote environment has no type")
+                .with_error_section(range, "configuration defined here")
+                .help("try indicating the type, the configuration could look like")
+                .help("  {proof}")
+                .emit();
+            return;
+        };
+
+        let tag = Tag::Proof(Proof {
+            kind,
+            label: cskvp.take_label(),
+            title: cskvp.take_double("title"),
+        });
+
+        self.buffer.push_back(WithRange(Event::Start(tag.clone()), range));
+        self.convert_until_end_inclusive(|t| if let CmarkTag::BlockQuote = t { true } else { false });
+        self.buffer.push_back(WithRange(Event::End(tag), range));
+    }
+
     fn convert_table(
         &mut self, WithRange(alignment, range): WithRange<Vec<Alignment>>, cskvp: Option<Cskvp<'a>>,
     ) {

src/generator/code_gen_units.rs

@@ -37,6 +37,7 @@ pub enum StackElement<'a, B: Backend<'a>> {
     InlineMath(B::InlineMath),
     MathBlock(B::MathBlock),
     Graphviz(B::Graphviz),
+    Proof(B::Proof),
 
     // resolve context
     Context(Context, Arc<Diagnostics<'a>>),
@@ -74,6 +75,7 @@ impl<'a, B: Backend<'a>> StackElement<'a, B> {
             Tag::InlineMath => Ok(InlineMath(B::InlineMath::new(cfg, WithRange((), range), gen)?)),
             Tag::MathBlock(block) => Ok(MathBlock(B::MathBlock::new(cfg, WithRange(block, range), gen)?)),
             Tag::Graphviz(graphviz) => Ok(Graphviz(B::Graphviz::new(cfg, WithRange(graphviz, range), gen)?)),
+            Tag::Proof(proof) => Ok(Proof(B::Proof::new(cfg, WithRange(proof, range), gen)?)),
         }
     }
 
@@ -104,6 +106,7 @@ impl<'a, B: Backend<'a>> StackElement<'a, B> {
             InlineMath(s) => s.output_redirect(),
             MathBlock(s) => s.output_redirect(),
             Graphviz(s) => s.output_redirect(),
+            Proof(s) => s.output_redirect(),
 
             Context(..) => None,
         }
@@ -136,6 +139,7 @@ impl<'a, B: Backend<'a>> StackElement<'a, B> {
             (InlineMath(s), Tag::InlineMath) => s.finish(gen, peek),
             (MathBlock(s), Tag::MathBlock(_)) => s.finish(gen, peek),
             (Graphviz(s), Tag::Graphviz(_)) => s.finish(gen, peek),
+            (Proof(s), Tag::Proof(_)) => s.finish(gen, peek),
             (state, tag) => unreachable!("invalid end tag {:?}, expected {:?}", tag, state),
         }
     }

src/generator/event.rs

@@ -23,6 +23,8 @@ pub use crate::frontend::{
     Table,
     TaskListMarker,
     Url,
+    Proof,
+    ProofKind,
 };
 pub use pulldown_cmark::Alignment;
 

test.md

@@ -43,6 +43,8 @@ Reference to [#test-heading].
 
 [include examples/functionality/math.md]
 
+[include examples/functionality/theorem.md]
+
 [include examples/functionality/latex-block.md]
 
 [appendix]