Fix/collapse bare tuple

MettaHyperonFull/Core/Bindings.lean

@@ -10,8 +10,9 @@ Purpose: The binding sets that matching and unification produce. A binding set i
   consistency-checking merge lives in Matching.lean.
 Imports: MettaHyperonFull.Core.Atom, MettaHyperonFull.Core.Pretty
 Trusted boundary: none
-Main exports: BindingRel, Bindings, Bindings.empty, Bindings.lookupVal, Bindings.eqClasses,
-  Bindings.removeVal, Bindings.hasLoop, Bindings.addValRaw, Bindings.addEqRaw
+Main exports: BindingRel, Bindings, Bindings.empty, Bindings.lookupVal, Bindings.eqClassOrdered,
+  Bindings.classValues, Bindings.resolve, Bindings.resolveAtom, Bindings.removeVal,
+  Bindings.hasLoop, Bindings.addValRaw, Bindings.addEqRaw
 Open obligations: none
 -/
 import MettaHyperonFull.Core.Atom
@@ -40,6 +41,128 @@ def lookupVal (b : Bindings) (x : VarName) : Option Atom :=
   | BindingRel.val y a :: rest => if x == y then some a else lookupVal rest x
   | _ :: rest => lookupVal rest x
 
+/-- One saturation pass for the symmetric equality closure. -/
+def eqStep (b : Bindings) (acc : List VarName) : List VarName :=
+  b.foldl (fun acc r => match r with
+    | BindingRel.eq x y =>
+        let acc := if acc.contains x && !acc.contains y then acc ++ [y] else acc
+        if acc.contains y && !acc.contains x then acc ++ [x] else acc
+    | _ => acc) acc
+
+/-- Fuelled saturation of the symmetric-transitive equality closure. -/
+def eqClassAux (b : Bindings) : Nat → List VarName → List VarName
+  | 0, acc => acc
+  | fuel + 1, acc => eqClassAux b fuel (eqStep b acc)
+
+/-- All variables explicitly equality-connected to `x`, including `x`. -/
+def eqClass (b : Bindings) (x : VarName) : List VarName :=
+  eqClassAux b (2 * b.length + 1) [x]
+
+/-- Variables mentioned by equality relations, in representative order. Raw
+    relations are newest-first, while matcher equalities store the rule endpoint
+    before the query endpoint, so oldest edges and their query endpoints come first. -/
+def eqVarsInOrder (b : Bindings) : List VarName :=
+  b.reverse.foldl (fun acc r => match r with
+    | BindingRel.eq x y =>
+        let acc := if acc.contains y then acc else acc ++ [y]
+        if acc.contains x then acc else acc ++ [x]
+    | _ => acc) []
+
+/-- The equality class of `x` in stable relation order. -/
+def eqClassOrdered (b : Bindings) (x : VarName) : List VarName :=
+  match (eqVarsInOrder b).filter (fun y => (eqClass b x).contains y) with
+  | [] => [x]
+  | cls => cls
+
+/-- Stable representative of `x`'s explicit equality class. -/
+def eqRepresentative (b : Bindings) (x : VarName) : VarName :=
+  (eqClassOrdered b x).headD x
+
+/-- Every direct value carried by a member of `x`'s equality class, in stable
+    class-member order. Direct lookup selects the unique normalized value for
+    each member, so raw relation-list permutations do not steer reconciliation. -/
+def classValues (b : Bindings) (x : VarName) : List Atom :=
+  (eqClassOrdered b x).filterMap (lookupVal b)
+
+@[simp] theorem classValues_empty (x : VarName) :
+    classValues [] x = [] := by
+  simp [classValues, eqClassOrdered, eqVarsInOrder, lookupVal]
+
+@[simp] theorem classValues_singleton_val_self
+    (x : VarName) (value : Atom) :
+    classValues [BindingRel.val x value] x = [value] := by
+  simp [classValues, eqClassOrdered, eqVarsInOrder, lookupVal]
+
+@[simp] theorem classValues_singleton_val_ne
+    {key x : VarName} (value : Atom) (h : x ≠ key) :
+    classValues [BindingRel.val key value] x = [] := by
+  simp [classValues, eqClassOrdered, eqVarsInOrder, lookupVal, h]
+
+theorem classValues_eq_lookupVal_toList_of_eqVarsInOrder_nil
+    {b : Bindings} (horder : eqVarsInOrder b = []) (x : VarName) :
+    classValues b x = (lookupVal b x).toList := by
+  unfold classValues
+  rw [show eqClassOrdered b x = [x] by
+    simp [eqClassOrdered, horder]]
+  cases hlookup : lookupVal b x <;> simp [hlookup]
+
+/-- Variables participating in a binding relation, including variables nested in values. -/
+def vars (b : Bindings) : List VarName :=
+  (b.flatMap fun r => match r with
+    | BindingRel.val x a => x :: a.vars
+    | BindingRel.eq x y => [x, y]).eraseDups
+
+/-- The contribution of one stored relation to recursive resolution fuel. -/
+def relationResolutionFuel : BindingRel → Nat
+  | BindingRel.val _ value => value.size + 1
+  | BindingRel.eq _ _ => 1
+
+/-- Structural fuel sufficient for traversing every stored value and relation. -/
+def resolutionFuel (b : Bindings) (a : Atom) : Nat :=
+  a.size + (b.map relationResolutionFuel).sum + 1
+
+/-- Resolve every variable in an atom through equality classes and class values.
+    `none` means a cyclic class/value dependency was encountered. Unknown variables
+    remain variables, matching Hyperon's recursive resolution behavior. -/
+def resolveAtomAux (b : Bindings) : Nat → List VarName → Atom → Option Atom
+  | 0, _, _ => none
+  | fuel + 1, visited, atom =>
+      match atom with
+      | Atom.var x =>
+          let cls := eqClassOrdered b x
+          if cls.any visited.contains then none
+          else
+            match classValues b x with
+            | [] => some (Atom.var (eqRepresentative b x))
+            | value :: _ =>
+                match value with
+                | Atom.var y =>
+                    if cls.contains y then
+                      if cls.length == 1 then none
+                      else some (Atom.var (eqRepresentative b x))
+                    else resolveAtomAux b fuel (cls ++ visited) value
+                | _ => resolveAtomAux b fuel (cls ++ visited) value
+      | Atom.expr xs =>
+          match xs.mapM (resolveAtomAux b fuel visited) with
+          | some ys => some (Atom.expr ys)
+          | none => none
+      | other => some other
+
+/-- Resolve a bound variable through its full equality class and recursively through
+    compound values. Returns `none` for an unbound variable or a dependency loop. -/
+def resolve (b : Bindings) (x : VarName) : Option Atom :=
+  let cls := eqClassOrdered b x
+  if cls == [x] && (classValues b x).isEmpty then none
+  else resolveAtomAux b (resolutionFuel b (Atom.var x)) [] (Atom.var x)
+
+/-- Resolve every variable occurrence in `a` through its full equality class.
+    A cyclic variable occurrence remains unchanged; runtime paths reject the
+    containing binding set with `hasLoop` before instantiation. -/
+def resolveAtom (b : Bindings) : Atom → Atom
+  | Atom.var x => (resolve b x).getD (Atom.var x)
+  | Atom.expr xs => Atom.expr (xs.map (resolveAtom b))
+  | other => other
+
 /-- The variables directly equated with `$x` by `eq` relations (one hop, both orientations). -/
 def eqClasses (b : Bindings) (x : VarName) : List VarName :=
   b.foldl (fun acc r => match r with
@@ -50,10 +173,15 @@ def eqClasses (b : Bindings) (x : VarName) : List VarName :=
 def removeVal (b : Bindings) (x : VarName) : Bindings :=
   b.filter (fun r => match r with | BindingRel.val y _ => y != x | _ => true)
 
-/-- True if the set contains a trivial self-loop (`$x ← $x` or `$x = $x`), a degenerate solution
-    that the matcher discards. -/
+/-- True when any variable participates in a direct self-loop or a longer cyclic
+    dependency through equality classes, variable chains, or compound values. -/
 def hasLoop (b : Bindings) : Bool :=
-  b.any (fun r => match r with | BindingRel.val x (Atom.var y) => x == y | BindingRel.eq x y => x == y | _ => false)
+  b.any (fun r => match r with
+    | BindingRel.val x (Atom.var y) => x == y
+    | BindingRel.eq x y => x == y
+    | _ => false) ||
+  (vars b).any (fun x =>
+    (resolveAtomAux b (resolutionFuel b (Atom.var x)) [] (Atom.var x)).isNone)
 
 /-- Bind `$x ← a`, dropping any previous value binding for `$x`. Raw: no occurs/consistency check
     (that is `addVarBinding`'s job). -/

MettaHyperonFull/Core/Matching.lean

@@ -12,7 +12,9 @@ Purpose: Nondeterministic pattern matching for MeTTa atoms and the consistency-c
 Imports: MettaHyperonFull.Core.Unification, MettaHyperonFull.Core.Bindings
 Trusted boundary: none
 Main exports: GroundMatcher, Bindings.addVarBinding, Bindings.addVarEquality, Bindings.mergeOne,
-  Bindings.merge, Bindings.ofSubst, matchAtomsWith, matchAll, matchAtoms, bindingsToSubst, instantiate
+  Bindings.merge, Bindings.ofSubst, Bindings.reconcileAll, Bindings.rebuildFromSubst,
+  Bindings.reconciliationAliases, Bindings.rebuildFromReconciliation,
+  matchAtomsWith, matchAll, matchAtoms, bindingsToSubst, instantiate
 Open obligations: none
 -/
 import MettaHyperonFull.Core.Unification
@@ -26,24 +28,119 @@ abbrev GroundMatcher := Atom → Atom → List Bindings
 /- Binding-set merge based on the algorithm in the Hyperon specification. -/
 namespace Bindings
 
-/-- Add `$x ← v` to `b` consistently: if `$x` is unbound, insert it; if already bound to `v`, keep
-    `b`; otherwise the old and new values must unify (else no result). The consistency-checking core
-    of `merge`. -/
-def addVarBinding (b : Bindings) (x : VarName) (v : Atom) : List Bindings :=
-  match lookupVal b x with
-  | none => [addValRaw b x v]
-  | some prev =>
-      if prev == v then [b]
-      else match Unify.unifyTop prev v with
-        | none => []
-        | some _ => [addValRaw b x v]
-
-/-- Add the alias `$x = $y` to `b` consistently: if both are already value-bound, those values must
-    be equal (else no result). -/
+/-- View a unifier as binding relations, preserving variable/variable constraints
+    as explicit equality rather than an oriented value assignment. -/
+def ofSubst (s : Subst) : Bindings :=
+  s.map (fun p => match p.2 with
+    | Atom.var y => BindingRel.eq p.1 y
+    | value => BindingRel.val p.1 value)
+
+/-- Add every relation from a unifier to a binding set without discarding its
+    reconciliation constraints. -/
+def addSubstRaw (b : Bindings) (s : Subst) : Bindings :=
+  (ofSubst s).foldl (fun b r => match r with
+    | BindingRel.val x value => addValRaw b x value
+    | BindingRel.eq x y => addEqRaw b x y) b
+
+/-- Unify all values carried by one equality class. -/
+def unifyValues : List Atom → Option Subst
+  | [] => some []
+  | [_] => some []
+  | first :: rest =>
+      let equations := rest.map (fun value => (first, value))
+      let fuel := first.size + (rest.map Atom.size).sum
+      Unify.unifyRounds fuel equations []
+
+/-- Present one binding relation as a first-order atom equation. -/
+def relationEquation : BindingRel → Atom × Atom
+  | BindingRel.val x value => (Atom.var x, value)
+  | BindingRel.eq x y => (Atom.var x, Atom.var y)
+
+/-- The complete first-order equation presentation of a binding set. -/
+def equations (b : Bindings) : List (Atom × Atom) :=
+  b.map relationEquation
+
+/-- Structural fuel covering every atom in an equation worklist. -/
+def equationFuel (work : List (Atom × Atom)) : Nat :=
+  (work.map fun equation => equation.1.size + equation.2.size).sum
+
+/-- Reconcile every existing binding relation together with new constraints.
+    This prevents a class-local unifier from overwriting an unrelated seeded
+    value that shares one of its internal variables. -/
+def reconcileAll (b : Bindings) (extra : List (Atom × Atom)) : Option Subst :=
+  let work := equations b ++ extra
+  Unify.unifyRounds (equationFuel work) work []
+
+/-- Retain the explicit equality graph while a whole-system unifier normalizes
+    every direct value relation. -/
+def equalitySkeleton : Bindings → Bindings
+  | [] => []
+  | BindingRel.val _ _ :: rest => equalitySkeleton rest
+  | BindingRel.eq x y :: rest => BindingRel.eq x y :: equalitySkeleton rest
+
+/-- Rebuild a normalized binding set without discarding explicit class edges. -/
+def rebuildFromSubst (b : Bindings) (sigma : Subst) : Bindings :=
+  equalitySkeleton b ++ ofSubst sigma
+
+/-- Every explicit variable alias encountered by whole-system reconciliation.
+The primary trace preserves the successful run's elimination order.  The
+collision-first trace exposes aliases inside newly joined compound values
+before seeded ground equations can normalize them away. -/
+def reconciliationAliases
+    (b : Bindings) (extra : List (Atom × Atom)) (_sigma : Subst) :
+    List (VarName × VarName) :=
+  let primary := equations b ++ extra
+  let collisionFirst := extra ++ equations b
+  Unify.aliasTrace (equationFuel primary) primary ++
+    Unify.aliasTrace (equationFuel collisionFirst) collisionFirst
+
+/-- Insert one alias only when its equality class is not already represented.
+This makes alias restoration conservative on existing normalized outputs. -/
+def restoreAlias (b : Bindings) (edge : VarName × VarName) : Bindings :=
+  if (eqClass b edge.1).contains edge.2 then b
+  else addEqRaw b edge.1 edge.2
+
+/-- Rebuild normalized values while retaining every alias discovered by a
+successful whole-system reconciliation.  Existing output is left
+unchanged whenever its equality closure already carries the alias. -/
+def rebuildFromReconciliation
+    (candidate source : Bindings) (extra : List (Atom × Atom))
+    (sigma : Subst) : Bindings :=
+  (reconciliationAliases source extra sigma).foldl restoreAlias
+    (rebuildFromSubst candidate sigma)
+
+/-- Add the alias `$x = $y` while reconciling every value already carried by
+    either equality class. Successful unifiers are retained as relations. -/
 def addVarEquality (b : Bindings) (x y : VarName) : List Bindings :=
-  match lookupVal b x, lookupVal b y with
-  | some vx, some vy => if vx == vy then [addEqRaw b x y] else []
-  | _, _ => [addEqRaw b x y]
+  let candidate := addEqRaw b x y
+  match unifyValues (classValues candidate x) with
+  | none => []
+  | some [] => [candidate]
+  | some (_ :: _) =>
+      match reconcileAll b [(Atom.var x, Atom.var y)] with
+      | none => []
+      | some sigma =>
+          [rebuildFromReconciliation candidate b
+            [(Atom.var x, Atom.var y)] sigma]
+
+/-- Add `$x ← v` consistently across `$x`'s whole equality class. Variable
+    values are aliases, and successful reconciliation constraints are retained
+    instead of replacing one direct value and discarding the unifier. -/
+def addVarBinding (b : Bindings) (x : VarName) (v : Atom) : List Bindings :=
+  match v with
+  | Atom.var y => addVarEquality b x y
+  | _ =>
+      match classValues b x with
+      | [] => [addValRaw b x v]
+      | values =>
+          match unifyValues (values ++ [v]) with
+          | none => []
+          | some [] => [b]
+          | some (_ :: _) =>
+              match reconcileAll b [(Atom.var x, v)] with
+              | none => []
+              | some sigma =>
+                  [rebuildFromReconciliation b b [(Atom.var x, v)] sigma]
 
 /-- Fold one binding relation `r` into every candidate set in `bs`, keeping only consistent
     extensions; it is nondeterministic, so a relation may yield zero, one, or several results. -/
@@ -56,9 +153,6 @@ def mergeOne (bs : List Bindings) (r : BindingRel) : List Bindings :=
     result is empty exactly when they conflict. -/
 def merge (a b : Bindings) : List Bindings := b.foldl mergeOne [a]
 
-/-- View a substitution as a binding set: each `x ↦ v` becomes a `val` relation. -/
-def ofSubst (s : Subst) : Bindings := s.map (fun p => BindingRel.val p.fst p.snd)
-
 end Bindings
 
 mutual
@@ -68,7 +162,7 @@ mutual
     only the right-hand atom is grounded, the custom matcher is called as `f r l`, arguments swapped. -/
 def matchAtomsWith (custom : Option GroundMatcher) : Atom → Atom → List Bindings
   | Atom.sym a, Atom.sym b => if a == b then [[]] else []
-  | Atom.var x, Atom.var y => if x == y then [[]] else [[BindingRel.val x (Atom.var y)]]
+  | Atom.var x, Atom.var y => if x == y then [[]] else [[BindingRel.eq x y]]
   | Atom.var x, r => if Subst.occurs x r then [] else [[BindingRel.val x r]]
   | l, Atom.var y => if Subst.occurs y l then [] else [[BindingRel.val y l]]
   | Atom.expr xs, Atom.expr ys => matchAll custom [[]] xs ys
@@ -96,8 +190,8 @@ def matchAtoms (l r : Atom) : List Bindings := matchAtomsWith none l r
 def bindingsToSubst (b : Bindings) : Subst :=
   b.foldr (fun r s => match r with | BindingRel.val x v => (x,v)::s | _ => s) []
 
-/-- Apply a binding set to an atom as a substitution (value bindings only, since `eq` aliases are
-    dropped by `bindingsToSubst`). -/
-def instantiate (b : Bindings) (a : Atom) : Atom := Subst.apply (bindingsToSubst b) a
+/-- Resolve a binding set throughout an atom, including equality classes,
+    variable chains, and variables nested in compound values. -/
+def instantiate (b : Bindings) (a : Atom) : Atom := Bindings.resolveAtom b a
 
 end Metta

MettaHyperonFull/Core/Unification.lean

@@ -11,8 +11,8 @@ Purpose: First-order syntactic unification of atoms, returning a most-general un
   function is total. Grounded atoms with custom matching are handled in Matching.lean.
 Imports: MettaHyperonFull.Core.Substitution
 Trusted boundary: none
-Main exports: Unify.decomposeEq, Unify.decomposeList, Unify.decomposeAll, Unify.unifyRounds,
-  Unify.unifyTop
+Main exports: Unify.decomposeEq, Unify.decomposeList, Unify.decomposeAll,
+  Unify.aliasConstraints, Unify.aliasTrace, Unify.unifyRounds, Unify.unifyTop
 Open obligations: none
 -/
 import MettaHyperonFull.Core.Substitution
@@ -57,6 +57,38 @@ def decomposeAll : List (Atom × Atom) → Option (List (VarName × Atom))
       | some c₁, some c₂ => some (c₁ ++ c₂)
       | _, _ => none
 
+/-- Explicit variable/variable constraints visible in one fully decomposed
+unification round.  These are retained separately from the normalized
+substitution because later elimination may ground both endpoints without
+erasing the alias relation discovered by matching. -/
+def aliasConstraints : List (VarName × Atom) → List (VarName × VarName)
+  | [] => []
+  | (x, Atom.var y) :: rest => (x, y) :: aliasConstraints rest
+  | _ :: rest => aliasConstraints rest
+
+/-- Alias constraints encountered throughout Robinson elimination.  Every
+round records all currently exposed variable/variable constraints before its
+first constraint is eliminated, so an earlier grounding substitution cannot
+erase an alias that appeared later in that same round. -/
+def aliasTrace : Nat → List (Atom × Atom) → List (VarName × VarName)
+  | 0, equations =>
+      match decomposeAll equations with
+      | some constraints => aliasConstraints constraints
+      | none => []
+  | fuel + 1, equations =>
+      match decomposeAll equations with
+      | none => []
+      | some [] => []
+      | some ((x, term) :: rest) =>
+          let here := aliasConstraints ((x, term) :: rest)
+          if Subst.occurs x term then here
+          else
+            let sub : Subst := [(x, term)]
+            let remaining := rest.map fun constraint =>
+              (Subst.apply sub (Atom.var constraint.1),
+                Subst.apply sub constraint.2)
+            here ++ aliasTrace fuel remaining
+
 /-- The unification main loop, recursing structurally on `fuel`. Each round fully decomposes the
     worklist, then eliminates one variable: it substitutes `x ↦ t` into the remaining constraints
     and records the binding. Because every round removes one distinct variable from the problem,