Fix a bug with class comparison

JetBrains · Mar 3, 2024 · 9c8c5eb · 9c8c5eb
1 parent dc6586e
commit 9c8c5eb
Show file tree

Hide file tree

Showing 2 changed files with 21 additions and 2 deletions.
diff --git a/base/src/main/java/org/arend/core/expr/visitor/CompareVisitor.java b/base/src/main/java/org/arend/core/expr/visitor/CompareVisitor.java
@@ -1431,8 +1431,8 @@ public Boolean visitClassCall(ClassCallExpression expr1, Expression expr2, Expre
       return true;
     }
 
-    for (ClassField field : classCall2.getImplementedHere().keySet()) {
-      if (!field.isProperty() && !expr1.isImplemented(field)) {
+    for (ClassField field : expr1.getImplementedHere().keySet()) {
+      if (!field.isProperty() && !classCall2.isImplemented(field)) {
         initResult(expr1, expr2);
         return false;
       }

diff --git a/src/test/java/org/arend/classes/RecordsTest.java b/src/test/java/org/arend/classes/RecordsTest.java
@@ -5,11 +5,16 @@
 import org.arend.core.definition.ClassDefinition;
 import org.arend.core.definition.FunctionDefinition;
 import org.arend.core.expr.DataCallExpression;
+import org.arend.core.expr.Expression;
 import org.arend.core.expr.NewExpression;
+import org.arend.core.expr.type.Type;
+import org.arend.core.expr.visitor.CompareVisitor;
 import org.arend.core.sort.Level;
 import org.arend.core.sort.Sort;
 import org.arend.core.subst.LevelPair;
+import org.arend.ext.core.ops.CMP;
 import org.arend.typechecking.TypeCheckingTestCase;
+import org.arend.typechecking.implicitargs.equations.DummyEquations;
 import org.junit.Assert;
 import org.junit.Test;
 
@@ -18,6 +23,7 @@
 
 import static org.arend.ExpressionFactory.Universe;
 import static org.junit.Assert.assertEquals;
+import static org.junit.Assert.assertFalse;
 
 public class RecordsTest extends TypeCheckingTestCase {
   @Test
@@ -410,4 +416,17 @@ public void resolveNotSuperImplement() {
       \\class C \\extends B { | A => \\new A { | x => 0 } }
       """, 1);
   }
+
+  @Test
+  public void comparisonTest() {
+    typeCheckModule("""
+      \\record R (n m : Nat)
+      \\func test1 => R
+      \\func test2 (n : Nat) => R n
+      """);
+    Expression expr1 = (Expression) ((FunctionDefinition) getDefinition("test1")).getBody();
+    Expression expr2 = (Expression) ((FunctionDefinition) getDefinition("test2")).getBody();
+    assertFalse(CompareVisitor.compare(DummyEquations.getInstance(), CMP.EQ, expr1, expr2, Type.OMEGA, null));
+    assertFalse(CompareVisitor.compare(DummyEquations.getInstance(), CMP.EQ, expr2, expr1, Type.OMEGA, null));
+  }
 }