Add "meta" referable kind

Fixes #349
JetBrains · Nov 20, 2024 · 900528c · 900528c
1 parent b499994
commit 900528c
Show file tree

Hide file tree

Showing 5 changed files with 12 additions and 8 deletions.
diff --git a/base/src/main/java/org/arend/module/serialization/ModuleDeserialization.java b/base/src/main/java/org/arend/module/serialization/ModuleDeserialization.java
@@ -244,6 +244,9 @@ private static GlobalReferable.Kind getDefinitionKind(DefinitionProtos.Definitio
       case CONSTRUCTOR -> {
         return GlobalReferable.Kind.DEFINED_CONSTRUCTOR;
       }
+      case META -> {
+        return GlobalReferable.Kind.META;
+      }
       default -> {
         return GlobalReferable.Kind.OTHER;
       }
@@ -269,7 +272,9 @@ private StaticGroup readGroup(ModuleProtos.Group groupProto, ChildGroup parent,
         referable = new FullModuleReferable(modulePath);
       } else {
         String name = referableProto.getName();
-        if (myPrelude && kind == GlobalReferable.Kind.FUNCTION && Prelude.ARRAY_NAME.equals(name)) {
+        if (kind == GlobalReferable.Kind.META) {
+          referable = new MetaReferable(AccessModifier.PUBLIC, readPrecedence(referableProto.getPrecedence()), name, "", null, null, parent.getReferable());
+        } else if (myPrelude && kind == GlobalReferable.Kind.FUNCTION && Prelude.ARRAY_NAME.equals(name)) {
           referable = new TypedLocatedReferable(AccessModifier.PUBLIC, readPrecedence(referableProto.getPrecedence()), name, parent.getReferable(), kind, null, null);
         } else {
           referable = new LocatedReferableImpl(AccessModifier.PUBLIC, readPrecedence(referableProto.getPrecedence()), name, parent.getReferable(), kind);
@@ -290,9 +295,7 @@ private StaticGroup readGroup(ModuleProtos.Group groupProto, ChildGroup parent,
     List<Statement> statements = new ArrayList<>(groupProto.getSubgroupCount());
 
     StaticGroup group;
-    if (def == null || def instanceof FunctionDefinition) {
-      group = new StaticGroup(referable, statements, Collections.emptyList(), parent);
-    } else if (def instanceof DataDefinition) {
+    if (def instanceof DataDefinition) {
       Set<Definition> invisibleRefs = new HashSet<>();
       for (Integer index : groupProto.getInvisibleInternalReferableList()) {
         invisibleRefs.add(myCallTargetProvider.getCallTarget(index));
@@ -326,7 +329,7 @@ private StaticGroup readGroup(ModuleProtos.Group groupProto, ChildGroup parent,
         dynamicReferables.add(subgroup.getReferable());
       }
     } else {
-      throw new IllegalStateException();
+      group = new StaticGroup(referable, statements, Collections.emptyList(), parent);
     }
 
     for (ModuleProtos.Group subgroup : groupProto.getSubgroupList()) {

diff --git a/base/src/main/java/org/arend/module/serialization/ModuleSerialization.java b/base/src/main/java/org/arend/module/serialization/ModuleSerialization.java
@@ -92,7 +92,7 @@ private ModuleProtos.Group writeGroup(Group group, ReferableConverter referableC
       refBuilder.setIndex(index);
       myCurrentDefinitions.add(index);
     }
-    if (tcReferable != null && (typechecked == null || !typechecked.status().noErrors()) && tcReferable.getKind() != GlobalReferable.Kind.OTHER) {
+    if (tcReferable != null && (typechecked == null || !typechecked.status().noErrors()) && tcReferable.getKind().isTypecheckable()) {
       myComplete = false;
     }
     builder.setReferable(refBuilder.build());

diff --git a/base/src/main/java/org/arend/naming/reference/GlobalReferable.java b/base/src/main/java/org/arend/naming/reference/GlobalReferable.java
@@ -17,6 +17,7 @@ enum Kind {
     },
     FIELD { @Override public boolean isTypecheckable() { return false; } },
     LEVEL { @Override public boolean isTypecheckable() { return false; } },
+    META { @Override public boolean isTypecheckable() { return false; } },
     OTHER { @Override public boolean isTypecheckable() { return false; } };
 
     public boolean isTypecheckable() {

diff --git a/base/src/main/java/org/arend/naming/reference/MetaReferable.java b/base/src/main/java/org/arend/naming/reference/MetaReferable.java
@@ -107,7 +107,7 @@ public Precedence getPrecedence() {
   @NotNull
   @Override
   public Kind getKind() {
-    return Kind.OTHER;
+    return Kind.META;
   }
 
   @Override

diff --git a/cli/src/main/java/org/arend/frontend/repl/action/ListLoadedModulesAction.java b/cli/src/main/java/org/arend/frontend/repl/action/ListLoadedModulesAction.java
@@ -52,7 +52,7 @@ private static void print(@NotNull CommonCliRepl api, Node node, String prefix,
       if (scope != null) {
         for (Referable referable : scope.getElements()) {
           if (referable instanceof TCDefReferable referable1) {
-            if (referable1.getTypechecked() == null && referable1.getKind() != GlobalReferable.Kind.OTHER)
+            if (referable1.getTypechecked() == null && referable1.getKind().isTypecheckable())
               failedDefs.add(referable);
             else successful++;
           }