Merge pull request #558 from alex999990009/alex99999/fixes

Fix #110

src/main/kotlin/org/arend/highlight/ArendSyntaxHighlighterFactory.kt

@@ -1,13 +1,19 @@
 package org.arend.highlight
 
+import com.intellij.openapi.fileTypes.FileType
 import com.intellij.openapi.fileTypes.SyntaxHighlighter
 import com.intellij.openapi.fileTypes.SyntaxHighlighterFactory
+import com.intellij.openapi.fileTypes.SyntaxHighlighterProvider
 import com.intellij.openapi.project.Project
 import com.intellij.openapi.vfs.VirtualFile
 
-class ArendSyntaxHighlighterFactory : SyntaxHighlighterFactory() {
+class ArendSyntaxHighlighterFactory : SyntaxHighlighterFactory(), SyntaxHighlighterProvider {
     override fun getSyntaxHighlighter(
             project: Project?,
             virtualFile: VirtualFile?
     ): SyntaxHighlighter = ArendSyntaxHighlighter()
+
+    override fun create(fileType: FileType, project: Project?, file: VirtualFile?): SyntaxHighlighter {
+        return ArendSyntaxHighlighter()
+    }
 }

src/main/kotlin/org/arend/psi/arc/ArcDecompiler.kt

@@ -0,0 +1,40 @@
+package org.arend.psi.arc
+
+import com.intellij.openapi.vfs.VirtualFile
+import com.intellij.psi.FileViewProvider
+import com.intellij.psi.PsiManager
+import com.intellij.psi.compiled.ClassFileDecompilers
+import com.intellij.psi.compiled.ClsStubBuilder
+import com.intellij.psi.stubs.PsiFileStub
+import com.intellij.util.indexing.FileContent
+
+class ArcDecompiler : ClassFileDecompilers.Full() {
+
+    private val myStubBuilder = ArcClsStubBuilder()
+
+    override fun accepts(file: VirtualFile): Boolean {
+        return file.fileType is ArcFileType
+    }
+
+    override fun getStubBuilder(): ClsStubBuilder {
+        return myStubBuilder
+    }
+
+    override fun createFileViewProvider(file: VirtualFile, manager: PsiManager, physical: Boolean): FileViewProvider {
+        return ArcFileViewProvider(manager, file, physical)
+    }
+
+    companion object {
+        const val STUB_VERSION: Int = 1
+
+        class ArcClsStubBuilder : ClsStubBuilder() {
+            override fun getStubVersion(): Int {
+                return STUB_VERSION
+            }
+
+            override fun buildFileStub(fileContent: FileContent): PsiFileStub<*>? {
+                return ArcFile.buildFileStub(fileContent.file, fileContent.content)
+            }
+        }
+    }
+}

src/main/kotlin/org/arend/psi/arc/ArcFile.kt

@@ -0,0 +1,78 @@
+package org.arend.psi.arc
+
+import com.intellij.openapi.components.service
+import com.intellij.openapi.project.ProjectLocator
+import com.intellij.openapi.vfs.VfsUtilCore
+import com.intellij.openapi.vfs.VirtualFile
+import com.intellij.psi.*
+import com.intellij.psi.impl.PsiManagerImpl
+import com.intellij.psi.impl.file.PsiBinaryFileImpl
+import com.intellij.psi.impl.java.stubs.PsiJavaFileStub
+import org.arend.ext.module.ModulePath
+import org.arend.ext.prettyprinting.PrettyPrinterConfig
+import org.arend.ext.serialization.DeserializationException
+import org.arend.module.config.ArendModuleConfigService
+import org.arend.module.error.DeserializationError
+import org.arend.naming.reference.TCDefReferable
+import org.arend.source.StreamBinarySource
+import org.arend.term.group.Group
+import org.arend.term.group.Statement
+import org.arend.term.group.StaticGroup
+import org.arend.term.prettyprint.ToAbstractVisitor
+import org.arend.typechecking.TypeCheckingService
+import org.arend.util.arendModules
+import java.util.zip.GZIPInputStream
+
+class ArcFile(viewProvider: FileViewProvider) : PsiBinaryFileImpl(viewProvider.manager as PsiManagerImpl, viewProvider) {
+    companion object {
+        fun decompile(virtualFile: VirtualFile): String {
+            val builder = StringBuilder()
+
+            val group = getGroup(virtualFile) ?: return builder.toString()
+
+            val lastStatement = group.statements.lastOrNull()
+            for (statement in group.statements.dropLast(1)) {
+                if (addStatement(statement, builder)) {
+                    builder.append("\n\n")
+                }
+            }
+            addStatement(lastStatement, builder)
+            return builder.toString()
+        }
+
+        private fun getGroup(virtualFile: VirtualFile): Group? {
+            val project = ProjectLocator.getInstance().guessProjectForFile(virtualFile) ?: return null
+            val psiManager = PsiManager.getInstance(project)
+            psiManager.findFile(virtualFile) ?: return null
+
+            val libraryManager = project.service<TypeCheckingService>().libraryManager
+            val config = project.arendModules.map { ArendModuleConfigService.getInstance(it) }.find {
+                it?.root?.let { root -> VfsUtilCore.isAncestor(root, virtualFile, true) } ?: false
+            } ?: ArendModuleConfigService.getInstance(project.arendModules.getOrNull(0))
+            val library = config?.library ?: return null
+
+            try {
+                virtualFile.inputStream.use { inputStream ->
+                    val group = StreamBinarySource.getGroup(GZIPInputStream(inputStream), libraryManager, library)
+                    return group
+                }
+            } catch (e : DeserializationException) {
+                libraryManager.libraryErrorReporter.report(DeserializationError(ModulePath(virtualFile.name), e))
+            }
+            return null
+        }
+
+        private fun addStatement(statement: Statement?, builder: StringBuilder): Boolean {
+            ((statement as? StaticGroup?)?.referable as? TCDefReferable?)?.typechecked?.let {
+                ToAbstractVisitor.convert(it, PrettyPrinterConfig.DEFAULT)
+                    .prettyPrint(builder, PrettyPrinterConfig.DEFAULT)
+            } ?: return false
+            return true
+        }
+
+        fun buildFileStub(file: VirtualFile, bytes: ByteArray): PsiJavaFileStub? {
+            // TODO like .class files
+            return null
+        }
+    }
+}

src/main/kotlin/org/arend/psi/arc/ArcFileDecompiler.kt

@@ -0,0 +1,37 @@
+package org.arend.psi.arc
+
+import com.intellij.openapi.fileTypes.BinaryFileDecompiler
+import com.intellij.openapi.project.DefaultProjectFactory
+import com.intellij.openapi.vfs.VirtualFile
+import com.intellij.psi.PsiManager
+import com.intellij.psi.compiled.ClassFileDecompilers
+import com.intellij.psi.impl.compiled.ClsFileImpl
+
+class ArcFileDecompiler : BinaryFileDecompiler {
+    override fun decompile(file: VirtualFile): CharSequence {
+        val decompiler = ClassFileDecompilers.getInstance().find(file, ClassFileDecompilers.Decompiler::class.java)
+        if (decompiler is ArcDecompiler) {
+            return ArcFile.decompile(file)
+        }
+
+        if (decompiler is ClassFileDecompilers.Full) {
+            val manager = PsiManager.getInstance(DefaultProjectFactory.getInstance().defaultProject)
+            return decompiler.createFileViewProvider(file, manager, true).contents
+        }
+
+        if (decompiler is ClassFileDecompilers.Light) {
+            return try {
+                decompiler.getText(file)
+            } catch (e: ClassFileDecompilers.Light.CannotDecompileException) {
+                ClsFileImpl.decompile(file)
+            }
+        }
+
+        throw IllegalStateException(decompiler.javaClass.name +
+                    " should be on of " +
+                    ClassFileDecompilers.Full::class.java.name +
+                    " or " +
+                    ClassFileDecompilers.Light::class.java.name
+        )
+    }
+}

src/main/kotlin/org/arend/psi/arc/ArcFileStubBuilder.kt

@@ -0,0 +1,54 @@
+package org.arend.psi.arc
+
+import com.intellij.openapi.vfs.VirtualFile
+import com.intellij.psi.compiled.ClassFileDecompilers
+import com.intellij.psi.stubs.BinaryFileStubBuilder
+import com.intellij.psi.stubs.Stub
+import com.intellij.util.cls.ClsFormatException
+import com.intellij.util.indexing.FileContent
+import java.util.stream.Stream
+
+class ArcFileStubBuilder : BinaryFileStubBuilder.CompositeBinaryFileStubBuilder<ClassFileDecompilers.Full> {
+    override fun acceptsFile(file: VirtualFile): Boolean {
+        return file.fileType is ArcFileType
+    }
+
+    override fun getStubVersion(): Int {
+        return STUB_VERSION
+    }
+
+    override fun getAllSubBuilders(): Stream<ClassFileDecompilers.Full> {
+        return ClassFileDecompilers.getInstance().EP_NAME.extensionList.stream()
+            .filter { d: ClassFileDecompilers.Decompiler? -> d is ClassFileDecompilers.Full }
+            .map { d: ClassFileDecompilers.Decompiler? -> d as ClassFileDecompilers.Full? }
+    }
+
+    override fun getSubBuilder(fileContent: FileContent): ClassFileDecompilers.Full? {
+        return fileContent.file.computeWithPreloadedContentHint(fileContent.content) {
+                ClassFileDecompilers.getInstance()
+                    .find(fileContent.file, ClassFileDecompilers.Full::class.java)
+            }
+    }
+
+    override fun getSubBuilderVersion(decompiler: ClassFileDecompilers.Full?): String {
+        if (decompiler == null) return "default"
+        val version = decompiler.stubBuilder.stubVersion
+        return decompiler.javaClass.name + ":" + version
+    }
+
+    override fun buildStubTree(fileContent: FileContent, decompiler: ClassFileDecompilers.Full?): Stub? {
+        if (decompiler == null) return null
+        return fileContent.file.computeWithPreloadedContentHint(fileContent.content) {
+            try {
+                return@computeWithPreloadedContentHint decompiler.stubBuilder.buildFileStub(fileContent)
+            } catch (_: ClsFormatException) {
+                // TODO()
+            }
+            null
+        }
+    }
+
+    companion object {
+        const val STUB_VERSION: Int = 1
+    }
+}

src/main/kotlin/org/arend/psi/arc/ArcFileType.kt

@@ -0,0 +1,21 @@
+package org.arend.psi.arc
+
+import com.intellij.openapi.fileTypes.FileType
+import org.arend.ArendIcons
+import org.arend.util.FileUtils
+
+open class ArcFileType : FileType {
+    override fun getName(): String = "Arc"
+
+    override fun getDescription(): String = "Arc files"
+
+    override fun getDefaultExtension(): String = FileUtils.SERIALIZED_EXTENSION.drop(1)
+
+    override fun getIcon() = ArendIcons.AREND_FILE
+
+    override fun isBinary(): Boolean = true
+
+    companion object {
+        val INSTANCE = ArcFileType()
+    }
+}

src/main/kotlin/org/arend/psi/arc/ArcFileViewProvider.kt

@@ -0,0 +1,20 @@
+package org.arend.psi.arc
+
+import com.intellij.openapi.fileTypes.FileType
+import com.intellij.openapi.project.Project
+import com.intellij.openapi.vfs.VirtualFile
+import com.intellij.psi.PsiFile
+import com.intellij.psi.PsiManager
+import com.intellij.psi.SingleRootFileViewProvider
+import org.arend.ArendLanguage
+
+class ArcFileViewProvider(manager: PsiManager, virtualFile: VirtualFile, eventSystemEnabled: Boolean = true) :
+    SingleRootFileViewProvider(manager, virtualFile, eventSystemEnabled, ArendLanguage.INSTANCE) {
+
+    override fun createFile(project: Project, file: VirtualFile, fileType: FileType): PsiFile? {
+        if (fileType is ArcFileType) {
+            return ArcFile(this)
+        }
+        return super.createFile(project, file, fileType)
+    }
+}

src/main/kotlin/org/arend/psi/arc/ArcFileViewProviderFactory.kt

@@ -0,0 +1,15 @@
+package org.arend.psi.arc
+
+import com.intellij.lang.Language
+import com.intellij.openapi.vfs.VirtualFile
+import com.intellij.psi.FileViewProvider
+import com.intellij.psi.FileViewProviderFactory
+import com.intellij.psi.PsiManager
+import com.intellij.psi.compiled.ClassFileDecompilers
+
+class ArcFileViewProviderFactory : FileViewProviderFactory {
+    override fun createFileViewProvider(file: VirtualFile, language: Language?, manager: PsiManager, eventSystemEnabled: Boolean): FileViewProvider {
+        val decompiler = ClassFileDecompilers.getInstance().find(file, ClassFileDecompilers.Full::class.java)
+        return decompiler.createFileViewProvider(file, manager, eventSystemEnabled)
+    }
+}

src/main/kotlin/org/arend/psi/arc/ArcNotificationProvider.kt

@@ -0,0 +1,40 @@
+package org.arend.psi.arc
+
+import com.intellij.openapi.fileEditor.FileDocumentManager
+import com.intellij.openapi.fileEditor.FileEditor
+import com.intellij.openapi.fileEditor.FileEditorManager
+import com.intellij.openapi.project.Project
+import com.intellij.openapi.vfs.VirtualFile
+import com.intellij.ui.EditorNotificationPanel
+import com.intellij.ui.EditorNotificationProvider
+import com.intellij.util.indexing.FileBasedIndex
+import org.arend.util.ArendBundle
+import java.util.function.Function
+import javax.swing.JComponent
+
+class ArcNotificationProvider : EditorNotificationProvider {
+    override fun collectNotificationData(project: Project, virtualFile: VirtualFile): Function<in FileEditor, out JComponent?>? {
+        if (virtualFile.fileType !is ArcFileType) {
+            return null
+        }
+        return Function<FileEditor, EditorNotificationPanel?> {
+            createPanel(project, virtualFile, it)
+        }
+    }
+
+    private fun createPanel(project: Project, virtualFile: VirtualFile, editor: FileEditor): EditorNotificationPanel {
+        val panel = EditorNotificationPanel(editor, EditorNotificationPanel.Status.Info)
+        panel.text = ArendBundle.message("arend.arc.update")
+        panel.createActionLabel(ArendBundle.message("arend.updateYamlConfiguration")) {
+            val editorManager = FileEditorManager.getInstance(project)
+            editorManager.closeFile(virtualFile)
+
+            FileBasedIndex.getInstance().invalidateCaches()
+            FileDocumentManager.getInstance()
+                .reloadFromDisk(FileDocumentManager.getInstance().getCachedDocument(virtualFile)!!)
+
+            editorManager.openFile(virtualFile, true)
+        }
+        return panel
+    }
+}

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

@@ -47,6 +47,7 @@
         <!-- File Type -->
 
         <fileType language="Arend" implementationClass="org.arend.ArendFileType" name="Arend" extensions="ard" />
+        <fileType fieldName="INSTANCE" implementationClass="org.arend.psi.arc.ArcFileType" name="Arc" extensions="arc" />
 
         <!-- Parser -->
 
@@ -65,6 +66,8 @@
 
         <!-- Syntax Highlighter -->
 
+        <syntaxHighlighter id="arend.arc" key="Arc"
+                                       factoryClass="org.arend.highlight.ArendSyntaxHighlighterFactory"/>
         <lang.syntaxHighlighterFactory language="Arend"
                                        implementationClass="org.arend.highlight.ArendSyntaxHighlighterFactory"/>
 
@@ -394,6 +397,8 @@
 
         <editorNotificationProvider implementation="org.arend.notification.FileOutsideSourcesProvider"/>
 
+        <editorNotificationProvider implementation="org.arend.psi.arc.ArcNotificationProvider"/>
+
         <!-- Configuration Options -->
 
         <editorSmartKeysConfigurable instance="org.arend.editor.ArendSmartKeysConfigurable"/>
@@ -429,8 +434,16 @@
         <liveTemplateContext contextId="AREND_EXPRESSION" baseContextId="AREND" implementation="org.arend.liveTemplates.ArendTemplateContextType$Expression"/>
 
         <!-- Starters -->
+
         <appStarter id="generateArendLibHtml" implementation="org.arend.documentation.GenerateArendLibHtmlStarter"/>
 
+        <!--  Decompiler tools  -->
+
+        <filetype.stubBuilder filetype="Arc" implementationClass="org.arend.psi.arc.ArcFileStubBuilder"/>
+        <filetype.decompiler filetype="Arc" implementationClass="org.arend.psi.arc.ArcFileDecompiler"/>
+        <fileType.fileViewProviderFactory filetype="Arc" implementationClass="org.arend.psi.arc.ArcFileViewProviderFactory"/>
+        <psi.classFileDecompiler implementation="org.arend.psi.arc.ArcDecompiler" order="first"/>
+
     </extensions>
 
     <actions>

src/main/resources/messages/ArendBundle.properties

@@ -207,4 +207,6 @@ arend.generateElimPatternMatchingClauses=Using \\elim to generate pattern matchi
 arend.updateYamlConfigurationQuestion=Would you like to update the settings from the YAML file?
 arend.updateYamlConfiguration=Update
 arend.message.fileOutsideSources=The file is located outside of sources
-arend.yaml.openDocumentation=Open the documentation
+arend.yaml.openDocumentation=Open the documentation
+
+arend.arc.update=Not all typechecked expressions may be displayed in the file. Try to update the contents of the file