Restart typechecking in smart mode correctly

JetBrains · Jun 28, 2024 · f0ac6d4 · f0ac6d4
1 parent 5962aa1
commit f0ac6d4
Show file tree

Hide file tree

Showing 2 changed files with 79 additions and 22 deletions.
diff --git a/src/main/kotlin/org/arend/typechecking/execution/TypeCheckProcessHandler.kt b/src/main/kotlin/org/arend/typechecking/execution/TypeCheckProcessHandler.kt
@@ -326,5 +326,5 @@ class TypeCheckProcessHandler(
     override fun getProcessInput(): OutputStream? = null
 }
 
-private class DefinitionNotFoundError(definitionName: String, modulePath: ModulePath? = null) :
+class DefinitionNotFoundError(definitionName: String, modulePath: ModulePath? = null) :
     GeneralError(Level.ERROR, if (modulePath == null) "Definition '$definitionName' cannot be located without a module name" else "Definition $definitionName not found in module $modulePath")
diff --git a/src/main/kotlin/org/arend/typechecking/execution/configurations/TypeCheckRunState.kt b/src/main/kotlin/org/arend/typechecking/execution/configurations/TypeCheckRunState.kt
@@ -1,9 +1,11 @@
 package org.arend.typechecking.execution.configurations
 
+import com.intellij.codeInsight.daemon.DaemonCodeAnalyzer
 import com.intellij.execution.DefaultExecutionResult
 import com.intellij.execution.ExecutionResult
 import com.intellij.execution.Executor
-import com.intellij.execution.configurations.CommandLineState
+import com.intellij.execution.configurations.DebuggingRunnerData
+import com.intellij.execution.configurations.RunProfileState
 import com.intellij.execution.process.ProcessAdapter
 import com.intellij.execution.process.ProcessEvent
 import com.intellij.execution.process.ProcessHandler
@@ -17,38 +19,93 @@ import com.intellij.execution.testframework.sm.runner.ui.SMTRunnerUIActionsHandl
 import com.intellij.execution.testframework.sm.runner.ui.SMTestRunnerResultsForm
 import com.intellij.execution.ui.ConsoleView
 import com.intellij.openapi.components.service
+import com.intellij.psi.PsiManager
+import org.arend.ext.module.ModulePath
+import org.arend.library.BaseLibrary
+import org.arend.library.error.LibraryError
+import org.arend.module.error.ModuleNotFoundError
+import org.arend.naming.reference.LocatedReferable
+import org.arend.naming.scope.Scope
+import org.arend.settings.ArendSettings
+import org.arend.typechecking.TypeCheckingService
+import org.arend.typechecking.error.NotificationErrorReporter
+import org.arend.typechecking.execution.DefinitionNotFoundError
 import org.arend.typechecking.execution.TypeCheckCommand
 import org.arend.typechecking.execution.TypeCheckProcessHandler
 import org.arend.typechecking.execution.TypecheckingEventsProcessor
 
-class TypeCheckRunState(
-        environment: ExecutionEnvironment,
-        private val command: TypeCheckCommand
-) : CommandLineState(environment) {
+class TypeCheckRunState(private val environment: ExecutionEnvironment, private val command: TypeCheckCommand) : RunProfileState {
+    override fun execute(executor: Executor, runner: ProgramRunner<*>): ExecutionResult? {
+        if (environment.runnerSettings !is DebuggingRunnerData && service<ArendSettings>().typecheckingMode == ArendSettings.TypecheckingMode.SMART) {
+            val tcService = environment.project.service<TypeCheckingService>()
+            val modulePath = if (command.modulePath == "") null else ModulePath(command.modulePath.split('.'))
+            if (command.definitionFullName != "" && modulePath == null) {
+                NotificationErrorReporter(environment.project).report(DefinitionNotFoundError(command.definitionFullName))
+                return null
+            }
+
+            val library = if (command.library == "") null else {
+                val library = tcService.libraryManager.getRegisteredLibrary(command.library)
+                if (library == null) {
+                    NotificationErrorReporter(environment.project).report(LibraryError.notFound(command.library))
+                    return null
+                }
+                if (library.isExternal || library !is BaseLibrary) {
+                    NotificationErrorReporter(environment.project).report(LibraryError.incorrectLibrary(command.library))
+                    return null
+                }
+                library
+            }
+
+            if (modulePath == null) {
+                if (library == null) {
+                    for (lib in tcService.libraryManager.registeredLibraries) {
+                        if (!lib.isExternal) {
+                            lib.reset()
+                        }
+                    }
+                } else {
+                    library.reset()
+                }
+            } else {
+                if (command.definitionFullName == "") {
+                    val group = library?.getModuleGroup(modulePath, false) ?: library?.getModuleGroup(modulePath, true)
+                    if (library == null || group == null) {
+                        NotificationErrorReporter(environment.project).report(ModuleNotFoundError(modulePath))
+                        return null
+                    }
+                    library.resetGroup(group)
+                } else {
+                    val scope = library?.moduleScopeProvider?.forModule(modulePath) ?: library?.testsModuleScopeProvider?.forModule(modulePath)
+                    if (library == null || scope == null) {
+                        NotificationErrorReporter(environment.project).report(ModuleNotFoundError(modulePath))
+                        return null
+                    }
+                    val ref = Scope.resolveName(scope, command.definitionFullName.split('.')) as? LocatedReferable
+                    if (ref == null) {
+                        NotificationErrorReporter(environment.project).report(DefinitionNotFoundError(command.definitionFullName, modulePath))
+                        return null
+                    }
+                    library.resetDefinition(ref)
+                }
+            }
 
-    override fun startProcess() = TypeCheckProcessHandler(environment.project.service(), command)
+            PsiManager.getInstance(environment.project).dropPsiCaches()
+            DaemonCodeAnalyzer.getInstance(environment.project).restart()
+            return null
+        }
 
-    override fun execute(executor: Executor, runner: ProgramRunner<*>): ExecutionResult {
-        val processHandler = startProcess()
+        val processHandler = TypeCheckProcessHandler(environment.project.service(), command)
         val console = createConsole(executor)
         console?.attachToProcess(processHandler)
         ProcessTerminatedListener.attach(processHandler)
-        return DefaultExecutionResult(
-                console,
-                processHandler,
-                *createActions(console, processHandler, executor)
-        )
+        return DefaultExecutionResult(console, processHandler)
     }
 
-    override fun createConsole(executor: Executor): ConsoleView? {
-        val runConfiguration = environment.runnerAndConfigurationSettings?.configuration
-                ?: return null
+    private fun createConsole(executor: Executor): ConsoleView? {
+        val runConfiguration = environment.runnerAndConfigurationSettings?.configuration ?: return null
         val testFrameworkName = "ArendTypeCheckRunner"
-        val consoleProperties = SMTRunnerConsoleProperties(
-                runConfiguration,
-                testFrameworkName,
-                executor
-        )
+        val consoleProperties = SMTRunnerConsoleProperties(runConfiguration, testFrameworkName, executor)
 
         val splitterPropertyName = "$testFrameworkName.Splitter.Proportion"
         val consoleView = SMTRunnerConsoleView(consoleProperties, splitterPropertyName)