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

elenchus_parser/
keywords.rs
