Skip to content

Commit

Permalink
align-names
Browse files Browse the repository at this point in the history
  • Loading branch information
JonathanStarup committed Jun 20, 2024
1 parent 1e80b7b commit 765c605
Showing 1 changed file with 6 additions and 6 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -446,7 +446,7 @@ object FastSetUnification {
while (changed) {
changed = false

var remaining: List[Equation] = Nil
var unsolved: List[Equation] = Nil
// OBS: subst.extended checks for conflicting mappings
for (e <- pending) {
e match {
Expand Down Expand Up @@ -478,7 +478,7 @@ object FastSetUnification {
changed = true
}
if (rest.nonEmpty) {
remaining = rest.map(Equation.mk(_, Term.Univ, loc)) ++ remaining
unsolved = rest.map(Equation.mk(_, Term.Univ, loc)) ++ unsolved
changed = true
}
}
Expand All @@ -496,17 +496,17 @@ object FastSetUnification {
changed = true
}
if (rest.nonEmpty) {
remaining = rest.map(Equation.mk(_, Term.Empty, loc)) ++ remaining
unsolved = rest.map(Equation.mk(_, Term.Empty, loc)) ++ unsolved
changed = true
}
}

case _ =>
remaining = e :: remaining
unsolved = e :: unsolved
}
}
// INVARIANT: We apply the current substitution to all remaining equations.
pending = subst(remaining)
// INVARIANT: We apply the current substitution to all unsolved equations.
pending = subst(unsolved)
}

// Reverse the unsolved equations to ensure they are returned in the original order.
Expand Down

0 comments on commit 765c605

Please sign in to comment.