diff --git a/src/frameit-mmt/src/info/kwarc/mmt/frameit/communication/datastructures/Codecs.scala b/src/frameit-mmt/src/info/kwarc/mmt/frameit/communication/datastructures/Codecs.scala index d12c23ffb..2f48ce9e5 100644 --- a/src/frameit-mmt/src/info/kwarc/mmt/frameit/communication/datastructures/Codecs.scala +++ b/src/frameit-mmt/src/info/kwarc/mmt/frameit/communication/datastructures/Codecs.scala @@ -6,7 +6,7 @@ import info.kwarc.mmt.api.utils.mmt import info.kwarc.mmt.api.{GlobalName, MPath, NamespaceMap, Path} import info.kwarc.mmt.frameit.business.datastructures.{FactReference, ScrollReference} import info.kwarc.mmt.frameit.communication.datastructures.DataStructures.{SCheckingError, SDynamicScrollInfo, SEquationSystemFact, SFact, SGeneralFact, SInvalidScrollAssignment, SMiscellaneousError, SNonTotalScrollApplication, SScroll, SScrollApplication, SScrollApplicationResult, SScrollAssignments, SValueEqFact} -import info.kwarc.mmt.frameit.communication.datastructures.SOMDoc.{OMDocBridge, SFloatingPoint, SInteger, SOMA, SOMS, SRawOMDoc, SRecArg, SString, STerm} +import info.kwarc.mmt.frameit.communication.datastructures.SOMDoc.{OMDocBridge, SFloatingPoint, SFunction, SFunctionType, SInteger, SOMA, SOMS, SRawOMDoc, SRecArg, SString, STerm} import io.circe.Decoder.Result import io.circe.generic.extras.Configuration import io.circe.generic.extras.semiauto.{deriveConfiguredDecoder, deriveConfiguredEncoder} @@ -92,6 +92,8 @@ private[communication] object Codecs { classOf[SString] -> "OMSTR", classOf[SInteger] -> "OMI", classOf[SRecArg] -> "RECARG", + classOf[SFunction] -> "FUN", + classOf[SFunctionType] -> "FUNTYPE", classOf[SRawOMDoc] -> "RAW" )) } diff --git a/src/frameit-mmt/src/info/kwarc/mmt/frameit/communication/datastructures/DataStructures.scala b/src/frameit-mmt/src/info/kwarc/mmt/frameit/communication/datastructures/DataStructures.scala index 4d5beda70..48bc233db 100644 --- a/src/frameit-mmt/src/info/kwarc/mmt/frameit/communication/datastructures/DataStructures.scala +++ b/src/frameit-mmt/src/info/kwarc/mmt/frameit/communication/datastructures/DataStructures.scala @@ -83,7 +83,7 @@ object DataStructures { * That is, it represents the most general form of facts. * * Overall, facts sent by the game engine or parsed from existing MMT formalizations - * should only become [[SGeneralFact]]s if other fact types don't match (most + * should only become [[SGeneralFact]]s if other fact types are not suitable (most * importantly [[SValueEqFact]]). */ sealed case class SGeneralFact( @@ -112,8 +112,8 @@ object DataStructures { /** * Represents facts of the form * - * - ''fact: Σ x: valueTp. ⊦ lhs ≐ x'' and - * - ''fact: Σ x: valueTp. ⊦ lhs ≐ x❘ = ⟨value, proof⟩''. + * - ''fact: Σ x: valueTp. ⊦ lhs ≐ x'' and + * - ''fact: Σ x: valueTp. ⊦ lhs ≐ x❘ = ⟨value, proof⟩''. * * If no valueTp is given, it is tried to infer it from value -- if that is given. * If inference fails (so far only works for real literals as values) or no value is given, diff --git a/src/frameit-mmt/src/info/kwarc/mmt/frameit/communication/datastructures/SOMDoc.scala b/src/frameit-mmt/src/info/kwarc/mmt/frameit/communication/datastructures/SOMDoc.scala index 0ffac59e8..d0e8be5ad 100644 --- a/src/frameit-mmt/src/info/kwarc/mmt/frameit/communication/datastructures/SOMDoc.scala +++ b/src/frameit-mmt/src/info/kwarc/mmt/frameit/communication/datastructures/SOMDoc.scala @@ -2,9 +2,9 @@ package info.kwarc.mmt.frameit.communication.datastructures import info.kwarc.mmt.frameit.archives.FrameIT.FrameWorld.{PosOrIntLiterals, RealLiterals, StringLiterals} import info.kwarc.mmt.api.GlobalName -import info.kwarc.mmt.api.objects.{OMA, OML, OMS, Term} +import info.kwarc.mmt.api.objects.{Context, OMA, OMBIND, OML, OMS, Term, VarDecl} import info.kwarc.mmt.frameit.archives.FrameIT.FrameWorld -import info.kwarc.mmt.lf.ApplySpine +import info.kwarc.mmt.lf.{ApplySpine, Arrow, FunTerm, FunType, Lambda} import info.kwarc.mmt.odk.LFX.{Product, Tuple} import io.circe.Json import io.circe.generic.extras.ConfiguredJsonCodec @@ -44,6 +44,12 @@ object SOMDoc { @ConfiguredJsonCodec case class SRecArg(name: String, value: STerm) extends STerm + @ConfiguredJsonCodec + case class SFunction(params: List[(String, STerm)], body: STerm) extends STerm + + @ConfiguredJsonCodec + case class SFunctionType(params: List[STerm], ret: STerm) extends STerm + /** * OMDoc terms that could not be represented with other SOMDoc case classes. * @@ -82,6 +88,12 @@ object SOMDoc { // for everything not from LFX, only support LF function application case ApplySpine(fun, args) => SOMA(encode(fun), args.map(encode)) + case FunTerm(params, body) => + // TODO: this might swallow named parameters + SFunction(params.map(_._2).map(encode), encode(body)) + case FunType(params, ret) => + // TODO: this might swallow named parameters + SFunctionType(params.map(_._2).map(encode), encode(ret)) case PosOrIntLiterals(value) => if (value.isValidInt) { @@ -112,6 +124,10 @@ object SOMDoc { case SInteger(value) => PosOrIntLiterals(value) case SFloatingPoint(value) => RealLiterals(value) case SString(value) => StringLiterals(value) + + // no cases for SFunction and SFunctionType since so far the game engine + // never sends functions to the MMT side + case SRawOMDoc(rawXml) => ??? } }