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

elenchus_parser/
keywords.rs
