Merge remote-tracking branch 'origin/devel' into newrelational

UniFormal · Jul 24, 2023 · 76099d8 · 76099d8
2 parents 01d9780 + 3ab0a26
commit 76099d8
Show file tree

Hide file tree

Showing 3 changed files with 24 additions and 6 deletions.
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
@@ -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
@@ -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
@@ -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) => ???
     }
   }