Skip to content

Commit

Permalink
splitted server into server and lobby
Browse files Browse the repository at this point in the history
  • Loading branch information
fastrich committed Aug 14, 2023
1 parent cb4edfe commit 9cc60d9
Show file tree
Hide file tree
Showing 6 changed files with 286 additions and 69 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -39,7 +39,7 @@ object ConcreteServerEndpoints extends ServerEndpoints {
* Since JSON is the default encoding in the frameit-mmt project, almost all endpoints should be aggregated by
* this function. Only some debugging endpoints might go to [[getPlaintextEndpointsForState()]].
*/
private def getJSONEndpointsForState(state: ServerState) =
private def getJSONEndpointsForState(state: LobbyState) =
addFact(state) :+: bulkaddFacts(state) :+: listFacts(state) :+: listAllScrolls(state) :+: listScrolls(state) :+:
applyScroll(state) :+: dynamicScroll(state) :+:
// meta/debug endpoints:
Expand All @@ -52,9 +52,9 @@ object ConcreteServerEndpoints extends ServerEndpoints {
* Since JSON is the default encoding in the frameit-mmt project, only some debugging endpoints should be
* aggregated here.
*/
private def getPlaintextEndpointsForState(state: ServerState) = printSituationTheory(state)
private def getPlaintextEndpointsForState(state: LobbyState) = printSituationTheory(state)

override protected def getCompiledOverallEndpoint(state: ServerState): Endpoint.Compiled[IO] = {
override protected def getCompiledOverallEndpoint(state: LobbyState): Endpoint.Compiled[IO] = {
def asUTF8[T](endpoint: Endpoint[IO, T]): Endpoint[IO, T] = {
endpoint.transformOutput(_.map(_.withCharset(StandardCharsets.UTF_8)))
}
Expand All @@ -76,29 +76,30 @@ object ConcreteServerEndpoints extends ServerEndpoints {
Ok(()) // unreachable anyway, but needed for typechecking
}

private def checkSituationSpace(state: ServerState): Endpoint[IO, List[api.Error]] = get(path("debug") :: path("space") :: path("check")) {
// ServerState to LobbyState
private def checkSituationSpace(state: LobbyState): Endpoint[IO, List[api.Error]] = get(path("debug") :: path("space") :: path("check")) {
Ok(state.check())
}

private def printSituationTheory(state: ServerState): Endpoint[IO, String] = get(path("debug") :: path("space") :: path("print")) {
private def printSituationTheory(state: LobbyState): Endpoint[IO, String] = get(path("debug") :: path("space") :: path("print")) {
Ok(state.presenter.asString(state.situationSpace))
}
// ---------------------------------------

// REAL ENDPOINTS FOR USE BY GAME ENGINE
// --------------------------------------- (up to the end of the file)
private def buildArchiveLight(state: ServerState): Endpoint[IO, Unit] = post(path("archive") :: path("build-light")) {
private def buildArchiveLight(state: LobbyState): Endpoint[IO, Unit] = post(path("archive") :: path("build-light")) {
state.ctrl.handleLine(s"build ${FrameWorld.archiveID} mmt-omdoc Scrolls")
Ok(())
}

private def buildArchive(state: ServerState): Endpoint[IO, Unit] = post(path("archive") :: path("build")) {
private def buildArchive(state: LobbyState): Endpoint[IO, Unit] = post(path("archive") :: path("build")) {
state.ctrl.handleLine(s"build ${FrameWorld.archiveID} mmt-omdoc")

Ok(())
}

private def reloadArchive(state: ServerState): Endpoint[IO, Unit] = post(path("archive") :: path("reload")) {
private def reloadArchive(state: LobbyState): Endpoint[IO, Unit] = post(path("archive") :: path("reload")) {
state.ctrl.backend.getArchive(FrameWorld.archiveID).map(frameWorldArchive => {
val root = frameWorldArchive.root

Expand All @@ -109,7 +110,7 @@ object ConcreteServerEndpoints extends ServerEndpoints {
}).getOrElse(NotFound(new Exception("MMT backend did not know FrameWorld archive by ID, but upon server start it did apparently (otherwise we would have aborted there). Something is inconsistent.")))
}

private def addFact_(state: ServerState, fact: SFact): Either[FactValidationException, FactReference] = {
private def addFact_(state: LobbyState, fact: SFact): Either[FactValidationException, FactReference] = {
val factConstant = fact.toFinalConstant(state.nextFactPath())

def makeException(errors: List[api.Error]): FactValidationException = {
Expand Down Expand Up @@ -141,41 +142,41 @@ object ConcreteServerEndpoints extends ServerEndpoints {
}
}

private def addFact(state: ServerState): Endpoint[IO, FactReference] = post(path("fact") :: path("add") :: jsonBody[SFact]) { (fact: SFact) => {
private def addFact(state: LobbyState): Endpoint[IO, FactReference] = post(path("fact") :: path("add") :: jsonBody[SFact]) { (fact: SFact) => {
addFact_(state, fact) match {
case Left(exception) => NotAcceptable(exception)
case Right(factRef) => Ok(factRef)
}
}}

private def bulkaddFacts(state: ServerState): Endpoint[IO, List[(Option[FactReference], String)]] = post(path("fact") :: path("bulkadd") :: jsonBody[List[SFact]]) { (facts: List[SFact]) => {
private def bulkaddFacts(state: LobbyState): Endpoint[IO, List[(Option[FactReference], String)]] = post(path("fact") :: path("bulkadd") :: jsonBody[List[SFact]]) { (facts: List[SFact]) => {
Ok(facts.map(addFact_(state, _)).map {
case Left(exception) => (None, exception.toString)
case Right(factRef) => (Some(factRef), "")
})
}}

private def listFacts(state: ServerState): Endpoint[IO, List[SFact]] = get(path("fact") :: path("list")) {
private def listFacts(state: LobbyState): Endpoint[IO, List[SFact]] = get(path("fact") :: path("list")) {
Ok(
Fact
.findAllIn(state.situationTheory, recurseOnInclusions = true)(state.ctrl)
.map(_.toSimple(state.ctrl))
)
}

private def listAllScrolls(state: ServerState): Endpoint[IO, List[SScroll]] = get(path("scroll") :: path("listall")) {
private def listAllScrolls(state: LobbyState): Endpoint[IO, List[SScroll]] = get(path("scroll") :: path("listall")) {
Ok(Scroll.findAll()(state.ctrl).map(_.renderSimple()(state.ctrl)))
}

private def listScrolls(state: ServerState): Endpoint[IO, List[SScroll]] = get(path("scroll") :: path("list")) {
private def listScrolls(state: LobbyState): Endpoint[IO, List[SScroll]] = get(path("scroll") :: path("list")) {
Ok(Scroll.findIncludedIn(state.situationTheory)(state.ctrl).map(_.renderSimple()(state.ctrl)))
}

private def applyScroll(state: ServerState): Endpoint[IO, SScrollApplicationResult] = post(path("scroll") :: path("apply") :: jsonBody[SScrollApplication]) { (scrollApp: SScrollApplication) =>
private def applyScroll(state: LobbyState): Endpoint[IO, SScrollApplicationResult] = post(path("scroll") :: path("apply") :: jsonBody[SScrollApplication]) { (scrollApp: SScrollApplication) =>
Scroll.fromReference(scrollApp.scroll)(state.ctrl) match {
case Some(scroll) =>
implicit val ctrl: Controller = state.ctrl
implicit val _state: ServerState = state
implicit val _state: LobbyState = state

val (scrollView, scrollViewPaths, errors) = prepScrollApplication(scrollApp)

Expand Down Expand Up @@ -239,7 +240,7 @@ object ConcreteServerEndpoints extends ServerEndpoints {
NotFound(InvalidScroll("Scroll not found or (meta)data invalid"))
}}

private def prepScrollApplication(scrollApp: SScrollApplication)(implicit state: ServerState): (View, List[Path], List[SCheckingError]) = {
private def prepScrollApplication(scrollApp: SScrollApplication)(implicit state: LobbyState): (View, List[Path], List[SCheckingError]) = {
// the scroll view and all paths (for later deletion from [[Controller]])
val (scrollView, scrollViewPaths) = {
val scrollViewName = state.nextScrollViewName()
Expand All @@ -259,7 +260,7 @@ object ConcreteServerEndpoints extends ServerEndpoints {
(scrollView, scrollViewPaths, errors)
}

private def getCompletions(scrollApp: SScrollApplication)(implicit state: ServerState): List[SScrollAssignments] = {
private def getCompletions(scrollApp: SScrollApplication)(implicit state: LobbyState): List[SScrollAssignments] = {
val canonicalCompletion = ViewCompletion.closeGaps(
scrollApp.assignments.toMMTList,
state.situationTheory.meta
Expand All @@ -272,11 +273,11 @@ object ConcreteServerEndpoints extends ServerEndpoints {
}
}

private def dynamicScroll(state: ServerState): Endpoint[IO, SDynamicScrollInfo] = post(path("scroll") :: path("dynamic") :: jsonBody[SScrollApplication]) { (scrollApp: SScrollApplication) =>
private def dynamicScroll(state: LobbyState): Endpoint[IO, SDynamicScrollInfo] = post(path("scroll") :: path("dynamic") :: jsonBody[SScrollApplication]) { (scrollApp: SScrollApplication) =>
Scroll.fromReference(scrollApp.scroll)(state.ctrl) match {
case Some(scroll) =>
implicit val ctrl: Controller = state.ctrl
implicit val _state: ServerState = state
implicit val _state: LobbyState = state

val (_, scrollViewPaths, errors) = prepScrollApplication(scrollApp)
val completions = getCompletions(scrollApp)
Expand Down
Empty file.
Original file line number Diff line number Diff line change
@@ -0,0 +1,161 @@
package info.kwarc.mmt.frameit.communication.server

import com.twitter.server.TwitterServer
import info.kwarc.mmt.api
import info.kwarc.mmt.api.frontend.{Controller, Logger, Report}
import info.kwarc.mmt.api.modules.Theory
import info.kwarc.mmt.api.objects.Context
import info.kwarc.mmt.api.presentation.MMTSyntaxPresenter
import info.kwarc.mmt.api.utils.{File, FilePath}
import info.kwarc.mmt.api.{ArchiveError, GeneralError, GlobalName, InvalidElement, LocalName, MPath}
import info.kwarc.mmt.frameit.archives.FrameIT.FrameWorld
import info.kwarc.mmt.frameit.business.{ContentValidator, SituationTheory, StandardContentValidator}

//?
import info.kwarc.mmt.api.frontend.{ConsoleHandler, Controller}

import java.util.concurrent.atomic.AtomicInteger

/**
* An object wrapping all mutable state our server endpoints below are able to mutate.
*
* It serves encapsulating state to be as immutable as possible.
*
* @todo Some parts are thread-safe (e.g. to multiple requests to the server), some are not.
* Current assumption is that everything is sequentially run only.
*/
class LobbyState(archiveRoot: File, debug: Boolean) extends Logger{

implicit val ctrl: Controller = new Controller() //private? But in then in ConcreteServerEndpoints Problems
// ctrl = new Controller()
ctrl.report.addHandler(ConsoleHandler)
ctrl.handleLine(s"log+ ${ServerState.logPrefix}")

ctrl.handleLine(s"mathpath archive ${archiveRoot}")
val frameitArchive = ctrl.backend.getArchive(FrameWorld.archiveID).getOrElse {
throw ArchiveError(FrameWorld.archiveID, "archive could not be found")
}

// force-read relational data as [[info.kwarc.mmt.frameit.business.datastructures.Scroll]] uses
// the depstore
frameitArchive.readRelational(FilePath("/"), ctrl, "rel")
// increase performance by prefetching archive content? ctrl.backend.getArchives.foreach(_.allContent)

val situationTheory_val = if (debug) Some(new SituationTheory(FrameWorld.debugSituationTheory)) else None
//val state = new ServerState(new StandardContentValidator, situationTheory)

//println(state.contentValidator.checkTheory(ctrl.getTheory(Path.parseM("http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace"))))
//sys.exit(0)


(if (debug) check() else Nil) match {
case Nil =>
println("Situation space successfully set-up and typechecked (the latter only in release mode).")
//state

case errors =>
errors.foreach(System.err.println)
throw InvalidElement(situationSpace, "Initial situation space does not typecheck, see stderr output for errors.")
}








val contentValidator = new StandardContentValidator //privat?
private val initialSituationTheory = if (debug) Some(new SituationTheory(FrameWorld.debugSituationTheory)) else None


// @SR: manage the following variables within lobbies
private val factCounter = new AtomicInteger(1)
private val scrollViewCounter = new AtomicInteger(1)
private val situationTheoryCounter = new AtomicInteger(1)

// @SR: maintain a list of lobbies here

// @SR: every pair (player, lobby) should have the notion of a current situation theory
var curSituationTheory: SituationTheory = initialSituationTheory.getOrElse {
new SituationTheory(FrameWorld.defaultRootSituationTheory).descend(nextSituationTheoryName())
}
println(s"Using situation space+theory: $situationSpace")

override val logPrefix: String = LobbyState.logPrefix
override protected def report: Report = ctrl.report

val presenter : MMTSyntaxPresenter = ctrl.extman.getOrAddExtension(classOf[MMTSyntaxPresenter], "present-text-notations").getOrElse(
throw GeneralError("could not get MMTSyntaxPresenter extension required for printing")
)

def situationSpace: Theory = curSituationTheory.spaceTheory
def situationTheory: Theory = curSituationTheory.theory


def nextScrollViewName(): LocalName = {
LocalName(s"ScrollView${scrollViewCounter.getAndAdd(1)}")
}

def nextSituationTheoryName(): LocalName = {
LocalName(s"SituationTheory${situationTheoryCounter.getAndAdd(1)}")
}

def nextFactPath(): GlobalName = {
this.synchronized {
val (factName, _) = Context.pickFresh(situationTheory.getInnerContext, LocalName(s"fact${factCounter.getAndAdd(1)}"))
situationTheory.path ? factName
}
}

def descendSituationTheory(name: LocalName): Theory = {
curSituationTheory = curSituationTheory.descend(name)
curSituationTheory.theory
}

def getPathForDescendedSituationTheory(name: LocalName): MPath = {
curSituationTheory.path.descend(name).module
}

def setSituationTheory(newSituationTheory: Theory): Unit = {
newSituationTheory.path match {
case MPath(doc, LocalName(steps :+ newName))
if doc == curSituationTheory.space.doc && steps == curSituationTheory.space.name.steps =>

curSituationTheory = new SituationTheory(curSituationTheory.path.descend(LocalName(newName)))

case _ =>
throw new Exception("New situation theory doesn't adhere to convention of where to store situation theories." +
s"Path was `${newSituationTheory.path}`.")
}
}

def getPathForView(name: LocalName): MPath = {
curSituationTheory.space.doc ? (curSituationTheory.space.name / name)
}

def check(): List[api.Error] = {
contentValidator.checkTheory(situationSpace)
}


/*
def initTwitterServer(): Unit = {
val restService = ConcreteServerEndpoints.getServiceForState(this)
val server = Http.serve(bindAddress(), restService)
onExit {
server.close()
}
Await.ready(server)
}*/


// make log methods from Logger public by trivially overriding them
// TODO logging does not work currently, messages go nowhere
override def log(e: api.Error): Unit = super.log(e)
override def log(s: => String, subgroup: Option[String] = None): Unit = super.log(s, subgroup)
}

object LobbyState {
val logPrefix = "frameit-mmt-server_lobby"
}
Original file line number Diff line number Diff line change
Expand Up @@ -24,12 +24,14 @@ object Server extends TwitterServer {
}

val state = initServerState(File(archiveRoot()))

val restService = ConcreteServerEndpoints.getServiceForState(state)
val server = Http.serve(bindAddress(), restService)
onExit {
server.close()
}


// Hack to run a dummy request to warm-up all MMT API caches and the JVM
//
// This reduces the time for a subsequent (user-initiated) request of /scroll/listall
Expand Down Expand Up @@ -63,10 +65,21 @@ object Server extends TwitterServer {
}
}.run() */


Await.ready(server)

}

def initServerState(archiveRoot: File): ServerState = {


def initServerState(archiveRoot: File): LobbyState = {

val state = new ServerState(archiveRoot, debug())
val lstate = state.initLobbyState_a()

lstate

/* to ServerState/LobbyState
implicit val ctrl: Controller = new Controller()
ctrl.report.addHandler(ConsoleHandler)
ctrl.handleLine(s"log+ ${ServerState.logPrefix}")
Expand Down Expand Up @@ -96,5 +109,8 @@ object Server extends TwitterServer {
errors.foreach(System.err.println)
throw InvalidElement(state.situationSpace, "Initial situation space does not typecheck, see stderr output for errors.")
}
*/
}

}
Original file line number Diff line number Diff line change
Expand Up @@ -73,9 +73,14 @@ trait ServerEndpoints extends Endpoint.Module[IO] {
import ServerErrorHandler._
// ^^^^^^^ END

protected def getCompiledOverallEndpoint(state: ServerState): Endpoint.Compiled[IO]
//protected def getCompiledOverallEndpoint(state: ServerState): Endpoint.Compiled[IO]
protected def getCompiledOverallEndpoint(state: LobbyState): Endpoint.Compiled[IO]

def getServiceForState(state: ServerState): Service[Request, Response] = {
//def getServiceForState(state: ServerState): Service[Request, Response] = {
// Endpoint.toService(filters(getCompiledOverallEndpoint(state)))
//}

def getServiceForState(state: LobbyState): Service[Request, Response] = {
Endpoint.toService(filters(getCompiledOverallEndpoint(state)))
}

Expand Down
Loading

0 comments on commit 9cc60d9

Please sign in to comment.