From 822485cd1f418d3981c4db082dd2f18ced381bdc Mon Sep 17 00:00:00 2001 From: "Aleksei.Luchinin" Date: Mon, 8 Apr 2024 12:22:51 +0300 Subject: [PATCH] Fix #165 --- .../ArendDocumentationLatexUtil.kt | 4 +- .../highlight/RedundantLetBindingPass.kt | 95 +++++++++++++++++++ .../RedundantLocalBindingPassFactory.kt | 27 ++++++ .../highlight/RedundantParameterNamePass.kt | 2 +- src/main/resources/META-INF/plugin.xml | 1 + .../resources/messages/ArendBundle.properties | 2 + .../NameShadowingTest.kt} | 3 +- .../PartiallyInfixOperatorPrefixFormTest.kt} | 3 +- .../highlight/RedundantLetBindingTest.kt | 44 +++++++++ .../RedundantParameterNameTest.kt} | 14 ++- .../ArendInspectionSuppressorTest.kt | 2 +- 11 files changed, 190 insertions(+), 7 deletions(-) create mode 100644 src/main/kotlin/org/arend/highlight/RedundantLetBindingPass.kt create mode 100644 src/main/kotlin/org/arend/highlight/RedundantLocalBindingPassFactory.kt rename src/test/kotlin/org/arend/{inspection/NameShadowingInspectionTest.kt => highlight/NameShadowingTest.kt} (91%) rename src/test/kotlin/org/arend/{inspection/PartiallyInfixOperatorPrefixFormInspectionTest.kt => highlight/PartiallyInfixOperatorPrefixFormTest.kt} (92%) create mode 100644 src/test/kotlin/org/arend/highlight/RedundantLetBindingTest.kt rename src/test/kotlin/org/arend/{inspection/RedundantParameterNameInspectionTest.kt => highlight/RedundantParameterNameTest.kt} (50%) diff --git a/src/main/kotlin/org/arend/documentation/ArendDocumentationLatexUtil.kt b/src/main/kotlin/org/arend/documentation/ArendDocumentationLatexUtil.kt index d34e17733..4debbf106 100644 --- a/src/main/kotlin/org/arend/documentation/ArendDocumentationLatexUtil.kt +++ b/src/main/kotlin/org/arend/documentation/ArendDocumentationLatexUtil.kt @@ -50,9 +50,9 @@ internal fun getHtmlLatexCode(title: String, latexCode: String, project: Project val file = File(latexImagesDir.path + File.separator + title + ".png") ImageIO.write(image, "png", file.getAbsoluteFile()) - val shift = ((1 - icon.baseLine) + icon.iconDepth / (font * FONT_DIFF_COEFFICIENT)) * 100 + val shift = -((1 - icon.baseLine) + icon.iconDepth / (font * FONT_DIFF_COEFFICIENT)) * 100 - return "" } catch (e: Exception) { if (e is ParseException) { diff --git a/src/main/kotlin/org/arend/highlight/RedundantLetBindingPass.kt b/src/main/kotlin/org/arend/highlight/RedundantLetBindingPass.kt new file mode 100644 index 000000000..33d0cd339 --- /dev/null +++ b/src/main/kotlin/org/arend/highlight/RedundantLetBindingPass.kt @@ -0,0 +1,95 @@ +package org.arend.highlight + +import com.intellij.codeInsight.daemon.impl.HighlightInfo +import com.intellij.codeInsight.daemon.impl.HighlightInfoProcessor +import com.intellij.codeInsight.daemon.impl.HighlightInfoType +import com.intellij.codeInspection.HintAction +import com.intellij.lang.annotation.HighlightSeverity +import com.intellij.openapi.editor.Editor +import com.intellij.openapi.progress.ProgressIndicator +import com.intellij.openapi.project.Project +import com.intellij.openapi.util.TextRange +import com.intellij.psi.PsiElement +import com.intellij.psi.PsiFile +import com.intellij.psi.PsiRecursiveElementVisitor +import com.intellij.psi.util.descendantsOfType +import com.intellij.refactoring.suggested.startOffset +import org.arend.naming.reference.Referable +import org.arend.psi.ArendFile +import org.arend.psi.deleteWithWhitespaces +import org.arend.psi.ext.ArendDefIdentifier +import org.arend.psi.ext.ArendLetClause +import org.arend.psi.ext.ArendLetExpr +import org.arend.psi.ext.ArendPattern +import org.arend.psi.findPrevSibling +import org.arend.util.ArendBundle + +class RedundantLetBindingPass(file: ArendFile, editor: Editor, highlightInfoProcessor: HighlightInfoProcessor): + BasePass(file, editor, "Arend redundant let binding", TextRange(0, editor.document.textLength), highlightInfoProcessor) { + + private fun addDefIdentifiers(arendPattern: ArendPattern?, defIdentifiers: MutableList) { + if (arendPattern == null) { + return + } + arendPattern.singleReferable?.let { defIdentifiers.add(it) } + for (subPatterns in arendPattern.sequence) { + addDefIdentifiers(subPatterns, defIdentifiers) + } + } + + override fun collectInformationWithProgress(progress: ProgressIndicator) { + file.descendantsOfType().filter { + val letExpr = it.parent as ArendLetExpr + var hasElement = false + + val defIdentifiers = mutableListOf() + it.referable?.let { defIdentifier -> defIdentifiers.add(defIdentifier) } + addDefIdentifiers(it.pattern, defIdentifiers) + + letExpr.expr?.accept(object : PsiRecursiveElementVisitor() { + override fun visitElement(element: PsiElement) { + if (element is Referable && defIdentifiers.contains(element.reference?.resolve())) { + hasElement = true + } + super.visitElement(element) + } + }) + !hasElement + }.forEach { + val builder = HighlightInfo + .newHighlightInfo(HighlightInfoType.WARNING) + .range(it.textRange) + .severity(HighlightSeverity.WARNING) + .descriptionAndTooltip(ArendBundle.message("arend.inspection.remove.letBinding.message")) + registerFix(builder, RemoveLetBindingHintAction(it)) + addHighlightInfo(builder) + } + } + + companion object { + class RemoveLetBindingHintAction(private val letClause: ArendLetClause) : HintAction { + + override fun startInWriteAction(): Boolean = true + + override fun getFamilyName(): String = text + + override fun getText(): String = ArendBundle.message("arend.inspection.remove.letBinding") + + override fun isAvailable(project: Project, editor: Editor?, file: PsiFile?): Boolean = true + + override fun invoke(project: Project, editor: Editor?, file: PsiFile?) { + val letExpr = letClause.parent as ArendLetExpr + if (letExpr.letClauses.size > 1) { + letClause.findPrevSibling { it.text == "|" }?.deleteWithWhitespaces() + letClause.deleteWithWhitespaces() + } else { + letExpr.startOffset.let { startOffset -> letExpr.expr?.startOffset?.let { endOffset -> + editor?.document?.deleteString(startOffset, endOffset) + } } + } + } + + override fun showHint(editor: Editor): Boolean = true + } + } +} diff --git a/src/main/kotlin/org/arend/highlight/RedundantLocalBindingPassFactory.kt b/src/main/kotlin/org/arend/highlight/RedundantLocalBindingPassFactory.kt new file mode 100644 index 000000000..805a1438a --- /dev/null +++ b/src/main/kotlin/org/arend/highlight/RedundantLocalBindingPassFactory.kt @@ -0,0 +1,27 @@ +package org.arend.highlight + +import com.intellij.codeHighlighting.TextEditorHighlightingPass +import com.intellij.codeHighlighting.TextEditorHighlightingPassFactoryRegistrar +import com.intellij.codeHighlighting.TextEditorHighlightingPassRegistrar +import com.intellij.codeInsight.daemon.impl.DefaultHighlightInfoProcessor +import com.intellij.openapi.components.service +import com.intellij.openapi.editor.Editor +import com.intellij.openapi.project.Project +import com.intellij.openapi.util.TextRange +import org.arend.psi.ArendFile + +class RedundantLocalBindingPassFactory: BasePassFactory(ArendFile::class.java), TextEditorHighlightingPassFactoryRegistrar { + private var myPassId = -1 + + override fun createPass(file: ArendFile, editor: Editor, textRange: TextRange): TextEditorHighlightingPass? { + return RedundantLetBindingPass(file, editor, DefaultHighlightInfoProcessor()) + } + + override fun getPassId(): Int = myPassId + + override fun registerHighlightingPassFactory(registrar: TextEditorHighlightingPassRegistrar, project: Project) { + val service = project.service() + myPassId = registrar.registerTextEditorHighlightingPass(this, intArrayOf(service.highlightingPassId), null, false, -1) + service.typecheckerPassId = myPassId + } +} diff --git a/src/main/kotlin/org/arend/highlight/RedundantParameterNamePass.kt b/src/main/kotlin/org/arend/highlight/RedundantParameterNamePass.kt index f89f61fcc..b7662bf85 100644 --- a/src/main/kotlin/org/arend/highlight/RedundantParameterNamePass.kt +++ b/src/main/kotlin/org/arend/highlight/RedundantParameterNamePass.kt @@ -56,7 +56,7 @@ class RedundantParameterNamePass(file: ArendFile, editor: Editor, highlightInfoP override fun invoke(project: Project, editor: Editor?, file: PsiFile?) { val psiFactory = ArendPsiFactory(project) val underlining = psiFactory.createUnderlining() - defIdentifier.replace(underlining) + defIdentifier.parent.replace(underlining) } override fun showHint(editor: Editor): Boolean = true diff --git a/src/main/resources/META-INF/plugin.xml b/src/main/resources/META-INF/plugin.xml index 94a24d8e5..dda4e4eb0 100644 --- a/src/main/resources/META-INF/plugin.xml +++ b/src/main/resources/META-INF/plugin.xml @@ -417,6 +417,7 @@ + diff --git a/src/main/resources/messages/ArendBundle.properties b/src/main/resources/messages/ArendBundle.properties index 481bda681..771e99d97 100644 --- a/src/main/resources/messages/ArendBundle.properties +++ b/src/main/resources/messages/ArendBundle.properties @@ -53,6 +53,8 @@ arend.inspection.unused.import.message.unused.definition=Definition is not used arend.inspection.name.shadowed=Name ''{0}'' shadowed arend.inspection.parameter.redundant=The parameter ''{0}'' is redundant arend.inspection.infix.partially.prefix.form=One explicit argument is to the right of the infix definition with two explicit arguments +arend.inspection.remove.letBinding=Remove unused the let binding +arend.inspection.remove.letBinding.message=The let binding is not used arend.generate.function=Generate function arend.generate.function.from.goal=Generate function from goal diff --git a/src/test/kotlin/org/arend/inspection/NameShadowingInspectionTest.kt b/src/test/kotlin/org/arend/highlight/NameShadowingTest.kt similarity index 91% rename from src/test/kotlin/org/arend/inspection/NameShadowingInspectionTest.kt rename to src/test/kotlin/org/arend/highlight/NameShadowingTest.kt index 4c2710a29..8dd6f2a18 100644 --- a/src/test/kotlin/org/arend/inspection/NameShadowingInspectionTest.kt +++ b/src/test/kotlin/org/arend/highlight/NameShadowingTest.kt @@ -1,5 +1,6 @@ -package org.arend.inspection +package org.arend.highlight +import org.arend.inspection.doWarningsCheck import org.arend.quickfix.QuickFixTestBase import org.arend.util.ArendBundle diff --git a/src/test/kotlin/org/arend/inspection/PartiallyInfixOperatorPrefixFormInspectionTest.kt b/src/test/kotlin/org/arend/highlight/PartiallyInfixOperatorPrefixFormTest.kt similarity index 92% rename from src/test/kotlin/org/arend/inspection/PartiallyInfixOperatorPrefixFormInspectionTest.kt rename to src/test/kotlin/org/arend/highlight/PartiallyInfixOperatorPrefixFormTest.kt index 729587af7..3d9470ff4 100644 --- a/src/test/kotlin/org/arend/inspection/PartiallyInfixOperatorPrefixFormInspectionTest.kt +++ b/src/test/kotlin/org/arend/highlight/PartiallyInfixOperatorPrefixFormTest.kt @@ -1,5 +1,6 @@ -package org.arend.inspection +package org.arend.highlight +import org.arend.inspection.doWarningsCheck import org.arend.quickfix.QuickFixTestBase import org.arend.util.ArendBundle diff --git a/src/test/kotlin/org/arend/highlight/RedundantLetBindingTest.kt b/src/test/kotlin/org/arend/highlight/RedundantLetBindingTest.kt new file mode 100644 index 000000000..4104c0beb --- /dev/null +++ b/src/test/kotlin/org/arend/highlight/RedundantLetBindingTest.kt @@ -0,0 +1,44 @@ +package org.arend.highlight + +import org.arend.inspection.doWarningsCheck +import org.arend.quickfix.QuickFixTestBase +import org.arend.util.ArendBundle + +class RedundantLetBindingTest : QuickFixTestBase() { + fun testOneLetClause() = doWarningsCheck(myFixture, """ + \func f : String => \let | ${bindingLetWarning("y => 1")} \in "" + """) + + fun testRemoveOneLetClause() = doRemoveLetClause(""" + \func f : String => \let | {-caret-}y => 1 \in "" + """, """ + \func f : String => "" + """) + + fun testManyLetClauses() = doWarningsCheck(myFixture, """ + \func f : String => \let | ${bindingLetWarning("y => 1")} | x => "" \in x + """) + + fun testRemoveOneFromManyLetClauses() = doRemoveLetClause(""" + \func f : String => \let | {-caret-}y => 1 | x => "" \in x + """, """ + \func f : String => \let | x => "" \in x + """) + + fun testPattern() = doWarningsCheck(myFixture, """ + \func foo : \Sigma Nat Nat => (1, 1) + + \class Bar { + | a : Nat + } + \func FooBar : Bar \cowith + | a => \have (b, c) => foo \in b + """) + + private fun doRemoveLetClause(before: String, after: String) = + typedQuickFixTest(ArendBundle.message("arend.inspection.remove.letBinding"), before, after) + + companion object { + fun bindingLetWarning(text: String) = "$text" + } +} diff --git a/src/test/kotlin/org/arend/inspection/RedundantParameterNameInspectionTest.kt b/src/test/kotlin/org/arend/highlight/RedundantParameterNameTest.kt similarity index 50% rename from src/test/kotlin/org/arend/inspection/RedundantParameterNameInspectionTest.kt rename to src/test/kotlin/org/arend/highlight/RedundantParameterNameTest.kt index d06684e48..ff815d53e 100644 --- a/src/test/kotlin/org/arend/inspection/RedundantParameterNameInspectionTest.kt +++ b/src/test/kotlin/org/arend/highlight/RedundantParameterNameTest.kt @@ -1,5 +1,6 @@ -package org.arend.inspection +package org.arend.highlight +import org.arend.inspection.doWarningsCheck import org.arend.quickfix.QuickFixTestBase import org.arend.util.ArendBundle @@ -9,6 +10,17 @@ class RedundantParameterNameInspectionTest : QuickFixTestBase() { \func f (${rpnWarning("x")} : Nat) => 0 """) + fun testRemoveRedundantParameterFunc() = doRemoveRedundantParameter( + """ + \func f (x{-caret-} : Nat) => 0 + """, """ + \func f (_ : Nat) => 0 + """ + ) + + private fun doRemoveRedundantParameter(before: String, after: String) = + typedQuickFixTest(ArendBundle.message("arend.inspection.redundant.parameter.message"), before, after) + companion object { fun rpnWarning(text: String) = "$text" } diff --git a/src/test/kotlin/org/arend/inspection/ArendInspectionSuppressorTest.kt b/src/test/kotlin/org/arend/inspection/ArendInspectionSuppressorTest.kt index 5f1a68acd..6657bed65 100644 --- a/src/test/kotlin/org/arend/inspection/ArendInspectionSuppressorTest.kt +++ b/src/test/kotlin/org/arend/inspection/ArendInspectionSuppressorTest.kt @@ -2,7 +2,7 @@ package org.arend.inspection import com.intellij.codeInspection.NonAsciiCharactersInspection import org.arend.ArendTestBase -import org.arend.inspection.PartiallyInfixOperatorPrefixFormInspectionTest.Companion.infixWarning +import org.arend.highlight.PartiallyInfixOperatorPrefixFormInspectionTest.Companion.infixWarning class ArendInspectionSuppressorTest : ArendTestBase() { override fun setUp() {