in src/main/kotlin/org/arend/typechecking/TypeCheckingService.kt [151:206]
fun initialize(): Boolean {
if (isInitialized) {
return false
}
synchronized(ArendPreludeLibrary::class.java) {
if (isInitialized) {
return false
}
// Initialize prelude
val preludeLibrary = ArendPreludeLibrary(project)
this.preludeLibrary = preludeLibrary
libraryManager.loadLibrary(preludeLibrary, null)
preludeLibrary.prelude?.generatedModuleLocation = Prelude.MODULE_LOCATION
if (Prelude.isInitialized()) {
val tcRefMap = preludeLibrary.prelude?.getTCRefMap(Referable.RefKind.EXPR)
if (tcRefMap != null) {
Prelude.forEach {
val name = it.referable.refLongName
tcRefMap[name] = it.referable as IntellijTCReferable
val dataRef = it.referable
if (dataRef is DataLocatedReferable) {
val ref = Scope.resolveName(preludeScope, name.toList())
if (ref is PsiLocatedReferable) {
dataRef.setPointer(ref)
}
}
}
}
}
val concreteProvider = PsiConcreteProvider(project, DummyErrorReporter.INSTANCE, null)
preludeLibrary.resolveNames(concreteProvider, libraryManager.libraryErrorReporter)
Prelude.PreludeTypechecking(InstanceProviderSet(), concreteProvider, ArendReferableConverter, PsiElementComparator).typecheckLibrary(preludeLibrary)
preludeLibrary.prelude?.let {
fillAdditionalNames(it, additionalNames)
}
// Set the listener that updates typechecked definitions
service<ArendPsiChangeService>().addListener(this)
// Listen for YAML files changes
val yamlFileListener = YAMLFileListener(project)
yamlFileListener.register()
EditorFactory.getInstance().eventMulticaster.addDocumentListener(yamlFileListener, project)
ModuleSynchronizer(project).install()
isInitialized = true
isLoaded = true
}
return true
}