Merge branch 'master' into fcc

include/mim/check.h

@@ -25,8 +25,8 @@ class Infer : public Def, public Setters<Infer> {
 
     /// Eliminate Infer%s that may have been resolved in the meantime by rebuilding.
     /// @returns `true`, if one of the arguements was in fact updated.
-    static bool eliminate(Vector<Ref*>);
-    static bool should_eliminate(Ref def) { return def->isa_imm() && def->has_dep(Dep::Infer); }
+    static bool zonk(Vector<Ref*>);
+    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

include/mim/def.h

@@ -93,7 +93,8 @@ class Ref {
     const Def* operator->() const { return refer(def_); }
     operator const Def*() const { return refer(def_); }
     explicit operator bool() const { return def_; }
-    static const Def* refer(const Def* def); ///< Retrieves Infer::arg from @p def.
+    static const Def* refer(const Def* def); ///< Same as Infer::find but does nothing if @p def is `nullptr`.
+    const Def* def() const { return def_; }  ///< Retrieve wrapped Def without Infer::refer%ing.
 
     friend std::ostream& operator<<(std::ostream&, Ref);
 

lit/fib.mim

@@ -20,7 +20,6 @@ con seq {A: *} (n: Nat) (body: Cn [Cn A][A]) (exit: Cn A) (acc: A)@tt =
             end;
     end;
 
-
 fun extern fib(n: Nat): Nat =
     seq n body exit (0, 1)
     where

src/mim/check.cpp

@@ -9,13 +9,13 @@ namespace mim {
 
 namespace {
 
-class InferRewriter : public Rewriter {
+class Zonker : public Rewriter {
 public:
-    InferRewriter(World& world)
+    Zonker(World& world)
         : Rewriter(world) {}
 
     Ref rewrite(Ref old_def) override {
-        if (Infer::should_eliminate(old_def)) return Rewriter::rewrite(old_def);
+        if (Infer::has_infer(old_def)) return Rewriter::rewrite(old_def);
         return old_def;
     }
 };
@@ -61,10 +61,11 @@ const Def* Infer::find(const Def* def) {
     return res;
 }
 
-bool Infer::eliminate(Vector<Ref*> refs) {
-    if (std::ranges::any_of(refs, [](auto pref) { return should_eliminate(*pref); })) {
+// TODO this vastly overaproximates the nodes to visit.
+bool Infer::zonk(Vector<Ref*> refs) {
+    if (std::ranges::any_of(refs, [](auto pref) { return has_infer(*pref); })) {
         auto& world = (*refs.front())->world();
-        InferRewriter rw(world);
+        Zonker rw(world);
         for (size_t i = 0, e = refs.size(); i != e; ++i) {
             auto ref = *refs[i];
             *refs[i] = ref->has_dep(Dep::Infer) ? rw.rewrite(ref) : ref;

src/mim/dot.cpp

@@ -7,6 +7,9 @@
 
 #include "mim/util/print.h"
 
+// Do not zonk here!
+// We want to see all Refs in the DOT graph.
+
 namespace mim {
 
 namespace {
@@ -60,7 +63,7 @@ class Dot {
         if (!def->is_set()) return;
 
         for (size_t i = 0, e = def->num_ops(); i != e; ++i) {
-            auto op = def->op(i);
+            auto op = def->op(i).def();
             recurse(op, max - 1);
             tab_.print(os_, "_{} -> _{}[taillabel=\"{}\",", def->gid(), op->gid(), i);
             if (op->isa<Lit>() || op->isa<Axiom>() || def->isa<Var>() || def->isa<Nat>() || def->isa<Idx>())
@@ -69,7 +72,7 @@ class Dot {
                 print(os_, "];\n");
         }
 
-        if (auto t = def->type(); t && types_) {
+        if (auto t = def->type().def(); t && types_) {
             recurse(t, max - 1);
             tab_.println(os_, "_{} -> _{}[color=\"#00000000\",constraint=false,style=dashed];", def->gid(), t->gid());
         }
@@ -91,7 +94,7 @@ class Dot {
     std::ostream& tooltip(const Def* def) {
         static constexpr auto NL = "&#13;&#10;";
         auto loc                 = escape(def->loc());
-        auto type                = escape(def->type());
+        auto type                = escape(def->type().def());
         escape(loc);
         print(os_, "tooltip=\"");
         print(os_, "<b>expr:</b> {}{}", def, NL);

src/mim/pass/pipelinebuilder.cpp

@@ -16,7 +16,7 @@
 namespace mim {
 
 void PipelineBuilder::def2pass(const Def* def, Pass* p) {
-    def->world().DLOG("associating {} with {}", def->gid(), p);
+    world().DLOG("associating {} with {}", def->gid(), p);
     def2pass_[def] = p;
 }
 Pass* PipelineBuilder::pass(const Def* def) { return def2pass_[def]; }