Fix #165

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 "<img ${if (isNewlineLatexCode) "style=\"margin: 0 auto;display: block;\"" else "style=\"vertical-align: -$shift%;margin: 1;\""} " +
+        return "<img ${if (isNewlineLatexCode) "style=\"margin: 0 auto;display: block;\"" else "style=\"vertical-align: $shift%;margin: 1;\""} " +
                 "src=\"file:///${file.absolutePath}\" title=$title width=\"${icon.iconWidth}\" height=\"${icon.iconHeight}\">"
     } catch (e: Exception) {
         if (e is ParseException) {

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<ArendDefIdentifier>) {
+        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<ArendLetClause>().filter {
+            val letExpr = it.parent as ArendLetExpr
+            var hasElement = false
+
+            val defIdentifiers = mutableListOf<ArendDefIdentifier>()
+            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
+        }
+    }
+}

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>(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<ArendPassFactoryService>()
+        myPassId = registrar.registerTextEditorHighlightingPass(this, intArrayOf(service.highlightingPassId), null, false, -1)
+        service.typecheckerPassId = myPassId
+    }
+}

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

src/main/resources/META-INF/plugin.xml

@@ -417,6 +417,7 @@
         <highlightingPassFactory implementation="org.arend.highlight.NameShadowingHighlighterPassFactory"/>
         <highlightingPassFactory implementation="org.arend.highlight.RedundantParameterNamePassFactory"/>
         <highlightingPassFactory implementation="org.arend.highlight.PartiallyInfixOperatorPrefixFormPassFactory"/>
+        <highlightingPassFactory implementation="org.arend.highlight.RedundantLocalBindingPassFactory"/>
 
         <!-- Tool Windows -->
 

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

src/test/kotlin/org/arend/inspection/NameShadowingInspectionTest.kt → 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
 

src/test/kotlin/org/arend/inspection/PartiallyInfixOperatorPrefixFormInspectionTest.kt → 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
 

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) = "<warning descr=\"${ArendBundle.message("arend.inspection.remove.letBinding.message")}\" textAttributesKey=\"WARNING_ATTRIBUTES\">$text</warning>"
+    }
+}

src/test/kotlin/org/arend/inspection/RedundantParameterNameInspectionTest.kt → 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) = "<warning descr=\"${ArendBundle.message("arend.inspection.parameter.redundant", text)}\" textAttributesKey=\"WARNING_ATTRIBUTES\">$text</warning>"
     }

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() {