elenchus_parser/
ast.rs

1//! The abstract syntax tree: the typed shape a `.vrf` source parses into.
2//!
3//! Everything here is zero-copy over the source `&str` (atoms/names borrow their
4//! slices) and every node that can be pointed at in an error carries its
5//! [`Span`] via [`Located`].
6
7use alloc::vec::Vec;
8
9use nom_locate::LocatedSpan;
10
11/// Source code fragment with line and column tracking.
12pub type Span<'a> = LocatedSpan<&'a str>;
13
14/// Container for data associated with its source location.
15#[derive(Debug, Clone, PartialEq)]
16pub struct Located<'a, T> {
17    /// The actual parsed data.
18    pub data: T,
19    /// The location in the source text (start of the construct).
20    pub span: Span<'a>,
21}
22
23/// An atom is the triple `(subject, predicate, object?)` — the unit of identity —
24/// optionally qualified by a domain (`physics.engine has fuel`).
25/// `Creature_A has flying` and `Creature_A has swimming` are DIFFERENT atoms.
26#[derive(Debug, Clone, PartialEq, Eq)]
27pub struct Atom<'a> {
28    /// The domain this atom is qualified into, written as a `domain.` prefix on
29    /// the subject (e.g. `physics` in `physics.engine has fuel`). `None` means the
30    /// atom belongs to the current file's own declared domain (no prefix).
31    pub domain: Option<&'a str>,
32    /// The entity the claim is about, e.g. `Creature_A` or `Motor`.
33    pub subject: &'a str,
34    /// The relation or property asserted, e.g. `has` or `over_100`.
35    pub predicate: &'a str,
36    /// Optional value the predicate relates the subject to, e.g. `flying`.
37    /// `None` for two-word atoms such as `Motor over_100`. The object is part of
38    /// identity: `has flying` and `has swimming` are different atoms.
39    pub object: Option<&'a str>,
40}
41
42/// A literal is an atom, optionally negated (`NOT ...`).
43#[derive(Debug, Clone, PartialEq, Eq)]
44pub struct Literal<'a> {
45    /// `true` when written with a leading `NOT` (asserts the atom is FALSE).
46    pub negated: bool,
47    /// The underlying atom being asserted true or false.
48    pub atom: Atom<'a>,
49}
50
51/// List constraint operators (body of a list-style `PREMISE`).
52///
53/// These are surface sugar; the compiler desugars each to `Impossible` clauses
54/// (see `elenchus-compiler`). The meanings below are *what the author asserts*.
55#[derive(Debug, Clone, Copy, PartialEq, Eq)]
56pub enum ListOp {
57    /// `EXCLUSIVE` — at most one of the listed atoms may be TRUE (mutual
58    /// exclusion). For n > 2 this is pairwise, not "not all at once".
59    Exclusive,
60    /// `FORBIDS` — at most one may be TRUE; a synonym of [`ListOp::Exclusive`]
61    /// (same pairwise expansion), kept as a separate word for readability.
62    Forbids,
63    /// `ONEOF` — exactly one is TRUE: at-most-one (pairwise) plus at-least-one.
64    OneOf,
65    /// `ATLEAST` — at least one of the listed atoms is TRUE.
66    AtLeast,
67}
68
69/// How the literals in a `WHEN`/`THEN` group combine. A single-literal group is
70/// always [`Conn::And`] (the connective is irrelevant with one literal).
71#[derive(Debug, Clone, Copy, PartialEq, Eq)]
72pub enum Conn {
73    /// Continuation lines used `AND` — all literals must hold.
74    And,
75    /// Continuation lines used `OR` — at least one literal must hold.
76    Or,
77}
78
79/// The body of an `PREMISE` or `RULE`.
80#[derive(Debug, Clone, PartialEq)]
81pub enum Body<'a> {
82    /// `EXCLUSIVE`/`FORBIDS`/`ONEOF`/`ATLEAST` over >= 2 atoms.
83    List {
84        /// Which list constraint this is.
85        op: ListOp,
86        /// The atoms it ranges over (the parser guarantees at least two).
87        atoms: Vec<Located<'a, Atom<'a>>>,
88    },
89    /// `WHEN ... [AND|OR ...] THEN ... [AND|OR ...]` — antecedent + consequent.
90    /// Within one group the continuation keyword is uniform (no mixing `AND`/`OR`).
91    Impl {
92        /// `WHEN`/`AND`/`OR` conditions.
93        antecedent: Vec<Located<'a, Literal<'a>>>,
94        /// How the antecedent literals combine.
95        ante_conn: Conn,
96        /// `THEN`/`AND`/`OR` results that follow when the antecedent holds.
97        consequent: Vec<Located<'a, Literal<'a>>>,
98        /// How the consequent literals combine.
99        cons_conn: Conn,
100    },
101}
102
103/// A top-level statement.
104#[derive(Debug, Clone, PartialEq)]
105pub enum Statement<'a> {
106    /// `DOMAIN <name>` — declare the domain this file's atoms belong to. Required
107    /// once per file, as the first statement; it is the identity namespace into
108    /// which bare atoms fall.
109    Domain(Located<'a, &'a str>),
110    /// `IMPORT "path" [AS <alias>]` — reuse another source (resolved by the
111    /// compiler). The optional `alias` is the local name the imported domain is
112    /// referenced by; without it, the imported file's own declared domain name is
113    /// used.
114    Import {
115        /// The quoted source path.
116        path: Located<'a, &'a str>,
117        /// The local alias for the imported domain, if `AS <alias>` was given.
118        alias: Option<Located<'a, &'a str>>,
119    },
120    /// `FACT <atom>` — a TRUE assertion.
121    Fact(Located<'a, Atom<'a>>),
122    /// `NOT <atom>` — a FALSE assertion.
123    Negation(Located<'a, Atom<'a>>),
124    /// `ASSUME [NOT] <atom>` — a *soft* (retractable) assertion. Same shape as a
125    /// `FACT`/`NOT`, but it is a hypothesis, not a commitment: when the
126    /// assumptions cannot all hold the solver names which to drop, and it never
127    /// blames a `FACT`/`PREMISE`. The `Literal` carries the optional `NOT`.
128    Assume(Located<'a, Literal<'a>>),
129    /// `PREMISE <name>: ...` — a checked first principle.
130    Premise {
131        /// The premise's label (a per-source name, not a global identifier).
132        name: Located<'a, &'a str>,
133        /// The constraint itself: a list body or a `WHEN … THEN` implication.
134        body: Body<'a>,
135    },
136    /// `RULE <name>: ...` — a fact-producing inference rule.
137    Rule {
138        /// The rule's label.
139        name: Located<'a, &'a str>,
140        /// Always an implication body (the grammar forbids a list body here).
141        body: Body<'a>,
142    },
143    /// `CHECK [subject] [BIDIRECTIONAL]` — a query.
144    Check {
145        /// Restrict the report to this subject; `None` checks everything.
146        subject: Option<Located<'a, &'a str>>,
147        /// `true` enables the backward (all-SAT) pass for UNDERDETERMINED.
148        bidirectional: bool,
149    },
150}
151
152/// A parsed program: a flat sequence of statements.
153#[derive(Debug, Clone, PartialEq)]
154pub struct Program<'a> {
155    /// Top-level statements in source order. The list is flat: PREMISE/RULE bodies
156    /// live inside their [`Statement`], not as separate entries.
157    pub statements: Vec<Statement<'a>>,
158}
elenchus_parser/ast.rs

elenchus_parser/
ast.rs
