logicaffeine_compile/optimize/egraph/
enode.rs

1//! The Architect's term language — flat, multi-arity, `Copy`.
2//!
3//! Children are `NodeId`s (e-class references after canonicalization).
4//! `Var` carries `(symbol index, version)` — versions partition reads of a
5//! mutable name so equality never leaks across a write. `Opaque` is the
6//! escape hatch: any expression the e-graph does not model (calls, indexing,
7//! collection literals, text) becomes an opaque leaf whose ORIGINAL `&Expr`
8//! pointer is held by the converter, so extraction reproduces it verbatim —
9//! effects and error behavior preserved by construction.
10
11use super::NodeId;
12
13#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
14pub enum CompilerENode {
15    Int(i64),
16    Bool(bool),
17    /// f64 bit pattern. Floats are NEVER arithmetic-rewritten (no identity,
18    /// no reassociation — bit-exactness is the contract); the variant exists
19    /// so float-valued subtrees still participate in congruence.
20    Float(u64),
21    /// (symbol index, version)
22    Var(u32, u32),
23    /// Index into the converter's originals table.
24    Opaque(u32),
25
26    Add(NodeId, NodeId),
27    Sub(NodeId, NodeId),
28    Mul(NodeId, NodeId),
29    Div(NodeId, NodeId),
30    Mod(NodeId, NodeId),
31    Shl(NodeId, NodeId),
32    Shr(NodeId, NodeId),
33    BitXor(NodeId, NodeId),
34    /// Bitwise `&`/`|` on Int (the surface `&`/`|` symbols; also what the
35    /// mod-pow2 mask rule synthesizes).
36    BitAnd(NodeId, NodeId),
37    BitOr(NodeId, NodeId),
38    /// Logical `and`/`or`: truthiness in, Bool out, short-circuit. Rules
39    /// consult class facts (`is_bool`) before rewriting.
40    And(NodeId, NodeId),
41    Or(NodeId, NodeId),
42    Not(NodeId),
43
44    Eq(NodeId, NodeId),
45    Ne(NodeId, NodeId),
46    Lt(NodeId, NodeId),
47    Le(NodeId, NodeId),
48    Gt(NodeId, NodeId),
49    Ge(NodeId, NodeId),
50
51    Concat(NodeId, NodeId),
52    Len(NodeId),
53    Index(NodeId, NodeId),
54    /// `copy of xs` — a fresh, unaliased deep copy. Total.
55    Copy(NodeId),
56    /// `xs sliced from a to b` (1-based, inclusive). NON-total: raises on
57    /// out-of-bounds, so rewrites may never delete one without proofs.
58    Slice(NodeId, NodeId, NodeId),
59    /// `xs contains x` — membership. Total; modeled for congruence/CSE
60    /// only (no rewrite touches its semantics).
61    Contains(NodeId, NodeId),
62}
63
64impl CompilerENode {
65    /// Children in evaluation order.
66    pub fn children(&self) -> Vec<NodeId> {
67        use CompilerENode::*;
68        match *self {
69            Int(_) | Bool(_) | Float(_) | Var(..) | Opaque(_) => vec![],
70            Not(a) | Len(a) | Copy(a) => vec![a],
71            Add(a, b) | Sub(a, b) | Mul(a, b) | Div(a, b) | Mod(a, b) | Shl(a, b)
72            | Shr(a, b) | BitXor(a, b) | BitAnd(a, b) | BitOr(a, b) | And(a, b) | Or(a, b)
73            | Eq(a, b) | Ne(a, b) | Lt(a, b) | Le(a, b) | Gt(a, b) | Ge(a, b)
74            | Concat(a, b) | Index(a, b) | Contains(a, b) => {
75                vec![a, b]
76            }
77            Slice(a, b, c) => vec![a, b, c],
78        }
79    }
80
81    /// Rebuild the node with each child mapped (canonicalization).
82    pub fn map_children(self, mut f: impl FnMut(NodeId) -> NodeId) -> Self {
83        use CompilerENode::*;
84        match self {
85            Int(_) | Bool(_) | Float(_) | Var(..) | Opaque(_) => self,
86            Not(a) => Not(f(a)),
87            Len(a) => Len(f(a)),
88            Add(a, b) => Add(f(a), f(b)),
89            Sub(a, b) => Sub(f(a), f(b)),
90            Mul(a, b) => Mul(f(a), f(b)),
91            Div(a, b) => Div(f(a), f(b)),
92            Mod(a, b) => Mod(f(a), f(b)),
93            Shl(a, b) => Shl(f(a), f(b)),
94            Shr(a, b) => Shr(f(a), f(b)),
95            BitXor(a, b) => BitXor(f(a), f(b)),
96            BitAnd(a, b) => BitAnd(f(a), f(b)),
97            BitOr(a, b) => BitOr(f(a), f(b)),
98            And(a, b) => And(f(a), f(b)),
99            Or(a, b) => Or(f(a), f(b)),
100            Eq(a, b) => Eq(f(a), f(b)),
101            Ne(a, b) => Ne(f(a), f(b)),
102            Lt(a, b) => Lt(f(a), f(b)),
103            Le(a, b) => Le(f(a), f(b)),
104            Gt(a, b) => Gt(f(a), f(b)),
105            Ge(a, b) => Ge(f(a), f(b)),
106            Concat(a, b) => Concat(f(a), f(b)),
107            Index(a, b) => Index(f(a), f(b)),
108            Copy(a) => Copy(f(a)),
109            Slice(a, b, c) => Slice(f(a), f(b), f(c)),
110            Contains(a, b) => Contains(f(a), f(b)),
111        }
112    }
113
114    /// Ops whose evaluation can never raise a runtime error, given total
115    /// children. Div/Mod (zero divisor), Index/Slice (bounds), and Opaque
116    /// (arbitrary effects) are the non-total ones — a rewrite may only
117    /// DELETE a subterm whose whole tree is total, or it would erase the
118    /// program's error/effect behavior. Len/Copy/Contains raise KIND
119    /// errors over non-collections, so they are non-total HERE and earn
120    /// totality through class facts in
121    /// [`super::CompilerEGraph::provably_total`].
122    pub fn op_is_total(&self) -> bool {
123        !matches!(
124            self,
125            CompilerENode::Div(..)
126                | CompilerENode::Mod(..)
127                | CompilerENode::Index(..)
128                | CompilerENode::Slice(..)
129                | CompilerENode::Len(..)
130                | CompilerENode::Copy(..)
131                | CompilerENode::Contains(..)
132                | CompilerENode::Opaque(_)
133        )
134    }
135}
logicaffeine_compile/optimize/egraph/enode.rs

logicaffeine_compile/optimize/egraph/
enode.rs
