in src/main/kotlin/org/arend/typechecking/execution/TypeCheckProcessHandler.kt [56:204]
override fun startNotify() {
super.startNotify()
val eventsProcessor = eventsProcessor ?: return
SaveAndSyncHandler.getInstance().scheduleSave(SaveAndSyncHandler.SaveTask(typeCheckerService.project))
val typecheckingErrorReporter = TypecheckingErrorReporter(typeCheckerService.project.service(), PrettyPrinterConfig.DEFAULT, eventsProcessor)
val modulePath = if (command.modulePath == "") null else ModulePath(command.modulePath.split('.'))
if (modulePath != null) {
eventsProcessor.onSuiteStarted(modulePath)
}
if (command.definitionFullName != "" && modulePath == null) {
typecheckingErrorReporter.report(DefinitionNotFoundError(command.definitionFullName))
eventsProcessor.onSuitesFinished()
destroyProcessImpl()
return
}
val registeredLibraries = typeCheckerService.libraryManager.registeredLibraries
val libraries = if (command.library == "" && modulePath == null) registeredLibraries.filterIsInstance<ArendRawLibrary>() else {
val library = if (command.library != "") typeCheckerService.libraryManager.getRegisteredLibrary(command.library) else findLibrary(modulePath!!, registeredLibraries, typecheckingErrorReporter)
if (library == null) {
if (command.library != "") {
typecheckingErrorReporter.report(LibraryError.notFound(command.library))
}
eventsProcessor.onSuitesFinished()
destroyProcessImpl()
return
}
if (library !is ArendRawLibrary) {
typecheckingErrorReporter.report(LibraryError.incorrectLibrary(library.name))
eventsProcessor.onSuitesFinished()
destroyProcessImpl()
return
}
listOf(library)
}
if (libraries.isEmpty()) {
destroyProcessImpl()
return
}
for (module in typeCheckerService.updatedModules) {
val library = typeCheckerService.libraryManager.getRegisteredLibrary(module.libraryName) as? SourceLibrary
if (library?.supportsPersisting() == true) {
library.deleteModule(module.modulePath)
}
}
typeCheckerService.updatedModules.clear()
PooledThreadExecutor.INSTANCE.execute {
val concreteProvider = PsiConcreteProvider(typeCheckerService.project, typecheckingErrorReporter, typecheckingErrorReporter.eventsProcessor)
val collector = CollectingOrderingListener()
val instanceProviderSet = PsiInstanceProviderSet()
val ordering = Ordering(instanceProviderSet, concreteProvider, collector, typeCheckerService.dependencyListener, ArendReferableConverter, PsiElementComparator)
try {
runReadAction {
for (library in libraries) {
if (indicator.isCanceled) {
break
}
val modulePaths = if (modulePath == null) library.loadedModules else listOf(modulePath)
val modules = modulePaths.mapNotNull {
val module = library.config.findArendFile(it, command.isTest)
if (module == null) {
typecheckingErrorReporter.report(LibraryError.moduleNotFound(it, library.name))
} else if (command.definitionFullName == "") {
val sourcesModuleScopeProvider = typeCheckerService.libraryManager.getAvailableModuleScopeProvider(library)
val moduleScopeProvider = if (module.moduleLocation?.locationKind == ModuleLocation.LocationKind.TEST) {
val testsModuleScopeProvider = library.testsModuleScopeProvider
ModuleScopeProvider { modulePath ->
sourcesModuleScopeProvider.forModule(modulePath)
?: testsModuleScopeProvider.forModule(modulePath)
}
} else sourcesModuleScopeProvider
DefinitionResolveNameVisitor(concreteProvider, ArendReferableConverter, typecheckingErrorReporter).resolveGroup(module, ScopeFactory.forGroup(module, moduleScopeProvider))
}
module
}
if (command.definitionFullName == "") {
for (module in modules) {
reportParserErrors(module, module, typecheckingErrorReporter)
resetGroup(module)
}
for (module in modules) {
orderGroup(module, ordering)
}
} else {
val ref = modules.firstOrNull()?.findGroupByFullName(command.definitionFullName.split('.'))?.referable
if (ref == null) {
if (modules.isNotEmpty()) {
typecheckingErrorReporter.report(DefinitionNotFoundError(command.definitionFullName, modulePath))
}
} else {
val tcReferable = ArendReferableConverter.toDataLocatedReferable(ref)
val typechecked =
if (tcReferable is TCDefReferable) {
if (PsiLocatedReferable.isValid(tcReferable)) {
tcReferable.typechecked
} else {
typeCheckerService.dependencyListener.update(tcReferable)
null
}
} else null
if (typechecked == null || !typechecked.status().isOK) {
val definition = concreteProvider.getConcrete(ref)
if (definition is Concrete.Definition) {
typeCheckerService.dependencyListener.update(definition.data)
ordering.order(definition)
} else if (definition != null) error(command.definitionFullName + " is not a definition")
} else {
if (ref is PsiLocatedReferable) {
typecheckingErrorReporter.eventsProcessor.onTestStarted(ref)
typecheckingErrorReporter.eventsProcessor.onTestFinished(ref)
}
}
}
}
}
}
if (!indicator.isCanceled) {
val typechecking = TestBasedTypechecking(typecheckingErrorReporter.eventsProcessor, instanceProviderSet, typeCheckerService, concreteProvider, typecheckingErrorReporter, typeCheckerService.dependencyListener)
try {
typechecking.typecheckCollected(collector, ProgressCancellationIndicator(indicator))
typeCheckerService.project.service<BinaryFileSaver>().saveAll()
} finally {
typecheckingErrorReporter.flush()
typeCheckerService.project.afterTypechecking(typechecking.filesToRestart)
}
}
}
catch (_: ProcessCanceledException) {}
catch (e: Exception) {
Logger.getInstance(TypeCheckingService::class.java).error(e)
}
finally {
typecheckingErrorReporter.eventsProcessor.onSuitesFinished()
ApplicationManager.getApplication().executeOnPooledThread {
destroyProcessImpl() //we prefer to call this method rather than "this@TypeCheckProcessHandler.destroyProcess()" for if processHandler state is not equal to PROCESS_RUNNING then destroyProcessImpl will not be invoked (this is true e.g. in the case when the user stops computation using Detach Process button)
}
}
}
}