Fix #388

JetBrains · Dec 20, 2024 · bf7ffe0 · bf7ffe0
1 parent 69c9ffd
commit bf7ffe0
Show file tree

Hide file tree

Showing 3 changed files with 95 additions and 13 deletions.
diff --git a/src/main/kotlin/org/arend/inspection/UnresolvedArendPatternInspection.kt b/src/main/kotlin/org/arend/inspection/UnresolvedArendPatternInspection.kt
@@ -3,27 +3,69 @@ package org.arend.inspection
 import com.intellij.codeInspection.ProblemsHolder
 import com.intellij.psi.PsiElement
 import com.intellij.psi.PsiElementVisitor
+import com.intellij.psi.stubs.StubIndex
+import com.intellij.psi.util.childrenOfType
+import org.arend.psi.ArendFile
+import org.arend.psi.ArendFileScope
+import org.arend.psi.ancestor
 import org.arend.psi.ext.*
+import org.arend.psi.stubs.index.ArendDefinitionIndex
+import org.arend.refactoring.isPrelude
+import org.arend.term.abs.Abstract
+import org.arend.term.group.Group
 import org.arend.util.ArendBundle
 
 class UnresolvedArendPatternInspection : ArendInspectionBase() {
     override fun buildArendVisitor(holder: ProblemsHolder, isOnTheFly: Boolean): PsiElementVisitor {
         return object : PsiElementVisitor() {
+
+            fun registerProblem(element: PsiElement) {
+                val message = ArendBundle.message("arend.inspection.unresolved.pattern", element.text)
+                holder.registerProblem(element, message)
+            }
+
             override fun visitElement(element: PsiElement) {
                 super.visitElement(element)
-                if (element is ArendPattern && element.parent !is ArendPattern) {
-                    val parent = element.parent
-                    if ((parent is ArendClause && parent.patterns.size > 1) || parent.parent is ArendFunctionClauses ||
-                        (parent.parent is ArendDataBody && (parent.parent as ArendDataBody).elim != null)) {
-                        return
-                    }
-                    val resolve = element.singleReferable?.reference?.resolve() ?: return
-                    if (resolve !is ArendConstructor && resolve !is ArendDefInstance) {
-                        val message = ArendBundle.message("arend.inspection.unresolved.pattern", element.text)
-                        holder.registerProblem(element, message)
+                if (element !is ArendPattern) {
+                    return
+                }
+
+                val identifier = element.singleReferable ?: return
+                val name = identifier.refName
+                val project = element.project
+                val constructors = StubIndex.getElements(ArendDefinitionIndex.KEY, name, project, ArendFileScope(project), PsiReferable::class.java).filterIsInstance<ArendConstructor>()
+                val resolve = identifier.reference?.resolve() ?: return
+
+                if (constructors.isNotEmpty() && (!constructors.contains(resolve) &&
+                    (resolve.containingFile as? ArendFile?)?.let { isPrelude(it) } == false)) {
+                    val group = (getTypeOfPattern(element) as? ArendLiteral?)?.longName?.resolve as? Group?
+                    val groupConstructors = group?.constructors ?: emptyList()
+                    if (groupConstructors.any { constructors.contains(it) }) {
+                        registerProblem(element)
                     }
                 }
             }
+
+            private fun getTypeOfPattern(pattern: ArendPattern): PsiElement? {
+                val patterns = pattern.parent?.childrenOfType<ArendPattern>()
+                val firstPattern = patterns?.first()
+                val firstPatternResolve = firstPattern?.singleReferable?.reference?.resolve()
+                val index = patterns?.indexOf(pattern) ?: -1
+                return if (firstPatternResolve is Abstract.ParametersHolder) {
+                    val parameter = firstPatternResolve.parameters[index - 1]
+                    parameter?.type as? PsiElement
+                } else if (pattern.parent is ArendPattern) {
+                    val parentGroup = getTypeOfPattern(pattern.parent as ArendPattern) as? Abstract.ParametersHolder?
+                    parentGroup?.parameters?.get(index)?.type as? PsiElement?
+                } else if (pattern.ancestor<ArendCaseExpr>() != null) {
+                    val caseArg = pattern.ancestor<ArendCaseExpr>()?.caseArguments?.get(index)
+                    val resolve = (caseArg?.expression as? ArendNewExpr?)?.argumentAppExpr?.atomFieldsAcc?.atom?.literal?.longName?.resolve
+                        ?: caseArg?.eliminatedReference?.resolve
+                    (resolve?.ancestor<ArendNameTele>()?.type as? ArendNewExpr?)?.argumentAppExpr?.atomFieldsAcc?.atom?.literal
+                } else {
+                    null
+                }
+            }
         }
     }
 }
diff --git a/src/main/kotlin/org/arend/psi/ArendFileScope.kt b/src/main/kotlin/org/arend/psi/ArendFileScope.kt
@@ -4,12 +4,16 @@ import com.intellij.openapi.project.Project
 import com.intellij.openapi.vfs.VirtualFile
 import com.intellij.psi.PsiManager
 import com.intellij.psi.search.ProjectAndLibrariesScope
+import org.arend.prelude.Prelude
 
 class ArendFileScope(project: Project): ProjectAndLibrariesScope(project) {
     override fun contains(file: VirtualFile): Boolean {
-        if (!super.contains(file)) return false
         val project = project ?: return false
-        val psiFile = PsiManager.getInstance(project).findFile(file)
-        return psiFile is ArendFile && psiFile.moduleLocation != null
+        val psiFile = PsiManager.getInstance(project).findFile(file) as? ArendFile ?: return false
+        if (psiFile.libraryName == Prelude.LIBRARY_NAME) {
+            return true
+        }
+        if (!super.contains(file)) return false
+        return psiFile.moduleLocation != null
     }
 }
diff --git a/src/test/kotlin/org/arend/inspection/UnresolvedArendPatternInspectionTest.kt b/src/test/kotlin/org/arend/inspection/UnresolvedArendPatternInspectionTest.kt
@@ -24,6 +24,42 @@ class UnresolvedArendPatternInspectionTest : QuickFixTestBase() {
         } 
     """)
 
+    fun testBoolBar() = doWarningsCheck(myFixture, """
+        -- ! Bool.ard
+        \import Data.Bool(Bool, if)
+
+        \data Bool | false | true 
+        
+        -- ! Main.ard
+        \import Bool(Bool)
+
+        \data Foo
+          | cons Bool Bool
+        
+        \func bar (b : Foo) : Nat => \case b \with {
+          | cons ${uapWarning("false")} ${uapWarning("true")} => 1
+          | cons ${uapWarning("true")} ${uapWarning("false")} => 0
+        }
+    """)
+
+    fun testBoolSigma() = doWarningsCheck(myFixture, """
+        -- ! Bool.ard
+        \import Data.Bool(Bool, if)
+
+        \data Bool | false | true 
+        
+        -- ! Main.ard
+        \import Bool(Bool)
+
+        \data Foo
+          | cons (\Sigma Bool Bool)
+        
+        \func bar (b : Foo) : Nat => \case b \with {
+          | cons (f, ${uapWarning("true")}) => 1
+          | cons (t, ${uapWarning("false")}) => 0
+        }
+    """)
+
     companion object {
         fun uapWarning(text: String) = "<warning descr=\"${ArendBundle.message("arend.inspection.unresolved.pattern", text)}\" textAttributesKey=\"WARNING_ATTRIBUTES\">$text</warning>"
     }