Fix typechecking bugs

JetBrains · Jun 13, 2024 · f08d0ff · f08d0ff
1 parent f992bf2
commit f08d0ff
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 2 deletions.
diff --git a/src/main/kotlin/org/arend/typechecking/execution/TypecheckRunConfigurationProducer.kt b/src/main/kotlin/org/arend/typechecking/execution/TypecheckRunConfigurationProducer.kt
@@ -44,7 +44,15 @@ class TypecheckRunConfigurationProducer: LazyRunConfigurationProducer<TypeCheckC
                 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)

diff --git a/src/main/kotlin/org/arend/typechecking/execution/TypecheckingEventsProcessor.kt b/src/main/kotlin/org/arend/typechecking/execution/TypecheckingEventsProcessor.kt
@@ -16,14 +16,15 @@ 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)
 }
 
 class TypecheckingEventsProcessor(project: Project, typeCheckingRootNode: SMTestProxy.SMRootTestProxy, typeCheckingFrameworkName: String)
     : GeneralTestEventsProcessor(project, typeCheckingFrameworkName, typeCheckingRootNode) {
-    private val definitionToProxy = mutableMapOf<PsiLocatedReferable, DefinitionProxy>()
+    private val definitionToProxy = ConcurrentHashMap<PsiLocatedReferable, DefinitionProxy>()
     private val fileToProxy = mutableMapOf<ModulePath, DefinitionProxy>()
     private val deferredActions = mutableMapOf<GlobalReferable, MutableList<ProxyAction>>()
     private var isTypeCheckingFinished = false