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}
33
34/// The correct-syntax reference for one keyword: its canonical written form (with
35/// `<slots>` and `[optional]` parts), a one-line plain meaning, and a real, valid
36/// example a model can copy. Mirrors `docs/SPEC.md`, "DSL: keywords".
37#[derive(Clone, Copy, PartialEq, Eq)]
38pub struct Card {
39    /// The canonical written form.
40    pub form: &'static str,
41    /// A one-line plain meaning.
42    pub gloss: &'static str,
43    /// A real, valid example line.
44    pub example: &'static str,
45}
46
47/// One keyword: its spelling, whether it may begin a top-level statement, and its
48/// syntax card.
49pub struct Keyword {
50    /// The CAPS spelling (a [`kw`] constant).
51    pub text: &'static str,
52    /// Whether it may begin a top-level statement — used by recovery resync and
53    /// the "expected one of these statements" menu.
54    pub top_level: bool,
55    /// The keyword's syntax card.
56    pub card: Card,
57}
58
59/// Shorthand for one [`Card`].
60const fn card(form: &'static str, gloss: &'static str, example: &'static str) -> Card {
61    Card {
62        form,
63        gloss,
64        example,
65    }
66}
67
68/// Every keyword, in teaching order. The top-level statements come first (so
69/// filtering `top_level` yields the menu order), then `IMPORT`/`AS`, then the
70/// body and modifier words.
71pub const KEYWORDS: &[Keyword] = &[
72    Keyword {
73        text: kw::DOMAIN,
74        top_level: true,
75        card: card(
76            "DOMAIN <name>",
77            "declare this file's domain (required, once, first) — the namespace bare atoms fall into",
78            "DOMAIN physics",
79        ),
80    },
81    Keyword {
82        text: kw::FACT,
83        top_level: true,
84        card: card(
85            "FACT [<domain>.]<Subject> <predicate> [<object>]",
86            "assert an atom is TRUE",
87            "FACT socrates is human",
88        ),
89    },
90    Keyword {
91        text: kw::NOT,
92        top_level: true,
93        card: card(
94            "NOT <Subject> <predicate> [<object>]",
95            "assert an atom is FALSE",
96            "NOT socrates is immortal",
97        ),
98    },
99    Keyword {
100        text: kw::ASSUME,
101        top_level: true,
102        card: card(
103            "ASSUME [NOT] <Subject> <predicate> [<object>]",
104            "a soft, retractable hypothesis (the solver may ask you to drop it)",
105            "ASSUME release is_ready",
106        ),
107    },
108    Keyword {
109        text: kw::PREMISE,
110        top_level: true,
111        card: card(
112            "PREMISE <name>:  then a list body or a WHEN ... THEN implication",
113            "a checked first principle (a constraint that must hold)",
114            "PREMISE wings:\n    WHEN bird has feathers\n    THEN bird can_fly",
115        ),
116    },
117    Keyword {
118        text: kw::RULE,
119        top_level: true,
120        card: card(
121            "RULE <name>:  then a WHEN ... THEN implication",
122            "an inference rule: when the WHEN holds, it derives the THEN as a fact",
123            "RULE mortal:\n    WHEN x is human\n    THEN x is mortal",
124        ),
125    },
126    Keyword {
127        text: kw::CHECK,
128        top_level: true,
129        card: card(
130            "CHECK [<subject>] [BIDIRECTIONAL]",
131            "run the query; an optional subject narrows the report",
132            "CHECK socrates",
133        ),
134    },
135    Keyword {
136        text: kw::IMPORT,
137        top_level: true,
138        card: card(
139            "IMPORT \"<path>\" [AS <alias>]",
140            "pull in another .vrf source for reuse; its atoms are named <domain>.<atom>",
141            "IMPORT \"physics.vrf\"",
142        ),
143    },
144    Keyword {
145        text: kw::AS,
146        top_level: false,
147        card: card(
148            "IMPORT \"<path>\" AS <alias>",
149            "give the imported domain a local name to reference it by",
150            "IMPORT \"physics.vrf\" AS phys",
151        ),
152    },
153    Keyword {
154        text: kw::WHEN,
155        top_level: false,
156        card: card(
157            "WHEN <literal>   (literal = [NOT] <Subject> <predicate> [<object>])",
158            "the condition (if-part) of an implication; continue with AND/OR",
159            "WHEN motor over_100",
160        ),
161    },
162    Keyword {
163        text: kw::THEN,
164        top_level: false,
165        card: card(
166            "THEN <literal>",
167            "the conclusion (then-part) of an implication; continue with AND/OR",
168            "THEN motor uses fast_path",
169        ),
170    },
171    Keyword {
172        text: kw::AND,
173        top_level: false,
174        card: card(
175            "AND <literal>",
176            "extend the current WHEN or THEN group (all must hold); do not mix with OR",
177            "AND motor is reviewed",
178        ),
179    },
180    Keyword {
181        text: kw::OR,
182        top_level: false,
183        card: card(
184            "OR <literal>",
185            "extend the current WHEN or THEN group (at least one holds); do not mix with AND",
186            "OR motor is hotfixed",
187        ),
188    },
189    Keyword {
190        text: kw::EXCLUSIVE,
191        top_level: false,
192        card: card(
193            "EXCLUSIVE  then one atom per line (>= 2 atoms)",
194            "at most one of the listed atoms may be TRUE",
195            "EXCLUSIVE\n    light is on\n    light is off",
196        ),
197    },
198    Keyword {
199        text: kw::FORBIDS,
200        top_level: false,
201        card: card(
202            "FORBIDS  then one atom per line (>= 2 atoms)",
203            "at most one may be TRUE (a synonym of EXCLUSIVE)",
204            "FORBIDS\n    door is open\n    door is locked",
205        ),
206    },
207    Keyword {
208        text: kw::ONEOF,
209        top_level: false,
210        card: card(
211            "ONEOF  then one atom per line (>= 2 atoms)",
212            "exactly one of the listed atoms is TRUE",
213            "ONEOF\n    mode is idle\n    mode is run",
214        ),
215    },
216    Keyword {
217        text: kw::ATLEAST,
218        top_level: false,
219        card: card(
220            "ATLEAST  then one atom per line (>= 2 atoms)",
221            "at least one of the listed atoms is TRUE",
222            "ATLEAST\n    plan has tests\n    plan has review",
223        ),
224    },
225    Keyword {
226        text: kw::BIDIRECTIONAL,
227        top_level: false,
228        card: card(
229            "CHECK [<subject>] BIDIRECTIONAL",
230            "a CHECK modifier: also run the backward pass (finds UNDERDETERMINED)",
231            "CHECK BIDIRECTIONAL",
232        ),
233    },
234];
235
236/// Whether `word` is a reserved keyword.
237pub fn is_reserved(word: &str) -> bool {
238    KEYWORDS.iter().any(|k| k.text == word)
239}
240
241/// Whether `word` can begin a top-level statement (used by recovery resync).
242pub fn is_top_level(word: &str) -> bool {
243    KEYWORDS.iter().any(|k| k.top_level && k.text == word)
244}
245
246/// The syntax card for `keyword`, or `None` if it is not a known keyword.
247pub fn card_for(keyword: &str) -> Option<&'static Card> {
248    KEYWORDS.iter().find(|k| k.text == keyword).map(|k| &k.card)
249}
250
251/// The keywords that may begin a top-level statement, in teaching order — shown
252/// as the menu when an error is not tied to one specific keyword.
253pub fn top_level_forms() -> impl Iterator<Item = &'static Keyword> {
254    KEYWORDS.iter().filter(|k| k.top_level)
255}
256
257/// The first keyword named anywhere in `message` (selects its card in a
258/// diagnostic). Splits on non-alphabetic characters and returns the first token
259/// that is a keyword.
260pub fn keyword_in(message: &str) -> Option<&'static str> {
261    message
262        .split(|c: char| !c.is_ascii_alphabetic())
263        .find_map(|w| KEYWORDS.iter().map(|k| k.text).find(|t| *t == w))
264}
elenchus_parser/keywords.rs

elenchus_parser/
keywords.rs
