diff --git a/src/main/kotlin/org/arend/actions/ArendActions.kt b/src/main/kotlin/org/arend/actions/ArendActions.kt index a153b723f..40b1fb2bf 100644 --- a/src/main/kotlin/org/arend/actions/ArendActions.kt +++ b/src/main/kotlin/org/arend/actions/ArendActions.kt @@ -3,7 +3,7 @@ package org.arend.actions import com.intellij.openapi.actionSystem.DefaultActionGroup import org.arend.ArendIcons.AREND -class ArendActions : DefaultActionGroup("Arend Actions", "Show Arend Actions", AREND) { +class ArendActions : DefaultActionGroup("Arend", "Show Arend Actions", AREND) { init { templatePresentation.isPopupGroup = true } diff --git a/src/main/kotlin/org/arend/actions/ArendGotoNextErrorAction.kt b/src/main/kotlin/org/arend/actions/ArendGotoNextErrorAction.kt index 8e866d928..034d11f37 100644 --- a/src/main/kotlin/org/arend/actions/ArendGotoNextErrorAction.kt +++ b/src/main/kotlin/org/arend/actions/ArendGotoNextErrorAction.kt @@ -45,34 +45,34 @@ fun selectErrorFromEditor(project: Project, editor: Editor, file: ArendFile?, al return } - var arendFile = file - if (arendFile == null) { - ApplicationManager.getApplication().run { - executeOnPooledThread { + ApplicationManager.getApplication().run { + executeOnPooledThread { + var arendFile = file + if (arendFile == null) { runReadAction { arendFile = PsiDocumentManager.getInstance(project).getPsiFile(document) as? ArendFile } - if (arendFile == null) { - return@executeOnPooledThread + } + if (arendFile == null) { + return@executeOnPooledThread + } + runInEdt { + val arendErrors = project.service().getErrors(arendFile!!) + if (arendErrors.isEmpty()) { + return@runInEdt } - runInEdt { - val arendErrors = project.service().getErrors(arendFile!!) - if (arendErrors.isEmpty()) { - return@runInEdt - } - val service = project.service() - for (arendError in arendErrors) { - if (always || arendError.error.satisfies(service.autoScrollFromSource)) { - val textRange = BasePass.getImprovedTextRange(arendError.error) ?: continue - if (textRange.containsOffset(offset)) { - val messagesService = project.service() - messagesService.view?.tree?.select(arendError.error) - if (activate) { - messagesService.activate(project, false) - } - break + val service = project.service() + for (arendError in arendErrors) { + if (always || arendError.error.satisfies(service.autoScrollFromSource)) { + val textRange = BasePass.getImprovedTextRange(arendError.error) ?: continue + if (textRange.containsOffset(offset)) { + val messagesService = project.service() + messagesService.view?.tree?.select(arendError.error) + if (activate) { + messagesService.activate(project, false) } + break } } } diff --git a/src/main/kotlin/org/arend/actions/SearchArendFilesContributor.kt b/src/main/kotlin/org/arend/actions/SearchArendFilesContributor.kt index 0ff01e515..276e78233 100644 --- a/src/main/kotlin/org/arend/actions/SearchArendFilesContributor.kt +++ b/src/main/kotlin/org/arend/actions/SearchArendFilesContributor.kt @@ -1,9 +1,6 @@ package org.arend.actions -import com.intellij.ide.actions.searcheverywhere.AbstractGotoSEContributor -import com.intellij.ide.actions.searcheverywhere.FileSearchEverywhereContributor -import com.intellij.ide.actions.searcheverywhere.SearchEverywhereContributor -import com.intellij.ide.actions.searcheverywhere.SearchEverywhereContributorFactory +import com.intellij.ide.actions.searcheverywhere.* import com.intellij.ide.util.gotoByName.FileTypeRef import com.intellij.ide.util.gotoByName.FilteringGotoByModel import com.intellij.ide.util.gotoByName.GotoFileModel @@ -44,6 +41,6 @@ class SearchArendFilesContributor(val event: AnActionEvent) : AbstractGotoSECont class ArendSECFactory : SearchEverywhereContributorFactory { override fun createContributor(initEvent: AnActionEvent): SearchEverywhereContributor { - return SearchArendFilesContributor(initEvent) + return PSIPresentationBgRendererWrapper(SearchArendFilesContributor(initEvent)) } } \ No newline at end of file diff --git a/src/main/kotlin/org/arend/graph/GraphSimulator.kt b/src/main/kotlin/org/arend/graph/GraphSimulator.kt index 356da339e..4576d0133 100644 --- a/src/main/kotlin/org/arend/graph/GraphSimulator.kt +++ b/src/main/kotlin/org/arend/graph/GraphSimulator.kt @@ -6,12 +6,19 @@ import com.intellij.openapi.project.Project import com.intellij.openapi.ui.DialogWrapper import com.intellij.openapi.ui.MessageType import com.intellij.openapi.updateSettings.impl.pluginsAdvertisement.notificationGroup +import com.intellij.ui.util.minimumHeight +import com.intellij.ui.util.minimumWidth import guru.nidi.graphviz.engine.Format import guru.nidi.graphviz.engine.Graphviz import guru.nidi.graphviz.model.Factory.graph import guru.nidi.graphviz.model.Factory.node import java.awt.Color +import java.awt.Image import java.awt.Toolkit +import java.awt.datatransfer.DataFlavor +import java.awt.datatransfer.Transferable +import java.awt.datatransfer.UnsupportedFlavorException +import java.awt.event.ActionEvent import java.awt.event.ComponentAdapter import java.awt.event.ComponentEvent import javax.swing.* @@ -40,18 +47,42 @@ class GraphSimulator( } val graphviz = Graphviz.fromGraph(graph) - val baseImageIcon = ImageIcon( - graphviz.render(Format.PNG).toImage() - ) + val image = graphviz.render(Format.PNG).toImage() + val imageIcon = ImageIcon(image) val screenSize = Toolkit.getDefaultToolkit().screenSize val screenWidth = screenSize.getWidth().toInt() val screenHeight = screenSize.getHeight().toInt() - var imageIcon = getImageIcon(baseImageIcon, graphviz, screenWidth, screenHeight) - var imageLabel = JLabel(imageIcon) + val baseImageIcon = if (imageIcon.iconWidth > screenWidth && imageIcon.iconHeight > screenHeight) { + ImageIcon(graphviz.width(screenWidth).height(screenHeight).render(Format.PNG).toImage()) + } else if (imageIcon.iconWidth > screenWidth) { + ImageIcon(graphviz.width(screenWidth).height(imageIcon.iconHeight).render(Format.PNG).toImage()) + } else if (imageIcon.iconWidth > screenWidth) { + ImageIcon(graphviz.width(imageIcon.iconWidth).height(screenHeight).render(Format.PNG).toImage()) + } else { + imageIcon + } + + var imageLabel = JLabel(baseImageIcon) val dialogWrapper = object : DialogWrapper(project, true) { + private var graphImage = image + private val copyImageAction = object : DialogWrapperAction("Copy Image") { + override fun doAction(e: ActionEvent?) { + val transferableImage = TransferableImage(graphImage) + Toolkit.getDefaultToolkit().systemClipboard.setContents(transferableImage, null) + buttonMap[this]?.isEnabled = false + } + } + + private val copyFullImageAction = object : DialogWrapperAction("Copy Full Image") { + override fun doAction(e: ActionEvent?) { + val transferableImage = TransferableImage(image) + Toolkit.getDefaultToolkit().systemClipboard.setContents(transferableImage, null) + } + } + init { init() } @@ -62,18 +93,46 @@ class GraphSimulator( panel.background = Color.WHITE panel.addComponentListener(object : ComponentAdapter() { override fun componentResized(e: ComponentEvent) { - imageIcon = getImageIcon(baseImageIcon, graphviz, e.component.width, e.component.height) + val component = panel.components.getOrNull(0) ?: return + panel.minimumWidth = baseImageIcon.iconWidth + size.width - e.component.width + panel.minimumHeight = baseImageIcon.iconHeight + size.height - e.component.height + + val imageIcon = getImageIcon(baseImageIcon, graphviz, e.component.width - component.bounds.x * 2, e.component.height - component.bounds.y * 2) imageLabel = JLabel(imageIcon) panel.removeAll() panel.add(imageLabel) panel.revalidate() + buttonMap[copyImageAction]?.isEnabled = true } }) return panel } - override fun createActions(): Array = emptyArray() + private fun getImageIcon(baseImageIcon: ImageIcon, graphviz: Graphviz, width: Int, height: Int): ImageIcon { + return when { + width <= baseImageIcon.iconWidth && height <= baseImageIcon.iconHeight -> { + graphImage = image + baseImageIcon + } + width <= baseImageIcon.iconWidth -> { + graphImage = graphviz.width(baseImageIcon.iconWidth).height(height).render(Format.PNG).toImage() + ImageIcon(graphImage) + } + height <= baseImageIcon.iconHeight -> { + graphImage =graphviz.width(width).height(baseImageIcon.iconHeight).render(Format.PNG).toImage() + ImageIcon(graphImage) + } + else -> { + graphImage = graphviz.width(width).height(height).render(Format.PNG).toImage() + ImageIcon(graphImage) + } + } + } + + override fun createActions(): Array { + return arrayOf(copyImageAction, copyFullImageAction) + } } dialogWrapper.pack() dialogWrapper.show() @@ -84,14 +143,22 @@ class GraphSimulator( } } - private fun getImageIcon(baseImageIcon: ImageIcon, graphviz: Graphviz, width: Int, height: Int): ImageIcon { - return when { - width <= baseImageIcon.iconWidth || height <= baseImageIcon.iconHeight -> { - ImageIcon( - graphviz.width(width).height(height).render(Format.PNG).toImage() - ) + companion object { + class TransferableImage(private val image: Image) : Transferable { + override fun getTransferDataFlavors(): Array { + return arrayOf(DataFlavor.imageFlavor) + } + + override fun isDataFlavorSupported(flavor: DataFlavor): Boolean { + return flavor.equals(DataFlavor.imageFlavor) + } + + override fun getTransferData(flavor: DataFlavor): Any { + if (flavor.equals(DataFlavor.imageFlavor)) { + return image + } + throw UnsupportedFlavorException(flavor) } - else -> baseImageIcon } } } diff --git a/src/main/kotlin/org/arend/hierarchy/clazz/ArendClassHierarchyBrowser.kt b/src/main/kotlin/org/arend/hierarchy/clazz/ArendClassHierarchyBrowser.kt index 256afd780..af5f92211 100644 --- a/src/main/kotlin/org/arend/hierarchy/clazz/ArendClassHierarchyBrowser.kt +++ b/src/main/kotlin/org/arend/hierarchy/clazz/ArendClassHierarchyBrowser.kt @@ -167,11 +167,11 @@ class ArendClassHierarchyBrowser(project: Project, method: PsiElement) : TypeHie } } - inner class ArendHierarchyGraphAction : AnAction(ArendIcons.ORTHOGONAL_GRAPH) { + inner class ArendHierarchyGraphAction : AnAction("Visualize as Orthogonal Diagram", "A hierarchical class graph", ArendIcons.ORTHOGONAL_GRAPH) { private val usedNodes = mutableSetOf() private val edges = mutableSetOf() - private fun findEdges(currentNode: DefaultMutableTreeNode) { + private fun findEdges(currentNode: DefaultMutableTreeNode, isSuperTypes: Boolean) { usedNodes.add(currentNode) val from = ((currentNode.userObject as ArendHierarchyNodeDescriptor).psiElement as ArendDefClass).fullName @@ -180,10 +180,14 @@ class ArendClassHierarchyBrowser(project: Project, method: PsiElement) : TypeHie for (child in children) { val to = (((child as DefaultMutableTreeNode).userObject as ArendHierarchyNodeDescriptor).psiElement as? ArendDefClass?)?.fullName ?: continue - edges.add(GraphEdge(from, to)) + if (isSuperTypes) { + edges.add(GraphEdge(to, from)) + } else { + edges.add(GraphEdge(from, to)) + } if (!usedNodes.contains(child)) { - findEdges(child) + findEdges(child, isSuperTypes) } } } @@ -195,7 +199,7 @@ class ArendClassHierarchyBrowser(project: Project, method: PsiElement) : TypeHie val tree = getJTree(currentViewType) ?: return val root = tree.model.root as DefaultMutableTreeNode - findEdges(root) + findEdges(root, myProject.service().data.hierarchyViewType == getSupertypesHierarchyType()) val simulator = GraphSimulator( e.project, diff --git a/src/main/kotlin/org/arend/highlight/RedundantParameterNamePass.kt b/src/main/kotlin/org/arend/highlight/RedundantParameterNamePass.kt deleted file mode 100644 index f89f61fcc..000000000 --- a/src/main/kotlin/org/arend/highlight/RedundantParameterNamePass.kt +++ /dev/null @@ -1,65 +0,0 @@ -package org.arend.highlight - -import com.intellij.codeInsight.daemon.impl.HighlightInfo -import com.intellij.codeInsight.daemon.impl.HighlightInfoProcessor -import com.intellij.codeInsight.daemon.impl.HighlightInfoType -import com.intellij.codeInspection.HintAction -import com.intellij.lang.annotation.HighlightSeverity -import com.intellij.openapi.editor.Editor -import com.intellij.openapi.progress.ProgressIndicator -import com.intellij.openapi.project.Project -import com.intellij.openapi.util.TextRange -import com.intellij.psi.PsiFile -import com.intellij.psi.util.descendantsOfType -import org.arend.psi.ArendFile -import org.arend.psi.ArendPsiFactory -import org.arend.psi.ext.ArendDefIdentifier -import org.arend.psi.ext.ArendNameTele -import org.arend.psi.ext.ArendRefIdentifier -import org.arend.util.ArendBundle - -class RedundantParameterNamePass(file: ArendFile, editor: Editor, highlightInfoProcessor: HighlightInfoProcessor): - BasePass(file, editor, "Arend redundant parameter name annotator", TextRange(0, editor.document.textLength), highlightInfoProcessor) { - - override fun collectInformationWithProgress(progress: ProgressIndicator) { - val identifiers = file.descendantsOfType().map { - it.identifierOrUnknownList - .filter { identifier -> identifier.defIdentifier != null } - .map { identifier -> identifier.defIdentifier!! } - }.flatten() - val arendRefIdentifiers = file.descendantsOfType().map { it.resolve }.toList() - - for (identifier in identifiers) { - if (!arendRefIdentifiers.contains(identifier)) { - val builder = HighlightInfo - .newHighlightInfo(HighlightInfoType.WARNING) - .range(identifier.textRange) - .severity(HighlightSeverity.WARNING) - .descriptionAndTooltip(ArendBundle.message("arend.inspection.parameter.redundant", identifier.name)) - registerFix(builder, RedundantParameterNameHintAction(identifier)) - addHighlightInfo(builder) - } - } - } - - companion object { - class RedundantParameterNameHintAction(private val defIdentifier: ArendDefIdentifier): HintAction { - - override fun startInWriteAction(): Boolean = true - - override fun getFamilyName(): String = text - - override fun getText(): String = ArendBundle.message("arend.inspection.redundant.parameter.message") - - override fun isAvailable(project: Project, editor: Editor?, file: PsiFile?): Boolean = true - - override fun invoke(project: Project, editor: Editor?, file: PsiFile?) { - val psiFactory = ArendPsiFactory(project) - val underlining = psiFactory.createUnderlining() - defIdentifier.replace(underlining) - } - - override fun showHint(editor: Editor): Boolean = true - } - } -} diff --git a/src/main/kotlin/org/arend/highlight/RedundantParameterNamePassFactory.kt b/src/main/kotlin/org/arend/highlight/RedundantParameterNamePassFactory.kt deleted file mode 100644 index 181509091..000000000 --- a/src/main/kotlin/org/arend/highlight/RedundantParameterNamePassFactory.kt +++ /dev/null @@ -1,27 +0,0 @@ -package org.arend.highlight - -import com.intellij.codeHighlighting.TextEditorHighlightingPass -import com.intellij.codeHighlighting.TextEditorHighlightingPassFactoryRegistrar -import com.intellij.codeHighlighting.TextEditorHighlightingPassRegistrar -import com.intellij.codeInsight.daemon.impl.DefaultHighlightInfoProcessor -import com.intellij.openapi.components.service -import com.intellij.openapi.editor.Editor -import com.intellij.openapi.project.Project -import com.intellij.openapi.util.TextRange -import org.arend.psi.ArendFile - -class RedundantParameterNamePassFactory: BasePassFactory(ArendFile::class.java), TextEditorHighlightingPassFactoryRegistrar { - private var myPassId = -1 - - override fun createPass(file: ArendFile, editor: Editor, textRange: TextRange): TextEditorHighlightingPass { - return RedundantParameterNamePass(file, editor, DefaultHighlightInfoProcessor()) - } - - override fun getPassId(): Int = myPassId - - override fun registerHighlightingPassFactory(registrar: TextEditorHighlightingPassRegistrar, project: Project) { - val service = project.service() - myPassId = registrar.registerTextEditorHighlightingPass(this, intArrayOf(service.highlightingPassId), null, false, -1) - service.typecheckerPassId = myPassId - } -} \ No newline at end of file diff --git a/src/main/kotlin/org/arend/inspection/RedundantParameterInspection.kt b/src/main/kotlin/org/arend/inspection/RedundantParameterInspection.kt new file mode 100644 index 000000000..50b83dd73 --- /dev/null +++ b/src/main/kotlin/org/arend/inspection/RedundantParameterInspection.kt @@ -0,0 +1,59 @@ +package org.arend.inspection + +import com.intellij.codeInspection.LocalQuickFixOnPsiElement +import com.intellij.codeInspection.ProblemsHolder +import com.intellij.openapi.project.Project +import com.intellij.psi.PsiElement +import com.intellij.psi.PsiElementVisitor +import com.intellij.psi.PsiFile +import com.intellij.psi.util.descendantsOfType +import org.arend.psi.ArendPsiFactory +import org.arend.psi.ext.ArendDefIdentifier +import org.arend.psi.ext.ArendNameTele +import org.arend.psi.ext.ArendRefIdentifier +import org.arend.util.ArendBundle + +class RedundantParameterInspection : ArendInspectionBase() { + + override fun buildArendVisitor(holder: ProblemsHolder, isOnTheFly: Boolean): PsiElementVisitor { + fun registerFix(element: ArendDefIdentifier) { + val message = ArendBundle.message("arend.inspection.parameter.redundant", element.name) + holder.registerProblem(element, message, RedundantParameterFix(element)) + } + + val file = holder.file + val arendRefIdentifiers = file.descendantsOfType().map { it.resolve }.toList() + + return object : PsiElementVisitor() { + override fun visitElement(element: PsiElement) { + super.visitElement(element) + if (element is ArendNameTele) { + val identifiers = element.identifierOrUnknownList + .filter { identifier -> identifier.defIdentifier != null } + .map { identifier -> identifier.defIdentifier!! } + + for (identifier in identifiers) { + if (!arendRefIdentifiers.contains(identifier)) { + registerFix(identifier) + } + } + } + } + } + } + + companion object { + class RedundantParameterFix(private val defIdentifier: ArendDefIdentifier): LocalQuickFixOnPsiElement(defIdentifier) { + + override fun getFamilyName(): String = text + + override fun getText(): String = ArendBundle.message("arend.inspection.redundant.parameter.fix") + + override fun invoke(project: Project, file: PsiFile, startElement: PsiElement, endElement: PsiElement) { + val psiFactory = ArendPsiFactory(project) + val underlining = psiFactory.createUnderlining() + defIdentifier.replace(underlining) + } + } + } +} diff --git a/src/main/kotlin/org/arend/module/AllArendFilesAndPackagesScope.kt b/src/main/kotlin/org/arend/module/AllArendFilesAndPackagesScope.kt new file mode 100644 index 000000000..68a7c14d1 --- /dev/null +++ b/src/main/kotlin/org/arend/module/AllArendFilesAndPackagesScope.kt @@ -0,0 +1,91 @@ +package org.arend.module + +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 +import org.arend.naming.reference.Referable +import org.arend.naming.scope.Scope +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, + private val extraPath: ModulePath = ModulePath(), + private val withPrelude: Boolean = true, + private val withArendExtension: Boolean = true +) : Scope { + override fun getElements(): Collection { + val result = ArrayList() + + 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) } + } else { + val dir = LibraryConfig.findArendFileOrDirectoryByModulePath(srcDir, extraPath) + dir?.let { addArendFiles(it, it, result) } + } + + if (withPrelude) { + val psiManager = PsiManager.getInstance(libraryConfig.project) + libraryConfig.project.service().prelude?.let { psiManager.findFile(it.virtualFile) }?.let { + result.add(PsiModuleReferable(listOf(it), Prelude.MODULE_PATH)) + } + } + return result + } + + private fun addArendFiles(root: VirtualFile, startFile: VirtualFile, result: MutableList) { + val psiManager = PsiManager.getInstance(libraryConfig.project) + val virtualFileVisitor = object : VirtualFileVisitor() { + 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)) + } + 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())) { + override fun textRepresentation(): String { + val fullName = listPath?.joinToString(".") ?: "" + return fullName + } + } + } + + override fun getElements(kind: Referable.RefKind?): Collection = 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) +} diff --git a/src/main/kotlin/org/arend/module/AllArendFilesScope.kt b/src/main/kotlin/org/arend/module/AllArendFilesScope.kt deleted file mode 100644 index a7efa05a6..000000000 --- a/src/main/kotlin/org/arend/module/AllArendFilesScope.kt +++ /dev/null @@ -1,69 +0,0 @@ -package org.arend.module - -import com.intellij.openapi.components.service -import com.intellij.openapi.vfs.LocalFileSystem -import com.intellij.openapi.vfs.VfsUtilCore -import com.intellij.openapi.vfs.VirtualFile -import com.intellij.openapi.vfs.VirtualFileVisitor -import com.intellij.psi.PsiManager -import org.arend.module.config.LibraryConfig -import org.arend.naming.reference.Referable -import org.arend.naming.scope.Scope -import org.arend.prelude.Prelude -import org.arend.psi.ArendFile -import org.arend.psi.ext.PsiModuleReferable -import org.arend.typechecking.TypeCheckingService -import java.io.File - -class AllArendFilesScope(private val libraryConfig: LibraryConfig, private val extraPath: String? = null, private val withPrelude: Boolean = true) : Scope { - override fun getElements(): Collection { - val result = ArrayList() - - val srcDir = getDirFile(libraryConfig.sourcesDir) - srcDir?.let { addArendFiles(it, extraPath, result) } - - val testDir = getDirFile(libraryConfig.testsDir) - testDir?.let { addArendFiles(it, extraPath, result) } - - if (withPrelude) { - val psiManager = PsiManager.getInstance(libraryConfig.project) - libraryConfig.project.service().prelude?.let { psiManager.findFile(it.virtualFile) }?.let { - result.add(PsiModuleReferable(listOf(it), Prelude.MODULE_PATH)) - } - } - - return result - } - - private fun getDirFile(dir: String): VirtualFile? { - return LocalFileSystem.getInstance().refreshAndFindFileByIoFile( - File((libraryConfig.root?.path ?: "") + File.separator + dir + (extraPath ?: "")) - ) - } - - private fun addArendFiles(virtualDir: VirtualFile, extraPath: String?, result: MutableList) { - val psiManager = PsiManager.getInstance(libraryConfig.project) - val virtualFileVisitor = object : VirtualFileVisitor() { - override fun visitFile(file: VirtualFile): Boolean { - val psiFile = psiManager.findFile(file) - if (psiFile is ArendFile) { - result.add(object : Referable { - override fun textRepresentation(): String { - return psiFile.fullName.removePrefix("${extraPath?.replace(File.separator, ".")?.removePrefix(".")}.") - } - - override fun getUnderlyingReferable(): Referable { - return psiFile - } - }) - } - return true - } - } - VfsUtilCore.visitChildrenRecursively(virtualDir, virtualFileVisitor) - } - - override fun getElements(kind: Referable.RefKind?): Collection = if (kind == null || kind == Referable.RefKind.EXPR) elements else emptyList() - - override fun resolveNamespace(name: String, onlyInternal: Boolean) = AllArendFilesScope(libraryConfig, extraPath?.let { "$it${File.separator}$name" } ?: "${File.separator}$name") -} diff --git a/src/main/kotlin/org/arend/module/ModuleScope.kt b/src/main/kotlin/org/arend/module/ModuleScope.kt index 7bdb9fd34..027553235 100644 --- a/src/main/kotlin/org/arend/module/ModuleScope.kt +++ b/src/main/kotlin/org/arend/module/ModuleScope.kt @@ -17,13 +17,22 @@ import org.arend.typechecking.TypeCheckingService import org.arend.util.FileUtils -class ModuleScope private constructor(private val libraryConfig: LibraryConfig?, private val inTests: Boolean, private val rootDirs: List?, private val prefix: List, private val additionalPaths: List>) : Scope { - constructor(libraryConfig: LibraryConfig, inTests: Boolean) : this(libraryConfig, inTests, null, emptyList(), ArrayList>().also { result -> - libraryConfig.forAvailableConfigs { config -> - config.additionalModulesSet.mapTo(result) { it.toList() } - null - } - }) +class ModuleScope private constructor( + private val libraryConfig: LibraryConfig?, + private val inTests: Boolean, + private val rootDirs: List?, + private val additionalPaths: List> +) : Scope { + constructor(libraryConfig: LibraryConfig, inTests: Boolean) : this( + libraryConfig, + inTests, + null, + ArrayList>().also { result -> + libraryConfig.forAvailableConfigs { config -> + config.additionalModulesSet.mapTo(result) { it.toList() } + null + } + }) private fun calculateRootDirs() = rootDirs ?: libraryConfig!!.availableConfigs.flatMap { conf -> (conf.sourcesDirFile?.let { listOf(it) } ?: emptyList()) + if (inTests) conf.testsDirFile?.let { listOf(it) } ?: emptyList() else emptyList() @@ -40,19 +49,19 @@ class ModuleScope private constructor(private val libraryConfig: LibraryConfig?, if (FileUtils.isModuleName(name)) { val dir = psiManager.findDirectory(file) if (dir != null) { - result.add(PsiModuleReferable(listOf(dir), ModulePath(prefix + name))) + result.add(PsiModuleReferable(listOf(dir), ModulePath(name))) } } } else if (name.endsWith(FileUtils.EXTENSION)) { (psiManager.findFile(file) as? ArendFile)?.let { - result.add(PsiModuleReferable(listOf(it), ModulePath(prefix + name.substring(0, name.length - FileUtils.EXTENSION.length)))) + result.add(PsiModuleReferable(listOf(it), ModulePath(name.substring(0, name.length - FileUtils.EXTENSION.length)))) } } } } } for (path in additionalPaths) { - result.add(ModuleReferable(ModulePath(prefix + path[0]))) + result.add(ModuleReferable(ModulePath(path[0]))) } if (rootDirs == null) { val psiManager = libraryConfig?.project?.let { PsiManager.getInstance(it) } @@ -75,6 +84,6 @@ class ModuleScope private constructor(private val libraryConfig: LibraryConfig?, return@mapNotNull null } val newPaths = additionalPaths.mapNotNull { if (it.size > 1 && it[0] == name) it.drop(1) else null } - return if (newRootDirs.isEmpty() && newPaths.isEmpty()) EmptyScope.INSTANCE else ModuleScope(if (newRootDirs.isEmpty()) null else libraryConfig, inTests, newRootDirs, prefix + name, newPaths) + return if (newRootDirs.isEmpty() && newPaths.isEmpty()) EmptyScope.INSTANCE else ModuleScope(if (newRootDirs.isEmpty()) null else libraryConfig, inTests, newRootDirs, newPaths) } } \ No newline at end of file diff --git a/src/main/kotlin/org/arend/module/config/LibraryConfig.kt b/src/main/kotlin/org/arend/module/config/LibraryConfig.kt index fd8acc916..a87bb0648 100644 --- a/src/main/kotlin/org/arend/module/config/LibraryConfig.kt +++ b/src/main/kotlin/org/arend/module/config/LibraryConfig.kt @@ -14,12 +14,14 @@ import org.arend.module.ArendRawLibrary import org.arend.module.IntellijClassLoaderDelegate import org.arend.module.ModuleLocation import org.arend.naming.reference.Referable +import org.arend.prelude.Prelude.MODULE_PATH import org.arend.psi.ArendFile import org.arend.psi.ext.PsiLocatedReferable import org.arend.util.getRelativeFile import org.arend.util.getRelativePath import org.arend.typechecking.TypeCheckingService import org.arend.util.FileUtils +import org.arend.util.FileUtils.EXTENSION import org.arend.util.Range import org.arend.util.Version import org.arend.util.mapFirstNotNull @@ -143,7 +145,7 @@ abstract class LibraryConfig(val project: Project) { } fun findArendFile(modulePath: ModulePath, inTests: Boolean): ArendFile? = - findParentDirectory(modulePath, inTests)?.findChild(modulePath.lastName + FileUtils.EXTENSION)?.let { + findParentDirectory(modulePath, inTests)?.findChild(modulePath.lastName + EXTENSION)?.let { PsiManager.getInstance(project).findFile(it) as? ArendFile } @@ -155,6 +157,37 @@ 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().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) @@ -168,7 +201,7 @@ abstract class LibraryConfig(val project: Project) { val psiManager = PsiManager.getInstance(project) val srcDir = findParentDirectory(modulePath, false) - srcDir?.findChild(modulePath.lastName + FileUtils.EXTENSION)?.let { + findArendFileOrDirectoryByModulePath(srcDir, modulePath)?.let { val file = psiManager.findFile(it) if (file is ArendFile) { return file @@ -176,14 +209,15 @@ abstract class LibraryConfig(val project: Project) { } val testDir = if (withTests) findParentDirectory(modulePath, true) else null - testDir?.findChild(modulePath.lastName + FileUtils.EXTENSION)?.let { + findArendFileOrDirectoryByModulePath(testDir, modulePath)?.let { val file = psiManager.findFile(it) if (file is ArendFile) { return file } } - return (srcDir?.findChild(modulePath.lastName) ?: testDir?.findChild(modulePath.lastName))?.let { + return (findArendFileOrDirectoryByModulePath(sourcesDirFile, modulePath) ?: + findArendFileOrDirectoryByModulePath(testsDirFile, modulePath))?.let { psiManager.findDirectory(it) } } @@ -235,4 +269,22 @@ abstract class LibraryConfig(val project: Project) { val libraryManager = project.service().libraryManager return deps.mapFirstNotNull { dep -> (libraryManager.getRegisteredLibrary(dep.name) as? ArendRawLibrary)?.config?.let { f(it) } } } -} \ No newline at end of file + + companion object { + fun findArendFileOrDirectoryByModulePath(root: VirtualFile?, modulePath: ModulePath): VirtualFile? { + 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) + } else { + curElement = curElement?.findChild(path[index]) + } + } + return curElement + } + } +} diff --git a/src/main/kotlin/org/arend/module/editor/ArendModuleConfigurationView.kt b/src/main/kotlin/org/arend/module/editor/ArendModuleConfigurationView.kt index 8372499b8..64e140cb7 100644 --- a/src/main/kotlin/org/arend/module/editor/ArendModuleConfigurationView.kt +++ b/src/main/kotlin/org/arend/module/editor/ArendModuleConfigurationView.kt @@ -209,7 +209,7 @@ class ArendModuleConfigurationView( fun createComponent() = panel { row("Current graph of Arend modules: ") { - actionButton(object : AnAction("Show Current Graph of Arend Modules", "A Graph of Arend Modules", ArendIcons.ORTHOGONAL_GRAPH) { + actionButton(object : AnAction("Show Current Graph of Arend Modules", "A graph of Arend modules", ArendIcons.ORTHOGONAL_GRAPH) { private val usedNodes = mutableSetOf() private val edges = mutableSetOf() diff --git a/src/main/kotlin/org/arend/psi/ArendFile.kt b/src/main/kotlin/org/arend/psi/ArendFile.kt index 698aeccf5..aed31ad6a 100644 --- a/src/main/kotlin/org/arend/psi/ArendFile.kt +++ b/src/main/kotlin/org/arend/psi/ArendFile.kt @@ -80,7 +80,7 @@ class ArendFile(viewProvider: FileViewProvider) : PsiFileBase(viewProvider, Aren val libraryName: String? get() = arendLibrary?.name ?: if (name == ArendPreludeLibrary.PRELUDE_FILE_NAME) Prelude.LIBRARY_NAME else null - val concreteDefinitions = HashMap() + val concreteDefinitions = ConcurrentHashMap() fun getTCRefMap(refKind: RefKind): ConcurrentHashMap { val location = moduleLocation ?: return ConcurrentHashMap() diff --git a/src/main/kotlin/org/arend/psi/ext/PsiReferable.kt b/src/main/kotlin/org/arend/psi/ext/PsiReferable.kt index 2c7d7041a..1c82da894 100644 --- a/src/main/kotlin/org/arend/psi/ext/PsiReferable.kt +++ b/src/main/kotlin/org/arend/psi/ext/PsiReferable.kt @@ -53,7 +53,7 @@ val Abstract.ParametersHolder.parametersText: String? return stringBuilder.toString() } -class PsiModuleReferable(val modules: List, modulePath: ModulePath) : ModuleReferable(modulePath) +open class PsiModuleReferable(val modules: List, val modulePath: ModulePath) : ModuleReferable(modulePath) abstract class PsiReferableImpl(node: ASTNode) : ArendCompositeElementImpl(node), PsiReferable { diff --git a/src/main/kotlin/org/arend/refactoring/ArendReferenceNameCalculatorUtils.kt b/src/main/kotlin/org/arend/refactoring/ArendReferenceNameCalculatorUtils.kt index 7ffdc950b..2ee5b8d1c 100644 --- a/src/main/kotlin/org/arend/refactoring/ArendReferenceNameCalculatorUtils.kt +++ b/src/main/kotlin/org/arend/refactoring/ArendReferenceNameCalculatorUtils.kt @@ -26,18 +26,22 @@ fun doCalculateReferenceName(defaultLocation: LocationData, deferredImports: List? = null): Pair> { val targetFile = defaultLocation.myContainingFile val targetModulePath = defaultLocation.myContainingFile.moduleLocation!! //safe to write - val alternativeLocation = when (defaultLocation.target) { - is ArendClassField, is ArendConstructor -> LocationData.createLocationData(defaultLocation.target, true) - else -> null - } - val aliasLocation = if (defaultLocation.target.hasAlias()) LocationData.createLocationData(defaultLocation.target, alias = true) else null + val locations: MutableList = ArrayList() - alternativeLocation?.let { locations.add(it) } - aliasLocation?.let { locations.add(it) } + locations.add(defaultLocation) + when (defaultLocation.target) { + is ArendClassField, is ArendConstructor -> LocationData.createLocationData(defaultLocation.target, true)?.let { locations.add(it) } + } + + if (defaultLocation.target.hasAlias()) { + LocationData.createLocationData(defaultLocation.target, alias = true)?.let { locations.add(it) } + when (defaultLocation.target) { + is ArendClassField, is ArendConstructor -> LocationData.createLocationData(defaultLocation.target, true, alias = true)?.let { locations.add(it) } + } + } - var modifyingImportsNeeded = false - var fallbackImportAction: NsCmdRefactoringAction? = null + var fallbackImportAction: NsCmdRefactoringAction? val fileGroup = object : Group by currentFile { override fun getStatements() = currentFile.statements.filter { it.group == null } @@ -70,35 +74,23 @@ fun doCalculateReferenceName(defaultLocation: LocationData, } } - if (isPrelude(targetFile) && !preludeImportedManually) { - defaultLocation.addLongNameAsReferenceName() // items from prelude are visible in any context - alternativeLocation?.addLongNameAsReferenceName() - fallbackImportAction = ImportFileAction(currentFile, targetFile, null) // however if long name is to be used "\import Prelude" will be added to imports - } - - if (locations.first().getReferenceNames().isEmpty() || protectedAccessModifier) { // target definition is inaccessible in current context - modifyingImportsNeeded = true - - defaultLocation.addLongNameAsReferenceName() - aliasLocation?.addLongNameAsReferenceName() - if (alternativeLocation != null) { - val alternativeFullName = alternativeLocation.getLongName() - if (importedScope.resolveName(alternativeFullName[0]) == null) alternativeLocation.addLongNameAsReferenceName() - } - - if (targetFileAlreadyImported) { // target definition is hidden or not included into using list but targetFile already has been imported - for (location in locations) if (location.getLongName().isNotEmpty()) + if (targetFileAlreadyImported) { // target definition is hidden or not included into using list but targetFile already has been imported + for (location in locations) + if ((location.getReferenceNames().isEmpty() || protectedAccessModifier) && location.getLongName().isNotEmpty()) { + location.addLongNameAsReferenceName() fileResolveActions[location] = AddIdToUsingAction(currentFile, targetFile, location) + } - fallbackImportAction = null - } else { // targetFile has not been imported - fallbackImportAction = ImportFileAction(currentFile, targetFile, if (minimalImportMode) emptyList() else null) + fallbackImportAction = null + } else { // targetFile has not been imported + fallbackImportAction = ImportFileAction(currentFile, targetFile, if (minimalImportMode) emptyList() else null) + if (isPrelude(targetFile) && !preludeImportedManually) fallbackImportAction = null - for (location in locations) { - val fName = location.getLongName() - val importList = if (fName.isEmpty()) emptyList() else singletonList(fName[0]) - fileResolveActions[location] = if (minimalImportMode) ImportFileAction(currentFile, targetFile, importList) else fallbackImportAction - } + for (location in locations) { + val fName = location.getLongName() + val importList = if (fName.isEmpty()) emptyList() else singletonList(fName[0]) + location.addLongNameAsReferenceName() + fileResolveActions[location] = if (minimalImportMode) ImportFileAction(currentFile, targetFile, importList) else fallbackImportAction } } @@ -121,6 +113,12 @@ fun doCalculateReferenceName(defaultLocation: LocationData, if (statements != null) ancestorGroups.add(0, Pair(containingGroup, statements.filter { it.kind == NamespaceCommand.Kind.OPEN })) + if (psi is ArendDefClass) { + val scope = ClassFieldImplScope(psi, true) + for (location in locations) + location.checkShortNameInScope(scope) + } + psi = psi.parent } @@ -139,7 +137,7 @@ fun doCalculateReferenceName(defaultLocation: LocationData, val scopes = singletonList(correctedScope) + deferredImports.map { it.getAmendedScope() } correctedScope = MergeScope(scopes) } - if (modifyingImportsNeeded && defaultLocation.getLongName().isNotEmpty()) + if (defaultLocation.getLongName().isNotEmpty()) correctedScope = MergeScope(correctedScope, defaultLocation.getComplementScope()) // calculate the scope imitating current scope after the imports have been fixed @@ -157,7 +155,9 @@ fun doCalculateReferenceName(defaultLocation: LocationData, for (location in locations) { location.getReferenceNames().map { referenceName -> - if (referenceName.isEmpty() || Scope.resolveName(correctedScope, referenceName)?.underlyingReferable == defaultLocation.target) { + if (referenceName.isEmpty() || + Scope.resolveName(correctedScope, referenceName)?.underlyingReferable + == defaultLocation.target) { resultingDecisions.add(ImportDecision(referenceName, fileResolveActions[location], location.alias)) } } @@ -165,6 +165,8 @@ fun doCalculateReferenceName(defaultLocation: LocationData, val veryLongName = ArrayList() if (resultingDecisions.isEmpty()) { + if (isPrelude(targetFile) && !preludeImportedManually && fallbackImportAction == null) + fallbackImportAction = ImportFileAction(currentFile, targetFile, null) veryLongName.addAll(targetModulePath.modulePath.toList()) // If we cannot resolve anything -- then perhaps there is some obstruction in scopes veryLongName.addAll(defaultLocation.getLongName()) // Let us use the "longest possible name" when referring to the anchor resultingDecisions.add(ImportDecision(veryLongName, fallbackImportAction, false)) @@ -236,6 +238,14 @@ class LocationData private constructor ( calculateRemainder(group)?.let { myReferenceNames.add(it) } } + fun checkShortNameInScope(scope: Scope) { + val elements = scope.elements.toList() + for (element in elements) { + val remainder = if (element is PsiLocatedReferable) calculateRemainder(element, withFirstName = true) else null + if (remainder != null) myReferenceNames.add(remainder) + } + } + fun addLongNameAsReferenceName() { myReferenceNames.add(getLongName()) } @@ -258,11 +268,12 @@ class LocationData private constructor ( return emptyList() } - private fun calculateRemainder(referable: PsiLocatedReferable): List? { + private fun calculateRemainder(referable: PsiLocatedReferable, withFirstName: Boolean = false): List? { var result: ArrayList? = if (referable == myContainingFile) ArrayList() else null for (entry in myLongNameWithRefs) { - result?.add(entry.first) + if (!withFirstName) result?.add(entry.first) if (entry.second == referable) result = ArrayList() + if (withFirstName) result?.add(entry.first) } return result } @@ -309,7 +320,7 @@ abstract class NsCmdRefactoringAction(val currentFile: ArendFile) { } class ImportFileAction(currentFile: ArendFile, - val targetFile: ArendFile, + private val targetFile: ArendFile, private val usingList: List?) : NsCmdRefactoringAction(currentFile) { override fun toString() = "Import file ${getLongName()}" @@ -333,8 +344,8 @@ class ImportFileAction(currentFile: ArendFile, } class AddIdToUsingAction(currentFile: ArendFile, - val targetFile: ArendFile, - val locationData: LocationData) : NsCmdRefactoringAction(currentFile) { + private val targetFile: ArendFile, + private val locationData: LocationData) : NsCmdRefactoringAction(currentFile) { private val myId = locationData.getLongName()[0] override fun toString(): String = "Add $myId to the \"using\" list of the namespace command `${getLongName()}`" diff --git a/src/main/kotlin/org/arend/refactoring/changeSignature/ArendChangeSignatureProcessor.kt b/src/main/kotlin/org/arend/refactoring/changeSignature/ArendChangeSignatureProcessor.kt index c89a1ccad..a4936c929 100644 --- a/src/main/kotlin/org/arend/refactoring/changeSignature/ArendChangeSignatureProcessor.kt +++ b/src/main/kotlin/org/arend/refactoring/changeSignature/ArendChangeSignatureProcessor.kt @@ -96,7 +96,7 @@ class ArendChangeSignatureProcessor(project: Project, fileChangeMap: MutableMap>>, rootPsiWithArendErrors: MutableSet, rootPsiWithErrors: MutableSet, - changeInfoNsCmds: MutableList, + changeInfoNsCmds: List, deferredNsCmds: MutableList): Runnable = Runnable { val concreteSet = LinkedHashSet() @@ -107,6 +107,10 @@ class ArendChangeSignatureProcessor(project: Project, .toCollection(LinkedHashSet()) val referableData = usages.map { it.task }.toCollection(HashSet()).toList() + for (action in changeInfoNsCmds) + if (!deferredNsCmds.contains(action)) + deferredNsCmds.add(action) + runReadAction { val progressIndicator = ProgressManager.getInstance().progressIndicator @@ -152,7 +156,7 @@ class ArendChangeSignatureProcessor(project: Project, for ((index, callEntry) in concreteSet.withIndex()) { progressIndicator.fraction = index.toDouble() / concreteSet.size progressIndicator.checkCanceled() - val refactoringContext = ChangeSignatureRefactoringContext(referableData, textReplacements, rangeData, changeInfoNsCmds) + val refactoringContext = ChangeSignatureRefactoringContext(referableData, textReplacements, rangeData, deferredNsCmds) rangeData.clear() try { @@ -211,8 +215,7 @@ class ArendChangeSignatureProcessor(project: Project, rootPsiWithErrors.add(callEntry.psi) } - deferredNsCmds.clear() - deferredNsCmds.addAll(refactoringContext.deferredNsCmds) + for (action in refactoringContext.deferredNsCmds) if (!deferredNsCmds.contains(action)) deferredNsCmds.add(action) } for ((psi, text) in textReplacements) { diff --git a/src/main/kotlin/org/arend/refactoring/move/ArendMoveMembersDialog.kt b/src/main/kotlin/org/arend/refactoring/move/ArendMoveMembersDialog.kt index 75eb2d206..8e9592609 100644 --- a/src/main/kotlin/org/arend/refactoring/move/ArendMoveMembersDialog.kt +++ b/src/main/kotlin/org/arend/refactoring/move/ArendMoveMembersDialog.kt @@ -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.AllArendFilesScope +import org.arend.module.AllArendFilesAndPackagesScope import org.arend.module.config.ArendModuleConfigService import org.arend.naming.reference.Referable import org.arend.naming.scope.EmptyScope @@ -75,7 +75,7 @@ class ArendMoveMembersDialog(project: Project, } val containingFile = container.containingFile as? ArendFile - val globalScope = containingFile?.libraryConfig?.let { AllArendFilesScope(it) } ?: EmptyScope.INSTANCE + val globalScope = containingFile?.libraryConfig?.let { AllArendFilesAndPackagesScope(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 = { diff --git a/src/main/kotlin/org/arend/refactoring/move/ArendMoveRefactoringProcessor.kt b/src/main/kotlin/org/arend/refactoring/move/ArendMoveRefactoringProcessor.kt index 9efbe8dcf..4f8c7ee1d 100644 --- a/src/main/kotlin/org/arend/refactoring/move/ArendMoveRefactoringProcessor.kt +++ b/src/main/kotlin/org/arend/refactoring/move/ArendMoveRefactoringProcessor.kt @@ -163,12 +163,16 @@ class ArendMoveRefactoringProcessor(project: Project, val (descriptors, changeSignatureUsages) = getUsagesToPreprocess(myMembers, insertIntoDynamicPart, myTargetContainer, thisVarNameMap) val fileChangeMap = LinkedHashMap>>() + val deferredNsCmds = ArrayList() val usagesPreprocessor = getUsagesPreprocessor(changeSignatureUsages, myProject, fileChangeMap, - HashSet(), HashSet(), ArrayList(), ArrayList()) //TODO: properly initialize these parameters + HashSet(), HashSet(), ArrayList(), deferredNsCmds) //TODO: properly initialize these parameters + usagesPreprocessor.run() writeFileChangeMap(myProject, fileChangeMap) + for (nsCmd in deferredNsCmds) nsCmd.execute() + for (descriptor in descriptors) descriptor.fixEliminator() diff --git a/src/main/kotlin/org/arend/resolving/ArendReference.kt b/src/main/kotlin/org/arend/resolving/ArendReference.kt index 67124dc35..92bf92799 100644 --- a/src/main/kotlin/org/arend/resolving/ArendReference.kt +++ b/src/main/kotlin/org/arend/resolving/ArendReference.kt @@ -10,6 +10,8 @@ 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 @@ -24,6 +26,7 @@ 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 @@ -127,8 +130,27 @@ abstract class ArendReferenceBase(element: T, range: (containingFile as? ArendFile)?.arendLibrary?.config?.forAvailableConfigs { it.findArendFileOrDirectory(ref.path, withAdditional = true, withTests = true) } } when (module) { - null -> LookupElementBuilder.create(ref, ref.path.lastName).withIcon(ArendIcons.DIRECTORY) - is ArendFile -> LookupElementBuilder.create(module, ref.path.lastName).withIcon(ArendIcons.AREND_FILE) + 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) } } diff --git a/src/main/kotlin/org/arend/search/proof/ArendProofSearchRenderer.kt b/src/main/kotlin/org/arend/search/proof/ArendProofSearchRenderer.kt index fb76da1e5..d6426e3f8 100644 --- a/src/main/kotlin/org/arend/search/proof/ArendProofSearchRenderer.kt +++ b/src/main/kotlin/org/arend/search/proof/ArendProofSearchRenderer.kt @@ -2,6 +2,7 @@ package org.arend.search.proof import com.intellij.ide.actions.SearchEverywherePsiRenderer import com.intellij.openapi.Disposable +import com.intellij.openapi.application.runReadAction import com.intellij.openapi.editor.Editor import com.intellij.openapi.editor.EditorFactory import com.intellij.openapi.editor.colors.EditorColors @@ -78,57 +79,59 @@ class ArendProofSearchRenderer(val project: Project) : ListCellRenderer { - val (def, renderingInfo) = value.entry - val (parameterRenders, codomainRender) = renderingInfo - val identifierRange: TextRange - val parameterRanges: List - val typeRange: TextRange - val locationRange: TextRange - val text = buildString { - append("${def.name} : ") - identifierRange = TextRange(0, length - 3) - val ranges = mutableListOf() - for (parameterIndex in parameterRenders.indices) { - append("(") + return runReadAction { + val bgColor = if (isSelected) selectionBgColor else UIUtil.getListBackground() + val fgColor = if (isSelected) selectionFgColor else list.foreground + when (value) { + is DefElement -> { + val (def, renderingInfo) = value.entry + val (parameterRenders, codomainRender) = renderingInfo + val identifierRange: TextRange + val parameterRanges: List + val typeRange: TextRange + val locationRange: TextRange + val text = buildString { + append("${def.name} : ") + identifierRange = TextRange(0, length - 3) + val ranges = mutableListOf() + for (parameterIndex in parameterRenders.indices) { + append("(") + val start = length + append(parameterRenders[parameterIndex].typeRep) + ranges.add(TextRange(start, length)) + append(")") + append(" -> ") + } + parameterRanges = ranges val start = length - append(parameterRenders[parameterIndex].typeRep) - ranges.add(TextRange(start, length)) - append(")") - append(" -> ") + append(codomainRender.typeRep) + typeRange = TextRange(start, length) + val location = getCompleteModuleLocation(def) + locationRange = if (location != null) { + append(" of $location") + TextRange(typeRange.endOffset, length) + } else { + TextRange(0, 0) + } } - parameterRanges = ranges - val start = length - append(codomainRender.typeRep) - typeRange = TextRange(start, length) - val location = getCompleteModuleLocation(def) - locationRange = if (location != null) { - append(" of $location") - TextRange(typeRange.endOffset, length) - } else { - TextRange(0, 0) + if (editor.document.text != text) { + editor.document.deleteString(0, editor.document.textLength - 1) + editor.document.insertString(0, text) } + editor.backgroundColor = bgColor + + setupHighlighting(isSelected, fgColor, text, identifierRange, parameterRanges, parameterRenders, typeRange, codomainRender, locationRange) + editor.component } - if (editor.document.text != text) { - editor.document.deleteString(0, editor.document.textLength - 1) - editor.document.insertString(0, text) + is MoreElement -> { + textArea.background = bgColor + textArea.foreground = fgColor + panel.font = UIUtil.getLabelFont().deriveFont(UIUtil.getFontSize(UIUtil.FontSize.SMALL)) + textArea.text = buildMoreHTML(fgColor) + panel.border = null + label.icon = null + panel } - editor.backgroundColor = bgColor - - setupHighlighting(isSelected, fgColor, text, identifierRange, parameterRanges, parameterRenders, typeRange, codomainRender, locationRange) - editor.component - } - is MoreElement -> { - textArea.background = bgColor - textArea.foreground = fgColor - panel.font = UIUtil.getLabelFont().deriveFont(UIUtil.getFontSize(UIUtil.FontSize.SMALL)) - textArea.text = buildMoreHTML(fgColor) - panel.border = null - label.icon = null - panel } } } diff --git a/src/main/kotlin/org/arend/typechecking/BinaryFileSaver.kt b/src/main/kotlin/org/arend/typechecking/BinaryFileSaver.kt index 08d267e05..cb2255a65 100644 --- a/src/main/kotlin/org/arend/typechecking/BinaryFileSaver.kt +++ b/src/main/kotlin/org/arend/typechecking/BinaryFileSaver.kt @@ -1,5 +1,6 @@ package org.arend.typechecking +import com.intellij.openapi.application.ApplicationManager import com.intellij.openapi.application.runReadAction import com.intellij.openapi.components.service import com.intellij.openapi.project.Project @@ -91,7 +92,9 @@ class BinaryFileSaver(private val project: Project) { synchronized(project) { val savedFiles = HashSet() for (entry in typecheckedModules) { - saveFile(entry.key, entry.value, typeCheckingService.libraryManager.libraryErrorReporter, savedFiles) + ApplicationManager.getApplication().executeOnPooledThread { + saveFile(entry.key, entry.value, typeCheckingService.libraryManager.libraryErrorReporter, savedFiles) + } } typecheckedModules.clear() updateFiles(savedFiles) diff --git a/src/main/kotlin/org/arend/typechecking/execution/TypeCheckProcessHandler.kt b/src/main/kotlin/org/arend/typechecking/execution/TypeCheckProcessHandler.kt index 1ab1a3341..7931da30e 100644 --- a/src/main/kotlin/org/arend/typechecking/execution/TypeCheckProcessHandler.kt +++ b/src/main/kotlin/org/arend/typechecking/execution/TypeCheckProcessHandler.kt @@ -9,6 +9,7 @@ import com.intellij.openapi.diagnostic.Logger import com.intellij.openapi.progress.ProcessCanceledException import com.intellij.openapi.progress.ProgressIndicator import com.intellij.openapi.progress.util.ProgressIndicatorBase +import com.intellij.psi.PsiDirectory import com.intellij.psi.PsiElement import com.intellij.psi.PsiErrorElement import com.intellij.psi.SmartPointerManager @@ -38,8 +39,10 @@ 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 @@ -119,22 +122,36 @@ 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 = true) - 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)) + 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() + } } - module + 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)) + } + } + items } if (command.definitionFullName == "") { @@ -203,6 +220,15 @@ class TypeCheckProcessHandler( } } + private fun getAllFilesInDirectory(directory: PsiDirectory): List { + val arendFiles = mutableListOf() + for (subDir in directory.subdirectories) { + arendFiles.addAll(getAllFilesInDirectory(subDir)) + } + arendFiles.addAll(directory.files.filterIsInstance()) + return arendFiles + } + private fun resetGroup(group: ArendGroup) { if (indicator.isCanceled) { return diff --git a/src/main/kotlin/org/arend/typechecking/execution/TypeCheckRunConfigurationEditor.kt b/src/main/kotlin/org/arend/typechecking/execution/TypeCheckRunConfigurationEditor.kt index 4557b085d..47868ae0b 100644 --- a/src/main/kotlin/org/arend/typechecking/execution/TypeCheckRunConfigurationEditor.kt +++ b/src/main/kotlin/org/arend/typechecking/execution/TypeCheckRunConfigurationEditor.kt @@ -9,16 +9,19 @@ import com.intellij.ui.EditorTextField import com.intellij.ui.dsl.builder.panel import org.arend.ArendFileTypeInstance import org.arend.definition.ArendFileDefinitionScope -import org.arend.module.AllArendFilesScope +import org.arend.ext.module.ModulePath +import org.arend.module.AllArendFilesAndPackagesScope import org.arend.module.AllModulesScope 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.psi.ArendFile +import org.arend.psi.ext.PsiModuleReferable import org.arend.refactoring.move.ArendLongNameCodeFragment import org.arend.typechecking.TypeCheckingService import org.arend.typechecking.execution.configurations.TypeCheckConfiguration +import org.arend.util.FileUtils import org.arend.util.aligned import javax.swing.JComponent @@ -37,7 +40,7 @@ class TypeCheckRunConfigurationEditor(private val project: Project) : SettingsEd } val module = ModuleManager.getInstance(project).findModuleByName(library) val arendModuleConfigService = ArendModuleConfigService.getInstance(module) - arendModuleConfigService?.let { AllArendFilesScope(it, withPrelude = false) } ?: EmptyScope.INSTANCE + arendModuleConfigService?.let { AllArendFilesAndPackagesScope(it, ModulePath(), withPrelude = true, withArendExtension = false) } ?: EmptyScope.INSTANCE }) modulePathComponent = EditorTextField(PsiDocumentManager.getInstance(project).getDocument(moduleDocument), project, ArendFileTypeInstance) definitionNameComponent = EditorTextField(PsiDocumentManager.getInstance(project).getDocument(ArendLongNameCodeFragment(project, DEFINITION_TEXT, null, customScopeGetter = { @@ -48,7 +51,7 @@ class TypeCheckRunConfigurationEditor(private val project: Project) : SettingsEd } else if (library == PRELUDE) { return@ArendLongNameCodeFragment EmptyScope.INSTANCE } - val arendFile = moduleDocument.scope.resolveName(module)?.underlyingReferable as? ArendFile? + val arendFile = (moduleDocument.scope.resolveName(module) as? PsiModuleReferable)?.modules?.get(0) as? ArendFile? ?: return@ArendLongNameCodeFragment EmptyScope.INSTANCE ArendFileDefinitionScope(arendFile) })), project, ArendFileTypeInstance) diff --git a/src/main/kotlin/org/arend/typechecking/execution/TypecheckRunConfigurationProducer.kt b/src/main/kotlin/org/arend/typechecking/execution/TypecheckRunConfigurationProducer.kt index 786adecfd..a8602dbb3 100644 --- a/src/main/kotlin/org/arend/typechecking/execution/TypecheckRunConfigurationProducer.kt +++ b/src/main/kotlin/org/arend/typechecking/execution/TypecheckRunConfigurationProducer.kt @@ -3,7 +3,9 @@ package org.arend.typechecking.execution import com.intellij.execution.actions.ConfigurationContext import com.intellij.execution.actions.LazyRunConfigurationProducer import com.intellij.openapi.util.Ref +import com.intellij.psi.PsiDirectory import com.intellij.psi.PsiElement +import org.arend.module.config.ArendModuleConfigService import org.arend.psi.ArendFile import org.arend.psi.ext.TCDefinition import org.arend.psi.ext.fullName @@ -11,6 +13,8 @@ import org.arend.psi.parentOfType import org.arend.typechecking.execution.configurations.ArendRunConfigurationFactory import org.arend.typechecking.execution.configurations.TypeCheckConfiguration import org.arend.typechecking.execution.configurations.TypecheckRunConfigurationType +import org.arend.util.FileUtils.EXTENSION +import org.arend.util.getRelativePath class TypecheckRunConfigurationProducer: LazyRunConfigurationProducer() { override fun getConfigurationFactory() = TYPECHECK_CONFIGURATION_FACTORY @@ -34,24 +38,59 @@ class TypecheckRunConfigurationProducer: LazyRunConfigurationProducer?): MyConfiguration? { val element = context.location?.psiElement - when (val definition = element?.parentOfType(false) ?: element?.parentOfType(false)) { + when (val definition = element?.parentOfType(false) ?: element?.parentOfType(false) ?: if (element is PsiDirectory) element else null) { is TCDefinition -> { val file = definition.containingFile as? ArendFile ?: return null val modulePath = file.moduleLocation ?: return null sourceElement?.set(definition) val fullName = definition.fullName - return MyConfiguration("Typecheck $fullName", TypeCheckCommand(file.libraryName ?: "", modulePath.toString(), fullName)) + + val test = ArendModuleConfigService.getInstance(context.module)?.testsDirFile + val fullNameTest = test?.getRelativePath(file.virtualFile)?.joinToString(".") + + return if (fullNameTest != null) { + MyConfiguration("Typecheck $fullName", TypeCheckCommand(file.libraryName ?: "", "$TEST_PREFIX.$modulePath$EXTENSION", fullName)) + } else { + MyConfiguration("Typecheck $fullName", TypeCheckCommand(file.libraryName ?: "", "$modulePath$EXTENSION", fullName)) + } } is ArendFile -> { sourceElement?.set(definition) val fullName = definition.moduleLocation?.toString() ?: return null - return MyConfiguration("Typecheck $fullName", TypeCheckCommand(definition.libraryName ?: "", fullName)) + val test = ArendModuleConfigService.getInstance(context.module)?.testsDirFile + val fullNameTest = test?.getRelativePath(definition.virtualFile)?.joinToString(".") + return if (fullNameTest != null) { + MyConfiguration("Typecheck $TEST_PREFIX.$fullName$EXTENSION", TypeCheckCommand(definition.libraryName ?: "", "$TEST_PREFIX.$fullName$EXTENSION")) + } else { + MyConfiguration("Typecheck $fullName$EXTENSION", TypeCheckCommand(definition.libraryName ?: "", "$fullName$EXTENSION")) + } + } + is PsiDirectory -> { + sourceElement?.set(definition) + val source = ArendModuleConfigService.getInstance(context.module)?.sourcesDirFile + val test = ArendModuleConfigService.getInstance(context.module)?.testsDirFile + val fullNameSrc = source?.getRelativePath(definition.virtualFile)?.joinToString(".") + val fullNameTest = test?.getRelativePath(definition.virtualFile)?.joinToString(".") + val libraryName = ArendModuleConfigService.getInstance(context.module)?.library?.name?: "" + return if (fullNameSrc != null) { + getMyConfiguration(fullNameSrc, source.name, libraryName) + } else if (fullNameTest != null) { + getMyConfiguration(if (fullNameTest.isEmpty()) "" else "$TEST_PREFIX.$fullNameTest", test.name, libraryName) + } else { + null + } } else -> return null } } + private fun getMyConfiguration(fullName: String, virtualFileName: String, libraryName: String): MyConfiguration { + return MyConfiguration("Typecheck ${fullName.ifEmpty { virtualFileName }}", + TypeCheckCommand(libraryName, fullName.ifEmpty { virtualFileName })) + } + companion object { private val TYPECHECK_CONFIGURATION_FACTORY = ArendRunConfigurationFactory(TypecheckRunConfigurationType()) + const val TEST_PREFIX = "Test" } } diff --git a/src/main/kotlin/org/arend/typechecking/execution/TypecheckingEventsProcessor.kt b/src/main/kotlin/org/arend/typechecking/execution/TypecheckingEventsProcessor.kt index 140833950..b02d84e36 100644 --- a/src/main/kotlin/org/arend/typechecking/execution/TypecheckingEventsProcessor.kt +++ b/src/main/kotlin/org/arend/typechecking/execution/TypecheckingEventsProcessor.kt @@ -16,6 +16,7 @@ import org.arend.naming.reference.ModuleReferable import org.arend.psi.ArendFile import org.arend.psi.ext.PsiLocatedReferable import org.arend.psi.ext.fullName +import java.util.concurrent.ConcurrentHashMap interface ProxyAction { fun runAction(p : SMTestProxy) @@ -23,7 +24,7 @@ interface ProxyAction { class TypecheckingEventsProcessor(project: Project, typeCheckingRootNode: SMTestProxy.SMRootTestProxy, typeCheckingFrameworkName: String) : GeneralTestEventsProcessor(project, typeCheckingFrameworkName, typeCheckingRootNode) { - private val definitionToProxy = mutableMapOf() + private val definitionToProxy = ConcurrentHashMap() private val fileToProxy = mutableMapOf() private val deferredActions = mutableMapOf>() private var isTypeCheckingFinished = false diff --git a/src/main/resources/META-INF/plugin.xml b/src/main/resources/META-INF/plugin.xml index 25f8b817f..7b9ddc4a5 100644 --- a/src/main/resources/META-INF/plugin.xml +++ b/src/main/resources/META-INF/plugin.xml @@ -190,6 +190,12 @@ enabledByDefault="true" unfair="true" implementationClass="org.arend.inspection.ArendUnusedImportInspection"/> + + Arend @@ -417,7 +423,6 @@ - diff --git a/src/main/resources/icons/orthogonal_graph.svg b/src/main/resources/icons/orthogonal_graph.svg index f1448ba10..058178075 100644 --- a/src/main/resources/icons/orthogonal_graph.svg +++ b/src/main/resources/icons/orthogonal_graph.svg @@ -1,42 +1,6 @@ - + - - + + - + \ No newline at end of file diff --git a/src/main/resources/inspectionDescriptions/RedundantParameter.html b/src/main/resources/inspectionDescriptions/RedundantParameter.html new file mode 100644 index 000000000..433b5f131 --- /dev/null +++ b/src/main/resources/inspectionDescriptions/RedundantParameter.html @@ -0,0 +1,6 @@ + + +Reports redundant parameters. + + + \ No newline at end of file diff --git a/src/main/resources/messages/ArendBundle.properties b/src/main/resources/messages/ArendBundle.properties index b2e987285..0bd2882e2 100644 --- a/src/main/resources/messages/ArendBundle.properties +++ b/src/main/resources/messages/ArendBundle.properties @@ -39,7 +39,8 @@ arend.expression.clarifyingParens.processingFailed=Failed to process binary oper arend.expression.clarifyingParens.unexpectedUseOfImplicitArgs=Unexpected use of implicit arguments after explicit ones arend.show.type.progress=Computing type representation... -arend.inspection.redundant.parameter.message=Replace the redundant parameter with _ +arend.inspection.redundant.parameter.message=Redundant parameter +arend.inspection.redundant.parameter.fix=Replace the redundant parameter with _ arend.inspection.redundant.parentheses.name=Redundant parentheses arend.inspection.redundant.parentheses.message=Redundant parentheses arend.unwrap.parentheses.fix=Unwrap parentheses diff --git a/src/test/kotlin/org/arend/codeInsight/completion/ArendFieldCompletionTest.kt b/src/test/kotlin/org/arend/codeInsight/completion/ArendFieldCompletionTest.kt index 197387f82..32e619709 100644 --- a/src/test/kotlin/org/arend/codeInsight/completion/ArendFieldCompletionTest.kt +++ b/src/test/kotlin/org/arend/codeInsight/completion/ArendFieldCompletionTest.kt @@ -107,6 +107,20 @@ class ArendFieldCompletionTest : ArendCompletionTestBase() { "\\func test (a : 0 + 1) => a.{-caret-}", listOf("f", "g")) + fun `test class field`() = + doSingleCompletionMultifile(""" + -- ! A.ard + \class Foo { + | <=-transitive \alias <=o : Nat -> Nat + } + -- ! Main.ard + \func lol => <=-tran{-caret-} + """, """ + \import A + + \func lol => <=o + """) + fun `_test pattern`() = checkCompletionVariants( "\\class A (f g : Nat)\n" + diff --git a/src/test/kotlin/org/arend/inspection/InspectionUtilTest.kt b/src/test/kotlin/org/arend/inspection/InspectionUtilTest.kt index e18917156..bd8abaa84 100644 --- a/src/test/kotlin/org/arend/inspection/InspectionUtilTest.kt +++ b/src/test/kotlin/org/arend/inspection/InspectionUtilTest.kt @@ -11,4 +11,14 @@ internal fun doWarningsCheck(myFixture: CodeInsightTestFixture, contents: String myFixture.doHighlighting() } myFixture.checkHighlighting(true, false, false) -} \ No newline at end of file +} + +internal fun doWeakWarningsCheck(myFixture: CodeInsightTestFixture, contents: String, typecheck: Boolean = false) { + val fileTree = fileTreeFromText(contents) + fileTree.create(myFixture.project, myFixture.findFileInTempDir(".")) + myFixture.configureFromTempProjectFile("Main.ard") + if (typecheck) { + myFixture.doHighlighting() + } + myFixture.checkHighlighting(false, false, true) +} diff --git a/src/test/kotlin/org/arend/inspection/RedundantParameterNameInspectionTest.kt b/src/test/kotlin/org/arend/inspection/RedundantParameterInspectionTest.kt similarity index 69% rename from src/test/kotlin/org/arend/inspection/RedundantParameterNameInspectionTest.kt rename to src/test/kotlin/org/arend/inspection/RedundantParameterInspectionTest.kt index d06684e48..e2199d08f 100644 --- a/src/test/kotlin/org/arend/inspection/RedundantParameterNameInspectionTest.kt +++ b/src/test/kotlin/org/arend/inspection/RedundantParameterInspectionTest.kt @@ -3,7 +3,11 @@ package org.arend.inspection import org.arend.quickfix.QuickFixTestBase import org.arend.util.ArendBundle -class RedundantParameterNameInspectionTest : QuickFixTestBase() { +class RedundantParameterInspectionTest : QuickFixTestBase() { + override fun setUp() { + super.setUp() + myFixture.enableInspections(RedundantParameterInspection::class.java) + } fun testFunc() = doWarningsCheck(myFixture, """ \func f (${rpnWarning("x")} : Nat) => 0 diff --git a/src/test/kotlin/org/arend/inspection/RedundantParensInspectionTest.kt b/src/test/kotlin/org/arend/inspection/RedundantParensInspectionTest.kt index 9bda44247..c0df24f8e 100644 --- a/src/test/kotlin/org/arend/inspection/RedundantParensInspectionTest.kt +++ b/src/test/kotlin/org/arend/inspection/RedundantParensInspectionTest.kt @@ -10,7 +10,7 @@ class RedundantParensInspectionTest : QuickFixTestBase() { myFixture.enableInspections(RedundantParensInspection::class.java) } - fun testNeverNeedsParens() = doWeakWarningsCheck(""" + fun testNeverNeedsParens() = doWeakWarningsCheck(myFixture, """ \open Nat (+) \func f2 {A : \Type} {B : \Type} (a : A) (b : B) => {?} @@ -45,7 +45,7 @@ class RedundantParensInspectionTest : QuickFixTestBase() { \func test14 => f2 (+) 1 """) - fun testNewExpression() = doWeakWarningsCheck(""" + fun testNewExpression() = doWeakWarningsCheck(myFixture,""" \class Pair (x y : Nat) \func test1 => \new ${rp("(Pair 1 2)")} @@ -55,7 +55,7 @@ class RedundantParensInspectionTest : QuickFixTestBase() { \func test3 => (pair 0).1 """) - fun testReturnExpression() = doWeakWarningsCheck(""" + fun testReturnExpression() = doWeakWarningsCheck(myFixture,""" \data Empty \func test1 : ${rp("(1 = 1)")} => idp @@ -63,7 +63,7 @@ class RedundantParensInspectionTest : QuickFixTestBase() { \func test2 : Empty $LEVEL ${rp("(prop-pi {Empty})")} => {?} """) - fun testParameterType() = doWeakWarningsCheck(""" + fun testParameterType() = doWeakWarningsCheck(myFixture,""" \func test1 {a : ${rp("(0 = 0)")}} (b : ${rp("(0 = 0)")}) => 1 \record A (f : ${rp("(0 = 0)")} -> Nat) @@ -81,7 +81,7 @@ class RedundantParensInspectionTest : QuickFixTestBase() { | test6 (a : ${rp("(0 = 0)")}) (${rp("(0 = 0)")}) """) - fun testBodyAndClauseAndCoClause() = doWeakWarningsCheck(""" + fun testBodyAndClauseAndCoClause() = doWeakWarningsCheck(myFixture,""" \open Nat (+) \class Pair (x y : Nat) @@ -104,7 +104,7 @@ class RedundantParensInspectionTest : QuickFixTestBase() { \func test7 => \new Pair 0 { | y => ${rp("(0 + 0)")} } """) - fun testClausePattern() = doWeakWarningsCheck(""" + fun testClausePattern() = doWeakWarningsCheck(myFixture,""" \func test1 (p : 1 = 1) : Nat | p : ${rp("(1 = 1)")} => 1 @@ -112,36 +112,36 @@ class RedundantParensInspectionTest : QuickFixTestBase() { | p \as p' : ${rp("(1 = 1)")} => 1 """) - fun testArrowExpression() = doWeakWarningsCheck(""" + fun testArrowExpression() = doWeakWarningsCheck(myFixture,""" \func test1 => (Nat -> Nat) -> Nat -- False negatives. But removing parens might hurt readability, especially in the second case. \func test2 => ${rp("(0 = 1)")} -> Nat \func test3 => (\Sigma Nat Nat) -> Nat """) - fun testSigmaExpression() = doWeakWarningsCheck(""" + fun testSigmaExpression() = doWeakWarningsCheck(myFixture,""" \func test1 => \Sigma Nat (Nat -> Nat) -- Without parens this Sigma turns into Arrow \func test2 => \Sigma (a : ${rp("(0 = 0)")}) (${rp("(0 = 0)")}) """) - fun testPiExpression() = doWeakWarningsCheck(""" + fun testPiExpression() = doWeakWarningsCheck(myFixture,""" \func test1 => \Pi (n : Nat) -> ${rp("(Nat -> Nat)")} \func test2 => \Pi (n : Nat) -> ${rp("(0 = 0)")} \func test3 => \Pi (a : ${rp("(0 = 0)")}) (${rp("(0 = 0)")}) -> Nat """) - fun testLambdaExpression() = doWeakWarningsCheck(""" + fun testLambdaExpression() = doWeakWarningsCheck(myFixture,""" \func test1 => \lam (x : Nat) => ${rp("(0 = 0)")} \func test2 => \lam {a : ${rp("(0 = 0)")}} (b : ${rp("(0 = 0)")}) => 1 """) - fun testLetExpression() = doWeakWarningsCheck(""" + fun testLetExpression() = doWeakWarningsCheck(myFixture,""" \func test1 => \let N => Nat \in ${rp("(N -> N)")} \func test2 => \let p => ${rp("(0 = 0)")} \in p \func test3 => \let p : ${rp("(1 = 1)")} => idp \in p """) - fun testTupleExpression() = doWeakWarningsCheck(""" + fun testTupleExpression() = doWeakWarningsCheck(myFixture,""" \open Nat (+) \func test1 => (${rp("(1 + 2)")} : Nat, ${rp("(3 + 4)")}) @@ -154,14 +154,14 @@ class RedundantParensInspectionTest : QuickFixTestBase() { \func test5 : \Sigma (0 = 1 -> Nat) Nat => (${rp("(\\case __ \\return Nat)")}, 2) """) - fun testMetaDefCallWithClauses() = doWeakWarningsCheck(""" + fun testMetaDefCallWithClauses() = doWeakWarningsCheck(myFixture,""" \func f2 {A : \Type} {B : \Type} (a : A) (b : B) => {?} \meta mcases => 1 \func test15 => f2 (mcases \with {}) 1 """) - fun testApplicationUsedAsBinOpArgument() = doWeakWarningsCheck(""" + fun testApplicationUsedAsBinOpArgument() = doWeakWarningsCheck(myFixture,""" \open Nat (+) \func test1 => ${rp("(f 1 2)")} + 3 @@ -213,7 +213,7 @@ class RedundantParensInspectionTest : QuickFixTestBase() { \func test : 0 = 0 => idp """) - fun `test issues`() = doWeakWarningsCheck(""" + fun `test issues`() = doWeakWarningsCheck(myFixture,""" \module Issue302 \where \func foo (F : Nat -> \Type) => ${rp("(F 0)")} -> ${rp("(F 0)")} \module Issue326 \where { @@ -231,7 +231,7 @@ class RedundantParensInspectionTest : QuickFixTestBase() { } """) - fun testReturnExpr() = doWeakWarningsCheck(""" + fun testReturnExpr() = doWeakWarningsCheck(myFixture,""" \data Bool | true | false \func lol (a : Bool) : Bool -> Bool => \case a \return (Bool -> Bool) \with { @@ -240,7 +240,7 @@ class RedundantParensInspectionTest : QuickFixTestBase() { } """) - fun test375() = doWeakWarningsCheck(""" + fun test375() = doWeakWarningsCheck(myFixture,""" \module Issue375 \where { \class Ring (E : \Set) | \infixl 6 + : E -> E -> E @@ -288,17 +288,6 @@ class RedundantParensInspectionTest : QuickFixTestBase() { \func test => \Sigma \Prop (Nat -> Nat) """) - private fun doWeakWarningsCheck(contents: String, typecheck: Boolean = false) { - val fileTree = fileTreeFromText(contents) - fileTree.create(myFixture.project, myFixture.findFileInTempDir(".")) - myFixture.configureFromTempProjectFile("Main.ard") - if (typecheck) { - //typecheck(fileTree.fileNames) - myFixture.doHighlighting() - } - myFixture.checkHighlighting(false, false, true) - } - private fun doTypedQuickFixTest(before: String, after: String) = typedQuickFixTest(ArendBundle.message("arend.unwrap.parentheses.fix"), before, after) @@ -306,6 +295,6 @@ class RedundantParensInspectionTest : QuickFixTestBase() { fun rp(text: String): String = "$text" - val LEVEL = "\\level" + const val LEVEL = "\\level" } } \ No newline at end of file