elenchus_compiler/ir.rs
1//! IR types: atom identity, literals, facts, clauses, rules, the compiled output.
2use alloc::string::String;
3use alloc::vec::Vec;
4
5// --- IR types --------------------------------------------------------------
6
7/// Dense atom identifier (also the SAT variable number).
8pub type AtomId = u32;
9
10/// The identity of an atom: the `domain` plus the triple
11/// `(subject, predicate, object?)`, owned so it survives across merged sources.
12/// The domain is the leading sort key, so atoms group by domain; ordering is
13/// otherwise lexicographic → canonical. Two atoms with the same triple in
14/// *different* domains are distinct (no cross-domain unification).
15#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord)]
16pub struct AtomKey {
17 /// The domain this atom belongs to (the resolved namespace, never a raw
18 /// alias). `physics.engine` and `plan.engine` are different atoms.
19 pub domain: String,
20 /// The entity the claim is about (owned copy of the parser's `subject`).
21 pub subject: String,
22 /// The relation or property asserted. `None` for a **bare proposition** — a
23 /// single-word atom introduced by a `VAR` port (e.g. `db_ready`). `None`
24 /// sorts before any `Some`, so existing (always-`Some`) atoms keep their order.
25 pub predicate: Option<String>,
26 /// Optional object; part of identity, so `has flying` ≠ `has swimming`. Always
27 /// `None` when `predicate` is `None`.
28 pub object: Option<String>,
29}
30
31/// The human label for a resolved atom (`domain.subject predicate object`), as
32/// shown in port diagnostics and reports.
33impl core::fmt::Display for AtomKey {
34 fn fmt(&self, f: &mut core::fmt::Formatter<'_>) -> core::fmt::Result {
35 write!(f, "{}.{}", self.domain, self.subject)?;
36 if let Some(p) = &self.predicate {
37 write!(f, " {p}")?;
38 }
39 if let Some(o) = &self.object {
40 write!(f, " {o}")?;
41 }
42 Ok(())
43 }
44}
45
46/// A literal as it appears *inside* an `Impossible` clause: an atom, optionally
47/// negated. `negated = true` means the literal is `NOT atom`.
48#[derive(Debug, Clone, Copy, PartialEq, Eq)]
49pub struct Lit {
50 /// Interned id of the atom (also its SAT variable number).
51 pub atom: AtomId,
52 /// `true` means this literal is `NOT atom` inside the clause.
53 pub negated: bool,
54}
55
56/// A confident truth value. UNKNOWN is the *absence* of a fact, never stored.
57#[derive(Debug, Clone, Copy, PartialEq, Eq)]
58pub enum Value {
59 /// The atom is asserted TRUE (from `FACT`).
60 True,
61 /// The atom is asserted FALSE (from `NOT`).
62 False,
63}
64
65/// Where a piece of IR came from — for readable conflict/warning pools.
66#[derive(Debug, Clone, PartialEq, Eq)]
67pub struct Origin {
68 /// The source label this came from (file name or `"<root>"`/`"<text>"`).
69 pub source: String,
70 /// 1-based line number of the originating statement.
71 pub line: u32,
72 /// The premise/rule name, if it came from a named construct.
73 pub premise: Option<String>,
74 /// Surface kind for the report. A surface keyword (a [`kw`] constant such as
75 /// `kw::FACT` / `kw::PREMISE`) for source constructs, or [`KIND_UNSAT`] for
76 /// the synthetic origin the solver attaches to a global unsatisfiability.
77 pub kind: &'static str,
78}
79
80/// The [`Origin::kind`] the solver stamps on a conflict that is not pinned to one
81/// source construct but to the program being jointly unsatisfiable. Not a
82/// keyword — so it lives here, next to the other kinds, as the one spelling both
83/// the solver (which sets it) and any reader (which matches it) share.
84pub const KIND_UNSAT: &str = "UNSAT";
85
86/// A confident fact (from `FACT` / `NOT`). Conflicting facts on the same atom
87/// are preserved (both kept) — the solver reports that as a CONFLICT.
88#[derive(Debug, Clone, PartialEq, Eq)]
89pub struct Fact {
90 /// The atom this fact pins down.
91 pub atom: AtomId,
92 /// The asserted truth value.
93 pub value: Value,
94 /// Where it came from (for the report).
95 pub origin: Origin,
96 /// `true` for an `ASSUME` (a *soft*, retractable hypothesis). A soft fact
97 /// behaves like a normal fact in the forward pass, but when the assumptions
98 /// cannot all hold the solver may drop it (and only it) to explain the
99 /// contradiction — a `FACT`/`NOT` is never retractable.
100 pub soft: bool,
101}
102
103/// An `Impossible` clause: the listed literals cannot all hold simultaneously.
104#[derive(Debug, Clone, PartialEq, Eq)]
105pub struct Clause {
106 /// The literals that cannot all hold at once (an `Impossible([...])`).
107 pub lits: Vec<Lit>,
108 /// Where it came from (for the report).
109 pub origin: Origin,
110}
111
112/// A forward-chaining rule (from `RULE`): if all antecedent literals hold, derive
113/// the consequent literals.
114#[derive(Debug, Clone, PartialEq, Eq)]
115pub struct Rule {
116 /// Literals that must all hold for the rule to fire.
117 pub antecedent: Vec<Lit>,
118 /// Literals derived (asserted) when the antecedent holds.
119 pub consequent: Vec<Lit>,
120 /// Where it came from (for the report).
121 pub origin: Origin,
122}
123
124/// A `CHECK` query.
125#[derive(Debug, Clone, PartialEq, Eq)]
126pub struct Check {
127 /// Restrict the report to this subject; `None` means check everything.
128 pub subject: Option<String>,
129 /// `true` runs the backward (all-SAT) pass to detect UNDERDETERMINED.
130 pub bidirectional: bool,
131}
132
133/// The compiled IR: the solver's input.
134#[derive(Debug, Clone, PartialEq, Eq)]
135pub struct Compiled {
136 /// Indexed by [`AtomId`]; canonically sorted.
137 pub atoms: Vec<AtomKey>,
138 /// Confident assertions from `FACT`/`NOT`.
139 pub facts: Vec<Fact>,
140 /// `Impossible` clauses (desugared premises + the built-in non-contradiction).
141 pub clauses: Vec<Clause>,
142 /// Forward-chaining rules from `RULE`.
143 pub rules: Vec<Rule>,
144 /// `CHECK` queries.
145 pub checks: Vec<Check>,
146 /// Imports seen but not yet resolved (only populated by [`compile_source`];
147 /// [`compile`] resolves them, leaving this empty).
148 pub pending_imports: Vec<String>,
149 /// Advisory: imports that a file makes but never references (no `domain.atom`
150 /// from that file uses the imported domain). Structural, per-file, and inert —
151 /// it never affects the solve. Only populated by [`compile`] (an unresolved
152 /// import in [`compile_source`] cannot be classified). See [`UnusedImport`].
153 pub unused_imports: Vec<UnusedImport>,
154 /// Atoms consumed as data by a relation `FOR EACH` (the edge facts, e.g. each
155 /// `a linked b`). They are read by the quantifier, so the solver must not
156 /// report them as ORPHAN facts even though no clause references them.
157 pub consumed: Vec<AtomId>,
158 /// One record per declared `VAR` port: how it resolved (supplied / default /
159 /// unset), its value and origin. Drives the report's PLACEHOLDERS section;
160 /// purely advisory. Filled by `compile_source_with` / `compile_with` after
161 /// [`Compiler::resolve_ports`]; empty when no port was declared.
162 pub placeholders: Vec<PlaceholderInfo>,
163}
164
165/// An advisory record: a file `IMPORT`s a domain it never references. Such an
166/// import is inert — no `domain.atom` in that file mentions it, so removing it
167/// would not change the result. It is almost always a leftover or a forgotten
168/// `domain.` prefix. **Purely informational** — it never changes the verdict.
169#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord)]
170pub struct UnusedImport {
171 /// The source that declared the unused `IMPORT`.
172 pub file: String,
173 /// The imported domain that is never referenced from `file`.
174 pub domain: String,
175 /// The local alias, if the import used `AS <alias>`.
176 pub alias: Option<String>,
177 /// 1-based line of the `IMPORT` statement in `file`.
178 pub line: u32,
179}
180
181/// One external value bound to a port `key`, supplied from outside the program
182/// (CLI / API / a data file). The `origin` is a short human tag used both in the
183/// placeholders report and in a [`CompileError::PortConflict`] message.
184#[derive(Debug, Clone, PartialEq, Eq)]
185pub struct PortBinding {
186 /// The boolean truth supplied for the port.
187 pub value: bool,
188 /// Where it came from: `"CLI"`, `"api"`, `"data:<file>"`, or `"PROVIDE <file>"`.
189 pub origin: String,
190}
191
192/// How a declared `VAR` port got (or did not get) its value — the per-port status
193/// shown in the report's PLACEHOLDERS section. Advisory only; never affects the
194/// verdict.
195#[derive(Debug, Clone, Copy, PartialEq, Eq)]
196pub enum PlaceholderStatus {
197 /// An external value (CLI/API/data) was supplied.
198 Supplied,
199 /// No external value; the port's `DEFAULT` was used.
200 DefaultUsed,
201 /// No external value and no `DEFAULT` — the port stays UNKNOWN.
202 Unset,
203}
204
205/// A reporting record for one declared `VAR` port: its key, how it resolved, the
206/// value it took (if any), and where that value came from.
207#[derive(Debug, Clone, PartialEq, Eq)]
208pub struct PlaceholderInfo {
209 /// The port's name (the external key).
210 pub key: String,
211 /// How it resolved (supplied / default / unset).
212 pub status: PlaceholderStatus,
213 /// The resolved boolean, or `None` when unset.
214 pub value: Option<bool>,
215 /// The origin of a supplied value (`None` for default/unset).
216 pub origin: Option<String>,
217}