logicaffeine_web/ui/components/
vernacular.rs

1//! Math mode's colouring, from the kernel's own vocabulary: its commands (`Definition`,
2//! `Inductive`, `Check`, …), the literate forms (`## To …:`, `Consider`, `When`, `Yield`,
3//! `## Theorem:` with `Statement:` and `Proof:`), the term grammar's binders and sorts
4//! (`forall`, `fun`, `Prop`), and the proof tactics. A test holds these lists to the kernel's
5//! parsers: every keyword they read is coloured, or named here as plain prose.
6
7use super::code_editor::{Token, TokenKind};
8
9/// The kernel's commands, the literate forms' structure words, and the term grammar's binders and
10/// annotations (`@[binder …]`, `@[source …]`, `@[mdata …]`).
11const KEYWORDS: &[&str] = &[
12    "Definition", "Inductive", "Check", "Eval", "Theorem", "Lemma", "Axiom", "Hypothesis",
13    "Variable", "Parameter", "Proof", "Qed", "Statement", "To", "Consider", "When", "Yield", "Let",
14    "let", "Theory", "Main", "Note", "Attribute", "Apply", "Name", "hint", "given", "prove",
15    "cites", "be", "yields", "fix", "forall", "fun", "exists", "match", "return", "with", "end",
16    "in", "if", "then", "else", "as", "by", "binder", "source", "mdata",
17];
18
19/// The literate forms' connectives.
20const CONNECTIVES: &[&str] = &["and", "or", "implies", "equals", "is", "either", "not"];
21
22/// The proof tactics, coloured in a proof.
23const TACTICS: &[&str] = &[
24    "intro", "intros", "assumption", "auto", "decide", "split", "left", "right", "ring", "refl",
25    "lia", "omega", "cc", "simp", "induction", "inversion", "rewrite", "apply", "exact",
26    "destruct", "cases", "reflexivity", "symmetry", "unfold", "trivial", "contradiction",
27    "constructor", "diagonalization",
28];
29
30/// The sorts.
31const SORTS: &[&str] = &["Prop", "Type", "Set"];
32
33/// Commands and headers whose next name is the one they declare.
34const DECLARERS: &[&str] = &["Definition", "Inductive", "Theorem", "Lemma", "Axiom", "Hypothesis", "Variable", "Parameter", "To", "Theory"];
35
36/// Operators, longest first.
37const OPERATORS: &[&str] = &[
38    "<->", "->", "=>", ":=", "<=", ">=", "<>", "/\\", "\\/", "::", "=", "<", ">", "+", "-", "*", "/", "|",
39    ":", "~", "^", "%",
40];
41
42const PUNCTUATION: &[char] = &['(', ')', '[', ']', '{', '}', '.', ',', ';'];
43
44/// `source` as the editor colours it, token by token; the tokens spell `source` back exactly.
45pub(crate) fn tokens(source: &str) -> Vec<Token> {
46    let mut out: Vec<Token> = Vec::new();
47    let mut at = 0;
48    // Tactics are words of a proof: from `Proof` to the next blank line, header or command.
49    let mut in_proof = false;
50    // The name after `Definition`, `## To`, `## Theorem:` … is the one it declares: a type
51    // after `Inductive`, a name to call or cite after the rest.
52    let mut declares: Option<TokenKind> = None;
53    let mut line_start = true;
54    while at < source.len() {
55        let rest = &source[at..];
56        let first = rest.chars().next().expect("a token starts somewhere");
57        let (len, kind) = if first.is_whitespace() {
58            let len = rest.find(|c: char| !c.is_whitespace()).unwrap_or(rest.len());
59            if rest[..len].matches('\n').count() > 1 {
60                in_proof = false;
61            }
62            (len, TokenKind::Identifier)
63        } else if rest.starts_with("--") {
64            (rest.find('\n').unwrap_or(rest.len()), TokenKind::Comment)
65        } else if rest.starts_with("##") {
66            in_proof = false;
67            (rest.find(|c: char| c != '#').unwrap_or(rest.len()), TokenKind::Punctuation)
68        } else if first == '"' {
69            (string_len(rest), TokenKind::String)
70        } else if first.is_ascii_digit() {
71            (rest.find(|c: char| !(c.is_ascii_digit() || c == '_')).unwrap_or(rest.len()), TokenKind::Number)
72        } else if first.is_alphabetic() || first == '_' {
73            let len = rest.find(|c: char| !(c.is_alphanumeric() || c == '_' || c == '\'')).unwrap_or(rest.len());
74            let word = &rest[..len];
75            if line_start && KEYWORDS.contains(&word) && word != "Proof" {
76                in_proof = false;
77            }
78            let kind = if let Some(declared) = declares.filter(|_| !KEYWORDS.contains(&word)) {
79                declares = None;
80                declared
81            } else if in_proof && TACTICS.contains(&word) {
82                TokenKind::Builtin
83            } else if KEYWORDS.contains(&word) {
84                declares = DECLARERS.contains(&word).then_some(if word == "Inductive" { TokenKind::Type } else { TokenKind::Builtin });
85                in_proof |= word == "Proof";
86                TokenKind::Keyword
87            } else if CONNECTIVES.contains(&word) {
88                TokenKind::Operator
89            } else if SORTS.contains(&word) || word.starts_with(char::is_uppercase) {
90                TokenKind::Type
91            } else {
92                TokenKind::Identifier
93            };
94            (len, kind)
95        } else if let Some(op) = OPERATORS.iter().find(|op| rest.starts_with(**op)) {
96            (op.len(), TokenKind::Operator)
97        } else if is_symbol(first) {
98            (first.len_utf8(), TokenKind::Operator)
99        } else if PUNCTUATION.contains(&first) {
100            (first.len_utf8(), TokenKind::Punctuation)
101        } else {
102            (first.len_utf8(), TokenKind::Identifier)
103        };
104        let text = &rest[..len];
105        line_start = if text.trim().is_empty() { line_start || text.contains('\n') } else { false };
106        out.push(Token { text: rest[..len].to_string(), kind });
107        at += len;
108    }
109    out
110}
111
112/// A logical or mathematical symbol: the arrows, the mathematical operators, and ¬ λ.
113fn is_symbol(c: char) -> bool {
114    matches!(c, '\u{2190}'..='\u{21FF}' | '\u{2200}'..='\u{22FF}' | '\u{27F0}'..='\u{27FF}' | '¬' | 'λ' | 'Π' | 'Σ')
115}
116
117/// The length of the string literal `rest` opens: to its closing quote, past escapes.
118fn string_len(rest: &str) -> usize {
119    let mut escaped = false;
120    for (i, c) in rest.char_indices().skip(1) {
121        match c {
122            '"' if !escaped => return i + 1,
123            '\\' if !escaped => escaped = true,
124            _ => escaped = false,
125        }
126    }
127    rest.len()
128}
129
130/// The spellings Logos Math Mono draws as symbols, and the characters that keep one from being
131/// drawn — as `scripts/web/build-math-font.py` builds them (a test holds the two together). Only the
132/// browser's caret uses them.
133#[cfg_attr(not(target_arch = "wasm32"), allow(dead_code))]
134pub(crate) const LIGATURE_WORDS: &[&str] = &["forall", "exists", "fun"];
135#[cfg_attr(not(target_arch = "wasm32"), allow(dead_code))]
136pub(crate) const LIGATURE_OPERATORS: &[&str] = &["->", "=>", "<=", ">="];
137#[cfg_attr(not(target_arch = "wasm32"), allow(dead_code))]
138pub(crate) const WORD_CHARS: &str = "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789_'";
139#[cfg_attr(not(target_arch = "wasm32"), allow(dead_code))]
140pub(crate) const OPERATOR_CHARS: &str = "-<>=|:!~*+/\\";
141
142/// The byte ranges of `text` the Math font draws as one symbol: a spelling with no word
143/// character beside a word, and no operator character beside an operator.
144#[cfg_attr(not(target_arch = "wasm32"), allow(dead_code))]
145pub(crate) fn ligatures(text: &str) -> Vec<std::ops::Range<usize>> {
146    let bytes = text.as_bytes();
147    // Each spelling with the characters that would join it to its neighbours.
148    let spellings = LIGATURE_WORDS
149        .iter()
150        .map(|s| (*s, WORD_CHARS))
151        .chain(LIGATURE_OPERATORS.iter().map(|s| (*s, OPERATOR_CHARS)));
152    let mut out = Vec::new();
153    let mut at = 0;
154    while at < text.len() {
155        let before = at.checked_sub(1).map(|i| bytes[i]);
156        let found = spellings.clone().find(|(spelling, joiners)| {
157            let joins = |b: u8| joiners.as_bytes().contains(&b);
158            text[at..].starts_with(spelling)
159                && !before.is_some_and(joins)
160                && !bytes.get(at + spelling.len()).is_some_and(|b| joins(*b))
161        });
162        match found {
163            Some((spelling, _)) => {
164                out.push(at..at + spelling.len());
165                at += spelling.len();
166            }
167            None => at += text[at..].chars().next().map_or(1, char::len_utf8),
168        }
169    }
170    out
171}
172
173/// Which edge of a ligature a caret inside it moves to.
174#[cfg_attr(not(target_arch = "wasm32"), allow(dead_code))]
175#[derive(Clone, Copy, Debug, PartialEq, Eq)]
176pub(crate) enum Snap {
177    Nearest,
178    Start,
179    End,
180}
181
182/// A caret at byte `at` of `text`, moved out of any ligature it sits inside, toward `snap`: the
183/// symbol is one character to the reader, so the caret never stands within its spelling.
184#[cfg_attr(not(target_arch = "wasm32"), allow(dead_code))]
185pub(crate) fn snap(text: &str, at: usize, snap: Snap) -> usize {
186    match ligatures(text).into_iter().find(|r| r.start < at && at < r.end) {
187        Some(r) => match snap {
188            Snap::Start => r.start,
189            Snap::End => r.end,
190            Snap::Nearest if at - r.start < r.end - at => r.start,
191            Snap::Nearest => r.end,
192        },
193        None => at,
194    }
195}
196
197#[cfg(test)]
198#[path = "../../../../../crates/logicaffeine_tests/unit/logicaffeine_web/ui/components/vernacular/tests.rs"]
199mod tests;
logicaffeine_web/ui/components/vernacular.rs

logicaffeine_web/ui/components/
vernacular.rs
