Merge pull request #547 from alex999990009/alex99999/fixes

Fix {?} and the Infer parameter quick fix and add the Intention to generate pattern matching clauses

src/main/kotlin/org/arend/actions/ArendOpenInReplAction.kt

@@ -1,6 +1,7 @@
 package org.arend.actions
 
 import com.intellij.execution.ui.ConsoleViewContentType
+import com.intellij.openapi.actionSystem.ActionUpdateThread
 import com.intellij.openapi.actionSystem.AnAction
 import com.intellij.openapi.actionSystem.AnActionEvent
 import com.intellij.openapi.actionSystem.CommonDataKeys
@@ -9,6 +10,8 @@ import org.arend.psi.ArendFile
 import org.arend.toolWindow.repl.ArendReplService
 
 class ArendOpenInReplAction : AnAction() {
+    override fun getActionUpdateThread(): ActionUpdateThread = ActionUpdateThread.BGT
+
     override fun update(e: AnActionEvent) {
         super.update(e)
         e.presentation.isEnabledAndVisible = module(e) != null

src/main/kotlin/org/arend/codeInsight/ArendTypedHandler.kt

@@ -9,6 +9,9 @@ import com.intellij.openapi.editor.Editor
 import com.intellij.openapi.project.Project
 import com.intellij.psi.PsiDocumentManager
 import com.intellij.psi.PsiFile
+import com.intellij.psi.util.elementType
+import com.intellij.refactoring.suggested.endOffset
+import com.intellij.refactoring.suggested.startOffset
 import com.intellij.util.text.CharArrayCharSequence
 import org.arend.psi.ArendElementTypes.*
 import org.arend.settings.ArendSettings
@@ -50,14 +53,24 @@ class ArendTypedHandler : TypedHandlerDelegate() {
         )
     }
 
+    private fun addParens(project: Project, editor: Editor, file: PsiFile) {
+        val element = file.findElementAt(editor.selectionModel.selectionStart) ?: return
+        val document = editor.document
+        PsiDocumentManager.getInstance(project).commitDocument(document)
+        document.insertString(element.startOffset, "(")
+        document.insertString(element.endOffset + 1, ")")
+    }
+
     override fun beforeSelectionRemoved(c: Char, project: Project, editor: Editor, file: PsiFile): Result {
-        if (BRACKETS.contains(c.toString())) {
-            val selectedText = editor.selectionModel.selectedText
+        val selectedText = editor.selectionModel.selectedText
+        val element = file.findElementAt(editor.selectionModel.selectionStart)
+        if (c == '(' && element?.elementType == TGOAL) {
+            addParens(project, editor, file)
+            return Result.STOP
+        } else if (BRACKETS.contains(c.toString())) {
             if (BRACKETS.contains(selectedText)) {
                 changeCorrespondingBracket(c, project, editor, file)
                 return Result.CONTINUE
-            } else if (selectedText == "{?}") {
-                return Result.CONTINUE
             }
         }
         return SelectionQuotingTypedHandler().beforeSelectionRemoved(c, project, editor, file)

src/main/kotlin/org/arend/highlight/BasePass.kt

@@ -63,7 +63,6 @@ import org.arend.typechecking.error.local.*
 import org.arend.typechecking.error.local.CertainTypecheckingError.Kind.*
 import org.arend.ext.error.InstanceInferenceError
 import org.arend.injection.InjectedArendEditor
-import org.arend.injection.actions.NormalizationCache
 import org.arend.naming.scope.CachingScope
 import org.arend.naming.scope.ConvertingScope
 import org.arend.psi.ArendExpressionCodeFragment
@@ -81,7 +80,6 @@ abstract class BasePass(protected open val file: IArendFile, editor: Editor, nam
 
     private val highlights = ArrayList<HighlightInfo>()
     private val errorList = ArrayList<GeneralError>()
-    private val normalizationCache: NormalizationCache = NormalizationCache()
     private val verboseLevelMap: MutableMap<Expression, Int> = mutableMapOf()
     private val verboseLevelParameterMap: MutableMap<DependentLink, Int> = mutableMapOf()
 

src/main/kotlin/org/arend/intention/SelfTargetingIntention.kt

@@ -79,7 +79,6 @@ abstract class SelfTargetingIntention<T : PsiElement>(
 
     final override fun invoke(project: Project, editor: Editor?, file: PsiFile) {
         editor ?: return
-        PsiDocumentManager.getInstance(project).commitAllDocuments()
         val target = getTarget(editor, file) ?: return
         if (!FileModificationService.getInstance().preparePsiElementForWrite(target)) return
         applyTo(target, project, editor)

src/main/kotlin/org/arend/intention/generating/GenerateElimMissingClausesIntention.kt

@@ -0,0 +1,51 @@
+package org.arend.intention.generating
+
+import com.intellij.codeInsight.template.Template
+import com.intellij.codeInsight.template.TemplateBuilderImpl
+import com.intellij.codeInsight.template.TemplateEditingAdapter
+import com.intellij.codeInsight.template.TemplateManager
+import com.intellij.codeInsight.template.impl.TemplateState
+import com.intellij.openapi.application.runWriteAction
+import com.intellij.openapi.editor.Editor
+import com.intellij.openapi.project.Project
+import com.intellij.psi.PsiElement
+import com.intellij.refactoring.suggested.endOffset
+import org.arend.intention.SelfTargetingIntention
+import org.arend.psi.ArendFile
+import org.arend.psi.ArendPsiFactory
+import org.arend.util.ArendBundle
+
+class GenerateElimMissingClausesIntention : SelfTargetingIntention<PsiElement>(PsiElement::class.java, ArendBundle.message("arend.generateElimPatternMatchingClauses")) {
+    override fun isApplicableTo(element: PsiElement, caretOffset: Int, editor: Editor): Boolean {
+        return checkMissingClauses(element, editor)
+    }
+
+    override fun applyTo(element: PsiElement, project: Project, editor: Editor) {
+        val file = element.containingFile as ArendFile
+        val (group, _) = deleteFunctionBody(element) ?: return
+
+        val psiFactory = ArendPsiFactory(project)
+        val elim = psiFactory.createElim(emptyList())
+        runWriteAction {
+            group.add(psiFactory.createWhitespace(" "))
+            group.add(elim)
+        }
+
+        val offset = group.endOffset
+        runWriteAction {
+            editor.document.insertString(offset, " ")
+        }
+        editor.caretModel.moveToOffset(offset + 1)
+
+        val builder = TemplateBuilderImpl(elim)
+        builder.replaceElement(elim, "")
+        val template = builder.buildTemplate()
+        TemplateManager.getInstance(project).startTemplate(editor, template, object : TemplateEditingAdapter() {
+            override fun beforeTemplateFinished(state: TemplateState, template: Template?) {
+                fixMissingClausesError(project, file, editor, group, state.currentVariableRange?.endOffset ?: return)
+            }
+        })
+    }
+
+    override fun startInWriteAction(): Boolean = false
+}

src/main/kotlin/org/arend/intention/generating/GenerateMissingClausesIntention.kt

@@ -0,0 +1,23 @@
+package org.arend.intention.generating
+
+import com.intellij.openapi.editor.Editor
+import com.intellij.openapi.project.Project
+import com.intellij.psi.PsiElement
+import org.arend.intention.SelfTargetingIntention
+import org.arend.psi.ArendFile
+import org.arend.util.ArendBundle
+
+class GenerateMissingClausesIntention : SelfTargetingIntention<PsiElement>(PsiElement::class.java, ArendBundle.message("arend.generatePatternMatchingClauses")) {
+    override fun isApplicableTo(element: PsiElement, caretOffset: Int, editor: Editor): Boolean {
+        return checkMissingClauses(element, editor)
+    }
+
+    override fun applyTo(element: PsiElement, project: Project, editor: Editor) {
+        val file = element.containingFile as ArendFile
+        val (group, startOffsetParent) = deleteFunctionBody(element) ?: return
+
+        fixMissingClausesError(project, file, editor, group, startOffsetParent - 1)
+    }
+
+    override fun startInWriteAction(): Boolean = false
+}

src/main/kotlin/org/arend/intention/generating/GenerateMissingClausesUtils.kt

@@ -0,0 +1,88 @@
+package org.arend.intention.generating
+
+import com.intellij.openapi.application.runWriteAction
+import com.intellij.openapi.components.service
+import com.intellij.openapi.editor.Editor
+import com.intellij.openapi.project.Project
+import com.intellij.psi.PsiElement
+import com.intellij.psi.SmartPointerManager
+import com.intellij.psi.util.elementType
+import com.intellij.refactoring.suggested.endOffset
+import com.intellij.refactoring.suggested.startOffset
+import org.arend.ext.error.MissingClausesError
+import org.arend.psi.ArendElementTypes
+import org.arend.psi.ArendFile
+import org.arend.psi.ArendPsiFactory
+import org.arend.psi.ext.*
+import org.arend.quickfix.ImplementMissingClausesQuickFix
+import org.arend.typechecking.ArendTypechecking
+import org.arend.typechecking.error.ErrorService
+
+internal fun checkMissingClauses(element: PsiElement, editor: Editor): Boolean {
+    if (element.elementType != ArendElementTypes.TGOAL) {
+        return false
+    }
+    var fileText = (element.containingFile as ArendFile).text
+
+    var parent: PsiElement? = element
+    while (parent !is ArendFunctionBody) {
+        parent = parent?.parent
+        if (parent == null) {
+            return false
+        }
+    }
+    fileText = fileText.removeRange(parent.startOffset, parent.endOffset)
+
+    val project = editor.project ?: return false
+    val psiFactory = ArendPsiFactory(project)
+    val newFile = psiFactory.createFromText(fileText) ?: return false
+
+    ArendTypechecking.create(project).typecheckModules(listOf(newFile), null)
+
+    val errorService = project.service<ErrorService>()
+    val error = errorService.getErrors(newFile).filter { it.error is MissingClausesError }.find {
+        it.definition?.endOffset?.plus(1) == parent.startOffset
+    }
+
+    errorService.clearNameResolverErrors(newFile)
+    errorService.clearTypecheckingErrors(newFile)
+    return error != null
+}
+
+internal fun deleteFunctionBody(element: PsiElement): Pair<ArendGroup, Int>? {
+    var parent: PsiElement? = element
+    while (parent !is ArendFunctionBody) {
+        parent = parent?.parent
+        if (parent == null) {
+            return null
+        }
+    }
+
+    val group = parent.parent as? ArendGroup? ?: return null
+    val startOffsetParent = parent.startOffset
+    runWriteAction {
+        parent.delete()
+    }
+    return Pair(group, startOffsetParent)
+}
+
+internal fun fixMissingClausesError(project: Project, file: ArendFile, editor: Editor, group: ArendGroup, offset: Int) {
+    val errorService = project.service<ErrorService>()
+    (group as? ArendDefFunction?)?.let { errorService.clearTypecheckingErrors(it) }
+
+    group.dropTypechecked()
+    ArendTypechecking.create(project).typecheckModules(listOf(group), null)
+
+    val error = errorService.getErrors(file).filter { it.error is MissingClausesError }.find {
+        it.definition?.endOffset == offset
+    } ?: return
+    (error.definition as? TCDefinition?)?.let {
+        errorService.clearTypecheckingErrors(it)
+    }
+    runWriteAction {
+        ImplementMissingClausesQuickFix(
+            error.error as MissingClausesError,
+            SmartPointerManager.createPointer(error.cause as ArendCompositeElement)
+        ).invoke(project, editor, file)
+    }
+}

src/main/kotlin/org/arend/psi/ArendPsiFactory.kt

@@ -209,4 +209,6 @@ class ArendPsiFactory(
     fun createUnderlining() = createFromText("\\func foo (_ : Nat)")?.descendantOfType<ArendNameTele>()?.descendantOfType<ArendIdentifierOrUnknown>() ?: error("Failed to create _")
 
     fun createUniverse(universeName: String) = createFromText("\\data D : $universeName")?.descendantOfType<ArendUniverseExpr>() ?: error("Failed to create ArendUniverseExpr")
+
+    fun createElim(params: List<String>) = createFromText("\\func foo (x : Bool) \\elim ${params.joinToString(", ")}")?.descendantOfType<ArendStat>()?.descendantOfType<ArendFunctionBody>()?.descendantOfType<ArendElim>() ?: error("Failed to create ArendElim")
 }

src/main/kotlin/org/arend/quickfix/FunctionArgInferenceQuickFix.kt

@@ -44,7 +44,7 @@ class FunctionArgInferenceQuickFix(
 
         val rootPsi = cause.element?.ancestor<ArendArgumentAppExpr>() ?: return
         val errorReporter = CountingErrorReporter(GeneralError.Level.ERROR, DummyErrorReporter.INSTANCE)
-        val concreteExpr = appExprToConcrete(rootPsi, false, errorReporter) as? Concrete.AppExpression ?: return
+        val concreteExpr = appExprToConcrete(rootPsi, false, errorReporter) ?: return
         val rangeData = HashMap<Concrete.SourceNode, TextRange>(); getBounds(concreteExpr, rootPsi.node.getChildren(null).toList(), rangeData)
 
         fun findSubExpr(expr: Concrete.Expression): Concrete.Expression? {
@@ -100,7 +100,10 @@ class FunctionArgInferenceQuickFix(
                 replacementText += if (error.index == i+1) if (param.isExplicit) " $TGOAL" else " {$TGOAL}" else  if (param.isExplicit) " _" else " {_}"
                 i++
             }
-            replacementText = "(${replacementText.trim()})"
+            replacementText = replacementText.trim()
+            if (concreteExpr != subExpr) {
+                replacementText = "($replacementText)"
+            }
             textPieceToReplace = rangeData[subExpr]
             caretShift = -1
         }

src/main/kotlin/org/arend/typechecking/ArendExpressionTypechecker.kt

@@ -21,8 +21,8 @@ class ArendExpressionTypechecker(private val checkedExprData: ArendExpr, errorRe
     private var diffDepthTop = -1
     private var diffDepthDown = -1
 
-    override fun checkExpr(expr: Concrete.Expression?, expectedType: Expression?): TypecheckingResult {
-        val result = super.checkExpr(expr, expectedType)
+    override fun checkExpr(expr: Concrete.Expression?, expectedType: Expression?): TypecheckingResult? {
+        val result = super.checkExpr(expr, expectedType) ?: return null
         val data = expr?.data as? PsiElement? ?: return result
         check(data, checkedExprData, result, true)
         check(checkedExprData, data, result, false)

src/main/kotlin/org/arend/typechecking/error/ErrorService.kt

@@ -158,6 +158,10 @@ class ErrorService : ErrorReporter {
         updateTypecheckingErrors(definition.containingFile as? ArendFile ?: return, definition)
     }
 
+    fun clearTypecheckingErrors(file: ArendFile) {
+        typecheckingErrors.remove(file)
+    }
+
     fun clearAllErrors() {
         nameResolverErrors.clear()
         typecheckingErrors.clear()

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

@@ -288,6 +288,18 @@
             <category>Arend</category>
         </intentionAction>
 
+        <intentionAction>
+            <language>Arend</language>
+            <className>org.arend.intention.generating.GenerateMissingClausesIntention</className>
+            <category>Arend</category>
+        </intentionAction>
+
+        <intentionAction>
+            <language>Arend</language>
+            <className>org.arend.intention.generating.GenerateElimMissingClausesIntention</className>
+            <category>Arend</category>
+        </intentionAction>
+
         <!-- <highlightRangeExtension implementation="org.arend.annotation.ArendHighlightRangeExtension"/> -->
 
         <daemon.changeLocalityDetector implementation="org.arend.highlight.ArendChangeLocalityDetector"/>

src/main/resources/intentionDescriptions/GenerateElimMissingClausesIntention/after.ard.template

@@ -0,0 +1,5 @@
+\import Data.Bool
+
+\func foo (n m : Nat) : Bool <spot>\elim n
+  | 0 => {?}
+  | suc n => {?}</spot>

src/main/resources/intentionDescriptions/GenerateElimMissingClausesIntention/before.ard.template

@@ -0,0 +1,3 @@
+\import Data.Bool
+
+\func foo (n m : Nat) : Bool => <spot>{?}</spot>

src/main/resources/intentionDescriptions/GenerateElimMissingClausesIntention/description.html

@@ -0,0 +1,5 @@
+<html>
+<body>
+Generates pattern matching clauses using \\elim
+</body>
+</html>

src/main/resources/intentionDescriptions/GenerateMissingClausesIntention/after.ard.template

@@ -0,0 +1,7 @@
+\import Data.Bool
+
+\func foo (n m : Nat) : Bool<spot>
+  | 0, 0 => {?}
+  | 0, suc m => {?}
+  | suc n, 0 => {?}
+  | suc n, suc m => {?}</spot>

src/main/resources/intentionDescriptions/GenerateMissingClausesIntention/before.ard.template

@@ -0,0 +1,3 @@
+\import Data.Bool
+
+\func foo (n m : Nat) : Bool => <spot>{?}</spot>

src/main/resources/intentionDescriptions/GenerateMissingClausesIntention/description.html

@@ -0,0 +1,5 @@
+<html>
+<body>
+Generates pattern matching clauses
+</body>
+</html>

src/main/resources/messages/ArendBundle.properties

@@ -201,6 +201,8 @@ arend.changeSignature.parseError=Unable to parse expression correctly
 
 arend.replaceBrackets=Replace with brackets
 arend.replaceParentheses=Replace with parentheses
+arend.generatePatternMatchingClauses=Generates pattern matching clauses
+arend.generateElimPatternMatchingClauses=Using \\elim to generate pattern matching clauses
 
 arend.updateYamlConfigurationQuestion=Would you like to update the settings from the YAML file?
 arend.updateYamlConfiguration=Update

src/test/kotlin/org/arend/codeInsight/ArendTypedHandlerTest.kt

@@ -29,4 +29,6 @@ class ArendTypedHandlerTest : ArendTestBase() {
     fun `test closing paren`() = check("""\func f (a : Nat){-caret-} => {?}""", """\func f {a : Nat} => {?}""", '}')
 
     fun `test closing brace`() = check("""\func f {a : Nat}{-caret-} => {?}""", """\func f (a : Nat) => {?}""", ')')
+
+    fun `test parens goal`() = check("""\func f => {-caret-}{?}""", """\func f => ({?})""", '(')
 }