logicaffeine_web/
composer.rs

1//! Composing a formula by hand: the symbol buttons beside a typed answer, and where a click puts
2//! its symbol.
3//!
4//! The pad holds every symbol a typed answer on /learn needs and nothing the grader cannot read
5//! (`learn_symbol_pad.rs` holds both directions). A logical symbol means what the Symbol Dictionary
6//! says it means, read from one table in the language crate.
7
8use logicaffeine_language::symbol_dict::notation;
9use std::sync::LazyLock;
10
11/// One button of the symbol pad.
12#[derive(Debug, Clone, PartialEq)]
13pub struct SymbolButton {
14    /// What a click types.
15    pub symbol: &'static str,
16    /// The short name under the symbol.
17    pub name: &'static str,
18    /// What the symbol means in a formula.
19    pub meaning: String,
20}
21
22impl SymbolButton {
23    /// The button's accessible name.
24    pub fn label(&self) -> String {
25        format!("Insert {}, {}", self.symbol, self.name)
26    }
27}
28
29/// The pad, in the order it shows its buttons: each symbol with its short name, and the meaning of a
30/// symbol the dictionary does not cover (the grouping marks).
31const PAD: &[(&str, &str, Option<&str>)] = &[
32    ("∀", "for every", None),
33    ("∃", "there is", None),
34    ("¬", "not", None),
35    ("∧", "and", None),
36    ("∨", "or", None),
37    ("→", "if then", None),
38    ("↔", "if and only if", None),
39    ("□", "necessarily", None),
40    ("◇", "possibly", None),
41    ("=", "is the same as", None),
42    ("(", "open", Some("starts a group, or a list of arguments")),
43    (")", "close", Some("ends a group, or a list of arguments")),
44    (",", "comma", Some("separates the arguments of a predicate")),
45];
46
47static BUTTONS: LazyLock<Vec<SymbolButton>> = LazyLock::new(|| {
48    let dictionary = notation();
49    PAD.iter()
50        .map(|&(symbol, name, own)| {
51            let meaning = match own {
52                Some(meaning) => meaning.to_string(),
53                None => dictionary
54                    .iter()
55                    .find(|entry| entry.symbol == symbol)
56                    .map(|entry| entry.description.clone())
57                    .unwrap_or_else(|| panic!("the symbol dictionary has no meaning for {symbol}")),
58            };
59            SymbolButton { symbol, name, meaning }
60        })
61        .collect()
62});
63
64/// Every button of the pad, in the order it shows them.
65pub fn symbol_buttons() -> &'static [SymbolButton] {
66    &BUTTONS
67}
68
69/// The byte offset in `text` at `units` UTF-16 code units from its start, rounded forward to a
70/// character boundary, and at most the end of the text.
71fn byte_at(text: &str, units: usize) -> usize {
72    let mut counted = 0;
73    for (at, c) in text.char_indices() {
74        if counted >= units {
75            return at;
76        }
77        counted += c.len_utf16();
78    }
79    text.len()
80}
81
82/// `text` with `insert` put in place of the selection from `start` to `end`, and where the caret
83/// lands after it. Positions count UTF-16 code units, as the browser counts them; a backwards
84/// selection is the same selection, and a position past the end is the end.
85pub fn insert_at(text: &str, start: usize, end: usize, insert: &str) -> (String, usize) {
86    let (from, to) = (byte_at(text, start.min(end)), byte_at(text, start.max(end)));
87    let mut out = String::with_capacity(text.len() + insert.len());
88    out.push_str(&text[..from]);
89    out.push_str(insert);
90    let caret = out.encode_utf16().count();
91    out.push_str(&text[to..]);
92    (out, caret)
93}
94
95#[cfg(test)]
96#[path = "../../../crates/logicaffeine_tests/unit/logicaffeine_web/composer/tests.rs"]
97mod tests;
logicaffeine_web/composer.rs

logicaffeine_web/
composer.rs
