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`. `None` for a
35 /// **bare proposition** — a single-word atom such as `db_ready`, introduced by
36 /// a `VAR` port and used directly in bodies (`WHEN db_ready THEN …`). The
37 /// compiler requires any bare-proposition atom to be a declared `VAR`.
38 pub predicate: Option<&'a str>,
39 /// Optional value the predicate relates the subject to, e.g. `flying`.
40 /// `None` for two-word atoms such as `Motor over_100`. The object is part of
41 /// identity: `has flying` and `has swimming` are different atoms. Always `None`
42 /// when `predicate` is `None` (a bare proposition has neither).
43 pub object: Option<&'a str>,
44}
45
46/// A literal is an atom, optionally negated (`NOT ...`).
47#[derive(Debug, Clone, PartialEq, Eq)]
48pub struct Literal<'a> {
49 /// `true` when written with a leading `NOT` (asserts the atom is FALSE).
50 pub negated: bool,
51 /// The underlying atom being asserted true or false.
52 pub atom: Atom<'a>,
53}
54
55/// List constraint operators (body of a list-style `PREMISE`).
56///
57/// These are surface sugar; the compiler desugars each to `Impossible` clauses
58/// (see `elenchus-compiler`). The meanings below are *what the author asserts*.
59#[derive(Debug, Clone, Copy, PartialEq, Eq)]
60pub enum ListOp {
61 /// `EXCLUSIVE` — at most one of the listed atoms may be TRUE (mutual
62 /// exclusion). For n > 2 this is pairwise, not "not all at once".
63 Exclusive,
64 /// `FORBIDS` — at most one may be TRUE; a synonym of [`ListOp::Exclusive`]
65 /// (same pairwise expansion), kept as a separate word for readability.
66 Forbids,
67 /// `ONEOF` — exactly one is TRUE: at-most-one (pairwise) plus at-least-one.
68 OneOf,
69 /// `ATLEAST` — at least one of the listed atoms is TRUE.
70 AtLeast,
71}
72
73/// How the literals in a `WHEN`/`THEN` group combine. A single-literal group is
74/// always [`Conn::And`] (the connective is irrelevant with one literal).
75#[derive(Debug, Clone, Copy, PartialEq, Eq)]
76pub enum Conn {
77 /// Continuation lines used `AND` — all literals must hold.
78 And,
79 /// Continuation lines used `OR` — at least one literal must hold.
80 Or,
81}
82
83/// A `FOR EACH` quantifier on a `PREMISE`/`RULE` header. It instantiates the
84/// premise's whole body **once per element**, substituting the binder. The
85/// quantifier lives in the *header* (not the body), so there is exactly one per
86/// statement and the body grammar is untouched — a second `FOR EACH` is
87/// structurally unrepresentable, which is what bounds the desugar to a linear
88/// number of clauses (no domain products).
89#[derive(Debug, Clone, PartialEq)]
90pub enum Quant<'a> {
91 /// `FOR EACH <binder> IN <set>` — range over the elements of a declared
92 /// [`Statement::Set`]. The binder is the name the body's atoms refer to.
93 InSet {
94 /// The name bound inside the body (substituted per element).
95 binder: Located<'a, &'a str>,
96 /// The declared set this ranges over.
97 set: Located<'a, &'a str>,
98 },
99 /// `FOR EACH <left> <predicate> <right>` — range over the declared `FACT`
100 /// pairs of that relation (e.g. every `FACT a linked b`), binding `left` to a
101 /// pair's subject and `right` to its object. This is the channel for
102 /// multi-element constraints (graphs, dependencies): the pair is *pinned by
103 /// data*, so the desugar is linear in the number of facts, never a product.
104 Relation {
105 /// Bound to each matching fact's subject.
106 left: Located<'a, &'a str>,
107 /// The relation predicate whose facts are ranged over.
108 predicate: Located<'a, &'a str>,
109 /// Bound to each matching fact's object.
110 right: Located<'a, &'a str>,
111 },
112}
113
114/// Which closure a `CLOSE` statement applies to a relation.
115#[derive(Debug, Clone, Copy, PartialEq, Eq)]
116pub enum CloseKind {
117 /// `TRANSITIVE` — add `a→c` whenever `a→b` and `b→c` hold (requires a DAG).
118 Transitive,
119}
120
121/// The body of an `PREMISE` or `RULE`.
122#[derive(Debug, Clone, PartialEq)]
123pub enum Body<'a> {
124 /// `EXCLUSIVE`/`FORBIDS`/`ONEOF`/`ATLEAST` over >= 2 atoms.
125 List {
126 /// Which list constraint this is.
127 op: ListOp,
128 /// The atoms it ranges over (the parser guarantees at least two).
129 atoms: Vec<Located<'a, Atom<'a>>>,
130 },
131 /// `WHEN ... [AND|OR ...] THEN ... [AND|OR ...]` — antecedent + consequent.
132 /// Within one group the continuation keyword is uniform (no mixing `AND`/`OR`).
133 Impl {
134 /// `WHEN`/`AND`/`OR` conditions.
135 antecedent: Vec<Located<'a, Literal<'a>>>,
136 /// How the antecedent literals combine.
137 ante_conn: Conn,
138 /// `THEN`/`AND`/`OR` results that follow when the antecedent holds.
139 consequent: Vec<Located<'a, Literal<'a>>>,
140 /// How the consequent literals combine.
141 cons_conn: Conn,
142 },
143}
144
145/// A top-level statement.
146#[derive(Debug, Clone, PartialEq)]
147pub enum Statement<'a> {
148 /// `DOMAIN <name>` — declare the domain this file's atoms belong to. Required
149 /// once per file, as the first statement; it is the identity namespace into
150 /// which bare atoms fall.
151 Domain(Located<'a, &'a str>),
152 /// `IMPORT "path" [AS <alias>]` — reuse another source (resolved by the
153 /// compiler). The optional `alias` is the local name the imported domain is
154 /// referenced by; without it, the imported file's own declared domain name is
155 /// used.
156 Import {
157 /// The quoted source path.
158 path: Located<'a, &'a str>,
159 /// The local alias for the imported domain, if `AS <alias>` was given.
160 alias: Option<Located<'a, &'a str>>,
161 },
162 /// `FACT <atom>` — a TRUE assertion.
163 Fact(Located<'a, Atom<'a>>),
164 /// `NOT <atom>` — a FALSE assertion.
165 Negation(Located<'a, Atom<'a>>),
166 /// `ASSUME [NOT] <atom>` — a *soft* (retractable) assertion. Same shape as a
167 /// `FACT`/`NOT`, but it is a hypothesis, not a commitment: when the
168 /// assumptions cannot all hold the solver names which to drop, and it never
169 /// blames a `FACT`/`PREMISE`. The `Literal` carries the optional `NOT`.
170 Assume(Located<'a, Literal<'a>>),
171 /// `SET <name>` then one element identifier per line — declare a finite set
172 /// to quantify a `PREMISE`/`RULE` over via `FOR EACH <binder> IN <name>`.
173 Set {
174 /// The set's name (referenced by `FOR EACH … IN <name>`).
175 name: Located<'a, &'a str>,
176 /// Its elements, one per line (at least one).
177 elements: Vec<Located<'a, &'a str>>,
178 },
179 /// `CLOSE <relation> TRANSITIVE` — close a relation's `FACT` pairs under the
180 /// given kind at compile time (a graph operation, no solver cost). A cycle is
181 /// a compile error.
182 Close {
183 /// The relation predicate to close (e.g. `depends_on`).
184 relation: Located<'a, &'a str>,
185 /// Which closure to apply.
186 kind: CloseKind,
187 },
188 /// `VAR <name> [DEFAULT true|false]` — declare an external boolean **port**: a
189 /// single-word proposition whose truth is supplied from outside (CLI/API/data).
190 /// `<name>` doubles as the proposition usable in bodies (`WHEN <name> THEN …`)
191 /// and as the key external values bind to. With no supplied value it falls back
192 /// to `default`, or stays UNKNOWN when there is none.
193 Var {
194 /// The port's name — both the bound proposition and the external key.
195 name: Located<'a, &'a str>,
196 /// The `DEFAULT true|false` fallback, if written.
197 default: Option<bool>,
198 },
199 /// `PROVIDE [<domain>.]<port|atom>: true|false` — bind an external value. The
200 /// data-carrying counterpart of `VAR`: it supplies a value (like a CLI/API
201 /// binding) rather than declaring a port. The target is parsed as a full
202 /// [`Atom`], so a lone word binds a `VAR` port (`PROVIDE db_ready: true`), a
203 /// multi-word form asserts an atom (`PROVIDE engine has_fuel: true`), and a
204 /// `domain.` prefix disambiguates across imports (`PROVIDE self.has_vision:
205 /// true`). Used in a data-only file (loaded via `--data`) or alongside the
206 /// program. Conflicting bindings for one target are a hard error.
207 Provide {
208 /// The port or atom this binds (a lone-subject atom is a `VAR` port).
209 atom: Located<'a, Atom<'a>>,
210 /// The boolean value supplied for it.
211 value: bool,
212 },
213 /// `PREMISE <name> [FOR EACH …]: ...` — a checked first principle, optionally
214 /// quantified over a declared set.
215 Premise {
216 /// The premise's label (a per-source name, not a global identifier).
217 name: Located<'a, &'a str>,
218 /// An optional `FOR EACH … IN …` header quantifier (at most one).
219 quant: Option<Quant<'a>>,
220 /// The constraint itself: a list body or a `WHEN … THEN` implication.
221 body: Body<'a>,
222 },
223 /// `RULE <name> [FOR EACH …]: ...` — a fact-producing inference rule.
224 Rule {
225 /// The rule's label.
226 name: Located<'a, &'a str>,
227 /// An optional `FOR EACH … IN …` header quantifier (at most one).
228 quant: Option<Quant<'a>>,
229 /// Always an implication body (the grammar forbids a list body here).
230 body: Body<'a>,
231 },
232 /// `CHECK [subject] [BIDIRECTIONAL]` — a query.
233 Check {
234 /// Restrict the report to this subject; `None` checks everything.
235 subject: Option<Located<'a, &'a str>>,
236 /// `true` enables the backward (all-SAT) pass for UNDERDETERMINED.
237 bidirectional: bool,
238 },
239}
240
241/// A parsed program: a flat sequence of statements.
242#[derive(Debug, Clone, PartialEq)]
243pub struct Program<'a> {
244 /// Top-level statements in source order. The list is flat: PREMISE/RULE bodies
245 /// live inside their [`Statement`], not as separate entries.
246 pub statements: Vec<Statement<'a>>,
247}