Fix a bug in ClassCallExpression

JetBrains · Apr 18, 2024 · a9399d9 · a9399d9
1 parent 5d1df89
commit a9399d9
Show file tree

Hide file tree

Showing 2 changed files with 26 additions and 4 deletions.
diff --git a/base/src/main/java/org/arend/core/expr/ClassCallExpression.java b/base/src/main/java/org/arend/core/expr/ClassCallExpression.java
@@ -387,9 +387,14 @@ public Expression visitFieldCall(FieldCallExpression expr, Void params) {
             }
           }
 
-          // TODO: This is a workaround for ClassParametersTest.classFieldParametersTest
           Expression arg = expr.getArgument().getUnderlyingExpression();
-          return arg instanceof ReferenceExpression && ((ReferenceExpression) arg).getBinding() == thisBinding && !newExpr.getClassCall().isImplemented(expr.getDefinition()) ? expr : FieldCallExpression.make(expr.getDefinition(), expr.getArgument().accept(this, null));
+          if (arg instanceof ReferenceExpression && ((ReferenceExpression) arg).getBinding() == thisBinding) {
+            Expression fieldImpl = newExpr.getClassCall().myImplementations.get(field);
+            if (fieldImpl != null) {
+              return expr.subst(myThisBinding, newExpr).accept(this, null);
+            }
+          }
+          return super.visitFieldCall(expr, null);
         }
 
         @Override

diff --git a/base/src/main/java/org/arend/typechecking/visitor/DefinitionTypechecker.java b/base/src/main/java/org/arend/typechecking/visitor/DefinitionTypechecker.java
@@ -3386,8 +3386,25 @@ private ClassField typecheckClassField(Concrete.BaseClassField def, ClassDefinit
           ok = false;
         }
       }
-      if (newDef) {
-        overrideField(typedDef, ok ? piType : new PiExpression(piType.getResultSort(), piType.getParameters(), new ErrorExpression()), parentClass, def);
+      if (ok) {
+        Set<ClassField> allowedFields = new HashSet<>();
+        for (ClassField field : parentClass.getNotImplementedFields()) {
+          if (field == typedDef) {
+            break;
+          }
+          allowedFields.add(field);
+        }
+        if (piType.accept(new SearchVisitor<Void>() {
+          @Override
+          protected CoreExpression.FindAction processDefCall(DefCallExpression expression, Void param) {
+            return expression.getDefinition() instanceof ClassField field && parentClass.isSubClassOf(field.getParentClass()) && !allowedFields.contains(field) && !parentClass.isImplemented(field) ? CoreExpression.FindAction.STOP : CoreExpression.FindAction.CONTINUE;
+          }
+        }, null)) {
+          ok = false;
+        }
+      }
+      if (newDef && ok) {
+        overrideField(typedDef, piType, parentClass, def);
       }
       if (!ok) {
         return null;