zonking now only happens locally till next mut

AnyDSL · Feb 12, 2025 · b40c59b · b40c59b
1 parent 11c9ce8
commit b40c59b
Show file tree

Hide file tree

Showing 3 changed files with 16 additions and 21 deletions.
diff --git a/include/mim/check.h b/include/mim/check.h
@@ -23,9 +23,6 @@ class Infer : public Def, public Setters<Infer> {
     Infer* unset() { return Def::unset()->as<Infer>(); }
     ///@}
 
-    /// Eliminate Infer%s that may have been resolved in the meantime by rebuilding.
-    static bool has_infer(Ref def) { return def->isa_imm() && def->has_dep(Dep::Infer); }
-
     /// [Union-Find](https://en.wikipedia.org/wiki/Disjoint-set_data_structure) to unify Infer nodes.
     /// Def::flags is used to keep track of rank for
     /// [Union by rank](https://en.wikipedia.org/wiki/Disjoint-set_data_structure#Union_by_rank).

diff --git a/src/mim/check.cpp b/src/mim/check.cpp
@@ -15,16 +15,15 @@ class Zonker : public Rewriter {
         : Rewriter(world) {}
 
     Ref rewrite(Ref old_def) override {
-        if (Infer::has_infer(old_def)) return Rewriter::rewrite(old_def);
+        if (old_def->has_dep(Dep::Infer)) return Rewriter::rewrite(old_def);
         return old_def;
     }
 };
 
 } // namespace
 
-// TODO this vastly overaproximates the nodes to visit.
 const Def* Def::zonk() const {
-    if (Infer::has_infer(this)) return Zonker(world()).rewrite(this);
+    if (has_dep(Dep::Infer)) return Zonker(world()).rewrite(this);
     return this;
 }
 
@@ -152,20 +151,6 @@ template<Checker::Mode mode> bool Checker::alpha_(Ref r1, Ref r2) {
         }
     }
 
-    auto mut1 = d1->isa_mut();
-    auto mut2 = d2->isa_mut();
-    if (mut1 && mut2 && mut1 == mut2) return true;
-    // Globals are HACKs and require additionaly HACKs:
-    // Unless they are pointer equal (above) always consider them unequal.
-    if (d1->isa<Global>() || d2->isa<Global>()) return false;
-
-    if (mut1) {
-        if (auto [i, ins] = done_.emplace(mut1, d2); !ins) return i->second == d2;
-    }
-    if (mut2) {
-        if (auto [i, ins] = done_.emplace(mut2, d1); !ins) return i->second == d1;
-    }
-
     auto i1 = d1->isa_mut<Infer>();
     auto i2 = d2->isa_mut<Infer>();
 
@@ -187,6 +172,20 @@ template<Checker::Mode mode> bool Checker::alpha_(Ref r1, Ref r2) {
         }
     }
 
+    auto mut1 = d1->isa_mut();
+    auto mut2 = d2->isa_mut();
+    if (mut1 && mut2 && mut1 == mut2) return true;
+    // Globals are HACKs and require additionaly HACKs:
+    // Unless they are pointer equal (above) always consider them unequal.
+    if (d1->isa<Global>() || d2->isa<Global>()) return false;
+
+    if (mut1) {
+        if (auto [i, ins] = done_.emplace(mut1, d2); !ins) return i->second == d2;
+    }
+    if (mut2) {
+        if (auto [i, ins] = done_.emplace(mut2, d1); !ins) return i->second == d1;
+    }
+
     // normalize:
     if ((d1->isa<Lit>() && !d2->isa<Lit>())             // Lit to right
         || (!d1->isa<UMax>() && d2->isa<UMax>())        // UMax to left

diff --git a/src/mim/world.cpp b/src/mim/world.cpp
@@ -168,7 +168,6 @@ Ref World::implicit_app(Ref callee, Ref arg) {
 }
 
 Ref World::app(Ref callee, Ref arg) {
-    // Infer::zonk(Vector<Ref*>{&callee, &arg});
     callee  = callee->zonk();
     auto pi = callee->type()->isa<Pi>();