type check lambdas when last op (body) is set

* fixed bug in alpha-equiv - relaged to #174?
* fixed bug in lower_matrix_mediumlevel.cpp (wrong filter type)
* still some problems when trying to infer return type of lam

dialects/matrix/passes/lower_matrix_mediumlevel.cpp

@@ -250,7 +250,7 @@ Ref LowerMatrixMediumLevel::rewrite_(Ref def) {
             iterator[idx]               = world.call<core::bitcast>(world.type_idx(dim_nat_def), iter);
             auto [new_mem, new_mat]     = new_acc->projs<2>();
             acc                         = {new_mem, new_mat};
-            current_mut->set(dim_nat_def, for_call);
+            current_mut->set(false, for_call); // TODO correct filter?
             current_mut = body;
         }
 
@@ -292,6 +292,7 @@ Ref LowerMatrixMediumLevel::rewrite_(Ref def) {
         acc  = {current_mem, element_acc};
         cont = write_back;
 
+        // TODO this is copy&paste code from above
         for (auto idx : in_indices) {
             char for_name[32];
             sprintf(for_name, "forIn_%lu", idx);
@@ -306,7 +307,7 @@ Ref LowerMatrixMediumLevel::rewrite_(Ref def) {
             iterator[idx]               = world.call<core::bitcast>(world.type_idx(dim_nat_def), iter);
             auto [new_mem, new_element] = new_acc->projs<2>();
             acc                         = {new_mem, new_element};
-            current_mut->set(dim_nat_def, for_call);
+            current_mut->set(false, for_call); // TODO
             current_mut = body;
         }
 

thorin/check.cpp

@@ -93,8 +93,19 @@ bool Checker::equiv_internal(Ref d1, Ref d2) {
     if (!equiv(d1->type(), d2->type())) return false;
     if (d1->isa<Top>() || d2->isa<Top>()) return equiv(d1->type(), d2->type());
 
+    struct Pop {
+        ~Pop() {
+            if (vars) vars->pop_back();
+        }
+
+        Vars* vars = nullptr;
+    } pop;
+
     if (auto n1 = d1->isa_mut()) {
-        if (auto n2 = d2->isa_mut()) vars_.emplace_back(n1, n2);
+        if (auto n2 = d2->isa_mut()) {
+            vars_.emplace_back(n1, n2);
+            pop.vars = &vars_; // make sure vars_ is popped again
+        }
     }
 
     if (d1->isa<Sigma, Arr>()) {
@@ -109,10 +120,18 @@ bool Checker::equiv_internal(Ref d1, Ref d2) {
 
     if (d1->node() != d2->node() || d1->flags() != d2->flags() || d1->num_ops() != d2->num_ops()) return false;
 
-    if (auto var = d1->isa<Var>()) { // vars are equal if they appeared under the same binder
-        for (auto [n1, n2] : vars_)
-            if (var->mut() == n1) return d2->as<Var>()->mut() == n2;
-        // TODO what if Var is free?
+    if (auto var1 = d1->isa<Var>()) { // vars are equal if they appeared under the same binder
+        auto var2   = d2->as<Var>();
+        bool bound1 = false, bound2 = false;
+        for (auto [n1, n2] : vars_) {
+            if (var1->mut() == n1) {
+                bound1 = true;
+                return d2->as<Var>()->mut() == n2;
+            }
+            assert(var1->mut() != n2);
+            if (var2->mut() == n1 || var2->mut() == n2) bound2 = true;
+        }
+        if (!bound1 && !bound2) return true; // both var1 and var2 are free
         return false;
     }
 
@@ -185,19 +204,17 @@ void Sigma::check() {
 
 void Lam::check() {
     auto& w = world();
-    return; // TODO
     if (!w.checker().equiv(filter()->type(), w.type_bool()))
         error(filter(), "filter '{}' of lambda is of type '{}' but must be of type '.Bool'", filter(),
               filter()->type());
     if (!w.checker().equiv(body()->type(), codom()))
-        error(body(), "body '{}' of lambda is of type '{}' but its codomain is of type '{}'", body(), body()->type(),
-              codom());
+        error(body(), "body '{}' of lambda is of type \n'{}' but its codomain is of type \n'{}'", body(),
+              body()->type(), codom());
 }
 
 void Pi::check() {
     auto& w = world();
     auto t  = infer(dom(), codom());
-
     if (!w.checker().equiv(t, type()))
         error(type(), "declared sort '{}' of function type does not match inferred one '{}'", type(), t);
 }

thorin/check.h

@@ -71,7 +71,8 @@ class Checker {
 
     World* world_;
     DefDefMap<Equiv> equiv_;
-    std::deque<std::pair<Def*, Def*>> vars_;
+    using Vars = std::deque<std::pair<Def*, Def*>>;
+    Vars vars_;
 };
 
 } // namespace thorin