elenchus_parser/
keywords.rs

1//! The single source of truth for the language's keywords.
2//!
3//! Every keyword's CAPS spelling lives exactly once, in [`kw`]. The [`KEYWORDS`]
4//! table attaches each one's role (may it begin a statement?) and its syntax card
5//! (canonical form, one-line gloss, a copy-paste example). Everything else in the
6//! workspace that needs to know a keyword — the reserved-word check, recovery
7//! resync, the diagnostic cards, the parser's `tag(...)` calls, and the compiler's
8//! provenance `kind` strings — derives from this table or references a [`kw`]
9//! constant, so a keyword string is never written twice.
10
11/// The CAPS spelling of every keyword — the one place each literal appears.
12pub mod kw {
13    #![allow(missing_docs)] // each constant is its own keyword; the name says it
14    pub const DOMAIN: &str = "DOMAIN";
15    pub const IMPORT: &str = "IMPORT";
16    pub const AS: &str = "AS";
17    pub const FACT: &str = "FACT";
18    pub const NOT: &str = "NOT";
19    pub const ASSUME: &str = "ASSUME";
20    pub const PREMISE: &str = "PREMISE";
21    pub const RULE: &str = "RULE";
22    pub const CHECK: &str = "CHECK";
23    pub const BIDIRECTIONAL: &str = "BIDIRECTIONAL";
24    pub const WHEN: &str = "WHEN";
25    pub const THEN: &str = "THEN";
26    pub const AND: &str = "AND";
27    pub const OR: &str = "OR";
28    pub const EXCLUSIVE: &str = "EXCLUSIVE";
29    pub const FORBIDS: &str = "FORBIDS";
30    pub const ONEOF: &str = "ONEOF";
31    pub const ATLEAST: &str = "ATLEAST";
32    pub const SET: &str = "SET";
33    pub const FOR: &str = "FOR";
34    pub const EACH: &str = "EACH";
35    pub const IN: &str = "IN";
36    pub const CLOSE: &str = "CLOSE";
37    pub const TRANSITIVE: &str = "TRANSITIVE";
38}
39
40/// The correct-syntax reference for one keyword: its canonical written form (with
41/// `<slots>` and `[optional]` parts), a one-line plain meaning, and a real, valid
42/// example a model can copy. Mirrors `docs/SPEC.md`, "DSL: keywords".
43#[derive(Clone, Copy, PartialEq, Eq)]
44pub struct Card {
45    /// The canonical written form.
46    pub form: &'static str,
47    /// A one-line plain meaning.
48    pub gloss: &'static str,
49    /// A real, valid example line.
50    pub example: &'static str,
51}
52
53/// One keyword: its spelling, whether it may begin a top-level statement, and its
54/// syntax card.
55pub struct Keyword {
56    /// The CAPS spelling (a [`kw`] constant).
57    pub text: &'static str,
58    /// Whether it may begin a top-level statement — used by recovery resync and
59    /// the "expected one of these statements" menu.
60    pub top_level: bool,
61    /// The keyword's syntax card.
62    pub card: Card,
63}
64
65/// Shorthand for one [`Card`].
66const fn card(form: &'static str, gloss: &'static str, example: &'static str) -> Card {
67    Card {
68        form,
69        gloss,
70        example,
71    }
72}
73
74/// Every keyword, in teaching order. The top-level statements come first (so
75/// filtering `top_level` yields the menu order), then `IMPORT`/`AS`, then the
76/// body and modifier words.
77pub const KEYWORDS: &[Keyword] = &[
78    Keyword {
79        text: kw::DOMAIN,
80        top_level: true,
81        card: card(
82            "DOMAIN <name>",
83            "declare this file's domain (required, once, first) — the namespace bare atoms fall into",
84            "DOMAIN physics",
85        ),
86    },
87    Keyword {
88        text: kw::FACT,
89        top_level: true,
90        card: card(
91            "FACT [<domain>.]<Subject> <predicate> [<object>]",
92            "assert an atom is TRUE",
93            "FACT socrates is human",
94        ),
95    },
96    Keyword {
97        text: kw::NOT,
98        top_level: true,
99        card: card(
100            "NOT <Subject> <predicate> [<object>]",
101            "assert an atom is FALSE",
102            "NOT socrates is immortal",
103        ),
104    },
105    Keyword {
106        text: kw::ASSUME,
107        top_level: true,
108        card: card(
109            "ASSUME [NOT] <Subject> <predicate> [<object>]",
110            "a soft, retractable hypothesis (the solver may ask you to drop it)",
111            "ASSUME release is_ready",
112        ),
113    },
114    Keyword {
115        text: kw::PREMISE,
116        top_level: true,
117        card: card(
118            "PREMISE <name>:  then a list body or a WHEN ... THEN implication",
119            "a checked first principle (a constraint that must hold)",
120            "PREMISE wings:\n    WHEN bird has feathers\n    THEN bird can_fly",
121        ),
122    },
123    Keyword {
124        text: kw::RULE,
125        top_level: true,
126        card: card(
127            "RULE <name>:  then a WHEN ... THEN implication",
128            "an inference rule: when the WHEN holds, it derives the THEN as a fact",
129            "RULE mortal:\n    WHEN x is human\n    THEN x is mortal",
130        ),
131    },
132    Keyword {
133        text: kw::CHECK,
134        top_level: true,
135        card: card(
136            "CHECK [<subject>] [BIDIRECTIONAL]",
137            "run the query; an optional subject narrows the report",
138            "CHECK socrates",
139        ),
140    },
141    Keyword {
142        text: kw::SET,
143        top_level: true,
144        card: card(
145            "SET <name>  then one element per line (>= 1)",
146            "declare a finite set of elements to quantify a PREMISE/RULE over (FOR EACH ... IN)",
147            "SET tasks\n    deploy\n    backup",
148        ),
149    },
150    Keyword {
151        text: kw::CLOSE,
152        top_level: true,
153        card: card(
154            "CLOSE <relation> TRANSITIVE",
155            "make a relation transitive at compile time (a->b, b->c implies a->c); a cycle is an error",
156            "CLOSE depends_on TRANSITIVE",
157        ),
158    },
159    Keyword {
160        text: kw::IMPORT,
161        top_level: true,
162        card: card(
163            "IMPORT \"<path>\" [AS <alias>]",
164            "pull in another .vrf source for reuse; its atoms are named <domain>.<atom>",
165            "IMPORT \"physics.vrf\"",
166        ),
167    },
168    Keyword {
169        text: kw::AS,
170        top_level: false,
171        card: card(
172            "IMPORT \"<path>\" AS <alias>",
173            "give the imported domain a local name to reference it by",
174            "IMPORT \"physics.vrf\" AS phys",
175        ),
176    },
177    Keyword {
178        text: kw::FOR,
179        top_level: false,
180        card: card(
181            "PREMISE <name> FOR EACH <binder> IN <set>:  then the usual body",
182            "quantify a PREMISE/RULE: instantiate its body once per element of <set>, binding <binder>",
183            "PREMISE colored FOR EACH n IN nodes:\n    ONEOF\n        n is red\n        n is blue",
184        ),
185    },
186    Keyword {
187        text: kw::EACH,
188        top_level: false,
189        card: card(
190            "FOR EACH <binder> IN <set>",
191            "part of the FOR EACH ... IN quantifier on a PREMISE/RULE header",
192            "FOR EACH t IN tasks",
193        ),
194    },
195    Keyword {
196        text: kw::IN,
197        top_level: false,
198        card: card(
199            "FOR EACH <binder> IN <set>",
200            "names the declared SET a FOR EACH quantifier ranges over",
201            "FOR EACH t IN tasks",
202        ),
203    },
204    Keyword {
205        text: kw::WHEN,
206        top_level: false,
207        card: card(
208            "WHEN <literal>   (literal = [NOT] <Subject> <predicate> [<object>])",
209            "the condition (if-part) of an implication; continue with AND/OR",
210            "WHEN motor over_100",
211        ),
212    },
213    Keyword {
214        text: kw::THEN,
215        top_level: false,
216        card: card(
217            "THEN <literal>",
218            "the conclusion (then-part) of an implication; continue with AND/OR",
219            "THEN motor uses fast_path",
220        ),
221    },
222    Keyword {
223        text: kw::AND,
224        top_level: false,
225        card: card(
226            "AND <literal>",
227            "extend the current WHEN or THEN group (all must hold); do not mix with OR",
228            "AND motor is reviewed",
229        ),
230    },
231    Keyword {
232        text: kw::OR,
233        top_level: false,
234        card: card(
235            "OR <literal>",
236            "extend the current WHEN or THEN group (at least one holds); do not mix with AND",
237            "OR motor is hotfixed",
238        ),
239    },
240    Keyword {
241        text: kw::EXCLUSIVE,
242        top_level: false,
243        card: card(
244            "EXCLUSIVE  then one atom per line (>= 2 atoms)",
245            "at most one of the listed atoms may be TRUE",
246            "EXCLUSIVE\n    light is on\n    light is off",
247        ),
248    },
249    Keyword {
250        text: kw::FORBIDS,
251        top_level: false,
252        card: card(
253            "FORBIDS  then one atom per line (>= 2 atoms)",
254            "at most one may be TRUE (a synonym of EXCLUSIVE)",
255            "FORBIDS\n    door is open\n    door is locked",
256        ),
257    },
258    Keyword {
259        text: kw::ONEOF,
260        top_level: false,
261        card: card(
262            "ONEOF  then one atom per line (>= 2 atoms)",
263            "exactly one of the listed atoms is TRUE",
264            "ONEOF\n    mode is idle\n    mode is run",
265        ),
266    },
267    Keyword {
268        text: kw::ATLEAST,
269        top_level: false,
270        card: card(
271            "ATLEAST  then one atom per line (>= 2 atoms)",
272            "at least one of the listed atoms is TRUE",
273            "ATLEAST\n    plan has tests\n    plan has review",
274        ),
275    },
276    Keyword {
277        text: kw::BIDIRECTIONAL,
278        top_level: false,
279        card: card(
280            "CHECK [<subject>] BIDIRECTIONAL",
281            "a CHECK modifier: also run the backward pass (finds UNDERDETERMINED)",
282            "CHECK BIDIRECTIONAL",
283        ),
284    },
285    Keyword {
286        text: kw::TRANSITIVE,
287        top_level: false,
288        card: card(
289            "CLOSE <relation> TRANSITIVE",
290            "the closure kind for CLOSE: a->b and b->c implies a->c",
291            "CLOSE depends_on TRANSITIVE",
292        ),
293    },
294];
295
296/// Whether `word` is a reserved keyword.
297pub fn is_reserved(word: &str) -> bool {
298    KEYWORDS.iter().any(|k| k.text == word)
299}
300
301/// Whether `word` can begin a top-level statement (used by recovery resync).
302pub fn is_top_level(word: &str) -> bool {
303    KEYWORDS.iter().any(|k| k.top_level && k.text == word)
304}
305
306/// The syntax card for `keyword`, or `None` if it is not a known keyword.
307pub fn card_for(keyword: &str) -> Option<&'static Card> {
308    KEYWORDS.iter().find(|k| k.text == keyword).map(|k| &k.card)
309}
310
311/// The keywords that may begin a top-level statement, in teaching order — shown
312/// as the menu when an error is not tied to one specific keyword.
313pub fn top_level_forms() -> impl Iterator<Item = &'static Keyword> {
314    KEYWORDS.iter().filter(|k| k.top_level)
315}
316
317/// The top-level keywords joined as an English menu — `"A, B, …, or Z"`, in
318/// teaching order. The single source for the "expected a statement" diagnostic,
319/// so that menu can never drift from [`KEYWORDS`] as keywords are added.
320pub fn top_level_menu() -> alloc::string::String {
321    use alloc::string::String;
322    let words: alloc::vec::Vec<&'static str> = top_level_forms().map(|k| k.text).collect();
323    let mut out = String::new();
324    for (i, w) in words.iter().enumerate() {
325        if i > 0 {
326            out.push_str(", ");
327            if i + 1 == words.len() {
328                out.push_str("or ");
329            }
330        }
331        out.push_str(w);
332    }
333    out
334}
335
336/// The first keyword named anywhere in `message` (selects its card in a
337/// diagnostic). Splits on non-alphabetic characters and returns the first token
338/// that is a keyword.
339pub fn keyword_in(message: &str) -> Option<&'static str> {
340    message
341        .split(|c: char| !c.is_ascii_alphabetic())
342        .find_map(|w| KEYWORDS.iter().map(|k| k.text).find(|t| *t == w))
343}
elenchus_parser/keywords.rs

elenchus_parser/
keywords.rs
