Serialize definitions with errors

JetBrains · Jan 9, 2024 · 776c2f0 · 776c2f0
1 parent 8982257
commit 776c2f0
Show file tree

Hide file tree

Showing 8 changed files with 20 additions and 37 deletions.
diff --git a/base/src/main/java/org/arend/core/definition/Definition.java b/base/src/main/java/org/arend/core/definition/Definition.java
@@ -268,10 +268,10 @@ public List<? extends ParametersLevel> getParametersLevels() {
   }
 
   public enum TypeCheckingStatus {
-    HAS_ERRORS, HAS_WARNINGS, DEP_ERRORS, DEP_WARNiNGS, NO_ERRORS, TYPE_CHECKING, NEEDS_TYPE_CHECKING;
+    HAS_ERRORS, HAS_WARNINGS, NO_ERRORS, TYPE_CHECKING, NEEDS_TYPE_CHECKING;
 
     public boolean isOK() {
-      return this.ordinal() >= DEP_WARNiNGS.ordinal();
+      return this.ordinal() >= NO_ERRORS.ordinal();
     }
 
     public boolean headerIsOK() {
@@ -282,20 +282,12 @@ public boolean hasErrors() {
       return this == HAS_ERRORS;
     }
 
-    public boolean hasDepErrors() {
-      return this == HAS_ERRORS || this == DEP_ERRORS;
-    }
-
-    public boolean hasDepWarnings() {
-      return this.ordinal() <= DEP_WARNiNGS.ordinal();
-    }
-
     public boolean needsTypeChecking() {
       return this == NEEDS_TYPE_CHECKING || this == TYPE_CHECKING;
     }
 
-    public boolean withoutErrors() {
-      return !hasDepErrors();
+    public boolean noErrors() {
+      return this == NO_ERRORS;
     }
 
     public TypeCheckingStatus max(TypeCheckingStatus status) {

diff --git a/base/src/main/java/org/arend/module/serialization/DefinitionDeserialization.java b/base/src/main/java/org/arend/module/serialization/DefinitionDeserialization.java
@@ -49,7 +49,7 @@ public void fillInDefinition(DefinitionProtos.Definition defProto, Definition de
       default -> throw new DeserializationException("Unknown Definition kind: " + defProto.getDefinitionDataCase());
     }
 
-    def.setStatus(Definition.TypeCheckingStatus.NO_ERRORS);
+    def.setStatus(defProto.getNoErrors() ? Definition.TypeCheckingStatus.NO_ERRORS : Definition.TypeCheckingStatus.NEEDS_TYPE_CHECKING);
     List<Pair<TCDefReferable, Integer>> parametersOriginalDefinitions = readParametersOriginalDefinitions(defProto.getParameterOriginalDefList());
     for (Pair<TCDefReferable, Integer> pair : parametersOriginalDefinitions) {
       myDependencyListener.dependsOn(def.getRef(), pair.proj1);

diff --git a/base/src/main/java/org/arend/module/serialization/DefinitionSerialization.java b/base/src/main/java/org/arend/module/serialization/DefinitionSerialization.java
@@ -55,6 +55,7 @@ DefinitionProtos.Definition writeDefinition(Definition definition) {
     out.setPLevelsDerived(definition.arePLevelsDerived());
     out.setHLevelsDerived(definition.areHLevelsDerived());
     out.setIsStdLevels(definition.getLevelParameters() == null);
+    out.setNoErrors(definition.status().noErrors());
     if (definition.getLevelParameters() != null) {
       out.addAllLevelParam(writeLevelParameters(definition.getLevelParameters()));
     }

diff --git a/base/src/main/java/org/arend/module/serialization/ModuleSerialization.java b/base/src/main/java/org/arend/module/serialization/ModuleSerialization.java
@@ -22,7 +22,7 @@ public class ModuleSerialization {
   private final Set<Integer> myCurrentDefinitions = new HashSet<>();
   private boolean myComplete;
 
-  static final int VERSION = 11;
+  static final int VERSION = 12;
 
   public ModuleSerialization(ErrorReporter errorReporter, DependencyListener dependencyListener) {
     myErrorReporter = errorReporter;
@@ -41,7 +41,7 @@ public ModuleProtos.Module writeModule(Group group, ModulePath modulePath, Refer
     // Now write the call target tree
     Map<ModulePath, Map<String, CallTargetTree>> moduleCallTargets = new HashMap<>();
     for (Map.Entry<TCReferable, Integer> entry : myCallTargetIndexProvider.getCallTargets()) {
-      if (myCurrentDefinitions.contains(entry.getValue()) || entry.getKey() instanceof TCDefReferable ref && !doSave(ref.getTypechecked())) {
+      if (myCurrentDefinitions.contains(entry.getValue())) {
         continue;
       }
 
@@ -75,10 +75,6 @@ public ModuleProtos.Module writeModule(Group group, ModulePath modulePath, Refer
     return out.build();
   }
 
-  private boolean doSave(Definition def) {
-    return def == null || def.status().withoutErrors();
-  }
-
   private ModuleProtos.Group writeGroup(Group group, ReferableConverter referableConverter) {
     ModuleProtos.Group.Builder builder = ModuleProtos.Group.newBuilder();
 
@@ -90,14 +86,13 @@ private ModuleProtos.Group writeGroup(Group group, ReferableConverter referableC
 
     TCReferable tcReferable = referableConverter.toDataLocatedReferable(referable);
     Definition typechecked = tcReferable instanceof TCDefReferable ? ((TCDefReferable) tcReferable).getTypechecked() : null;
-    boolean save = typechecked != null && typechecked.status().withoutErrors() && typechecked.getGoals().isEmpty();
-    if (save && !(typechecked instanceof Constructor || typechecked instanceof ClassField)) {
+    if (typechecked != null && !(typechecked instanceof Constructor || typechecked instanceof ClassField)) {
       builder.setDefinition(myDefinitionSerialization.writeDefinition(typechecked));
       int index = myCallTargetIndexProvider.getDefIndex(typechecked);
       refBuilder.setIndex(index);
       myCurrentDefinitions.add(index);
     }
-    if (tcReferable != null && !save && tcReferable.getKind() != GlobalReferable.Kind.OTHER) {
+    if (tcReferable != null && (typechecked == null || !typechecked.status().noErrors()) && tcReferable.getKind() != GlobalReferable.Kind.OTHER) {
       myComplete = false;
     }
     builder.setReferable(refBuilder.build());

diff --git a/base/src/main/java/org/arend/typechecking/visitor/CheckTypeVisitor.java b/base/src/main/java/org/arend/typechecking/visitor/CheckTypeVisitor.java
@@ -1796,11 +1796,6 @@ private CallableDefinition getTypeCheckedDefinition(TCDefReferable definition, C
       errorReporter.report(new HasErrors(GeneralError.Level.ERROR, definition, expr));
       return null;
     } else {
-      if (typeCheckedDefinition.status().hasDepErrors()) {
-        setStatus(Definition.TypeCheckingStatus.DEP_ERRORS);
-      } else if (typeCheckedDefinition.status().hasDepWarnings()) {
-        setStatus(Definition.TypeCheckingStatus.DEP_WARNiNGS);
-      }
       return (CallableDefinition) typeCheckedDefinition;
     }
   }

diff --git a/base/src/main/java/org/arend/typechecking/visitor/DefinitionTypechecker.java b/base/src/main/java/org/arend/typechecking/visitor/DefinitionTypechecker.java
@@ -170,9 +170,6 @@ public List<ExtElimClause> visitFunction(Concrete.BaseFunctionDefinition def, Vo
       definition.setStatus(Definition.TypeCheckingStatus.TYPE_CHECKING);
     }
     typecheckFunctionHeader(definition, def, localInstancePool);
-    if (myNewDef) {
-      myNewDef = typechecked == null;
-    }
     return typecheckFunctionBody(definition, def);
   }
 

diff --git a/proto/src/main/proto/Definition.proto b/proto/src/main/proto/Definition.proto
@@ -27,6 +27,7 @@ message Definition {
     bool is_std_levels = 14;
     repeated ParameterOriginalDef parameter_original_def = 15;
     repeated int32 axiom = 16;
+    bool no_errors = 17;
 
     message RefList {
         repeated int32 ref = 1;

diff --git a/src/test/java/org/arend/library/CachingTest.java b/src/test/java/org/arend/library/CachingTest.java
@@ -34,17 +34,19 @@ public void statusSerialization() {
     assertThat(errorList, hasSize(1));
     errorList.clear();
 
-    Definition.TypeCheckingStatus aStatus = getDef(aClass.getGroupScope(), "a").getTypechecked().status();
+    assertThat(getDef(aClass.getGroupScope(), "a").getTypechecked().status(), is(equalTo(Definition.TypeCheckingStatus.NO_ERRORS)));
+    assertThat(getDef(aClass.getGroupScope(), "b1").getTypechecked().status(), is(equalTo(Definition.TypeCheckingStatus.HAS_ERRORS)));
+    assertThat(getDef(aClass.getGroupScope(), "b2").getTypechecked().status(), is(equalTo(Definition.TypeCheckingStatus.NO_ERRORS)));
 
     libraryManager.unloadLibrary(library);
 
     assertTrue(libraryManager.loadLibrary(library, null));
     aClass = library.getModuleGroup(new ModulePath("A"));
     assertThat(aClass, is(notNullValue()));
 
-    assertThat(getDef(aClass.getGroupScope(), "a").getTypechecked().status(), is(equalTo(aStatus)));
-    assertThat(getDef(aClass.getGroupScope(), "b1").getTypechecked(), is(nullValue()));
-    assertThat(getDef(aClass.getGroupScope(), "b2").getTypechecked(), is(nullValue()));
+    assertThat(getDef(aClass.getGroupScope(), "a").getTypechecked().status(), is(equalTo(Definition.TypeCheckingStatus.NO_ERRORS)));
+    assertThat(getDef(aClass.getGroupScope(), "b1").getTypechecked().status(), is(equalTo(Definition.TypeCheckingStatus.NEEDS_TYPE_CHECKING)));
+    assertThat(getDef(aClass.getGroupScope(), "b2").getTypechecked().status(), is(equalTo(Definition.TypeCheckingStatus.NO_ERRORS)));
   }
 
   @Test
@@ -109,9 +111,9 @@ public void errorInHeader() {
     aGroup = library.getModuleGroup(new ModulePath("A"));
     assertThat(aGroup, is(notNullValue()));
 
-    assertThat(getDef(aGroup.getGroupScope(), "D").getTypechecked(), is(notNullValue()));
-    assertThat(getDef(aGroup.getGroupScope(), "a").getTypechecked(), is(nullValue()));
-    assertThat(getDef(aGroup.getGroupScope(), "b").getTypechecked(), is(nullValue()));
+    assertThat(getDef(aGroup.getGroupScope(), "D").getTypechecked().status(), is(equalTo(Definition.TypeCheckingStatus.NO_ERRORS)));
+    assertThat(getDef(aGroup.getGroupScope(), "a").getTypechecked().status(), is(equalTo(Definition.TypeCheckingStatus.NEEDS_TYPE_CHECKING)));
+    assertThat(getDef(aGroup.getGroupScope(), "b").getTypechecked().status(), is(equalTo(Definition.TypeCheckingStatus.NO_ERRORS)));
   }
 
   @Test