Fix a bug with scopes in patterns

JetBrains · Aug 31, 2023 · 01f21bd · 01f21bd
1 parent 58e3bc4
commit 01f21bd
Showing 1 changed file with 18 additions and 0 deletions.
diff --git a/base/src/main/java/org/arend/naming/scope/ScopeFactory.java b/base/src/main/java/org/arend/naming/scope/ScopeFactory.java
@@ -349,6 +349,24 @@ public static Scope forSourceNode(Scope parentScope, Abstract.SourceNode sourceN
       return new PatternScope(parentScope, ((Abstract.Clause) parentSourceNode).getPatterns());
     }
 
+    // Extend the scope with previous patterns for the type in a pattern
+   if (sourceNode instanceof Abstract.Expression && parentSourceNode instanceof Abstract.Pattern) {
+     Abstract.SourceNode parentParentSourceNode = parentSourceNode.getParentSourceNode();
+     List<? extends Abstract.Pattern> patterns = parentParentSourceNode instanceof Abstract.Clause clause ? clause.getPatterns() : parentParentSourceNode instanceof Abstract.Pattern pattern ? pattern.getSequence() : Collections.emptyList();
+     if (!patterns.isEmpty()) {
+       List<Abstract.Pattern> newPatterns = new ArrayList<>(patterns.size());
+       for (Abstract.Pattern pattern : patterns) {
+         if (pattern == parentSourceNode) {
+           break;
+         }
+         newPatterns.add(pattern);
+       }
+       if (!newPatterns.isEmpty()) {
+         return new PatternScope(parentScope, newPatterns);
+       }
+     }
+   }
+
     return parentScope;
   }
 }