Add some functions to resolver API

Author: valis

api/src/main/java/org/arend/ext/reference/ExpressionResolver.java

@@ -10,6 +10,11 @@
 import java.util.Set;
 
 public interface ExpressionResolver {
+  /**
+   * Resolves the specified short name.
+   */
+  @Nullable ArendRef resolveName(@NotNull String name);
+
   /**
    * Resolves names in the given expression.
    */
@@ -40,6 +45,16 @@ public interface ExpressionResolver {
    */
   void registerDeclaration(@NotNull ArendRef ref);
 
+  /**
+   * @return the original reference of a redirecting one.
+   */
+  @NotNull ArendRef getOriginalRef(@NotNull ArendRef ref);
+
+  /**
+   * Checks if {@code ref} is unresolved.
+   */
+  boolean isUnresolved(@NotNull ArendRef ref);
+
   /**
    * Checks if {@code ref} is unresolved and contains more than 1 name separated by dots.
    */

base/src/main/java/org/arend/naming/resolving/visitor/ExpressionResolveNameVisitor.java

@@ -71,6 +71,12 @@ public List<Referable> getContext() {
     return myContext;
   }
 
+  @Override
+  public @Nullable ArendRef resolveName(@NotNull String name) {
+    Referable result = tryResolve(new NamedUnresolvedReference(null, name), myScope, null);
+    return result != null && !(result instanceof NamedUnresolvedReference) ? convertReferable(result, null, false) : null;
+  }
+
   @Override
   public @NotNull ConcreteExpression resolve(@NotNull ConcreteExpression expression) {
     if (!(expression instanceof Concrete.Expression)) {
@@ -140,6 +146,19 @@ public void registerDeclaration(@NotNull ArendRef ref) {
     }
   }
 
+  @Override
+  public @NotNull ArendRef getOriginalRef(@NotNull ArendRef ref) {
+    while (ref instanceof RedirectingReferable) {
+      ref = ((RedirectingReferable) ref).getOriginalReferable();
+    }
+    return ref;
+  }
+
+  @Override
+  public boolean isUnresolved(@NotNull ArendRef ref) {
+    return ref instanceof UnresolvedReference;
+  }
+
   @Override
   public boolean isLongUnresolvedReference(@NotNull ArendRef ref) {
     return ref instanceof LongUnresolvedReference && ((LongUnresolvedReference) ref).getPath().size() > 1;
@@ -230,21 +249,25 @@ void resolveLocal(Concrete.ReferenceExpression expr) {
     }
   }
 
-  private Referable convertChecked(Referable origRef, Object data) {
+  private Referable convertChecked(Referable origRef, Object data, boolean reportError) {
     if (origRef instanceof ErrorReference) {
       return origRef;
     }
     Referable ref = myReferableConverter.convert(origRef);
     if (ref != null) {
       return ref;
     }
-    NameResolverError error = new NameResolverError("Invalid reference", data);
-    myErrorReporter.report(error);
-    return new ErrorReference(error, origRef.getRefName());
+    if (reportError) {
+      NameResolverError error = new NameResolverError("Invalid reference", data);
+      myErrorReporter.report(error);
+      return new ErrorReference(error, origRef.getRefName());
+    } else {
+      return null;
+    }
   }
 
-  Referable convertReferable(Referable referable, Object data) {
-    Referable origRef = referable instanceof RedirectingReferable ? ((RedirectingReferable) referable).getOriginalReferable() : referable;
+  private Referable convertReferable(Referable referable, Object data, boolean reportError) {
+    Referable origRef = referable;
     while (origRef instanceof RedirectingReferable) {
       origRef = ((RedirectingReferable) origRef).getOriginalReferable();
     }
@@ -256,14 +279,18 @@ Referable convertReferable(Referable referable, Object data) {
       return referable;
     }
 
-    origRef = convertChecked(origRef, data);
+    origRef = convertChecked(origRef, data, reportError);
     if (referable instanceof RedirectingReferable) {
       return new RedirectingReferableImpl(origRef, ((RedirectingReferable) referable).getPrecedence(), referable.textRepresentation());
     } else {
       return origRef;
     }
   }
 
+  Referable convertReferable(Referable referable, Object data) {
+    return convertReferable(referable, data, true);
+  }
+
   private void convertExpr(Concrete.ReferenceExpression expr) {
     if (expr.getReferent() instanceof GlobalReferable && !(expr.getReferent() instanceof TCDefReferable)) {
       expr.setReferent(convertReferable(expr.getReferent(), expr.getData()));
@@ -814,7 +841,7 @@ public void resolvePattern(Concrete.Pattern pattern) {
     Referable origReferable = ((Concrete.ConstructorPattern) pattern).getConstructor();
     if (origReferable instanceof UnresolvedReference) {
       List<Referable> resolvedList = myResolverListener == null ? null : new ArrayList<>();
-      Referable referable = convertChecked(resolve(origReferable, myParentScope, false, resolvedList, Referable.RefKind.EXPR), ((UnresolvedReference) origReferable).getData());
+      Referable referable = convertChecked(resolve(origReferable, myParentScope, false, resolvedList, Referable.RefKind.EXPR), ((UnresolvedReference) origReferable).getData(), true);
       if (referable instanceof ErrorReference) {
         myErrorReporter.report(((ErrorReference) referable).getError());
       } else if (referable instanceof GlobalReferable && !((GlobalReferable) referable).getKind().isConstructor()) {
@@ -902,7 +929,7 @@ Referable visitClassFieldReference(Concrete.ClassElement element, Referable oldF
       if (field instanceof ErrorReference) {
         myErrorReporter.report(((ErrorReference) field).getError());
       } else if (field instanceof GlobalReferable && !(field instanceof TCDefReferable)) {
-        field = convertChecked(field, ((UnresolvedReference) oldField).getData());
+        field = convertChecked(field, ((UnresolvedReference) oldField).getData(), true);
       }
       if (element instanceof Concrete.CoClauseElement) {
         ((Concrete.CoClauseElement) element).setImplementedField(field);