diff --git a/src/mmt-api/resources/mmt-web/stex/queries.html b/src/mmt-api/resources/mmt-web/stex/queries.html new file mode 100644 index 0000000000..24a86da88c --- /dev/null +++ b/src/mmt-api/resources/mmt-web/stex/queries.html @@ -0,0 +1,55 @@ + + + + + + + + + + + + +
+

sTeX Queries

+
+ Queries: + + + +
+ Custom SPARQL Query:
(See here for the ontology used) + + +
+ Result: + 
{{n.short}}
{{n.long}}
+
+ + \ No newline at end of file diff --git a/src/mmt-api/resources/mmt-web/stex/queries.js b/src/mmt-api/resources/mmt-web/stex/queries.js new file mode 100644 index 0000000000..af0834b166 --- /dev/null +++ b/src/mmt-api/resources/mmt-web/stex/queries.js @@ -0,0 +1,42 @@ +angular.module('QueryApp', []).controller('QueryViewer', [ '$scope', '$http', function($scope, $http) { + + + + $scope.query_test = function() { + document.getElementById("query_return").innerHTML = "Loading..."; + $http.get('/:sTeX/query/test').success(function(data) { + document.getElementById("query_return").innerHTML = JSON.stringify(data,null,2); + }); + }; + + + + $scope.query_all = function() { + document.getElementById("query_return").innerHTML = "Loading..."; + $http.get('/:sTeX/query/all').success(function(data) { + document.getElementById("query_return").innerHTML = JSON.stringify(data,null,2); + }); + }; + $scope.query_all_undefined = function() { + document.getElementById("query_return").innerHTML = "Loading..."; + $http.get('/:sTeX/query/all_undefined').success(function(data) { + document.getElementById("query_return").innerHTML = JSON.stringify(data,null,2); + }); + }; + $scope.query_all_with_data = function() { + document.getElementById("query_return").innerHTML = "Loading..."; + $http.get('/:sTeX/query/all_with_data').success(function(data) { + document.getElementById("query_return").innerHTML = JSON.stringify(data,null,2); + }); + }; + $scope.do_query = function(s) { + document.getElementById("query_return").innerHTML = "Loading..."; + $http.post('/:query/sparql',s).success(function(data) { + document.getElementById("query_return").innerHTML = JSON.stringify(data,null,2); + }); + }; + $scope.queryString ="SELECT ?x WHERE { \n (|||)+ ?x .\n ?x .\n}"; + $scope.query_custom = function() { + $scope.do_query($scope.queryString) + }; +}]); \ No newline at end of file diff --git a/src/mmt-api/src/main/info/kwarc/mmt/api/ontology/ULO.scala b/src/mmt-api/src/main/info/kwarc/mmt/api/ontology/ULO.scala index f911e6fdbc..81a478d37a 100644 --- a/src/mmt-api/src/main/info/kwarc/mmt/api/ontology/ULO.scala +++ b/src/mmt-api/src/main/info/kwarc/mmt/api/ontology/ULO.scala @@ -592,8 +592,8 @@ object ULO { object RDFStore { val memory = URI.scheme("mmt") colon "memory" - def archive(id:String) = iri(memory.toString + "/archive#" + id) - def archiveId(iri: IRI) = if (iri.getNamespace == memory.toString + "/archive") { + def archive(id:String) = iri(memory.toString + "archive#" + id) + def archiveId(iri: IRI) = if (iri.getNamespace == memory.toString + "archive") { Some(iri.getLocalName) } else None import org.eclipse.rdf4j.rio.RDFFormat @@ -976,7 +976,10 @@ object SPARQL { sealed trait Object { def toObjString : String } - sealed trait Subject extends this.Object + sealed trait SubjectT extends this.Object + case class Subject(s:String) extends SubjectT { + def toObjString = "<" + s + ">" + } private case class Trans(p:Predicate) extends Predicate { def predString: String = p.predString + "+" @@ -998,17 +1001,17 @@ object SPARQL { } implicit def asPred(u:ULOPredicate): Predicate = UloPred(u) - private case class PathO(p:Path) extends Subject { + private case class PathO(p:Path) extends SubjectT { override def toObjString: String = "<" + pathToIri(p).toString + ">" } private case class IriO(i:IRI) extends Object { override def toObjString: String = "<" + i.toString + ">" } - case class V(s:String) extends Subject with Predicate { + case class V(s:String) extends SubjectT with Predicate { def toObjString = s"?$s" def predString: String = s"?$s" } - implicit def pathtosubject(p:Path): Subject = PathO(p) + implicit def pathtosubject(p:Path): SubjectT = PathO(p) implicit def classtoobject(p: ULOClass): Object = IriO(p.toIri) private case class SelectWhere(vars:List[String],where:SparqlQuery) extends SparqlQuery { @@ -1018,10 +1021,10 @@ object SPARQL { def WHERE(q : SparqlQuery): SparqlQuery = SelectWhere(`var`.toList,q) } import org.eclipse.rdf4j.sparqlbuilder.core.query.Queries._ - case class T(subject: Subject,predicate: this.Predicate,`object`:this.Object) extends SparqlQuery { + case class T(subject: SubjectT, predicate: this.Predicate, `object`:this.Object) extends SparqlQuery { def queryString: String = s"${subject.toObjString} ${predicate.predString} ${`object`.toObjString} ." } - case class HASTYPE(subject: Subject,`object`:this.Object) extends SparqlQuery { + case class HASTYPE(subject: SubjectT, `object`:this.Object) extends SparqlQuery { override def queryString: String = s"${subject.toObjString} ${`object`.toObjString} ." } diff --git a/src/mmt-stex/src/info/kwarc/mmt/stex/Extensions/QueryExtension.scala b/src/mmt-stex/src/info/kwarc/mmt/stex/Extensions/QueryExtension.scala new file mode 100644 index 0000000000..24cf4c873d --- /dev/null +++ b/src/mmt-stex/src/info/kwarc/mmt/stex/Extensions/QueryExtension.scala @@ -0,0 +1,83 @@ +package info.kwarc.mmt.stex.Extensions + +import info.kwarc.mmt.api.{GlobalName, Path} +import info.kwarc.mmt.api.ontology.SPARQL.T +import info.kwarc.mmt.api.ontology.ULO +import info.kwarc.mmt.api.utils.{JSONArray, JSONNull, JSONObject, JSONString} +import info.kwarc.mmt.api.web.ServerResponse.{JsonResponse, ResourceResponse} +import info.kwarc.mmt.api.web.{ServerRequest, ServerResponse} +import info.kwarc.mmt.stex.STeXServer + +trait QueryExtension { this : STeXServer => + protected def queryRequest(request: ServerRequest): ServerResponse = { + request.path.lastOption match { + case Some("all") => + JsonResponse(JSONArray(getAll.map(p => JSONString(p.toString)) :_*)) + case Some("all_undefined") => + JsonResponse(JSONArray(undefineds.map(p => JSONString(p.toString)): _*)) + case Some("all_with_data") => + JsonResponse(JSONArray(symbols_with_stuff.map(p => + JSONObject( + ("path", JSONString(p._1.toString)), + ("macro", p._2.map(s => JSONString("\\" + s)).getOrElse(JSONNull)), + //("notations", JSONArray(p._3.map(JSONString): _*)) + )):_*)) + case Some("test") => + JsonResponse(JSONArray(test.map(p => JSONString(p.toString)): _*)) + case _ => + ResourceResponse("stex/queries.html") + } + } + + private lazy val archives = controller.backend.getArchives.filter { a => + a.properties.get("format").contains("stex") + } + + private lazy val getAll: List[Path] = { // TODO hacky; should be more systematic + archives.flatMap(a => { + import info.kwarc.mmt.api.ontology.SPARQL._ + controller.depstore.query( + SELECT("x") WHERE ( + ( + T(Subject(s"mmt://memory/archive#${a.id}"), ULO.contains, V("y")) UNION + T(Subject(s"mmt://memory//archive#${a.id}"), ULO.contains, V("y")) + ) AND + T(V("y"),(ULO.contains | ULO.declares | ULO.specifies)+,V("x")) AND + HASTYPE(V("x"),ULO.constant) + ) + ).getPaths.filter(p => !p.asInstanceOf[GlobalName].module.parent.last.endsWith(".omdoc")) + }) + } + + private def symbols_with_stuff: List[(Path,Option[String])] = { + getAll.map{p => + (p, + controller.getO(p).flatMap(SHTMLContentManagement.getMacroName), + //SHTMLContentManagement.getNotations(p.asInstanceOf[GlobalName])(controller).map{n => n.notation.toString} + ) + } + } + + private def undefineds: List[Path] = { + getAll.filter{p => + import info.kwarc.mmt.api.ontology.SPARQL._ + controller.depstore.query( + SELECT("x") WHERE ( + T(p,ULO.docref,V("x")) UNION T(V("x"),ULO.defines,p) + ) + ).getPaths.isEmpty + } + } + + private def test: List[Path] = { + archives.flatMap(a => { + import info.kwarc.mmt.api.ontology.SPARQL._ + controller.depstore.query( + SELECT("x") WHERE ( + T(Subject(s"mmt://memory/archive#${a.id}"), ULO.contains, V("x")) UNION + T(Subject(s"mmt://memory//archive#${a.id}"), ULO.contains, V("x")) + ) + ).getPaths + }) + } +} diff --git a/src/mmt-stex/src/info/kwarc/mmt/stex/STeXServer.scala b/src/mmt-stex/src/info/kwarc/mmt/stex/STeXServer.scala index e7250c275d..157f218e69 100644 --- a/src/mmt-stex/src/info/kwarc/mmt/stex/STeXServer.scala +++ b/src/mmt-stex/src/info/kwarc/mmt/stex/STeXServer.scala @@ -8,7 +8,7 @@ import info.kwarc.mmt.api.presentation.Presenter import info.kwarc.mmt.api.utils.time.Time import info.kwarc.mmt.api.utils.{File, FilePath, JSON, JSONArray, JSONObject, JSONString, MMTSystem, XMLEscaping} import info.kwarc.mmt.api.web.{ServerExtension, ServerRequest, ServerResponse} -import info.kwarc.mmt.stex.Extensions.{Definienda, ExportExtension, FrontendExtension, NotationExtractor, OMDocHTML, OMDocSHTMLRules, SHTMLBrowser, SHTMLContentManagement, SHTMLDocumentServer, STeXRelationals} +import info.kwarc.mmt.stex.Extensions.{Definienda, ExportExtension, FrontendExtension, NotationExtractor, OMDocHTML, OMDocSHTMLRules, QueryExtension, SHTMLBrowser, SHTMLContentManagement, SHTMLDocumentServer, STeXRelationals} import info.kwarc.mmt.stex.lsp.{MathHubServer, RemoteLSP, STeXLSPServer, SearchResultServer} import info.kwarc.mmt.stex.rules.MathStructureFeature import info.kwarc.mmt.stex.vollki.{FullsTeXGraph, JupyterBookArchive, VirtualArchive, VollKi} @@ -24,7 +24,8 @@ case class ErrorReturn(s : String) extends Throwable { } -class STeXServer extends ServerExtension("sTeX") with OMDocSHTMLRules with SHTMLDocumentServer with SHTMLBrowser with OMDocHTML with ExportExtension with FrontendExtension { +class STeXServer extends ServerExtension("sTeX") with OMDocSHTMLRules with SHTMLDocumentServer with SHTMLBrowser + with OMDocHTML with ExportExtension with FrontendExtension with QueryExtension { def ctrl = controller def getArchives = controller.backend.getStores.collect { case a : Archive if a.properties.get("format").contains("stex") => a @@ -101,6 +102,7 @@ class STeXServer extends ServerExtension("sTeX") with OMDocSHTMLRules with SHTML lazy val htmlpres = new MMTsTeXPresenter(texPresenter,xhtmlPresenter) override def apply(request: ServerRequest): ServerResponse = try { + if (request.path.startsWith(List(":sTeX","query"))) return queryRequest(request.copy(path=request.path.drop(2))) request.path.lastOption match { case Some("document" | "pdf" | "fullhtml" | "documentTop" | "fulldocument" | "fragment" | "rawfragment" | "symbol" | "declaration" | "variable" | "css" | "sections" | "definienda" | "lo" | "loraw") =>