Add Theorems

Cargo.toml

@@ -6,7 +6,7 @@ edition = "2018"
 
 [dependencies]
 pulldown-cmark = "0.4.0"
-str-concat = "0.1.4"
+str-concat = "0.2.0"
 structopt = "0.2.10"
 void = "1.0.2"
 boolinator = "2.4"

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/math.rs

@@ -1,11 +1,11 @@
+use std::borrow::Cow;
 use std::io::Write;
 
-use crate::backend::latex::InlineEnvironment;
 use crate::backend::{Backend, CodeGenUnit};
 use crate::config::Config;
 use crate::error::Result;
 use crate::frontend::range::WithRange;
-use crate::generator::event::{Equation, Event};
+use crate::generator::event::{Event, MathBlock, MathBlockKind};
 use crate::generator::Generator;
 
 #[derive(Debug)]
@@ -30,62 +30,36 @@ impl<'a> CodeGenUnit<'a, ()> for InlineMathGen {
 }
 
 #[derive(Debug)]
-pub struct EquationGen<'a> {
-    inline_fig: InlineEnvironment<'a>,
+pub struct MathBlockGen<'a> {
+    _label: Option<WithRange<Cow<'a, str>>>,
+    kind: MathBlockKind,
 }
 
-impl<'a> CodeGenUnit<'a, Equation<'a>> for EquationGen<'a> {
+impl<'a> CodeGenUnit<'a, MathBlock<'a>> for MathBlockGen<'a> {
     fn new(
-        _cfg: &Config, eq: WithRange<Equation<'a>>,
+        _cfg: &Config, eq: WithRange<MathBlock<'a>>,
         gen: &mut Generator<'a, impl Backend<'a>, impl Write>,
     ) -> Result<Self> {
-        let WithRange(Equation { label, caption }, _range) = eq;
-        let inline_fig = InlineEnvironment::new_figure(label, caption);
+        let WithRange(MathBlock { kind, label, caption }, _range) = eq;
         let out = gen.get_out();
-        inline_fig.write_begin(&mut *out)?;
 
-        writeln!(out, "\\begin{{align*}}")?;
+        match kind {
+            MathBlockKind::Equation => writeln!(out, "\\begin{{align*}}")?,
+            MathBlockKind::NumberedEquation => writeln!(out, "\\begin{{align}}")?,
+        }
 
-        Ok(EquationGen { inline_fig })
+        Ok(MathBlockGen { _label: label, kind })
     }
 
     fn finish(
         self, gen: &'_ mut Generator<'a, impl Backend<'a>, impl Write>,
         _peek: Option<WithRange<&Event<'a>>>,
     ) -> Result<()> {
         let out = gen.get_out();
-        writeln!(out, "\\end{{align*}}")?;
-        self.inline_fig.write_end(out)?;
-        Ok(())
-    }
-}
-
-#[derive(Debug)]
-pub struct NumberedEquationGen<'a> {
-    inline_fig: InlineEnvironment<'a>,
-}
-
-impl<'a> CodeGenUnit<'a, Equation<'a>> for NumberedEquationGen<'a> {
-    fn new(
-        _cfg: &Config, eq: WithRange<Equation<'a>>,
-        gen: &mut Generator<'a, impl Backend<'a>, impl Write>,
-    ) -> Result<Self> {
-        let WithRange(Equation { label, caption }, _range) = eq;
-        let inline_fig = InlineEnvironment::new_figure(label, caption);
-        let out = gen.get_out();
-        inline_fig.write_begin(&mut *out)?;
-
-        writeln!(out, "\\begin{{align}}")?;
-        Ok(NumberedEquationGen { inline_fig })
-    }
-
-    fn finish(
-        self, gen: &'_ mut Generator<'a, impl Backend<'a>, impl Write>,
-        _peek: Option<WithRange<&Event<'a>>>,
-    ) -> Result<()> {
-        let out = gen.get_out();
-        writeln!(out, "\\end{{align}}")?;
-        self.inline_fig.write_end(out)?;
+        match self.kind {
+            MathBlockKind::Equation => writeln!(out, "\\end{{align*}}")?,
+            MathBlockKind::NumberedEquation => writeln!(out, "\\end{{align}}")?,
+        }
         Ok(())
     }
 }

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;
@@ -23,7 +24,8 @@ pub use self::htmlblock::HtmlBlockGen;
 pub use self::inline::{InlineCodeGen, InlineEmphasisGen, InlineStrikethroughGen, InlineStrongGen};
 pub use self::link::{InterLinkWithContentGen, UrlWithContentGen};
 pub use self::list::{EnumerateGen, ItemGen, ListGen};
-pub use self::math::{EquationGen, InlineMathGen, NumberedEquationGen};
+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

@@ -57,9 +57,9 @@ impl<'a> Backend<'a> for Article {
     type InlineCode = latex::InlineCodeGen;
     type InlineMath = latex::InlineMathGen;
 
-    type Equation = latex::EquationGen<'a>;
-    type NumberedEquation = latex::NumberedEquationGen<'a>;
+    type MathBlock = latex::MathBlockGen<'a>;
     type Graphviz = latex::GraphvizGen<'a>;
+    type Proof = latex::ProofGen;
 
     fn new() -> Self {
         Article

src/backend/latex/document/beamer.rs

@@ -134,9 +134,9 @@ impl<'a> Backend<'a> for Beamer {
     type InlineCode = latex::InlineCodeGen;
     type InlineMath = latex::InlineMathGen;
 
-    type Equation = latex::EquationGen<'a>;
-    type NumberedEquation = latex::NumberedEquationGen<'a>;
+    type MathBlock = latex::MathBlockGen<'a>;
     type Graphviz = latex::GraphvizGen<'a>;
+    type Proof = latex::ProofGen;
 
     fn new() -> Self {
         Beamer {

src/backend/latex/document/report.rs

@@ -57,9 +57,9 @@ impl<'a> Backend<'a> for Report {
     type InlineCode = latex::InlineCodeGen;
     type InlineMath = latex::InlineMathGen;
 
-    type Equation = latex::EquationGen<'a>;
-    type NumberedEquation = latex::NumberedEquationGen<'a>;
+    type MathBlock = latex::MathBlockGen<'a>;
     type Graphviz = latex::GraphvizGen<'a>;
+    type Proof = latex::ProofGen;
 
     fn new() -> Self {
         Report

src/backend/latex/document/thesis.rs

@@ -65,9 +65,9 @@ impl<'a> Backend<'a> for Thesis {
     type InlineCode = latex::InlineCodeGen;
     type InlineMath = latex::InlineMathGen;
 
-    type Equation = latex::EquationGen<'a>;
-    type NumberedEquation = latex::NumberedEquationGen<'a>;
+    type MathBlock = latex::MathBlockGen<'a>;
     type Graphviz = latex::GraphvizGen<'a>;
+    type Proof = latex::ProofGen;
 
     fn new() -> Self {
         Thesis

src/backend/latex/mod.rs

@@ -38,7 +38,6 @@ use self::complex::{
     BookHeaderGen,
     CodeBlockGen,
     EnumerateGen,
-    EquationGen,
     FigureGen,
     FootnoteDefinitionGen,
     GraphvizGen,
@@ -53,8 +52,9 @@ use self::complex::{
     InterLinkWithContentGen,
     ItemGen,
     ListGen,
-    NumberedEquationGen,
+    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

@@ -14,7 +14,6 @@ use crate::generator::event::{
     BiberReference,
     CodeBlock,
     Enumerate,
-    Equation,
     Event,
     Figure,
     FootnoteDefinition,
@@ -24,10 +23,12 @@ use crate::generator::event::{
     Image,
     Svg,
     InterLink,
+    MathBlock,
     Pdf,
     Table,
     TaskListMarker,
     Url,
+    Proof,
 };
 use crate::generator::{Generator, Stack};
 
@@ -92,9 +93,9 @@ pub trait Backend<'a>: Sized + Debug {
     type InlineCode: StatefulCodeGenUnit<'a, Self, ()>;
     type InlineMath: StatefulCodeGenUnit<'a, Self, ()>;
 
-    type Equation: StatefulCodeGenUnit<'a, Self, Equation<'a>>;
-    type NumberedEquation: StatefulCodeGenUnit<'a, Self, Equation<'a>>;
+    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/concat.rs

@@ -42,7 +42,7 @@ impl<'a> Iterator for Concat<'a> {
 
             match t {
                 Cow::Borrowed(b) => match next {
-                    Cow::Borrowed(next) => match str_concat::concat(b, next) {
+                    Cow::Borrowed(next) => match unsafe { str_concat::concat(b, next) } {
                         Ok(res) => t = Cow::Borrowed(res),
                         Err(_) => t = Cow::Owned(b.to_string() + next),
                     },