rossi-cli 0.1.0

Command-line interface for the Rossi Event-B toolchain
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89

//! Emacs Quail input method (`editors/emacs/eventb-input.el`).
//!
//! Whole-file: a complete, self-contained Quail package (agda-input style) so an
//! Emacs user can `(set-input-method "eventb")` and type Event-B Unicode with a
//! backslash leader (`\to` → `→`, `\and` → `∧`, `\NAT` → `ℕ`).
//!
//! ## Leader-only by design
//!
//! Unlike the as-you-type substitution the Neovim/VS Code input methods offer,
//! the Emacs method is **leader-only**: every rule is prefixed with `\`. This is
//! the idiomatic Emacs choice (it mirrors `TeX`/`agda-input`), keeps the method
//! from hijacking ordinary symbol typing, and means the [`OperatorRow::eager`]
//! policy is irrelevant here — we never emit bare, non-backslash rules.
//!
//! ## Rules emitted per [`eventb_lsp::server::operator_rows`] row
//!
//! - One `("\\<alias>" "<unicode>")` rule for every curated alias.
//! - For non-symbolic (alphabetic) rows only, an extra `("\\<ascii>" "<unicode>")`
//!   rule so `\NAT`, `\POW` work — skipped when an alias already spells the
//!   ASCII form identically (`or`, `not`, `circ`) to avoid a redundant rule.
//!   Symbolic ASCII spellings (`=>`, `|->`, …) are reachable through their
//!   aliases and would make awkward backslash rules, so they are omitted.
//!
//! Rows come from the same source as the LSP operator table, so the input method
//! can never drift from the canonical ASCII↔Unicode mapping (guarded by
//! [`super::tests::emacs_quail_matches_lsp_rows`]).

use eventb_lsp::server::operator_rows;

const NOTICE: &str =
    "Generated by `rossi gen-grammars` from the canonical operator table. Do not edit by hand.";

/// Render the complete `eventb-input.el` Quail package.
pub fn render() -> String {
    let mut out = String::new();
    out.push_str(
        ";;; eventb-input.el --- Event-B Unicode input method -*- lexical-binding: t; -*-\n",
    );
    out.push_str(&format!(";; {NOTICE}\n"));
    out.push_str(";;; Commentary:\n");
    out.push_str(
        ";; A Quail input method (agda-input style) for typing Event-B Unicode\n\
         ;; operators with a backslash leader, e.g. `\\to' -> RIGHTWARDS ARROW.\n",
    );
    out.push_str(";;; Code:\n\n");
    out.push_str("(require 'quail)\n\n");

    out.push_str("(quail-define-package\n");
    out.push_str(" \"eventb\"                       ; name\n");
    out.push_str(" \"UTF-8\"                         ; language\n");
    out.push_str(" \"EvB\"                           ; title (mode-line indicator)\n");
    out.push_str(" t                              ; guidance\n");
    out.push_str(
        " \"Event-B Unicode input method (backslash leader, e.g. \\\\to -> RIGHTWARDS ARROW).\"\n",
    );
    out.push_str(" nil                            ; translation-keys\n");
    // forget-last-selection deterministic kbd-translate show-layout
    // create-decode-map maximum-shortest overlay-plist
    // update-translation-function conversion-keys simple
    out.push_str(" nil t nil nil nil nil nil nil nil t)\n\n");

    out.push_str("(quail-define-rules\n");
    for row in operator_rows() {
        let unicode = super::elisp_string(&row.unicode);
        // Curated aliases first (every row that has them).
        for alias in &row.aliases {
            out.push_str(&format!(" ({} {})\n", backslash_key(alias), unicode));
        }
        // Alphabetic ASCII spellings also get a direct `\<ascii>` rule, unless
        // an alias already spells it the same way (`or`, `not`, `circ`), which
        // would emit a redundant identical rule.
        if !row.symbolic && !row.aliases.contains(&row.ascii) {
            out.push_str(&format!(" ({} {})\n", backslash_key(&row.ascii), unicode));
        }
    }
    out.push_str(" )\n\n");

    out.push_str("(provide 'eventb-input)\n");
    out.push_str(";;; eventb-input.el ends here\n");
    out
}

/// An Elisp string literal for the `\<key>` leader sequence: a literal backslash
/// followed by the key, both inside a quoted, escaped Elisp string.
fn backslash_key(key: &str) -> String {
    let mut s = String::from("\\");
    s.push_str(key);
    super::elisp_string(&s)
}