Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix Run Configurations problems #523

Merged
merged 2 commits into from
Jun 28, 2024
+77 −178
Merged

Fix Run Configurations problems #523

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
d758397
Fix Run Configuration
alex999990009 Jun 28, 2024
fbb3366
Fix SlowOperations
alex999990009 Jun 28, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
55 changes: 23 additions & 32 deletions ...d/module/AllArendFilesAndPackagesScope.kt → ...in/org/arend/module/AllArendFilesScope.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,6 @@ import com.intellij.openapi.components.service
import com.intellij.openapi.vfs.VfsUtilCore
import com.intellij.openapi.vfs.VirtualFile
import com.intellij.openapi.vfs.VirtualFileVisitor
import com.intellij.psi.PsiFileSystemItem
import com.intellij.psi.PsiManager
import org.arend.ext.module.ModulePath
import org.arend.module.config.LibraryConfig
Expand All @@ -14,34 +13,37 @@ import org.arend.prelude.Prelude
import org.arend.psi.ArendFile
import org.arend.psi.ext.PsiModuleReferable
import org.arend.typechecking.TypeCheckingService
import org.arend.typechecking.execution.TypecheckRunConfigurationProducer.Companion.TEST_PREFIX
import org.arend.util.FileUtils
import org.arend.util.getRelativePath

class AllArendFilesAndPackagesScope(
val libraryConfig: LibraryConfig,
class AllArendFilesScope(
private val libraryConfig: LibraryConfig,
private val extraPath: ModulePath = ModulePath(),
private val withPrelude: Boolean = true,
private val withArendExtension: Boolean = true
private val isTest: Boolean = false,
private val withPrelude: Boolean = true
) : Scope {
override fun getElements(): Collection<Referable> {
val result = ArrayList<Referable>()

val srcDir = libraryConfig.sourcesDirFile
val testDir = libraryConfig.testsDirFile

if (extraPath.size() == 0) {
srcDir?.let { addArendFiles(it, it, result) }
testDir?.let { addArendFiles(it, it.parent, result) }
} else if (extraPath.firstName == TEST_PREFIX) {
val dir = LibraryConfig.findArendFileOrDirectoryByModulePath(testDir, ModulePath(extraPath.toList().subList(1, extraPath.size())))
dir?.let { addArendFiles(it, it, result) }
val dir = if (extraPath.size() == 0) {
if (isTest) {
testDir
} else {
srcDir
}
} else {
val dir = LibraryConfig.findArendFileOrDirectoryByModulePath(srcDir, extraPath)
dir?.let { addArendFiles(it, it, result) }
if (isTest) {
LibraryConfig.findArendFileOrDirectoryByModulePath(testDir, extraPath)
} else {
LibraryConfig.findArendFileOrDirectoryByModulePath(srcDir, extraPath)
}
}
dir?.let { addArendFiles(it, result) }

if (withPrelude) {
if (withPrelude && !isTest) {
val psiManager = PsiManager.getInstance(libraryConfig.project)
libraryConfig.project.service<TypeCheckingService>().prelude?.let { psiManager.findFile(it.virtualFile) }?.let {
result.add(PsiModuleReferable(listOf(it), Prelude.MODULE_PATH))
Expand All @@ -50,34 +52,23 @@ class AllArendFilesAndPackagesScope(
return result
}

private fun addArendFiles(root: VirtualFile, startFile: VirtualFile, result: MutableList<Referable>) {
private fun addArendFiles(root: VirtualFile, result: MutableList<Referable>) {
val psiManager = PsiManager.getInstance(libraryConfig.project)
val virtualFileVisitor = object : VirtualFileVisitor<Any>() {
override fun visitFile(file: VirtualFile): Boolean {
val psiFile = psiManager.findFile(file)
if (psiFile is ArendFile) {
result.add(createPsiModuleReferable(psiFile, root, startFile))
}
val psiDirectory = psiManager.findDirectory(file)
if (psiDirectory != null) {
result.add(createPsiModuleReferable(psiDirectory, root, startFile))
result.add(createPsiModuleReferable(psiFile, root))
}
return true
}
}
VfsUtilCore.visitChildrenRecursively(root, virtualFileVisitor)
}

private fun createPsiModuleReferable(psiItem: PsiFileSystemItem, root: VirtualFile, startFile: VirtualFile): PsiModuleReferable {
val listPath = startFile.getRelativePath(psiItem.virtualFile, if (withArendExtension) FileUtils.EXTENSION else "")
?.apply {
if (root != startFile) {
if (size > 1) {
set(0, TEST_PREFIX)
}
}
}
return object : PsiModuleReferable(listOf(psiItem), ModulePath(listPath ?: emptyList())) {
private fun createPsiModuleReferable(file: ArendFile, root: VirtualFile): PsiModuleReferable {
val listPath = root.getRelativePath(file.virtualFile, FileUtils.EXTENSION)
return object : PsiModuleReferable(listOf(file), ModulePath(listPath ?: emptyList())) {
override fun textRepresentation(): String {
val fullName = listPath?.joinToString(".") ?: ""
return fullName
Expand All @@ -87,5 +78,5 @@ class AllArendFilesAndPackagesScope(

override fun getElements(kind: Referable.RefKind?): Collection<Referable> = if (kind == null || kind == Referable.RefKind.EXPR) elements else emptyList()

override fun resolveNamespace(name: String, onlyInternal: Boolean) = AllArendFilesAndPackagesScope(libraryConfig, ModulePath(extraPath.toList() + name), false, withArendExtension)
override fun resolveNamespace(name: String, onlyInternal: Boolean) = AllArendFilesScope(libraryConfig, ModulePath(extraPath.toList() + name), isTest, false)
}
3 changes: 0 additions & 3 deletions src/main/kotlin/org/arend/module/AllModulesScope.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,10 +4,8 @@ import com.intellij.openapi.project.Project
import com.intellij.openapi.roots.ModuleRootManager
import com.intellij.psi.PsiManager
import org.arend.ext.module.ModulePath
import org.arend.naming.reference.ModuleReferable
import org.arend.naming.reference.Referable
import org.arend.naming.scope.Scope
import org.arend.prelude.Prelude.MODULE_PATH
import org.arend.psi.ext.PsiModuleReferable
import org.arend.util.allModules

Expand All @@ -20,7 +18,6 @@ class AllModulesScope(private val project: Project) : Scope {
val psiModuleFile = psiManager.findDirectory(moduleFile) ?: return@forEach
result.add(PsiModuleReferable(listOf(psiModuleFile), ModulePath(listOf(it.name))))
}
result.add(ModuleReferable(MODULE_PATH))
return result
}

Expand Down
40 changes: 3 additions & 37 deletions src/main/kotlin/org/arend/module/config/LibraryConfig.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -157,37 +157,6 @@ abstract class LibraryConfig(val project: Project) {
findArendFile(modulePath, false) ?: if (withTests) findArendFile(modulePath, true) else null
}

fun getArendDirectoryOrFile(modulePath: ModulePath, isTest: Boolean): PsiFileSystemItem? {
val psiManager = PsiManager.getInstance(project)
return if (modulePath.size() == 0) {
if (isTest) {
psiManager.findDirectory(testsDirFile!!)
} else {
psiManager.findDirectory(sourcesDirFile!!)
}
} else {
getArendSubdirectoryOrFile(modulePath, isTest)
}
}

fun getArendSubdirectoryOrFile(modulePath: ModulePath, isTest: Boolean): PsiFileSystemItem? {
val psiManager = PsiManager.getInstance(project)
if (modulePath == MODULE_PATH) {
return project.service<TypeCheckingService>().prelude
}
return if (isTest) {
(findArendFileOrDirectoryByModulePath(testsDirFile, modulePath) ?:
findArendFileOrDirectoryByModulePath(sourcesDirFile, modulePath))?.let {
psiManager.findDirectory(it) ?: psiManager.findFile(it)
} ?: findArendFile(modulePath, withAdditional = false, withTests = true)
} else {
(findArendFileOrDirectoryByModulePath(sourcesDirFile, modulePath) ?:
findArendFileOrDirectoryByModulePath(testsDirFile, modulePath))?.let {
psiManager.findDirectory(it) ?: psiManager.findFile(it)
} ?: findArendFile(modulePath, withAdditional = false, withTests = true)
}
}

fun findArendFileOrDirectory(modulePath: ModulePath, withAdditional: Boolean, withTests: Boolean): PsiFileSystemItem? {
if (modulePath.size() == 0) {
return findArendDirectory(modulePath)
Expand Down Expand Up @@ -275,13 +244,10 @@ abstract class LibraryConfig(val project: Project) {
val path = modulePath.toList()
var curElement = root
for (index in path.indices) {
if (index == path.indices.last - 1 && path[index + 1] == EXTENSION.drop(1)) {
curElement = curElement?.findChild(path[index] + EXTENSION)
break
} else if (index == path.indices.last) {
curElement = curElement?.findChild(path[index]) ?: curElement?.findChild(path[index] + EXTENSION)
curElement = if (index == path.indices.last) {
curElement?.findChild(path[index]) ?: curElement?.findChild(path[index] + EXTENSION)
} else {
curElement = curElement?.findChild(path[index])
curElement?.findChild(path[index])
}
}
return curElement
Expand Down
4 changes: 2 additions & 2 deletions src/main/kotlin/org/arend/refactoring/move/ArendMoveMembersDialog.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@ import com.intellij.util.Alarm
import org.arend.ArendFileTypeInstance
import org.arend.codeInsight.ArendCodeInsightUtils
import org.arend.ext.module.ModulePath
import org.arend.module.AllArendFilesAndPackagesScope
import org.arend.module.AllArendFilesScope
import org.arend.module.config.ArendModuleConfigService
import org.arend.naming.reference.Referable
import org.arend.naming.scope.EmptyScope
Expand Down Expand Up @@ -75,7 +75,7 @@ class ArendMoveMembersDialog(project: Project,
}

val containingFile = container.containingFile as? ArendFile
val globalScope = containingFile?.libraryConfig?.let { AllArendFilesAndPackagesScope(it) } ?: EmptyScope.INSTANCE
val globalScope = containingFile?.libraryConfig?.let { AllArendFilesScope(it) } ?: EmptyScope.INSTANCE

targetFileField = EditorTextField(PsiDocumentManager.getInstance(project).getDocument(ArendLongNameCodeFragment(project, fullName?.modulePath?.toString() ?: "", null, customScopeGetter = { globalScope })), project, ArendFileTypeInstance)
targetModuleField = EditorTextField(PsiDocumentManager.getInstance(project).getDocument(ArendLongNameCodeFragment(project, fullName?.longName?.toString() ?: "", null, customScopeGetter = {
Expand Down
22 changes: 0 additions & 22 deletions src/main/kotlin/org/arend/resolving/ArendReference.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,8 +10,6 @@ import org.arend.codeInsight.completion.ReplaceInsertHandler
import org.arend.core.definition.Definition
import org.arend.error.DummyErrorReporter
import org.arend.ext.module.ModulePath
import org.arend.module.AREND_LIB
import org.arend.module.AllArendFilesAndPackagesScope
import org.arend.naming.reference.*
import org.arend.naming.reference.Referable.RefKind
import org.arend.naming.reference.converter.ReferableConverter
Expand All @@ -26,7 +24,6 @@ import org.arend.psi.ext.*
import org.arend.psi.ext.ArendDefMeta
import org.arend.psi.ext.ReferableBase
import org.arend.refactoring.ArendNamesValidator
import org.arend.refactoring.move.ArendLongNameCodeFragment
import org.arend.term.abs.Abstract
import org.arend.term.abs.ConcreteBuilder
import org.arend.term.concrete.Concrete
Expand Down Expand Up @@ -136,25 +133,6 @@ abstract class ArendReferenceBase<T : ArendReferenceElement>(element: T, range:
when (module) {
null -> LookupElementBuilder.create(ref, ref.path.toString()).withIcon(ArendIcons.DIRECTORY)
is ArendFile -> LookupElementBuilder.create(module, ref.path.toString()).withIcon(ArendIcons.AREND_FILE)
is PsiDirectory -> {
val libraryConfig = ((containingFile as? ArendLongNameCodeFragment?)?.scope as? AllArendFilesAndPackagesScope?)?.libraryConfig
if (ref is PsiModuleReferable) {
if (ref.modulePath.size() == 0 || (ref.modulePath.size() == 1 && ref.modulePath.firstName == libraryConfig?.testsDirFile?.name)) {
if (libraryConfig?.sourcesDirFile == module.virtualFile ||
(libraryConfig?.testsDirFile == module.virtualFile && ref.modulePath.size() != 0)) {
LookupElementBuilder.create(module, module.name).withIcon(module.getIcon(0))
} else {
null
}
} else if (ref.toString() == AREND_LIB) {
LookupElementBuilder.create(module, ref.modulePath.toString()).withIcon(ArendIcons.AREND)
} else {
LookupElementBuilder.create(module, ref.modulePath.toString()).withIcon(ArendIcons.DIRECTORY)
}
} else {
LookupElementBuilder.create(ref, ref.path.toString()).withIcon(ArendIcons.DIRECTORY)
}
}
else -> LookupElementBuilder.createWithIcon(module)
}
}
Expand Down
1 change: 1 addition & 0 deletions src/main/kotlin/org/arend/typechecking/execution/TypeCheckCommand.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@ package org.arend.typechecking.execution

data class TypeCheckCommand(
val library: String = "",
val isTest: Boolean = false,
val modulePath: String = "",
val definitionFullName: String = ""
)
55 changes: 15 additions & 40 deletions src/main/kotlin/org/arend/typechecking/execution/TypeCheckProcessHandler.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -39,10 +39,8 @@ import org.arend.term.concrete.Concrete
import org.arend.typechecking.*
import org.arend.typechecking.error.ParserError
import org.arend.typechecking.error.TypecheckingErrorReporter
import org.arend.typechecking.execution.TypecheckRunConfigurationProducer.Companion.TEST_PREFIX
import org.arend.typechecking.order.Ordering
import org.arend.typechecking.order.listener.CollectingOrderingListener
import org.arend.util.FileUtils.EXTENSION
import org.arend.util.afterTypechecking
import org.jetbrains.ide.PooledThreadExecutor
import java.io.OutputStream
Expand Down Expand Up @@ -122,36 +120,22 @@ class TypeCheckProcessHandler(
}

val modulePaths = if (modulePath == null) library.loadedModules else listOf(modulePath)
val modules = modulePaths.flatMap {
var newModulePath = it
val isTest = (newModulePath.firstName == TEST_PREFIX && newModulePath.toList().getOrNull(1) != EXTENSION.drop(1)) ||
(newModulePath.size() == 1 && newModulePath.firstName == library.config.testsDirFile?.name)
val isSource = newModulePath.firstName == library.config.sourcesDirFile?.name
if (isTest || isSource) {
newModulePath = ModulePath(newModulePath.toList().subList(1, newModulePath.size()))
}
val items = when (val fileItem = library.config.getArendDirectoryOrFile(newModulePath, isTest)) {
is ArendFile -> listOf(fileItem)
is PsiDirectory -> getAllFilesInDirectory(fileItem)
else -> {
typecheckingErrorReporter.report(LibraryError.moduleNotFound(newModulePath, library.name))
emptyList()
}
}
for (module in items) {
if (command.definitionFullName == "") {
val sourcesModuleScopeProvider = typeCheckerService.libraryManager.getAvailableModuleScopeProvider(library)
val moduleScopeProvider = if (module.moduleLocation?.locationKind == ModuleLocation.LocationKind.TEST) {
val testsModuleScopeProvider = library.testsModuleScopeProvider
ModuleScopeProvider { modulePath ->
sourcesModuleScopeProvider.forModule(modulePath)
?: testsModuleScopeProvider.forModule(modulePath)
}
} else sourcesModuleScopeProvider
DefinitionResolveNameVisitor(concreteProvider, ArendReferableConverter, typecheckingErrorReporter).resolveGroup(module, ScopeFactory.forGroup(module, moduleScopeProvider))
}
val modules = modulePaths.mapNotNull {
val module = library.config.findArendFile(it, withAdditional = false, withTests = command.isTest)
if (module == null) {
typecheckingErrorReporter.report(LibraryError.moduleNotFound(it, library.name))
} else if (command.definitionFullName == "") {
val sourcesModuleScopeProvider = typeCheckerService.libraryManager.getAvailableModuleScopeProvider(library)
val moduleScopeProvider = if (module.moduleLocation?.locationKind == ModuleLocation.LocationKind.TEST) {
val testsModuleScopeProvider = library.testsModuleScopeProvider
ModuleScopeProvider { modulePath ->
sourcesModuleScopeProvider.forModule(modulePath)
?: testsModuleScopeProvider.forModule(modulePath)
}
} else sourcesModuleScopeProvider
DefinitionResolveNameVisitor(concreteProvider, ArendReferableConverter, typecheckingErrorReporter).resolveGroup(module, ScopeFactory.forGroup(module, moduleScopeProvider))
}
items
module
}

if (command.definitionFullName == "") {
Expand Down Expand Up @@ -220,15 +204,6 @@ class TypeCheckProcessHandler(
}
}

private fun getAllFilesInDirectory(directory: PsiDirectory): List<ArendFile> {
val arendFiles = mutableListOf<ArendFile>()
for (subDir in directory.subdirectories) {
arendFiles.addAll(getAllFilesInDirectory(subDir))
}
arendFiles.addAll(directory.files.filterIsInstance<ArendFile>())
return arendFiles
}

private fun resetGroup(group: ArendGroup) {
if (indicator.isCanceled) {
return
Expand Down
Loading
Loading