Skip to content

Commit

Permalink
Merge pull request #584 from UniFormal/master
Browse files Browse the repository at this point in the history
Release 26
  • Loading branch information
Jazzpirate authored Oct 16, 2023
2 parents ad2c952 + 297b0e1 commit 157f664
Show file tree
Hide file tree
Showing 116 changed files with 5,796 additions and 2,929 deletions.
1 change: 1 addition & 0 deletions .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -37,6 +37,7 @@ target
out/

.DS_Store
*~

# Artifact of https://github.com/coursier/coursier when working with IntelliJ
src/null
3 changes: 2 additions & 1 deletion deploy/run-file.bat
Original file line number Diff line number Diff line change
Expand Up @@ -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
56 changes: 41 additions & 15 deletions src/build.sbt
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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"
)


Expand Down Expand Up @@ -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(
Expand All @@ -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")).
Expand Down
107 changes: 101 additions & 6 deletions src/frameit-mmt/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -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.**
Expand Down Expand Up @@ -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": "..."}`.
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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)
}
Expand All @@ -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),
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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}
Expand Down Expand Up @@ -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>",
))
}

Expand All @@ -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 {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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(
Expand Down Expand Up @@ -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,
Expand Down
Loading

0 comments on commit 157f664

Please sign in to comment.