elenchus-parser 0.9.0

//! The single source of truth for the language's keywords.
//!
//! Every keyword's CAPS spelling lives exactly once, in [`kw`]. The [`KEYWORDS`]
//! table attaches each one's role (may it begin a statement?) and its syntax card
//! (canonical form, one-line gloss, a copy-paste example). Everything else in the
//! workspace that needs to know a keyword — the reserved-word check, recovery
//! resync, the diagnostic cards, the parser's `tag(...)` calls, and the compiler's
//! provenance `kind` strings — derives from this table or references a [`kw`]
//! constant, so a keyword string is never written twice.

/// The CAPS spelling of every keyword — the one place each literal appears.
pub mod kw {
    #![allow(missing_docs)] // each constant is its own keyword; the name says it
    pub const DOMAIN: &str = "DOMAIN";
    pub const IMPORT: &str = "IMPORT";
    pub const AS: &str = "AS";
    pub const FACT: &str = "FACT";
    pub const NOT: &str = "NOT";
    pub const ASSUME: &str = "ASSUME";
    pub const PREMISE: &str = "PREMISE";
    pub const RULE: &str = "RULE";
    pub const CHECK: &str = "CHECK";
    pub const BIDIRECTIONAL: &str = "BIDIRECTIONAL";
    pub const WHEN: &str = "WHEN";
    pub const THEN: &str = "THEN";
    pub const AND: &str = "AND";
    pub const OR: &str = "OR";
    pub const EXCLUSIVE: &str = "EXCLUSIVE";
    pub const FORBIDS: &str = "FORBIDS";
    pub const ONEOF: &str = "ONEOF";
    pub const ATLEAST: &str = "ATLEAST";
    pub const SET: &str = "SET";
    pub const FOR: &str = "FOR";
    pub const EACH: &str = "EACH";
    pub const IN: &str = "IN";
    pub const CLOSE: &str = "CLOSE";
    pub const TRANSITIVE: &str = "TRANSITIVE";
}

/// The correct-syntax reference for one keyword: its canonical written form (with
/// `<slots>` and `[optional]` parts), a one-line plain meaning, and a real, valid
/// example a model can copy. Mirrors `docs/SPEC.md`, "DSL: keywords".
#[derive(Clone, Copy, PartialEq, Eq)]
pub struct Card {
    /// The canonical written form.
    pub form: &'static str,
    /// A one-line plain meaning.
    pub gloss: &'static str,
    /// A real, valid example line.
    pub example: &'static str,
}

/// One keyword: its spelling, whether it may begin a top-level statement, and its
/// syntax card.
pub struct Keyword {
    /// The CAPS spelling (a [`kw`] constant).
    pub text: &'static str,
    /// Whether it may begin a top-level statement — used by recovery resync and
    /// the "expected one of these statements" menu.
    pub top_level: bool,
    /// The keyword's syntax card.
    pub card: Card,
}

/// Shorthand for one [`Card`].
const fn card(form: &'static str, gloss: &'static str, example: &'static str) -> Card {
    Card {
        form,
        gloss,
        example,
    }
}

/// Every keyword, in teaching order. The top-level statements come first (so
/// filtering `top_level` yields the menu order), then `IMPORT`/`AS`, then the
/// body and modifier words.
pub const KEYWORDS: &[Keyword] = &[
    Keyword {
        text: kw::DOMAIN,
        top_level: true,
        card: card(
            "DOMAIN <name>",
            "declare this file's domain (required, once, first) — the namespace bare atoms fall into",
            "DOMAIN physics",
        ),
    },
    Keyword {
        text: kw::FACT,
        top_level: true,
        card: card(
            "FACT [<domain>.]<Subject> <predicate> [<object>]",
            "assert an atom is TRUE",
            "FACT socrates is human",
        ),
    },
    Keyword {
        text: kw::NOT,
        top_level: true,
        card: card(
            "NOT <Subject> <predicate> [<object>]",
            "assert an atom is FALSE",
            "NOT socrates is immortal",
        ),
    },
    Keyword {
        text: kw::ASSUME,
        top_level: true,
        card: card(
            "ASSUME [NOT] <Subject> <predicate> [<object>]",
            "a soft, retractable hypothesis (the solver may ask you to drop it)",
            "ASSUME release is_ready",
        ),
    },
    Keyword {
        text: kw::PREMISE,
        top_level: true,
        card: card(
            "PREMISE <name>:  then a list body or a WHEN ... THEN implication",
            "a checked first principle (a constraint that must hold)",
            "PREMISE wings:\n    WHEN bird has feathers\n    THEN bird can_fly",
        ),
    },
    Keyword {
        text: kw::RULE,
        top_level: true,
        card: card(
            "RULE <name>:  then a WHEN ... THEN implication",
            "an inference rule: when the WHEN holds, it derives the THEN as a fact",
            "RULE mortal:\n    WHEN x is human\n    THEN x is mortal",
        ),
    },
    Keyword {
        text: kw::CHECK,
        top_level: true,
        card: card(
            "CHECK [<subject>] [BIDIRECTIONAL]",
            "run the query; an optional subject narrows the report",
            "CHECK socrates",
        ),
    },
    Keyword {
        text: kw::SET,
        top_level: true,
        card: card(
            "SET <name>  then one element per line (>= 1)",
            "declare a finite set of elements to quantify a PREMISE/RULE over (FOR EACH ... IN)",
            "SET tasks\n    deploy\n    backup",
        ),
    },
    Keyword {
        text: kw::CLOSE,
        top_level: true,
        card: card(
            "CLOSE <relation> TRANSITIVE",
            "make a relation transitive at compile time (a->b, b->c implies a->c); a cycle is an error",
            "CLOSE depends_on TRANSITIVE",
        ),
    },
    Keyword {
        text: kw::IMPORT,
        top_level: true,
        card: card(
            "IMPORT \"<path>\" [AS <alias>]",
            "pull in another .vrf source for reuse; its atoms are named <domain>.<atom>",
            "IMPORT \"physics.vrf\"",
        ),
    },
    Keyword {
        text: kw::AS,
        top_level: false,
        card: card(
            "IMPORT \"<path>\" AS <alias>",
            "give the imported domain a local name to reference it by",
            "IMPORT \"physics.vrf\" AS phys",
        ),
    },
    Keyword {
        text: kw::FOR,
        top_level: false,
        card: card(
            "PREMISE <name> FOR EACH <binder> IN <set>:  then the usual body",
            "quantify a PREMISE/RULE: instantiate its body once per element of <set>, binding <binder>",
            "PREMISE colored FOR EACH n IN nodes:\n    ONEOF\n        n is red\n        n is blue",
        ),
    },
    Keyword {
        text: kw::EACH,
        top_level: false,
        card: card(
            "FOR EACH <binder> IN <set>",
            "part of the FOR EACH ... IN quantifier on a PREMISE/RULE header",
            "FOR EACH t IN tasks",
        ),
    },
    Keyword {
        text: kw::IN,
        top_level: false,
        card: card(
            "FOR EACH <binder> IN <set>",
            "names the declared SET a FOR EACH quantifier ranges over",
            "FOR EACH t IN tasks",
        ),
    },
    Keyword {
        text: kw::WHEN,
        top_level: false,
        card: card(
            "WHEN <literal>   (literal = [NOT] <Subject> <predicate> [<object>])",
            "the condition (if-part) of an implication; continue with AND/OR",
            "WHEN motor over_100",
        ),
    },
    Keyword {
        text: kw::THEN,
        top_level: false,
        card: card(
            "THEN <literal>",
            "the conclusion (then-part) of an implication; continue with AND/OR",
            "THEN motor uses fast_path",
        ),
    },
    Keyword {
        text: kw::AND,
        top_level: false,
        card: card(
            "AND <literal>",
            "extend the current WHEN or THEN group (all must hold); do not mix with OR",
            "AND motor is reviewed",
        ),
    },
    Keyword {
        text: kw::OR,
        top_level: false,
        card: card(
            "OR <literal>",
            "extend the current WHEN or THEN group (at least one holds); do not mix with AND",
            "OR motor is hotfixed",
        ),
    },
    Keyword {
        text: kw::EXCLUSIVE,
        top_level: false,
        card: card(
            "EXCLUSIVE  then one atom per line (>= 2 atoms)",
            "at most one of the listed atoms may be TRUE",
            "EXCLUSIVE\n    light is on\n    light is off",
        ),
    },
    Keyword {
        text: kw::FORBIDS,
        top_level: false,
        card: card(
            "FORBIDS  then one atom per line (>= 2 atoms)",
            "at most one may be TRUE (a synonym of EXCLUSIVE)",
            "FORBIDS\n    door is open\n    door is locked",
        ),
    },
    Keyword {
        text: kw::ONEOF,
        top_level: false,
        card: card(
            "ONEOF  then one atom per line (>= 2 atoms)",
            "exactly one of the listed atoms is TRUE",
            "ONEOF\n    mode is idle\n    mode is run",
        ),
    },
    Keyword {
        text: kw::ATLEAST,
        top_level: false,
        card: card(
            "ATLEAST  then one atom per line (>= 2 atoms)",
            "at least one of the listed atoms is TRUE",
            "ATLEAST\n    plan has tests\n    plan has review",
        ),
    },
    Keyword {
        text: kw::BIDIRECTIONAL,
        top_level: false,
        card: card(
            "CHECK [<subject>] BIDIRECTIONAL",
            "a CHECK modifier: also run the backward pass (finds UNDERDETERMINED)",
            "CHECK BIDIRECTIONAL",
        ),
    },
    Keyword {
        text: kw::TRANSITIVE,
        top_level: false,
        card: card(
            "CLOSE <relation> TRANSITIVE",
            "the closure kind for CLOSE: a->b and b->c implies a->c",
            "CLOSE depends_on TRANSITIVE",
        ),
    },
];

/// Whether `word` is a reserved keyword.
pub fn is_reserved(word: &str) -> bool {
    KEYWORDS.iter().any(|k| k.text == word)
}

/// Whether `word` can begin a top-level statement (used by recovery resync).
pub fn is_top_level(word: &str) -> bool {
    KEYWORDS.iter().any(|k| k.top_level && k.text == word)
}

/// The syntax card for `keyword`, or `None` if it is not a known keyword.
pub fn card_for(keyword: &str) -> Option<&'static Card> {
    KEYWORDS.iter().find(|k| k.text == keyword).map(|k| &k.card)
}

/// The keywords that may begin a top-level statement, in teaching order — shown
/// as the menu when an error is not tied to one specific keyword.
pub fn top_level_forms() -> impl Iterator<Item = &'static Keyword> {
    KEYWORDS.iter().filter(|k| k.top_level)
}

/// The top-level keywords joined as an English menu — `"A, B, …, or Z"`, in
/// teaching order. The single source for the "expected a statement" diagnostic,
/// so that menu can never drift from [`KEYWORDS`] as keywords are added.
pub fn top_level_menu() -> alloc::string::String {
    use alloc::string::String;
    let words: alloc::vec::Vec<&'static str> = top_level_forms().map(|k| k.text).collect();
    let mut out = String::new();
    for (i, w) in words.iter().enumerate() {
        if i > 0 {
            out.push_str(", ");
            if i + 1 == words.len() {
                out.push_str("or ");
            }
        }
        out.push_str(w);
    }
    out
}

/// The first keyword named anywhere in `message` (selects its card in a
/// diagnostic). Splits on non-alphabetic characters and returns the first token
/// that is a keyword.
pub fn keyword_in(message: &str) -> Option<&'static str> {
    message
        .split(|c: char| !c.is_ascii_alphabetic())
        .find_map(|w| KEYWORDS.iter().map(|k| k.text).find(|t| *t == w))
}