Skip to content

Commit

Permalink
feat(mmt-lsp): go-to-definition for module references
Browse files Browse the repository at this point in the history
  • Loading branch information
@ComFreek
ComFreek committed Jan 25, 2024
1 parent f7dfbda commit 07fab6a
Showing 1 changed file with 109 additions and 47 deletions.
156 changes: 109 additions & 47 deletions src/mmt-lsp/src/info/kwarc/mmt/lsp/mmt/MMTFile.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,13 +7,31 @@ import info.kwarc.mmt.api.frontend.Controller
import info.kwarc.mmt.api.metadata.HasMetaData
import info.kwarc.mmt.api.modules.Theory
import info.kwarc.mmt.api.notations.Pragmatics
import info.kwarc.mmt.api.objects.{OMA, OMMOD, Traverser}
import info.kwarc.mmt.api.objects._
import info.kwarc.mmt.api.parser._
import info.kwarc.mmt.api.symbols._
import info.kwarc.mmt.api.utils.URI
import info.kwarc.mmt.lsp.{AnnotatedDocument, ClientWrapper, LSPDocument}
import org.eclipse.lsp4j.SymbolKind

/**
* TODOs
*
* - We cannot have two annotations on the same textual range of an [[MMTFile]] that provide *complementary* information
* because [[AnnotatedDocument.Annotations.addReg()]] cannot cope with that.
* It - if I'm not mistaken (I didn't write that code) - assumes that annotations on the same textual range are
* redundant.
*
* But we would like sometimes to have two complementary annotations on the exact same textual range.
* For example, when have an MMT file with code `theory T : ?SomeMeta`, we may want to have a `meta ?SomeMeta`
* field in VSCode's outline (which builds on an annotation on `?SomeMeta`) and *complementarily* have a second
* annotation on `?SomeMeta` that provides a go-to-by-definition to the source of `SomeMeta`.
* Of course, we could change our code such that we only produce one annotation.
* However, that would make some of our nice recursive algorithms non-compositional, stateful, and ugly.
*
*/


/**
* Language Server Protocol specific functionality for MMT documents and files.
*/
Expand Down Expand Up @@ -113,24 +131,62 @@ class MMTFile(uri: String, client: ClientWrapper[MMTClient], server: MMTLSPServe
}
case t: Theory =>
forSource(t) { reg => Annotations.addReg(t, reg, SymbolKind.Module, t.name.toString, true) }
t.metaC.get.foreach(mt => {
annotateTerm(mt, Context.empty)

/*
todo: For now we cannot a possibly clashing annotation to possibly the exact same range as `mt`
because of the issue elaborated on at the beginning of this file.
forSource(mt) { mtReg =>
Annotations.addReg(mt, mtReg, SymbolKind.Field, s"meta ${mt.head.map(_.name.toString).getOrElse("??")}")
}
*/
})

t.getPrimitiveDeclarations.foreach(annotateElement)
case d: DerivedDeclaration =>
forSource(d) { reg => Annotations.addReg(d, reg, SymbolKind.Struct, d.name.toString, true) }
d.getPrimitiveDeclarations.foreach(annotateElement)
case s: Structure =>
val shortFromName = s.from match {
case OMMOD(mp) => mp.name.toString
case OMA(OMMOD(mp), _) => mp.name.toString
case t => t.toString // default to full-blown stringification
}
forSource(s) { reg =>
Annotations.addReg(s, reg, SymbolKind.Constant, s.from match {
case OMMOD(mp) => mp.toString
case OMA(OMMOD(mp), _) => mp.toString
case _ =>
print("")
???
}, !s.isInclude)
Annotations.addReg(
s,
reg,
SymbolKind.Constant,
if (s.isInclude) s"include $shortFromName" else s"structure $shortFromName",
!s.isInclude
)
}
/*
todo: For now we cannot a possibly clashing annotation to possibly the exact same range as `dom`
to have a `domain: ?from`-style thing in VSCode's outline.
The reason is described at the beginning of this file.
forSource(s.from) { tpReg =>
val a = Annotations.addReg(
s.from,
tpReg,
// for brevity, hide include domains in outline view since they are already reproduced by the upper
// annotation created above for the whole structure/include
if (s.isInclude) null else SymbolKind.Field,
s"domain: $shortFromName"
)
a.setHover {
s.from.toString
}
}
*/
annotateTerm(s.from, Context.empty)

s.getPrimitiveDeclarations.foreach(annotateElement)
case c: Constant =>
forSource(c) { reg => Annotations.addReg(c, reg, SymbolKind.Constant, c.name.toString, true) }
val hl = new HighlightList(c)

c.getComponents.collect {
case x if x.value.isInstanceOf[TermContainer] => (x.key, x.name, x.value.asInstanceOf[TermContainer])
Expand All @@ -142,12 +198,12 @@ class MMTFile(uri: String, client: ClientWrapper[MMTClient], server: MMTLSPServe
forSource(t) { reg =>
Annotations.addReg(tc, reg, SymbolKind.Object, key.toString, true)
}
annotateTerm(t, hl)
annotateTerm(t, Context(c.parent))
}

case rc: RuleConstant =>
forSource(rc) { reg =>
val a = Annotations.addReg(rc, reg, SymbolKind.Constant, rc.name.toString)
val a = Annotations.addReg(rc, reg, SymbolKind.Constant, s"rule ${rc.name.toString}")
a.setHover {
rc.df.map(_.getClass.getCanonicalName).getOrElse("could not determine fully qualified name of instantiated rule class")
}
Expand All @@ -160,20 +216,6 @@ class MMTFile(uri: String, client: ClientWrapper[MMTClient], server: MMTLSPServe
print("")
}

private class HighlightList(val parent: Constant) {
lazy val th = controller.get(parent.parent)

private def cmeta(se: StructuralElement): Option[MPath] = se match {
case t: Theory => t.meta
case d: Declaration => cmeta(controller.get(d.parent))
case _ =>
print("")
None
}

lazy val meta = cmeta(th)
}

private val pragmatics = controller.extman.get(classOf[Pragmatics]).headOption

/**
Expand All @@ -183,11 +225,11 @@ class MMTFile(uri: String, client: ClientWrapper[MMTClient], server: MMTLSPServe
*
* @see [[annotateElement]] for the same task on the level of [[StructuralElement]]s
*/
private object annotateTerm extends Traverser[HighlightList] {
private object annotateTerm extends StatelessTraverser {

import info.kwarc.mmt.api.objects._

def traverse(t: Term)(implicit con: Context, state: HighlightList): Term = {
override def traverse(t: Term)(implicit con: Context, state: Unit): Term = {
/* def infer(tm : Term) = Try(Solver.infer(controller,Context(state.th.path match {
case mp : MPath => mp
case gn : GlobalName => gn.module
Expand Down Expand Up @@ -225,6 +267,19 @@ class MMTFile(uri: String, client: ClientWrapper[MMTClient], server: MMTLSPServe
})
}
Traverser(this, t)

case tm@OMAorAny(dom@OMMOD(mp), args) =>
forSource(dom) { reg =>
val a = Annotations.addReg(dom, reg, null, mp.name.toString)
a.setHover { mp.toString }

// "GO TO INCLUDE/DOMAIN" functionality on OMMOD terms
addDefinitionForSourceRef(mp, Seq(a))
}

args.foreach(Traverser(this, _))
tm

case tm if tm.head.isDefined =>
lazy val pragma = pragmatics.map(_.mostPragmatic(tm)).getOrElse(tm)

Expand Down Expand Up @@ -253,26 +308,14 @@ class MMTFile(uri: String, client: ClientWrapper[MMTClient], server: MMTLSPServe
}))

val headFromMeta = pragma.head.exists(p => {
state.meta.exists(mt => controller.library.hasImplicit(p.module, mt))
con.getIncludes.exists(mp => controller.library.hasImplicit(p.module, mp))
})
if (headFromMeta) {
annotations.foreach(_.setSemanticHighlightingClass(Colors.termconstantmeta))
}

// "GO TO DEFINITION" functionality on terms
// =================================================
val headDecl = pragma.head.flatMap(controller.getO)
headDecl.flatMap(SourceRef.get).foreach((src: SourceRef) => {
server.resolveSourceFilepath(src) foreach(originFile => {
val originRegion = src.region

annotations.foreach(_.addDefinitionLC(
originFile.toURI.getPath,
(originRegion.start.line, originRegion.start.column),
(originRegion.end.line, originRegion.end.column)
))
})
})
pragma.head.foreach(addDefinitionForSourceRef(_, annotations))
}

Traverser(this, t)
Expand All @@ -291,7 +334,7 @@ class MMTFile(uri: String, client: ClientWrapper[MMTClient], server: MMTLSPServe
}
}

override def traverseContext(cont: Context)(implicit con: Context, state: HighlightList): Context = {
override def traverseContext(cont: Context)(implicit con: Context, state: Unit): Context = {
cont.foreach { vd =>
forSource(vd) { reg =>
val nreg = reg.copy(end = reg.start.copy(offset = reg.start.offset + vd.name.length, column = reg.start.column + vd.name.length))
Expand All @@ -306,11 +349,30 @@ class MMTFile(uri: String, client: ClientWrapper[MMTClient], server: MMTLSPServe
}
}

//private var annotated : AnnotatedText = null

//private var _highlights : List[Highlight] = Nil

//override def getHighlights: List[Highlight] = synchronized { _highlights }
/**
* Given some [[DocAnnotation annotations]], add go-to-definition functionality to them resolving to the textual
* range in the file, wherein the MMT element referred to by `p` was declared (if any such file or metadata
* information exists).
*
* For example, if you already have constructed an annotation and you would want it to resolve via go-to-definition
* to where the theory `http://cds.omdoc.org/mmt?TermsTypesKinds` is declared, call this method with this very
* path on your annotation.
* Your annotation will then get added a definition resolving (as of January 2024's state of urtheories) to
* a certain textual range within the file `lf.mmt` in the urtheories archive.
*/
private def addDefinitionForSourceRef(p: Path, annotations: Seq[DocAnnotation]): Unit = {
controller.getO(p).flatMap(SourceRef.get).foreach((src: SourceRef) => {
server.resolveSourceFilepath(src).foreach(originFile => {
val originRegion = src.region

annotations.foreach(_.addDefinitionLC(
originFile.toURI.getPath,
(originRegion.start.line, originRegion.start.column),
(originRegion.end.line, originRegion.end.column)
))
})
})
}

/**
* (Re)parse the whole MMT document and (re)set all LSP annotations and warnings.
Expand Down

0 comments on commit 07fab6a

Please sign in to comment.