Added graph of inverse dependencies of definitions

src/main/kotlin/org/arend/ArendIcons.kt

@@ -41,7 +41,7 @@ object ArendIcons {
     val TURNSTILE = getIcon("/icons/turnstile.svg")
     val CHECKMARK = getIcon("/icons/checkmark.svg")
 
-    val GRAPH = getIcon("/icons/graph.svg")
+    val ORTHOGONAL_GRAPH = getIcon("/icons/orthogonal_graph.svg")
 
     // Source code elements
 

src/main/kotlin/org/arend/actions/ArendDefinitionInverseDependenciesGraphAction.kt

@@ -0,0 +1,94 @@
+package org.arend.actions
+
+import com.intellij.openapi.actionSystem.AnAction
+import com.intellij.openapi.actionSystem.AnActionEvent
+import com.intellij.openapi.actionSystem.PlatformDataKeys
+import com.intellij.psi.PsiElement
+import com.intellij.psi.PsiElementVisitor
+import org.arend.ArendIcons
+import org.arend.graph.GraphEdge
+import org.arend.graph.GraphNode
+import org.arend.graph.GraphSimulator
+import org.arend.psi.ext.*
+
+class ArendDefinitionInverseDependenciesGraphAction : AnAction(ArendIcons.ORTHOGONAL_GRAPH) {
+
+    private val usedNodes = mutableSetOf<String>()
+    private val edges = mutableSetOf<GraphEdge>()
+
+    private fun findEdge(nameFrom: String, element: PsiElement) {
+        element.accept(object : PsiElementVisitor() {
+            override fun visitElement(element: PsiElement) {
+                if (element is ArendReferenceElement) {
+                    val resolve = element.resolve
+                    if (resolve is ArendDefinition<*>) {
+                        val nameTo = resolve.getName()
+                        if (nameTo != null) {
+                            edges.add(GraphEdge(nameFrom, nameTo))
+                            if (!usedNodes.contains(nameTo)) {
+                                findEdges(resolve)
+                            }
+                        }
+                    }
+                }
+                element.children.forEach { it.accept(this) }
+            }
+        })
+    }
+
+    private fun findEdges(definition: ArendDefinition<*>, optionalNameFrom: String? = null) {
+        val nameFrom = optionalNameFrom ?: definition.getName() ?: return
+        usedNodes.add(nameFrom)
+
+        for (param in definition.parametersExt) {
+            (param.type as? PsiElement?)?.let { findEdge(nameFrom, it) }
+        }
+        when (definition) {
+            is ArendFunctionDefinition -> {
+                definition.returnExpr?.let { findEdge(nameFrom, it) }
+                definition.body?.let { findEdge(nameFrom, it) }
+            }
+            is ArendDefClass -> {
+                definition.fields.forEach { findEdge(nameFrom, it) }
+                if (optionalNameFrom == null) {
+                    definition.superClassList.forEach { findEdges(it.longName.resolve as ArendDefinition<*>, nameFrom) }
+                } else {
+                    definition.superClassList.forEach { findEdges(it.longName.resolve as ArendDefinition<*>, optionalNameFrom) }
+                }
+            }
+            is ArendDefData -> definition.dataBody?.let { findEdge(nameFrom, it) }
+            is ArendDefMeta -> definition.expr?.let { findEdge(nameFrom, it) }
+        }
+    }
+
+    override fun actionPerformed(e: AnActionEvent) {
+        usedNodes.clear()
+        edges.clear()
+
+        val definition = getArendDefinition(e) as? ArendDefinition<*> ?: return
+        findEdges(definition)
+
+        val graphSimulator = GraphSimulator(this.toString(), edges, usedNodes.map { GraphNode(it) }.toSet())
+        graphSimulator.displayOrthogonal()
+    }
+
+    override fun update(e: AnActionEvent) {
+        e.presentation.isEnabled = getArendDefinition(e) != null
+    }
+
+    private fun getArendDefinition(e: AnActionEvent): PsiElement? {
+        val editor = e.getData(PlatformDataKeys.EDITOR)
+        val psiFile = e.getData(PlatformDataKeys.PSI_FILE)
+
+        if (editor == null || psiFile == null) {
+            return null
+        }
+
+        val offset = editor.caretModel.offset
+        var currentPsiElement = psiFile.findElementAt(offset)
+        while (currentPsiElement != null && currentPsiElement !is ArendDefinition<*>) {
+            currentPsiElement = currentPsiElement.parent
+        }
+        return currentPsiElement
+    }
+}

src/main/kotlin/org/arend/graph/GraphSimulator.kt

@@ -12,17 +12,19 @@ import javax.swing.ImageIcon
 import javax.swing.JFrame
 import javax.swing.JLabel
 
+data class GraphNode(val id: String)
+
 data class GraphEdge(val from: String, val to: String)
 
 class GraphSimulator(
-    private val graphId: String, private val edges: Set<GraphEdge>, private val vertices: Set<String>
+    private val graphId: String, private val edges: Set<GraphEdge>, private val vertices: Set<GraphNode>
 ) {
 
-    fun display() {
+    fun displayOrthogonal() {
         var graph = graph(graphId).directed()
 
         for (vertex in vertices) {
-            graph = graph.with(node(vertex))
+            graph = graph.with(node(vertex.id))
         }
 
         for (edge in edges) {

src/main/kotlin/org/arend/hierarchy/clazz/ArendClassHierarchyBrowser.kt

@@ -21,6 +21,7 @@ import com.intellij.ui.tree.StructureTreeModel
 import com.intellij.util.ui.tree.TreeUtil
 import org.arend.ArendIcons
 import org.arend.graph.GraphEdge
+import org.arend.graph.GraphNode
 import org.arend.graph.GraphSimulator
 import org.arend.hierarchy.ArendHierarchyNodeDescriptor
 import org.arend.psi.ext.ArendDefClass
@@ -166,14 +167,14 @@ class ArendClassHierarchyBrowser(project: Project, method: PsiElement) : TypeHie
         }
     }
 
-    inner class ArendHierarchyGraphAction : AnAction(ArendIcons.GRAPH) {
+    inner class ArendHierarchyGraphAction : AnAction(ArendIcons.ORTHOGONAL_GRAPH) {
         private val usedNodes = mutableSetOf<TreeNode>()
+        private val edges = mutableSetOf<GraphEdge>()
 
-        private fun findEdges(currentNode: DefaultMutableTreeNode): Set<GraphEdge> {
+        private fun findEdges(currentNode: DefaultMutableTreeNode) {
             usedNodes.add(currentNode)
 
             val from = ((currentNode.userObject as ArendHierarchyNodeDescriptor).psiElement as ArendDefClass).fullName
-            val edges = mutableSetOf<GraphEdge>()
 
             val children = TreeUtil.listChildren(currentNode)
             for (child in children) {
@@ -182,25 +183,29 @@ class ArendClassHierarchyBrowser(project: Project, method: PsiElement) : TypeHie
                 edges.add(GraphEdge(from, to))
 
                 if (!usedNodes.contains(child)) {
-                    edges.addAll(findEdges(child))
+                    findEdges(child)
                 }
             }
-            return edges
         }
 
         override fun actionPerformed(e: AnActionEvent) {
+            usedNodes.clear()
+            edges.clear()
+
             val tree = getJTree(currentViewType) ?: return
             val root = tree.model.root as DefaultMutableTreeNode
 
-            usedNodes.clear()
+            findEdges(root)
+
             val simulator = GraphSimulator(
                 this.toString(),
-                findEdges(root),
-                usedNodes.map { (((it as DefaultMutableTreeNode).userObject as ArendHierarchyNodeDescriptor).psiElement as? ArendDefClass?)?.fullName!! }
-                    .toSet()
+                edges,
+                usedNodes.map {
+                    GraphNode(
+                        (((it as DefaultMutableTreeNode).userObject as ArendHierarchyNodeDescriptor).psiElement as? ArendDefClass?)?.fullName!!
+                    ) }.toSet()
             )
-
-            simulator.display()
+            simulator.displayOrthogonal()
         }
     }
 }

src/main/kotlin/org/arend/module/ArendModuleDependenciesGraphAction.kt

@@ -6,45 +6,46 @@ import com.intellij.openapi.module.Module
 import com.intellij.openapi.module.ModuleManager
 import org.arend.ArendIcons
 import org.arend.graph.GraphEdge
+import org.arend.graph.GraphNode
 import org.arend.graph.GraphSimulator
 import org.arend.module.config.ArendModuleConfigService
 
-class ArendModuleDependenciesGraphAction : AnAction(ArendIcons.GRAPH) {
+class ArendModuleDependenciesGraphAction : AnAction(ArendIcons.ORTHOGONAL_GRAPH) {
     private val usedNodes = mutableSetOf<Module>()
+    private val edges = mutableSetOf<GraphEdge>()
 
-    private fun findEdges(currentNode: Module, modules: List<Module>): Set<GraphEdge> {
+    private fun findEdges(currentNode: Module, modules: List<Module>) {
         usedNodes.add(currentNode)
 
         val from = currentNode.name
         val edges = mutableSetOf<GraphEdge>()
 
-        val arendModuleConfigService = ArendModuleConfigService.getInstance(currentNode) ?: return emptySet()
+        val arendModuleConfigService = ArendModuleConfigService.getInstance(currentNode) ?: return
         val dependencyNames = arendModuleConfigService.dependencies.map { it.name }
         val children = modules.filter { dependencyNames.contains(it.name) }
 
         for (child in children) {
             edges.add(GraphEdge(from, child.name))
 
             if (!usedNodes.contains(child)) {
-                edges.addAll(findEdges(child, modules))
+                findEdges(child, modules)
             }
         }
-        return edges
     }
 
     override fun actionPerformed(e: AnActionEvent) {
+        usedNodes.clear()
+        edges.clear()
+
         val moduleManager = e.project?.let { ModuleManager.getInstance(it) } ?: return
         val modules = moduleManager.modules.toList()
-
-        usedNodes.clear()
-        val edges = mutableSetOf<GraphEdge>()
         for (module in modules) {
             if (!usedNodes.contains(module)) {
-                edges.addAll(findEdges(module, modules))
+                findEdges(module, modules)
             }
         }
 
-        val simulator = GraphSimulator(this.toString(), edges, usedNodes.map { it.name }.toSet())
-        simulator.display()
+        val simulator = GraphSimulator(this.toString(), edges, usedNodes.map { GraphNode(it.name) }.toSet())
+        simulator.displayOrthogonal()
     }
 }

src/main/kotlin/org/arend/psi/ext/ArendDefClass.kt

@@ -46,6 +46,9 @@ class ArendDefClass : ArendDefinition<ArendDefClassStub>, ClassReferable, TCDefi
     val extendsKw: PsiElement?
         get() = findChildByType(EXTENDS_KW)
 
+    override val parametersExt: List<Abstract.Parameter>
+        get() = parameters
+
     override fun getReferable() = this
 
     override fun isRecord(): Boolean = hasChildOfType(RECORD_KW)

src/main/kotlin/org/arend/psi/ext/ArendDefMeta.kt

@@ -34,6 +34,9 @@ class ArendDefMeta : ArendDefinition<ArendDefMetaStub>, Abstract.MetaDefinition,
             tcReferableCache = value
         }
 
+    override val parametersExt: List<Abstract.Parameter>
+        get() = parameters
+
     override fun getDescription() = documentation?.toString() ?: ""
 
     private fun prepareTCRef(data: SmartPsiElementPointer<PsiLocatedReferable>?, parent: LocatedReferable?) =

src/main/kotlin/org/arend/psi/ext/ArendDefinition.kt

@@ -74,7 +74,7 @@ where StubT : ArendNamedStub, StubT : StubElement<*> {
         return null
     }
 
-    protected open val parametersExt: List<Abstract.Parameter>
+    open val parametersExt: List<Abstract.Parameter>
         get() = emptyList()
 
     override fun getExternalParameters(): List<ParameterReferable> {

src/main/kotlin/org/arend/psi/ext/ArendFunctionDefinition.kt

@@ -30,6 +30,9 @@ where StubT : ArendNamedStub, StubT : StubElement<*> {
     val returnExpr: ArendReturnExpr?
         get() = childOfType()
 
+    override val parametersExt: List<Abstract.Parameter>
+        get() = parameters
+
     override fun getParameters(): List<ArendNameTele> = getChildrenOfType()
 
     override fun getResultType() = returnExpr?.type

src/main/resources/META-INF/plugin.xml

@@ -461,7 +461,7 @@
 
         <action id="ArendModuleDependenciesGraphAction"
                 class="org.arend.module.ArendModuleDependenciesGraphAction"
-                text="Show Graph of Arend Modules">
+                text="Show a Graph of Arend Modules">
             <add-to-group group-id="ProjectViewPopupMenu" anchor="after" relative-to-action="ProjectViewPopupMenuModifyGroup"/>
         </action>
 
@@ -563,6 +563,11 @@
         <action id="ArendUnmarkRootAction" class="org.arend.actions.ArendUnmarkRootAction">
             <add-to-group group-id="MarkRootGroup" anchor="first"/>
         </action>
+        <action id="ArendDefinitionInverseDependenciesGraphAction"
+                class="org.arend.actions.ArendDefinitionInverseDependenciesGraphAction"
+                text="Show a Graph of Inverse Dependencies of Definitions">
+            <add-to-group group-id="EditorPopupMenu" anchor="after" relative-to-action="EditorPopupMenu3"/>
+        </action>
     </actions>
 
     <resource-bundle>messages.ArendBundle</resource-bundle>