xlog_ir/
eir.rs

1//! Epistemic Intermediate Representation.
2
3/// Epistemic semantics mode selected for an EIR program.
4#[derive(Debug, Clone, Copy, PartialEq, Eq)]
5pub enum EirEpistemicMode {
6    /// G91 compatibility semantics.
7    G91,
8    /// Founded Autoepistemic Equilibrium Logic semantics.
9    Faeel,
10}
11
12/// Epistemic operator attached to an atom.
13#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
14pub enum EirEpistemicOp {
15    /// The atom is known/believed true in the selected epistemic mode.
16    Know,
17    /// The atom is possible/consistent in the selected epistemic mode.
18    Possible,
19}
20
21/// Term representation preserved at the epistemic boundary.
22#[derive(Debug, Clone, PartialEq, Eq)]
23pub enum EirTerm {
24    /// Named logic variable.
25    Variable(String),
26    /// Anonymous wildcard.
27    Anonymous,
28    /// Integer literal.
29    Integer(i64),
30    /// Floating-point literal represented by its IEEE-754 bits.
31    FloatBits(u64),
32    /// Quoted string literal.
33    String(String),
34    /// Interned symbol identifier.
35    Symbol(u32),
36    /// Finite list literal.
37    List(Vec<EirTerm>),
38    /// Finite cons pattern.
39    Cons {
40        /// Head term.
41        head: Box<EirTerm>,
42        /// Tail term.
43        tail: Box<EirTerm>,
44    },
45    /// Finite compound term.
46    Compound {
47        /// Functor name.
48        functor: String,
49        /// Compound arguments.
50        args: Vec<EirTerm>,
51    },
52    /// Static predicate reference.
53    PredRef(String),
54    /// Aggregate term preserved from a rule head.
55    Aggregate {
56        /// Aggregate operator name.
57        op: String,
58        /// Variable being aggregated.
59        variable: String,
60    },
61}
62
63/// Atom summary carried across the EIR boundary.
64#[derive(Debug, Clone, PartialEq, Eq)]
65pub struct EirAtom {
66    /// Predicate name.
67    pub predicate: String,
68    /// Predicate arity.
69    pub arity: usize,
70    /// Source atom terms preserved for tuple-key matching.
71    pub terms: Vec<EirTerm>,
72}
73
74/// Explicit epistemic body literal.
75#[derive(Debug, Clone, PartialEq, Eq)]
76pub struct EirEpistemicLiteral {
77    /// Epistemic operator.
78    pub op: EirEpistemicOp,
79    /// Whether the epistemic literal is explicitly negated.
80    pub negated: bool,
81    /// Atom under the epistemic operator.
82    pub atom: EirAtom,
83}
84
85/// Body literal at the epistemic boundary.
86#[derive(Debug, Clone, PartialEq, Eq)]
87pub enum EirBodyLiteral {
88    /// Non-epistemic relational atom.
89    Relational {
90        /// Whether the relational atom is negated.
91        negated: bool,
92        /// Atom summary.
93        atom: EirAtom,
94    },
95    /// Explicit epistemic atom.
96    Epistemic(EirEpistemicLiteral),
97    /// Non-relational constraint or comparison.
98    Constraint,
99    /// Variable binding expression.
100    Binding,
101}
102
103/// Rule represented at the EIR boundary.
104#[derive(Debug, Clone, PartialEq, Eq)]
105pub struct EirRule {
106    /// Rule head.
107    pub head: EirAtom,
108    /// Rule body.
109    pub body: Vec<EirBodyLiteral>,
110}
111
112/// Integrity constraint represented at the EIR boundary.
113///
114/// A constraint has no head: the conjunction of its body literals must never
115/// be satisfiable. Epistemic body literals are preserved first-class so that
116/// `know`/`possible` integrity constraints constrain accepted world views,
117/// rather than being silently rewritten into ordinary relational constraints.
118#[derive(Debug, Clone, PartialEq, Eq)]
119pub struct EirConstraint {
120    /// Constraint body whose conjunction must never hold in an accepted world view.
121    pub body: Vec<EirBodyLiteral>,
122}
123
124/// Program represented at the EIR boundary.
125#[derive(Debug, Clone, PartialEq, Eq)]
126pub struct EirProgram {
127    /// Selected epistemic semantics mode.
128    pub mode: EirEpistemicMode,
129    /// Rules in source order.
130    pub rules: Vec<EirRule>,
131    /// Integrity constraints in source order.
132    pub constraints: Vec<EirConstraint>,
133}
xlog_ir/eir.rs

xlog_ir/
eir.rs
