From bf7ffe0befda557565657e56f082729bb5bd8d09 Mon Sep 17 00:00:00 2001 From: Aleksei Luchinin Date: Thu, 19 Dec 2024 17:06:56 +0100 Subject: [PATCH] Fix #388 --- .../UnresolvedArendPatternInspection.kt | 62 ++++++++++++++++--- .../kotlin/org/arend/psi/ArendFileScope.kt | 10 ++- .../UnresolvedArendPatternInspectionTest.kt | 36 +++++++++++ 3 files changed, 95 insertions(+), 13 deletions(-) diff --git a/src/main/kotlin/org/arend/inspection/UnresolvedArendPatternInspection.kt b/src/main/kotlin/org/arend/inspection/UnresolvedArendPatternInspection.kt index 137feff79..dc026f949 100644 --- 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() + 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() + 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() != null) { + val caseArg = pattern.ancestor()?.caseArguments?.get(index) + val resolve = (caseArg?.expression as? ArendNewExpr?)?.argumentAppExpr?.atomFieldsAcc?.atom?.literal?.longName?.resolve + ?: caseArg?.eliminatedReference?.resolve + (resolve?.ancestor()?.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 index 34f0f505a..861e697e9 100644 --- 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 } } \ No newline at end of file diff --git a/src/test/kotlin/org/arend/inspection/UnresolvedArendPatternInspectionTest.kt b/src/test/kotlin/org/arend/inspection/UnresolvedArendPatternInspectionTest.kt index 7d9cb5521..194a833fd 100644 --- 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) = "$text" }