Skip to content

Commit

Permalink
Merge pull request #523 from alex999990009/alex99999/fixes
Browse files Browse the repository at this point in the history 
Fix Run Configurations problems
  • Loading branch information
@sxhya
sxhya authored Jun 28, 2024
2 parents f0ac6d4 + fbb3366 commit 8e2f609
Show file tree
Hide file tree
Showing 11 changed files with 77 additions and 178 deletions.
55 changes: 23 additions & 32 deletions ...d/module/AllArendFilesAndPackagesScope.kt → ...in/org/arend/module/AllArendFilesScope.kt
View file
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
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
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
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
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
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
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

0 comments on commit 8e2f609

Please sign in to comment.