nibli_semantics/
ir.rs

1//! First-Order Logic intermediate representation.
2//!
3//! Defines [`IrTerm`] (atomic terms) and [`IrForm`] (well-formed formulas)
4//! that the semantic compiler produces from the `AstBuffer` the nibli-kr
5//! emitter builds. The reasoning engine consumes these via the flattener in
6//! `lib.rs`.
7//!
8//! INTERN-THEN-RESOLVE BOUNDARY: every name in this IR is a [`lasso::Spur`]
9//! key into the compiler's per-compilation `Rodeo` — Spurs NEVER survive into
10//! `LogicBuffer`. `flatten_form` (lib.rs) resolves each Spur to an owned
11//! `String` at the flattening boundary, so nibli-reason and everything
12//! downstream see only strings. Variable identity is the `$`-prefixed
13//! interned string — the sigil survives interning, and the free-variable and
14//! scope-marker passes key on it.
15
16use lasso::Spur;
17
18/// The atomic arguments of a predicate.
19#[derive(Debug, PartialEq, Clone)]
20pub enum IrTerm {
21    /// A bound logic variable (a `$`-prefixed name, e.g. `$x`)
22    Variable(Spur),
23    /// A named constant entity (a Name like `Adam`, or a pronoun constant)
24    Constant(Spur),
25    /// An entity described by a predicate (`some dog` / `the dog`)
26    Description(Spur),
27    /// An explicitly unspecified argument (`_` or an omitted place)
28    Unspecified,
29    /// Numeric literal.
30    Number(f64),
31}
32
33/// The Well-Formed Formulas (WFFs) of our First-Order Logic engine.
34#[derive(Debug, PartialEq, Clone)]
35pub enum IrForm {
36    /// An n-ary predicate: P(t1, t2, ..., tn)
37    Predicate { relation: Spur, args: Vec<IrTerm> },
38    /// Universal quantification: ∀x. P(x)
39    ForAll(Spur, Box<IrForm>),
40    /// Existential quantification: ∃x. P(x)
41    Exists(Spur, Box<IrForm>),
42    /// Logical Conjunction: A ∧ B
43    And(Box<IrForm>, Box<IrForm>),
44    /// Logical Disjunction: A ∨ B
45    Or(Box<IrForm>, Box<IrForm>),
46    /// Logical Negation: ¬A
47    Not(Box<IrForm>),
48    /// Past tense wrapper (`past P`): P was true.
49    Past(Box<IrForm>),
50    /// Present tense wrapper (`now P`): P is true now.
51    Present(Box<IrForm>),
52    /// Future tense wrapper (`future P`): P will be true.
53    Future(Box<IrForm>),
54    /// Deontic obligation (`must P`): P ought to be true.
55    Obligatory(Box<IrForm>),
56    /// Deontic permission (`may P`): P is permitted.
57    Permitted(Box<IrForm>),
58    /// Exactly `count` distinct x satisfy `body`.
59    /// Count(var, count, body)
60    Count {
61        var: Spur,
62        count: u32,
63        body: Box<IrForm>,
64    },
65    /// Biconditional: A ↔ B  (expanded at flattening to And(Or(Not(A), B), Or(Not(B), A)))
66    Biconditional(Box<IrForm>, Box<IrForm>),
67    /// Exclusive or: A ⊕ B  (expanded at flattening to And(Or(A, B), Not(And(A, B))))
68    Xor(Box<IrForm>, Box<IrForm>),
69}
nibli_semantics/ir.rs

nibli_semantics/
ir.rs
