Skip to content

Commit

Permalink
Fix desugarer
Browse files Browse the repository at this point in the history
  • Loading branch information
@valis
valis committed Feb 21, 2024
1 parent ccdf428 commit 4ea5828
Show file tree
Hide file tree
Showing 4 changed files with 276 additions and 224 deletions.
103 changes: 51 additions & 52 deletions base/src/main/java/org/arend/typechecking/visitor/DefinitionTypechecker.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2651,6 +2651,57 @@ private void typecheckClass(Concrete.ClassDefinition def, ClassDefinition typedD

fixClassElements(typedDef, def, def.getElements());

// Set level fields
{
findLevelsParentsInClass(typedDef, def);
List<LevelVariable> levelParams = typecheckLevelParameters(def);
if (myNewDef) {
typedDef.setLevelParameters(levelParams);
}
}

List<LocalInstance> localInstances = new ArrayList<>();
boolean hasClassifyingField = false;
if (!def.isRecord() && !def.withoutClassifying()) {
if (def.getClassifyingField() != null) {
hasClassifyingField = true;
} else {
for (ClassDefinition superClass : typedDef.getSuperClasses()) {
if (superClass.getClassifyingField() != null) {
hasClassifyingField = true;
break;
}
}
}
}

// Typecheck class parameters
{
Concrete.Expression previousType = null;
ClassField previousField = null;
for (Concrete.ClassElement element : def.getElements()) {
if (element instanceof Concrete.ClassField field) {
if (!field.getData().isParameterField()) {
continue;
}
if (previousType == field.getResultType()) {
if (myNewDef && previousField != null) {
ClassField newField = addField(field.getData(), typedDef, previousField.getType(), previousField.getTypeLevel());
newField.setStatus(previousField.status());
newField.setUniverseKind(previousField.getUniverseKind());
newField.setNumberOfParameters(previousField.getNumberOfParameters());
if (field.isCoerce()) {
newField.setHideable(true);
}
}
} else {
previousType = field.getResultType();
previousField = typecheckClassField(field, typedDef, localInstances, hasClassifyingField, def);
}
}
}
}

// Process super classes
for (Concrete.ReferenceExpression aSuperClass : def.getSuperClasses()) {
ClassDefinition superClass = typechecker.referableToDefinition(aSuperClass.getReferent(), ClassDefinition.class, "Expected a class", aSuperClass);
Expand All @@ -2661,21 +2712,11 @@ private void typecheckClass(Concrete.ClassDefinition def, ClassDefinition typedD
errorReporter.report(new TypecheckingError("Array cannot be extended", aSuperClass));
continue;
}

if (myNewDef) {
typedDef.addSuperClass(superClass);
}
}

// Set level fields
{
findLevelsParentsInClass(typedDef, def);
List<LevelVariable> levelParams = typecheckLevelParameters(def);
if (myNewDef) {
typedDef.setLevelParameters(levelParams);
}
}

Levels idLevels = typedDef.makeIdLevels();

// Set super class levels
Expand Down Expand Up @@ -2759,48 +2800,6 @@ protected Void forDependencies(ClassDefinition unit) {
}
}

List<LocalInstance> localInstances = new ArrayList<>();
boolean hasClassifyingField = false;
if (!def.isRecord() && !def.withoutClassifying()) {
if (def.getClassifyingField() != null) {
hasClassifyingField = true;
} else {
for (ClassDefinition superClass : typedDef.getSuperClasses()) {
if (superClass.getClassifyingField() != null) {
hasClassifyingField = true;
break;
}
}
}
}

// Typecheck class parameters
{
Concrete.Expression previousType = null;
ClassField previousField = null;
for (Concrete.ClassElement element : def.getElements()) {
if (element instanceof Concrete.ClassField field) {
if (!field.getData().isParameterField()) {
continue;
}
if (previousType == field.getResultType()) {
if (myNewDef && previousField != null) {
ClassField newField = addField(field.getData(), typedDef, previousField.getType(), previousField.getTypeLevel());
newField.setStatus(previousField.status());
newField.setUniverseKind(previousField.getUniverseKind());
newField.setNumberOfParameters(previousField.getNumberOfParameters());
if (field.isCoerce()) {
newField.setHideable(true);
}
}
} else {
previousType = field.getResultType();
previousField = typecheckClassField(field, typedDef, localInstances, hasClassifyingField, def);
}
}
}
}

// Copy data from super classes
for (ClassDefinition superClass : typedDef.getSuperClasses()) {
typedDef.addFields(superClass.getNotImplementedFields());
Expand Down
12 changes: 8 additions & 4 deletions base/src/main/java/org/arend/typechecking/visitor/DesugarVisitor.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -146,6 +146,7 @@ public Void visitData(Concrete.DataDefinition def, Void params) {
@Override
public Void visitClass(Concrete.ClassDefinition def, Void params) {
Set<TCDefReferable> fields = new HashSet<>();
Set<TCDefReferable> myFields = new HashSet<>();
for (Concrete.ReferenceExpression superClass : def.getSuperClasses()) {
if (superClass.getReferent() instanceof TCDefReferable) {
getFields((TCDefReferable) superClass.getReferent(), fields);
Expand All @@ -157,6 +158,7 @@ public Void visitClass(Concrete.ClassDefinition def, Void params) {
if (element instanceof Concrete.ClassField) {
classFields.add((Concrete.ClassField) element);
fields.add(((Concrete.ClassField) element).getData());
myFields.add(((Concrete.ClassField) element).getData());
}
}

Expand All @@ -177,23 +179,25 @@ public Void visitClass(Concrete.ClassDefinition def, Void params) {

// Check fields
ClassFieldChecker classFieldChecker = new ClassFieldChecker(null, def.getRecursiveDefinitions(), def.getData(), superClasses, fields, futureFields, myErrorReporter);
ClassFieldChecker myClassFieldChecker = new ClassFieldChecker(null, def.getRecursiveDefinitions(), def.getData(), superClasses, myFields, futureFields, myErrorReporter);
Concrete.Expression previousType = null;
for (int i = 0; i < classFields.size(); i++) {
Concrete.ClassField classField = classFields.get(i);
ClassFieldChecker checker = classField.getData().isParameterField() ? myClassFieldChecker : classFieldChecker;
Concrete.Expression fieldType = classField.getResultType();
Referable thisParameter = new HiddenLocalReferable("this");
classFieldChecker.setThisParameter(thisParameter);
checker.setThisParameter(thisParameter);
if (fieldType == previousType && classField.getParameters().isEmpty()) {
classField.getParameters().addAll(classFields.get(i - 1).getParameters());
classField.setResultType(classFields.get(i - 1).getResultType());
classField.setResultTypeLevel(classFields.get(i - 1).getResultTypeLevel());
} else {
previousType = classField.getParameters().isEmpty() ? fieldType : null;
classFieldChecker.visitParameters(classField.getParameters(), null);
checker.visitParameters(classField.getParameters(), null);
classField.getParameters().add(0, new Concrete.TelescopeParameter(classField.getParameters().isEmpty() ? fieldType.getData() : classField.getParameters().get(0).getData(), false, Collections.singletonList(thisParameter), makeThisClassCall(fieldType.getData(), def.getData()), false));
classField.setResultType(fieldType.accept(classFieldChecker, null));
classField.setResultType(fieldType.accept(checker, null));
if (classField.getResultTypeLevel() != null) {
classField.setResultTypeLevel(classField.getResultTypeLevel().accept(classFieldChecker, null));
classField.setResultTypeLevel(classField.getResultTypeLevel().accept(checker, null));
}
}
futureFields.remove(classField.getData());
Expand Down
18 changes: 14 additions & 4 deletions src/test/java/org/arend/classes/ClassParametersTest.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,8 +11,7 @@
import java.util.Objects;

import static junit.framework.TestCase.assertEquals;
import static org.arend.Matchers.notInScope;
import static org.arend.Matchers.typeMismatchError;
import static org.arend.Matchers.*;

public class ClassParametersTest extends TypeCheckingTestCase {
@Test
Expand Down Expand Up @@ -378,19 +377,30 @@ public void implicitParameterNew() {
""");
}

// TODO: We should probably forbid such dependencies.
// TODO: We should probably forbid such dependencies or put overridden fields after the fields they depend on.
// Currently, there is a workaround for this; see ClassCallExpression.java
@Test
public void classFieldParametersTest() {
typeCheckModule("""
\\record A
\\record B (n : Nat) \\extends A
\\record R (a : A)
\\record S (k : Nat) \\extends R {
\\record S \\extends R {
| k : Nat
\\override a : B k
}
\\func test => S
""");
((ClassCallExpression) Objects.requireNonNull(((FunctionDefinition) getDefinition("test")).getBody())).getClassFieldParameters();
}

@Test
public void superDependency() {
typeCheckModule("""
\\record A
| n : Nat
\\record B (p : n = n) \\extends A
""", 2);
assertThatErrorsAre(argInferenceError(), argInferenceError());
}
}
Loading

0 comments on commit 4ea5828

Please sign in to comment.