Make projections of fields into boxed expressions

JetBrains · Dec 4, 2022 · 6b9d8ce · 6b9d8ce
1 parent a6849d4
commit 6b9d8ce
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 3 deletions.
diff --git a/src/main/kotlin/org/arend/highlight/ArendHighlightingPass.kt b/src/main/kotlin/org/arend/highlight/ArendHighlightingPass.kt
@@ -108,7 +108,7 @@ class ArendHighlightingPass(file: ArendFile, editor: Editor, textRange: TextRang
                 super.patternResolved(originalRef, pattern, resolvedRefs)
                 val dataPattern = pattern.data as? ArendPattern ?: return
                 val constructors =
-                        dataPattern.sequence.takeIf { it.isNotEmpty() }?.mapNotNull { it.referenceElement?.referenceNameElement?.takeIf { el -> el.text == pattern.constructor.refName } }
+                        dataPattern.sequence.takeIf { it.isNotEmpty() }?.mapNotNull { it.referenceElement?.referenceNameElement?.takeIf { el -> el.text == pattern.constructor?.refName } }
                         ?: dataPattern.takeIf { it.singleReferable != null }?.let { listOfNotNull(it.referenceElement?.referenceNameElement) }
                         ?: return
                 for (psi in constructors) {

diff --git a/src/main/kotlin/org/arend/quickfix/ExpectedConstructorQuickFix.kt b/src/main/kotlin/org/arend/quickfix/ExpectedConstructorQuickFix.kt
@@ -825,7 +825,7 @@ class ExpectedConstructorQuickFix(val error: ExpectedConstructorError, val cause
                 is Concrete.ConstructorPattern -> { //TODO: Code too similar to "matchConcreteWithWellTyped". Could we somehow isolate common pieces of code for these functions?
                     val existingConstructor = concretePattern.constructor
                     val substitutedConstructor = (pattern.constructor)?.referable
-                    if (pattern is ConstructorExpressionPattern && substitutedConstructor == existingConstructor) {
+                    if (pattern is ConstructorExpressionPattern && existingConstructor != null && substitutedConstructor == existingConstructor) {
                         val bindingsIterator = DependentLink.Helper.toList(substitutedConstructor.typechecked.parameters).iterator()
                         val constructorExpressionParameters = pattern.subPatterns.iterator()
                         val concreteSubPatternsIterator = concretePattern.patterns.iterator()

diff --git a/src/main/kotlin/org/arend/resolving/ArendResolverListener.kt b/src/main/kotlin/org/arend/resolving/ArendResolverListener.kt
@@ -64,7 +64,8 @@ open class ArendResolverListener(private val resolverCache: ArendResolveCache) :
     }
 
     override fun patternResolved(originalRef: Referable?, pattern: Concrete.ConstructorPattern, resolvedRefs: List<Referable?>) {
-        resolveReference(pattern.data, pattern.constructor, resolvedRefs)
+        val ref = pattern.constructor
+        if (ref != null) resolveReference(pattern.data, ref, resolvedRefs)
     }
 
     override fun patternResolved(pattern: Concrete.NamePattern) {