From 31dad759df5cd6d11922f56987febd6e9ff249f3 Mon Sep 17 00:00:00 2001 From: valis Date: Thu, 4 Jul 2024 14:35:25 +0300 Subject: [PATCH] Fix the scope in run configuration --- .../definition/ArendFileDefinitionScope.kt | 34 ------------------- .../execution/TypeCheckProcessHandler.kt | 2 +- .../TypeCheckRunConfigurationEditor.kt | 7 ++-- .../configurations/TypeCheckRunState.kt | 4 +-- 4 files changed, 5 insertions(+), 42 deletions(-) delete mode 100644 src/main/kotlin/org/arend/definition/ArendFileDefinitionScope.kt diff --git a/src/main/kotlin/org/arend/definition/ArendFileDefinitionScope.kt b/src/main/kotlin/org/arend/definition/ArendFileDefinitionScope.kt deleted file mode 100644 index 503abe797..000000000 --- a/src/main/kotlin/org/arend/definition/ArendFileDefinitionScope.kt +++ /dev/null @@ -1,34 +0,0 @@ -package org.arend.definition - -import org.arend.error.DummyErrorReporter -import org.arend.ext.module.ModulePath -import org.arend.naming.reference.GlobalReferable -import org.arend.naming.reference.Referable -import org.arend.naming.scope.Scope -import org.arend.psi.ArendFile -import org.arend.resolving.PsiConcreteProvider -import org.arend.term.concrete.Concrete - -class ArendFileDefinitionScope(private val arendFile: ArendFile, private val extraPath: ModulePath = ModulePath()) : Scope { - override fun getElements(): Collection { - val result = ArrayList() - val concreteProvider = PsiConcreteProvider(arendFile.project, DummyErrorReporter.INSTANCE, null) - arendFile.getTCRefMap(Referable.RefKind.EXPR).forEach { - if (ModulePath(it.key.toList().subList(0, extraPath.size())) == extraPath) { - val ref = concreteProvider.getConcrete(it.value as GlobalReferable) - if (ref is Concrete.Definition) { - val referable = it.value - referable.displayName = referable.refLongName.toString().removePrefix(extraPath.toString()).removePrefix(".") - if (referable.displayName!!.isNotEmpty()) { - result.add(referable) - } - } - } - } - return result - } - - override fun getElements(kind: Referable.RefKind?): Collection = if (kind == null || kind == Referable.RefKind.EXPR) elements else emptyList() - - override fun resolveNamespace(name: String, onlyInternal: Boolean) = ArendFileDefinitionScope(arendFile, ModulePath(extraPath.toList() + name)) -} diff --git a/src/main/kotlin/org/arend/typechecking/execution/TypeCheckProcessHandler.kt b/src/main/kotlin/org/arend/typechecking/execution/TypeCheckProcessHandler.kt index 412a3f77e..4a2c0f610 100644 --- a/src/main/kotlin/org/arend/typechecking/execution/TypeCheckProcessHandler.kt +++ b/src/main/kotlin/org/arend/typechecking/execution/TypeCheckProcessHandler.kt @@ -121,7 +121,7 @@ class TypeCheckProcessHandler( val modulePaths = if (modulePath == null) library.loadedModules else listOf(modulePath) val modules = modulePaths.mapNotNull { - val module = library.config.findArendFile(it, withAdditional = false, withTests = command.isTest) + val module = library.config.findArendFile(it, command.isTest) if (module == null) { typecheckingErrorReporter.report(LibraryError.moduleNotFound(it, library.name)) } else if (command.definitionFullName == "") { diff --git a/src/main/kotlin/org/arend/typechecking/execution/TypeCheckRunConfigurationEditor.kt b/src/main/kotlin/org/arend/typechecking/execution/TypeCheckRunConfigurationEditor.kt index f2616c079..8ae4b7926 100644 --- a/src/main/kotlin/org/arend/typechecking/execution/TypeCheckRunConfigurationEditor.kt +++ b/src/main/kotlin/org/arend/typechecking/execution/TypeCheckRunConfigurationEditor.kt @@ -9,7 +9,6 @@ import com.intellij.ui.EditorTextField import com.intellij.ui.components.JBCheckBox import com.intellij.ui.dsl.builder.panel import org.arend.ArendFileTypeInstance -import org.arend.definition.ArendFileDefinitionScope import org.arend.ext.module.ModulePath import org.arend.module.AllArendFilesScope import org.arend.module.AllModulesScope @@ -17,6 +16,7 @@ import org.arend.module.ArendPreludeLibrary.Companion.PRELUDE import org.arend.module.ArendPreludeScope import org.arend.module.config.ArendModuleConfigService import org.arend.naming.scope.EmptyScope +import org.arend.naming.scope.LexicalScope import org.arend.psi.ArendFile import org.arend.psi.ext.PsiModuleReferable import org.arend.refactoring.move.ArendLongNameCodeFragment @@ -57,7 +57,7 @@ class TypeCheckRunConfigurationEditor(private val project: Project) : SettingsEd } val arendFile = (moduleDocument.scope.resolveName(module) as? PsiModuleReferable)?.modules?.get(0) as? ArendFile? ?: return@ArendLongNameCodeFragment EmptyScope.INSTANCE - ArendFileDefinitionScope(arendFile) + LexicalScope.opened(arendFile) })), project, ArendFileTypeInstance) } @@ -84,9 +84,6 @@ class TypeCheckRunConfigurationEditor(private val project: Project) : SettingsEd aligned("$IS_TEST_TEXT:", isTestComponent) aligned("$MODULE_TEXT:", modulePathComponent) aligned("$DEFINITION_TEXT:", definitionNameComponent) - row { - text("If the definitions from the $MODULE_TEXT (Arend file) are not loaded, then either they are not there, or they have not loaded completely. Try opening the $MODULE_TEXT (Arend file) in the editor and re-view the list of definitions in the Run configuration window") - } } companion object { diff --git a/src/main/kotlin/org/arend/typechecking/execution/configurations/TypeCheckRunState.kt b/src/main/kotlin/org/arend/typechecking/execution/configurations/TypeCheckRunState.kt index fa78cac16..4c116eada 100644 --- a/src/main/kotlin/org/arend/typechecking/execution/configurations/TypeCheckRunState.kt +++ b/src/main/kotlin/org/arend/typechecking/execution/configurations/TypeCheckRunState.kt @@ -70,7 +70,7 @@ class TypeCheckRunState(private val environment: ExecutionEnvironment, private v } } else { if (command.definitionFullName == "") { - val group = library?.getModuleGroup(modulePath, false) ?: library?.getModuleGroup(modulePath, true) + val group = library?.getModuleGroup(modulePath, command.isTest) if (library == null || group == null) { NotificationErrorReporter(environment.project).report(ModuleNotFoundError(modulePath)) return null @@ -83,7 +83,7 @@ class TypeCheckRunState(private val environment: ExecutionEnvironment, private v } } } else { - val scope = library?.moduleScopeProvider?.forModule(modulePath) ?: library?.testsModuleScopeProvider?.forModule(modulePath) + val scope = if (command.isTest) library?.testsModuleScopeProvider?.forModule(modulePath) else library?.moduleScopeProvider?.forModule(modulePath) if (library == null || scope == null) { NotificationErrorReporter(environment.project).report(ModuleNotFoundError(modulePath)) return null