Make constructors and fields of private data and records private

JetBrains · May 6, 2024 · 38fe801 · 38fe801
1 parent a8a2cf1
commit 38fe801
Show file tree

Hide file tree

Showing 4 changed files with 69 additions and 10 deletions.
diff --git a/base/src/main/java/org/arend/term/group/AccessModifier.java b/base/src/main/java/org/arend/term/group/AccessModifier.java
@@ -1,3 +1,9 @@
 package org.arend.term.group;
 
-public enum AccessModifier { PUBLIC, PROTECTED, PRIVATE }
+public enum AccessModifier {
+  PUBLIC, PROTECTED, PRIVATE;
+
+  public AccessModifier max(AccessModifier modifier) {
+    return compareTo(modifier) > 0 ? this : modifier;
+  }
+}
diff --git a/cli/src/main/java/org/arend/frontend/parser/BuildVisitor.java b/cli/src/main/java/org/arend/frontend/parser/BuildVisitor.java
@@ -253,7 +253,7 @@ public Precedence visitWithPrecedence(WithPrecedenceContext ctx) {
     return new Precedence(prec.associativity, (byte) priority, prec.isInfix);
   }
 
-  private record PrecedenceWithoutPriority(Precedence.Associativity associativity, boolean isInfix) {}
+  public record PrecedenceWithoutPriority(Precedence.Associativity associativity, boolean isInfix) {}
 
   @Override
   public PrecedenceWithoutPriority visitNonAssocInfix(NonAssocInfixContext ctx) {
@@ -723,7 +723,7 @@ private StaticGroup visitDefData(AccessModifier accessModifier, DefDataContext c
     Concrete.DataDefinition dataDefinition = new Concrete.DataDefinition(referable, visitPlevelParams(topDefId.plevelParams()), visitHlevelParams(topDefId.hlevelParams()), visitTeles(ctx.tele(), true), eliminatedReferences, ctx.TRUNCATED() != null, universe, new ArrayList<>());
     dataDefinition.enclosingClass = enclosingClass;
     referable.setDefinition(dataDefinition);
-    visitDataBody(dataBodyCtx, dataDefinition, constructors);
+    visitDataBody(dataBodyCtx, dataDefinition, constructors, accessModifier);
 
     List<Statement> statements = new ArrayList<>();
     DataGroup resultGroup = new DataGroup(referable, constructors, statements, makeParameterReferableList(referable), parent);
@@ -756,7 +756,7 @@ private void collectUsedDefinitions(List<? extends Statement> statements, List<T
     }
   }
 
-  private void visitDataBody(DataBodyContext ctx, Concrete.DataDefinition def, List<InternalConcreteLocatedReferable> constructors) {
+  private void visitDataBody(DataBodyContext ctx, Concrete.DataDefinition def, List<InternalConcreteLocatedReferable> constructors, AccessModifier dataAccessModifier) {
     if (ctx instanceof DataClausesContext) {
       ConstructorClausesContext conClauses = ((DataClausesContext) ctx).constructorClauses();
       List<ConstructorClauseContext> clauseCtxList;
@@ -774,17 +774,17 @@ private void visitDataBody(DataBodyContext ctx, Concrete.DataDefinition def, Lis
           for (PatternContext patternCtx : clauseCtx.pattern()) {
             patterns.add(visitPattern(patternCtx));
           }
-          def.getConstructorClauses().add(new Concrete.ConstructorClause(tokenPosition(clauseCtx.start), patterns, visitConstructors(clauseCtx.constructor(), def, constructors)));
+          def.getConstructorClauses().add(new Concrete.ConstructorClause(tokenPosition(clauseCtx.start), patterns, visitConstructors(clauseCtx.constructor(), def, constructors, dataAccessModifier)));
         } catch (ParseException ignored) {
 
         }
       }
     } else if (ctx instanceof DataConstructorsContext) {
-      def.getConstructorClauses().add(new Concrete.ConstructorClause(tokenPosition(ctx.start), null, visitConstructors(((DataConstructorsContext) ctx).constructor(), def, constructors)));
+      def.getConstructorClauses().add(new Concrete.ConstructorClause(tokenPosition(ctx.start), null, visitConstructors(((DataConstructorsContext) ctx).constructor(), def, constructors, dataAccessModifier)));
     }
   }
 
-  private List<Concrete.Constructor> visitConstructors(List<ConstructorContext> conContexts, Concrete.DataDefinition def, List<InternalConcreteLocatedReferable> constructors) {
+  private List<Concrete.Constructor> visitConstructors(List<ConstructorContext> conContexts, Concrete.DataDefinition def, List<InternalConcreteLocatedReferable> constructors, AccessModifier dataAccessModifier) {
     List<Concrete.Constructor> result = new ArrayList<>(conContexts.size());
     for (ConstructorContext conCtx : conContexts) {
       try {
@@ -799,7 +799,11 @@ private List<Concrete.Constructor> visitConstructors(List<ConstructorContext> co
 
         DefIdContext defId = conCtx.defId();
         Pair<String, Precedence> alias = visitAlias(defId.alias());
-        InternalConcreteLocatedReferable reference = new InternalConcreteLocatedReferable(tokenPosition(defId.ID().getSymbol()), visitAccessModifier(conCtx.accessMod()), defId.ID().getText(), visitPrecedence(defId.precedence()), alias.proj1, alias.proj2, true, def.getData(), LocatedReferableImpl.Kind.CONSTRUCTOR);
+        AccessModifier accessModifier = visitAccessModifier(conCtx.accessMod());
+        if (accessModifier != AccessModifier.PUBLIC && accessModifier.compareTo(dataAccessModifier) <= 0) {
+          myErrorReporter.report(new ParserError(GeneralError.Level.WARNING_UNUSED, tokenPosition(conCtx.accessMod().start), "Access modifier is redundant"));
+        }
+        InternalConcreteLocatedReferable reference = new InternalConcreteLocatedReferable(tokenPosition(defId.ID().getSymbol()), accessModifier.max(dataAccessModifier), defId.ID().getText(), visitPrecedence(defId.precedence()), alias.proj1, alias.proj2, true, def.getData(), LocatedReferableImpl.Kind.CONSTRUCTOR);
         Concrete.Constructor constructor = new Concrete.Constructor(reference, def, visitTeles(conCtx.tele(), true), visitElim(elimCtx), clauses, conCtx.COERCE() != null);
         reference.setDefinition(constructor);
         Expr2Context type = conCtx.expr2();
@@ -835,7 +839,12 @@ private Concrete.ClassField visitClassFieldDef(ClassFieldDefContext ctx, ClassFi
     Pair<Concrete.Expression,Concrete.Expression> returnPair = visitReturnExpr(ctx.returnExpr());
     DefIdContext defId = ctx.defId();
     Pair<String, Precedence> alias = visitAlias(defId.alias());
-    ConcreteClassFieldReferable reference = new ConcreteClassFieldReferable(tokenPosition(defId.ID().getSymbol()), visitAccessModifier(ctx.accessMod()), defId.ID().getText(), visitPrecedence(defId.precedence()), alias.proj1, alias.proj2, true, true, false, parentClass.getData());
+    AccessModifier accessModifier = visitAccessModifier(ctx.accessMod());
+    AccessModifier classAccessModifier = parentClass.getData().getAccessModifier();
+    if (accessModifier != AccessModifier.PUBLIC && accessModifier.compareTo(classAccessModifier) <= 0) {
+      myErrorReporter.report(new ParserError(GeneralError.Level.WARNING_UNUSED, tokenPosition(ctx.accessMod().start), "Access modifier is redundant"));
+    }
+    ConcreteClassFieldReferable reference = new ConcreteClassFieldReferable(tokenPosition(defId.ID().getSymbol()), accessModifier.max(classAccessModifier), defId.ID().getText(), visitPrecedence(defId.precedence()), alias.proj1, alias.proj2, true, true, false, parentClass.getData());
     Concrete.ClassField field = new Concrete.ClassField(reference, parentClass, true, kind, parameters, returnPair.proj1, returnPair.proj2, ctx.COERCE() != null);
     reference.setDefinition(field);
     if (ctx.CLASSIFYING() != null) {

diff --git a/src/test/java/org/arend/naming/AccessModifiersTest.java b/src/test/java/org/arend/naming/AccessModifiersTest.java
@@ -1,8 +1,12 @@
 package org.arend.naming;
 
+import org.arend.Matchers;
+import org.arend.term.group.AccessModifier;
 import org.junit.Test;
 
 import static org.arend.Matchers.notInScope;
+import static org.junit.Assert.assertEquals;
+import static org.junit.Assert.assertNull;
 
 public class AccessModifiersTest extends NameResolverTestCase {
   @Test
@@ -380,4 +384,44 @@ public void testDynamicProtectedOpen() {
       """, 1);
     assertThatErrorsAre(notInScope("foo"));
   }
+
+  @Test
+  public void testConstructor() {
+    resolveNamesModule("""
+      \\private \\data D
+        | cons
+      """);
+    assertEquals(AccessModifier.PRIVATE, get("D.cons").getAccessModifier());
+  }
+
+  @Test
+  public void testConstructor2() {
+    lastGroup = parseModule("""
+      \\private \\data D
+        | \\private cons
+      """, 1);
+    resolveNamesModule(lastGroup, 1);
+    assertEquals(AccessModifier.PRIVATE, get("D.cons").getAccessModifier());
+    assertThatErrorsAre(Matchers.warning());
+  }
+
+  @Test
+  public void testField() {
+    resolveNamesModule("""
+      \\private \\record R
+        | field : Nat
+      """);
+    assertNull(get("R.field"));
+  }
+
+  @Test
+  public void testField2() {
+    lastGroup = parseModule("""
+      \\private \\data R
+        | \\private field : Nat
+      """, 1);
+    resolveNamesModule(lastGroup, 1);
+    assertEquals(AccessModifier.PRIVATE, get("R.field").getAccessModifier());
+    assertThatErrorsAre(Matchers.warning());
+  }
 }
diff --git a/src/test/java/org/arend/naming/NameResolverTestCase.java b/src/test/java/org/arend/naming/NameResolverTestCase.java
@@ -124,7 +124,7 @@ protected Concrete.GeneralDefinition getDefinition(TCDefReferable ref) {
     return typechecking.getConcreteProvider().getConcrete(ref);
   }
 
-  private void resolveNamesModule(ChildGroup group, int errors) {
+  protected void resolveNamesModule(ChildGroup group, int errors) {
     Scope scope = CachingScope.make(new MergeScope(ScopeFactory.forGroup(group, moduleScopeProvider), metaScope));
     new DefinitionResolveNameVisitor(ConcreteReferableProvider.INSTANCE, null, errorReporter).resolveGroupWithTypes(group, scope);
     libraryManager.getInstanceProviderSet().collectInstances(group, CachingScope.make(ScopeFactory.parentScopeForGroup(group, moduleScopeProvider, true)), IdReferableConverter.INSTANCE);