diff --git a/base/src/main/java/org/arend/module/serialization/ModuleDeserialization.java b/base/src/main/java/org/arend/module/serialization/ModuleDeserialization.java index b7c7a8f97..5e559ae7f 100644 --- 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 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 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 index 22f31e5da..98cde84b4 100644 --- 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 index 7ed2eed5e..587e995ed 100644 --- 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 index ec96acc75..1f16b39dc 100644 --- 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 index 759e08e29..ce50ea119 100644 --- 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++; }