Fix bug in pattern resolving

JetBrains · Sep 8, 2023 · 052cdb0 · 052cdb0
1 parent 099a95f
commit 052cdb0
Showing 1 changed file with 12 additions and 1 deletion.
diff --git a/base/src/main/java/org/arend/naming/resolving/visitor/ExpressionResolveNameVisitor.java b/base/src/main/java/org/arend/naming/resolving/visitor/ExpressionResolveNameVisitor.java
@@ -35,6 +35,7 @@
 import org.jetbrains.annotations.Nullable;
 
 import java.util.*;
+import java.util.function.Supplier;
 
 public class ExpressionResolveNameVisitor extends BaseConcreteExpressionVisitor<Void> implements ExpressionResolver, ConcreteLevelExpressionVisitor<LevelVariable, Concrete.LevelExpression> {
   private final ReferableConverter myReferableConverter;
@@ -643,7 +644,17 @@ private Concrete.Pattern visitPattern(Concrete.Pattern pattern, Map<String, Refe
 
       if (namePattern.type == null || referable instanceof LongUnresolvedReference) {
         List<Referable> resolvedRefs = new ArrayList<>();
-        Referable resolved = referable instanceof LongUnresolvedReference ? ((LongUnresolvedReference) referable).resolve(myParentScope, resolvedRefs) : referable instanceof UnresolvedReference ? ((UnresolvedReference) referable).tryResolve(myParentScope, resolvedRefs) : myParentScope.resolveName(referable.getRefName());
+
+        Supplier<Referable> c = () -> {
+          Referable r = myParentScope.resolveName(referable.getRefName());
+          resolvedRefs.add(r);
+          return r;
+        };
+
+        Referable resolved = referable instanceof LongUnresolvedReference ? ((LongUnresolvedReference) referable).resolve(myParentScope, resolvedRefs) :
+          referable instanceof UnresolvedReference ? ((UnresolvedReference) referable).tryResolve(myParentScope, resolvedRefs) :
+            c.get();
+
         Referable ref = resolved == null || resolved instanceof ErrorReference ? resolved : myReferableConverter.convert(RedirectingReferable.getOriginalReferable(resolved));
         if (ref instanceof GlobalReferable && ((GlobalReferable) ref).getKind().isConstructor()) {
           if (pattern.getAsReferable() != null) {