diff --git a/examples/functionality/theorem.md b/examples/functionality/theorem.md new file mode 100644 index 0000000..132d23f --- /dev/null +++ b/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. diff --git a/src/backend/latex/complex/mod.rs b/src/backend/latex/complex/mod.rs index 8591df6..1c9985e 100644 --- a/src/backend/latex/complex/mod.rs +++ b/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}; diff --git a/src/backend/latex/complex/proof.rs b/src/backend/latex/complex/proof.rs new file mode 100644 index 0000000..07084fd --- /dev/null +++ b/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>, + gen: &mut Generator<'a, impl Backend<'a>, impl Write>, + ) -> Result { + 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>>, + ) -> Result<()> { + write!(gen.get_out(), "\\end{{{}}}", self.kind.context_name())?; + Ok(()) + } +} diff --git a/src/backend/latex/document/article.rs b/src/backend/latex/document/article.rs index 3ac5061..fdaea27 100644 --- a/src/backend/latex/document/article.rs +++ b/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 diff --git a/src/backend/latex/document/beamer.rs b/src/backend/latex/document/beamer.rs index b1f9cdd..e2331d5 100644 --- a/src/backend/latex/document/beamer.rs +++ b/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 { diff --git a/src/backend/latex/document/report.rs b/src/backend/latex/document/report.rs index 90c3eca..36d3d16 100644 --- a/src/backend/latex/document/report.rs +++ b/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 diff --git a/src/backend/latex/document/thesis.rs b/src/backend/latex/document/thesis.rs index a0fc8b5..7f51bc0 100644 --- a/src/backend/latex/document/thesis.rs +++ b/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 diff --git a/src/backend/latex/mod.rs b/src/backend/latex/mod.rs index 8fdca58..bfa5eac 100644 --- a/src/backend/latex/mod.rs +++ b/src/backend/latex/mod.rs @@ -54,6 +54,7 @@ use self::complex::{ ListGen, MathBlockGen, ParagraphGen, + ProofGen, RuleGen, BeamerRuleGen, TableCellGen, diff --git a/src/backend/latex/preamble.rs b/src/backend/latex/preamble.rs index e3c1555..5b68432 100644 --- a/src/backend/latex/preamble.rs +++ b/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} +"#; diff --git a/src/backend/mod.rs b/src/backend/mod.rs index e8bf287..85eb33c 100644 --- a/src/backend/mod.rs +++ b/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<()>; diff --git a/src/cskvp.rs b/src/cskvp.rs index 979e891..ecc3ab4 100644 --- a/src/cskvp.rs +++ b/src/cskvp.rs @@ -160,6 +160,14 @@ impl<'a> Cskvp<'a> { self.double.remove(key) } + pub fn take_single(&mut self) -> Option>> { + 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. diff --git a/src/frontend/event.rs b/src/frontend/event.rs index 8785915..905a6ba 100644 --- a/src/frontend/event.rs +++ b/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>>, pub height: Option>>, } + +#[derive(Debug, Clone)] +pub struct Proof<'a> { + pub kind: ProofKind, + pub label: Option>>, + pub title: Option>>, +} + +#[derive(Debug, Clone)] +pub enum ProofKind { + Corollary, + Definition, + Theorem, + Lemma, + Proof, +} diff --git a/src/frontend/mod.rs b/src/frontend/mod.rs index f2411bf..3f8fd25 100644 --- a/src/frontend/mod.rs +++ b/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>, cskvp: Option>, ) { diff --git a/src/generator/code_gen_units.rs b/src/generator/code_gen_units.rs index 303c3a3..28875eb 100644 --- a/src/generator/code_gen_units.rs +++ b/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>), @@ -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), } } diff --git a/src/generator/event.rs b/src/generator/event.rs index 085365f..6ed91b4 100644 --- a/src/generator/event.rs +++ b/src/generator/event.rs @@ -23,6 +23,8 @@ pub use crate::frontend::{ Table, TaskListMarker, Url, + Proof, + ProofKind, }; pub use pulldown_cmark::Alignment; diff --git a/test.md b/test.md index ba7e179..0a35da4 100644 --- a/test.md +++ b/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]