Solve a unification constraint
(
&mut self,
arena: &mut Arena,
_env: &Environment,
_ctx: &Context,
t1: TermId,
t2: TermId,
)
| 139 | |
| 140 | /// Solve a unification constraint |
| 141 | fn solve_unify( |
| 142 | &mut self, |
| 143 | arena: &mut Arena, |
| 144 | _env: &Environment, |
| 145 | _ctx: &Context, |
| 146 | t1: TermId, |
| 147 | t2: TermId, |
| 148 | ) -> crate::Result<()> { |
| 149 | // Fast path: already equal |
| 150 | if t1 == t2 { |
| 151 | return Ok(()); |
| 152 | } |
| 153 | |
| 154 | // Apply current substitution |
| 155 | let t1 = self.apply_subst(arena, t1)?; |
| 156 | let t2 = self.apply_subst(arena, t2)?; |
| 157 | |
| 158 | if t1 == t2 { |
| 159 | return Ok(()); |
| 160 | } |
| 161 | |
| 162 | let kind1 = arena.kind(t1).ok_or_else(|| { |
| 163 | crate::Error::Internal(format!("Invalid term ID: {:?}", t1)) |
| 164 | })?.clone(); |
| 165 | |
| 166 | let kind2 = arena.kind(t2).ok_or_else(|| { |
| 167 | crate::Error::Internal(format!("Invalid term ID: {:?}", t2)) |
| 168 | })?.clone(); |
| 169 | |
| 170 | match (kind1, kind2) { |
| 171 | // ?m = t or t = ?m |
| 172 | (TermKind::MVar(m), _) => { |
| 173 | if !self.subst.is_assigned(m) { |
| 174 | if self.occurs_check(m, t2, arena)? { |
| 175 | return Err(crate::Error::UnificationError( |
| 176 | "Occurs check failed".to_string(), |
| 177 | )); |
| 178 | } |
| 179 | self.subst.assign(m, t2); |
| 180 | Ok(()) |
| 181 | } else { |
| 182 | let assigned = self.subst.lookup(m).unwrap(); |
| 183 | self.solve_unify(arena, _env, _ctx, assigned, t2) |
| 184 | } |
| 185 | } |
| 186 | |
| 187 | (_, TermKind::MVar(m)) => { |
| 188 | if !self.subst.is_assigned(m) { |
| 189 | if self.occurs_check(m, t1, arena)? { |
| 190 | return Err(crate::Error::UnificationError( |
| 191 | "Occurs check failed".to_string(), |
| 192 | )); |
| 193 | } |
| 194 | self.subst.assign(m, t1); |
| 195 | Ok(()) |
| 196 | } else { |
| 197 | let assigned = self.subst.lookup(m).unwrap(); |
| 198 | self.solve_unify(arena, _env, _ctx, t1, assigned) |
no test coverage detected