Merge pull request #584 from UniFormal/master

Release 26
UniFormal · Oct 16, 2023 · 157f664 · 157f664
2 parents ad2c952 + 297b0e1
commit 157f664
Show file tree

Hide file tree

Showing 116 changed files with 5,796 additions and 2,929 deletions.
diff --git a/.gitignore b/.gitignore
@@ -37,6 +37,7 @@ target
 out/
 
 .DS_Store
+*~
 
 # Artifact of https://github.com/coursier/coursier when working with IntelliJ
 src/null
diff --git a/deploy/run-file.bat b/deploy/run-file.bat
@@ -2,4 +2,5 @@
 rem This is like run.bat except that it automatically loads an msl file passed as an argument.
 rem You may want to associate the msl file ending with this script.
 
-java -Xmx1024m -cp %~dp0/mmt.jar info.kwarc.mmt.api.frontend.Run :file %1
+call java -Xmx1024m -cp %~dp0/mmt.jar info.kwarc.mmt.api.frontend.Run :file %1
+pause
diff --git a/src/build.sbt b/src/build.sbt
@@ -176,7 +176,18 @@ lazy val src = (project in file(".")).
     // add the test folder to the test sources
     // but don't actually run any of them
     Test / scalaSource := baseDirectory.value / "test",
-    test := {}
+    test := {},
+
+    // This silences a dependency semver version conflict from the frameit project.
+    // It is necessary to have this silencing mechanism both in the frameit project
+    // and here in the super project (I guess because the version conflict somehow
+    // bubbles up?)
+    libraryDependencySchemes ++= Seq(
+      // see https://github.com/circe/circe-iteratee/issues/261
+      "io.circe" %% "circe-jawn" % VersionScheme.Always,
+      // see https://github.com/sbt/sbt/issues/7140#issuecomment-1464119328
+      "io.circe" % "circe-jawn_2.13" % VersionScheme.Always
+    )
   )
 
 // This is the main project. 'mmt/deploy' compiles all relevants subprojects, builds a self-contained jar file, and puts into the deploy folder, from where it can be run.
@@ -229,6 +240,11 @@ lazy val api = (project in file("mmt-api")).
     Compile / scalaSource := baseDirectory.value / "src" / "main",
     Compile / unmanagedJars ++= apiJars(utils.value),
     Test / unmanagedJars ++= apiJars(utils.value),
+    libraryDependencies += "org.eclipse.rdf4j" % "rdf4j-repository-sail" % "4.3.3",
+    libraryDependencies += "org.eclipse.rdf4j" % "rdf4j-sail-memory" % "4.3.3",
+    libraryDependencies += "org.eclipse.rdf4j" % "rdf4j-sparqlbuilder" % "4.3.3",
+    libraryDependencies += "org.eclipse.rdf4j" % "rdf4j-rio-rdfxml" % "4.3.3",
+    libraryDependencies += "org.eclipse.rdf4j" % "rdf4j-rio-binary" % "4.3.3"
   )
 
 
@@ -407,34 +423,45 @@ lazy val mizar = (project in file("mmt-mizar")).
 // use of MMT in the frameit system, here for ease of deployment but not part of the main mmt target
 // reponsible: Navid
 // finch is an HTTP server library (https://github.com/finagle/finch), a FrameIT dependency
-val finchVersion = "0.32.1"
-// Circe is a JSON library (https://circe.github.io/circe/), a FrameIT dependency
-val circeVersion = "0.13.0"
+val finchVersion = "0.34.1"
+
 lazy val frameit = (project in file("frameit-mmt"))
   .dependsOn(api, lf, odk)
   .settings(mmtProjectsSettings("frameit-mmt"): _*)
   .settings(
     libraryDependencies ++= Seq(
       //  a server infrastructure library
-      "com.twitter" %% "twitter-server" % "20.12.0",
+      "com.twitter" %% "twitter-server" % "22.12.0",
 
       // an incarnation of an HTTP server library for the above infrastructure
-      "com.github.finagle" %% "finchx-core" % finchVersion,
+      "com.github.finagle" %% "finch-core" % finchVersion,
       // with ability to automatically encode/decode JSON payloads via the circe library below
-      "com.github.finagle" %% "finchx-circe" % finchVersion,
-      "com.github.finagle" %% "finchx-generic" % finchVersion,
+      "com.github.finagle" %% "finch-circe" % finchVersion,
+      "com.github.finagle" %% "finch-generic" % finchVersion,
 
       // and with testing abilities
-      "com.github.finagle" %% "finchx-test" % finchVersion % "test",
-      "com.github.finagle" %% "finchx-json-test" % finchVersion % "test",
+      "com.github.finagle" %% "finch-test" % finchVersion % "test",
+      "com.github.finagle" %% "finch-json-test" % finchVersion % "test",
 
       "org.scalatest" %% "scalatest" % "3.2.3" % "test",
 
-      // a JSON library
-      "io.circe" %% "circe-generic" % circeVersion,
+      // io.circe is a JSON library
+      "io.circe" %% "circe-core" % "0.14.5",
+      "io.circe" %% "circe-parser" % "0.14.5",
       // with extras to support encoding/decoding a case class hierarchy
-      "io.circe" %% "circe-generic-extras" % circeVersion,
-      "io.circe" %% "circe-parser"  % circeVersion,
+      "io.circe" %% "circe-generic-extras" % "0.14.3"
+      // (as for why the versions for circe-core and circe-generic-extras are different, see
+      //  https://github.com/circe/circe-generic-extras/issues/279)
+    ),
+
+    // This silences a dependency semver version conflict.
+    // It is necessary to have this silencing mechanism both here and in the super project src
+    // (I guess because the version conflict somehow bubbles up?)
+    libraryDependencySchemes ++= Seq(
+      // see https://github.com/circe/circe-iteratee/issues/261
+      "io.circe" %% "circe-jawn" % VersionScheme.Always,
+      // see https://github.com/sbt/sbt/issues/7140#issuecomment-1464119328
+      "io.circe" % "circe-jawn_2.13" % VersionScheme.Always
     ),
 
     Compile / scalacOptions ++= Seq(
@@ -451,7 +478,6 @@ lazy val frameit = (project in file("frameit-mmt"))
     Compile / mainClass  := Some("info.kwarc.mmt.frameit.communication.server.Server"),
     assembly / mainClass := Some("info.kwarc.mmt.frameit.communication.server.Server")
   )
-
 
 // plugin for mathscheme-related functionality. Obsolete
 lazy val mathscheme = (project in file("mmt-mathscheme")).

diff --git a/src/frameit-mmt/README.md b/src/frameit-mmt/README.md
@@ -10,6 +10,7 @@ This is the server component of the [FrameIT project](https://uframeit.org), pri
 ## REST API
 
 We use UTF-8-encoded JSON payloads for both HTTP request and response bodies.
+All non-empty requests must employ `Content-Type: application/json`.
 All endpoints indicate success by a 2xx response status code and failure by any other status code.
 
 **Playground.**
@@ -215,12 +216,106 @@ JSON (sub)formats shared by multiple endpoints above.
     SOMDoc is a JSON representation of a subset of [OMDoc](https://www.omdoc.org/). It is simpler than the [OpenMath-JSON standard](https://omjson.kwarc.info/) and *almost* implements a subset of it.
     Below is a representative list of all possible SOMDoc terms as JSON:
     
-    - `{"kind": "OMS", "uri": /* MMT  URI */}`
-    - `{"kind": "OMA", "applicant": /* SOMDoc */, "arguments": /* array of SOMDoc */}`
-    - `{"kind": "OMI", "decimal": 42}`
-    - `{"kind": "OMF", "float": 0.1234}`
-    - `{"kind": "OMSTR", "string": "string in UTF-8"}`
-    - `{"kind": "RAW", "xml": "OMDoc XML as string in UTF-8"}` (our addition to the (insert link here to omdoc json standard))
+    - <details><summary>OMS</summary>
+	
+		```javascript
+		{
+			"kind": "OMS",
+			"uri": /* MMT  URI */
+		}
+		```
+		
+	  </details>
+	  
+    - <details><summary>OMA</summary>
+	
+		```javascript
+		{
+			"kind": "OMA", 
+			"applicant": /* SOMDoc */, 
+			"arguments": Array[/* SOMDoc */]
+		}
+		```
+		
+	  </details>
+	  
+    - <details><summary>OML</summary>
+	
+		```javascript
+		{
+			"kind": "OML", 
+			"name": /* string in UTF-8 */, 
+			"tp": /* optional type as SOMDoc*/, 
+			"df": /* optional defines as SOMDOc */
+		}
+		```
+		
+	  </details>
+	  
+    - <details><summary>FUNTYPE</summary>
+	
+		```javascript
+		{
+			"kind": "FUNTYPE",
+			"params": Array[/* types as SOMDoc */], 
+			"ret": /* type as SOMDOc */
+		}
+		```
+		
+	  </details>
+	  
+    - <details><summary>FUN</summary>
+	
+		```javascript
+		{
+			"kind": "FUN",
+			"params": Array[
+					{
+						"name": /* string in UTF-8 */, 
+						"type": /* SOMDOc */
+					}
+				], 
+			"body": /* SOMDOc */
+		}
+		```
+		
+	  </details>
+	  
+    - <details><summary>OMLIT</summary>
+	
+		```javascript
+		{
+			"kind": "OMLIT<Boolean>" | "OMLIT<Int32>" | "OMLIT<Double>" | "OMLIT<String>",
+			"type": /* MMT  URI */
+			"value": /*e.g.: true|false, 1, 0.675, "test-string"*/
+		}
+		```
+		With "kind" specifying the Type of "value" 
+		
+	  </details>
+	  
+    - <details><summary>Wrapper</summary>
+	
+		```javascript
+		{
+			"Wrapper": /* SOMDOc */
+		}
+		```
+		(Needed because of a bug in Serialization)
+		
+	  </details>
+	  
+    - <details><summary>RAW</summary>
+	
+		```javascript
+		{
+			"kind": "RAW", 
+			"xml": "OMDoc XML as string in UTF-8"
+		}
+		```
+		(our addition to the (insert link here to omdoc json standard))
+		
+	  </details>
     
     In contrast to OpenMath-JSON, OMS terms simply encode the full MMT URI as a string instead of specifying its components separately. (E.g., OpenMath-JSON would provide fields `cd`, `cdbase`, and `name`.)
     Moreover, as all but the last bullet point above only represent a subset of OMDoc, we need a way to encode unrepresented terms: we do so by `{kind: "RAW", "xml": "..."}`.

diff --git a/src/frameit-mmt/src/info/kwarc/mmt/frameit/business/datastructures/Fact.scala b/src/frameit-mmt/src/info/kwarc/mmt/frameit/business/datastructures/Fact.scala
@@ -72,14 +72,14 @@ sealed case class Fact(
   private def _toSimple(implicit ctrl: Controller): SFact = {
     val simplify: Term => Term = {
       val ctx = Context(ref.uri.module) ++ additionalContext
-      val simplificationRules: RuleSet = {
+      val simplificationRules: RuleSet = Fact.ruleCache.computeIfAbsent(ctx, _ => {
         val rules = RuleSet.collectRules(ctrl, ctx)
         rules.add(new LabelVerbalizationRule()(ctrl.globalLookup))
 
         rules
-      }
+      })
 
-      val simplicationUnit = SimplificationUnit(ctx, expandVarDefs = true, expandConDefs = true, fullRecursion = true)
+      val simplicationUnit = SimplificationUnit(ctx, expandVarDefs = true, expandConDefs = true, fullRecursion = false)
 
       ctrl.simplifier(_, simplicationUnit, simplificationRules)
     }
@@ -101,9 +101,16 @@ sealed case class Fact(
 
 object Fact {
   /**
-    * A cache to speed up [[Fact.toSimple]].
+    * A cache to speed up [[Fact.toSimple]] when one and the same fact is simplified over again.
     */
   private val sfactCache: ConcurrentHashMap[Fact, SFact] = new ConcurrentHashMap
+  /**
+    * A cache to speed up [[Fact.toSimple]] when facts are simplified in one and the same context (most likely the
+    * problem or solution theory).
+    * The cache stores [[RuleSet RuleSets]] because redundantly calling [[RuleSet.collectRules]] every time as part of
+    * [[Fact.toSimple]] is slow.
+    */
+  private val ruleCache: ConcurrentHashMap[Context, RuleSet] = new ConcurrentHashMap
 
   def fromConstant(c: Constant)(implicit ctrl: Controller): Fact = Fact(
     FactReference(c.path),

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._
 import io.circe.Decoder.Result
 import io.circe.generic.extras.Configuration
 import io.circe.generic.extras.semiauto.{deriveConfiguredDecoder, deriveConfiguredEncoder}
@@ -88,11 +88,21 @@ private[communication] object Codecs {
       implicit val somdocConfig: Configuration = kindedJsonConfig(Map(
         classOf[SOMA] -> "OMA",
         classOf[SOMS] -> "OMS",
-        classOf[SFloatingPoint] -> "OMF",
-        classOf[SString] -> "OMSTR",
-        classOf[SInteger] -> "OMI",
-        classOf[SRecArg] -> "RECARG",
-        classOf[SRawOMDoc] -> "RAW"
+        classOf[SVariable] -> "VAR",
+        // mapping as Wrapper for SFunction because of custom codec below
+        classOf[SFunction] -> "Wrapper",
+        classOf[SFunctionType] -> "FUNTYPE",
+        classOf[SRawOMDoc] -> "RAW",
+        classOf[SOML] -> "OML",
+        classOf[OMLITBool] -> "OMLIT<Boolean>",
+        classOf[OMLITByte] -> "OMLIT<Byte>",
+        classOf[OMLITShort] -> "OMLIT<Int16>",
+        classOf[OMLITInt] -> "OMLIT<Int32>",
+        classOf[OMLITLong] -> "OMLIT<Int64>",
+        classOf[OMLITFloat] -> "OMLIT<Single>",
+        classOf[OMLITDouble] -> "OMLIT<Double>",
+        classOf[OMLITChar] -> "OMLIT<Char>",
+        classOf[OMLITString] -> "OMLIT<String>",
       ))
     }
 
@@ -109,6 +119,19 @@ private[communication] object Codecs {
     implicit val termEncoder: Encoder[Term] = (tm: Term) => {
       stermEncoder(OMDocBridge.encode(tm))
     }
+
+    implicit val functionEncoder: Encoder[SFunction] = (f: SFunction) => {
+      Json.obj(
+        ("kind", Json.fromString("FUN")),
+        ("params", Json.arr(f.params.map {
+          case (argname, argtp) => Json.obj(
+            ("name", Json.fromString(argname)),
+            ("tp", stermEncoder(argtp))
+          )
+        } : _*)),
+        ("body", stermEncoder(f.body))
+      )
+    }
   }
 
   object DataStructureCodecs {

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,