Communication Format for Virtual World Updates

[richardmarcus]

We want a simple format to transmit updates to the virtual world (e.g. new facts: point, angle, etc) to MMT.
@Jazzpirate and @ComFreek should design the format.
It should be a JSON file but encode the information like this
OMS(p : URI)
Real(3.14159)
Point(3.1,2.8,0.3)
OMA(f,a1,...,an)
NewPoint(name,Point(...))
NewReal(name,Real(...))
NewFact(name,LeftSide,RightSide)
LeftSide ::= OMS | OMA
RightSide ::= Real | Point
name : |- \doteq
or maybe like this: https://gl.kwarc.info/FrameIT/blue/-/blob/master/interchange-language.md

To implement the requests on the Unity side, @richardmarcus and @SESch93 would like to know how the requests for the tree example should look in this format.

The following events are possible:

• point (coordinate)
• line (id1, id2)
• angle(id1, id2, id3)

We currently do not allow creation of lines or angles without creating points first.

[Jazzpirate]

Correction:
we want NewFact(name,LeftSide,RightSide), where LeftSide ::= OMS | OMA and RightSide ::= Real | Point
and which elaborates to name : |- LeftSide \doteq RightSide.

The following events are possible:
point (coordinate)
line (id1, id2)
angle(id1, id2, i3)
We currently do not allow creation of lines or angles without creating points first.

A line is given as a constructor (let's call it LfromP) taking two points as an argument - i.e. a line is really a term OMA(LfromP,p1,p2). An angle is (from the point of view of MMT) simply a real number, so all of those can be represented already, expect for when we want/need to create new constants for them.

If we really need constants of type Line, we need to think of a more general syntax for new declarations. I suspect we don't...?

[kohlhase]

I am getting a bit worried, that this is very FramWorld1-specific, and that the DSL will keep growing.
I think that a language that makes the concept of a MMT declaration a primitive would be better.
Instead of newPoint(foo,point(a,b,c)) I would prefer mmtdec(foo,point,OMA(point,a,b,c))
and instead of newFact(foo,left,right) similarly mmtdec(foo,prop,OMA(doteq,left,right)) here we could leave out the ded, since we always put it in for type prop.
That would at least keep the grammar finite, when we introduce lines, angles, ....

[Jazzpirate]

In that case, we can get rid of "Point" altogether and replace it by a generic tuple syntax (point is just R^3 anyway).

mmtdec(foo,prop,OMA(doteq,left,right)) <- that I would suggest we avoid unless necessary. The point was to simplify syntax for facts after all, with a built in sanity check that the kinds of facts we have really are all equations with a atomic term on the right.

[kohlhase]

In that case, we can get rid of "Point" altogether and replace it by a generic tuple syntax (point is just R^3 anyway).

I thought of point as the point constructor, actually I meant OMA(point,a,b,c).

[kohlhase]

mmtdec(foo,prop,OMA(doteq,left,right)) <- that I would suggest we avoid unless necessary. The point was to simplify syntax for facts after all, with a built in sanity check that the kinds of facts we have really are all equations with a atomic term on the right.

I can live with that. Facts are a UFrameIT level thing, not a particular-game-level thing.

[Jazzpirate]

In that case, we can get rid of "Point" altogether and replace it by a generic tuple syntax (point is just R^3 anyway).

I thought of point as the point constructor, actually I meant OMA(point,a,b,c).

actually, what we probably want ultimately is something like mmtdec(name,point,<x,y,z>) - that's what I meant by getting rid of "Point". The point constructor is just the \Sigma-type introduction form ;) Something like Tuple(x,y,z) would alos be okay. Either way, we can abstract away tuples from our specific current use case ("Point" in euclidean space)

[kohlhase]

yes, either way is good.

[ComFreek]

@Jazzpirate | the kinds of facts we have really are all equations with a atomic term on the right.

I still don't believe in this, but let's try it for FrameWorld-1 😄 @Jazzpirate can you come up with the sample JSON reponses by the MMT server that the OP asks for?

@kohlhase | That would at least keep the grammar finite, when we introduce lines, angles, ....

@kohlhase | I am getting a bit worried, that this is very FramWorld1-specific, and that the DSL will keep growing.

I resonate with this. But I guess, let's just try it.

I looked a bit into whether JSON is still the right format for the tree structures that we have now.
I couldn't find a way to (JSON tree)-pattern match in C# easily as is, for instance, the case with Scala and XML:

xmlNode match {
  case <div>{{ x }}</div> => /* ... */
}

But then again C# and its ecosystem apparently don't support pattern matching that good. Support for it has only been introduced in C# 8.0 last year. I googled around for "c# json pattern matching", "c# xml pattern matching" and found nothing.
So we might as well stick to JSON and investigate a bit into UFrameIT API to smoothen gadget creation.

[kohlhase]

There must be a JSON library in C# which inputs JSON into objects, and then you can use the objects to pattern-match?

[Jazzpirate]

@Jazzpirate can you come up with the sample JSON reponses by the MMT server that the OP asks for?

Can you elaborate? i.e. which component wants to communicate what information to whom?

[ComFreek]

There must be a JSON library in C# which inputs JSON into objects, and then you can use the objects to pattern-match?

Yes, by an if-cascade, that I wanted to avoid. Oh, and @richardmarcus said that the native JSON library of Unity can only extract JSON whose structure is given by a class at compile time. So I guess we need to use another JSON library there?

Can you elaborate? i.e. which component wants to communicate what information to whom?

• If a user creates a new point in Unity, how does the request body to the MMT server look like in detail?
• If a user creates a new line from two previously existing points in Unity, how does the request body to the MMT server look like in detail?

[Jazzpirate]

First attempt:

1. Requests are JSON Arrays of length 2, the first element is the "kind" of request (as String), the second represents the specifics
2. The specifics of an "mmtdecl" request is a JSON Object with a name "name" and a definiens "def"
3. An OMS is is a JSON object with elements "DPath", "Theory" and "name", representing the MMT URI of the symbol
4. An OMA is a JSON object with elements "op" (a JSON encoding of a term) and "args" (a JSON Array of JSON encodings of terms)
5. A tuple is represented as OMA("tuple",args)
6. A floating point number is represented as a JSON string

If a user creates a new point in Unity, how does the request body to the MMT server look like in detail?

So user creates a point with name A and coordinates x,y,z. Then Unity sends to MMT e.g.:

["mmtdecl",{
  "name" : "A"
  "def" : {
    "op": "tuple"
    "args": ["x","y","z"]
  }
}]

If a user creates a new line from two previously existing points in Unity, how does the request body to the MMT server look like in detail?

There isn't technically a need for this, since a line is a term. If you want to name a line (i.e. generate a new constant for it), you can, but I'm not entirely sure that's necessary. Anyway, if you want to name the line from point p1 to point p2 as l, then:

["mmtdecl",{
  "name" : "l"
  "def" : {
    "op": {
      "DPath": "http://mathhub.info/MitM/core/geometry"
      "Theory": "Geometry/Common"
      "name": "lineOf"
    }
    "args": ["p1","p2"]
  }
}]

Note that once a MMT context is initialized (i.e. the virtual theory for the game world is created), we need to inform MMT that the meta-theory for the virtual theory is 3DGeometry, so that the constants in (the parametric theory) Geometry/Common are properly identified

[richardmarcus]

I don't think we should hardcode information like this inside Unity:

 "DPath": "http://mathhub.info/MitM/core/geometry"
 "Theory": "Geometry/Common"
 "name": "lineOf"

There should be something like a "database" file on the MMT side, which the server and or Unity can access to match lineOf(?) to its MMT URI.

[Jazzpirate]

I don't think we should hardcode information like this inside Unity:

I somewhat disagree. Unity needs to "hardcode" the concept of a line anyway, MMT doesn't. So MMT shouldn't hardcode (or provide) what the exact URI for a line is. To MMT, "line" is a constant identified via a URI and nothing more.

How you teach Unity which URI to match to which concept is up to you. I suggest something like an .ini file, so it can be easily adapted without having to recompile anything

[richardmarcus]

I am specifically refering to Geometry/Common and mathhub/... These do not belong to the concept of a line(?). In any case, the main problem I see is unnecessary duplication of information. Plus, if the dpath ever changes, it should not be required to adapt this in Unity.

[Jazzpirate]

I am specifically refering to Geometry/Common and mathhub/... These do not belong to the concept of a line(?).

Well, yes, they do. Both theory name and DPath are specific to the concept of a line. If you want to use circles, the theory name will be different. If you want to use gears, the DPath will be different as well.

In any case, the main problem I see is unnecessary duplication of information.

Which information is duplicated?

Plus, if the dpath ever changes, it should not be required to adapt this in Unity.

As I said: Ideally that information would be in a .ini or .cfg file or something. But if the dpath changes, then something in Unity will have to change, unless you want to hardcode every concept in both unity and the server.

[richardmarcus]

Ideally, I do not want to hardcode anything like that. I assumed that we can just crawl through the mmt files, extract a list of "Facts" and send this information to the server. This should allow us to just use the names during communication and fetch the remaining information when needed. Possibly, this could also serve as a specification for the Unity developer so that he knows which fact types are implemented on the MMT side.

[Jazzpirate]

I assumed that we can just crawl through the mmt files, extract a list of "Facts" and send this information to the server.

That's not going to work. MitM currently has hundreds of concepts and their URI's are (occasionally) non-trivial to compute.

This should allow us to just use the names during communication and fetch the remaining information when needed.

That won't work. There are already name clashes between e.g. lines in 2D and lines in 3D.

Either way, none of that changes the problem, that ultimately some component needs to tell MMT what the full URI for some concept that Unity wants to communicate is. Unity needs to hardcode that concept anyway, and Unity needs to send something to the server to communicate "this is a line". The URI does exactly that natively, so why invent an additional code on top of URIs that serves the exact same purpose?

[ComFreek]

I think I know where you're coming from, @richardmarcus: to you the MMT URI seems like a possibly changing artifact of a formalization, right? And that's why you don't want to hardcode it in Unity. (Neither should we in MMT by that reasoning.)

So if I understand you correctly, you propose that we make Unity only depend on an ontological middle layer that has concepts of points, lines etc. Then, via some alignment (from whatever source) of this ontology to the MMT formalization, the MMT server can translate between them.

But then how do you know which arguments a point or a line takes? Basically, you would need to extend this ontological middle layer by a concept of arguments. I think you'll end up with a subset of MMT syntax.

Perhaps it helps to view OMDoc documents as both ontologies and formalizations in one thing. Possibly, we could separate the ontological from the purely formalization-technical parts by structuring the theories in the right way. In a sense, you want an ontological interface exported by the formalization.

[Jazzpirate]

only depend on an ontological middle layer that has concepts of points, lines etc.

In a sense, you want an ontological interface exported by the formalization.

...we do have such an ontological middle layer, consisting of ontological interfaces. It's called Math-in-the-Middle and is written in MMT xD

No, seriously, that's exactly why MitM was developed ;)

[ComFreek]

Cool, haven't seen MitM in that light yet.

Would you say gadgets (ideally whole Unity side) depending on MitM is okay, but it must not depend on FrameIT/frameworld in any way?
Or rather: if a gadget uses a concept in FrameIT/frameworld, we should move it to MitM.

[Jazzpirate]

Cool, haven't seen MitM in that light yet.

See https://research-repository.st-andrews.ac.uk/bitstream/handle/10023/8918/Dehaye_2016_OpenDreamKit_CICM_AAM.pdf?sequence=1 ;)

Would you say gadgets (ideally whole Unity side) depending on MitM is okay, but it must not depend on FrameIT/frameworld in any way?
Or rather: if a gadget uses a concept in FrameIT/frameworld, we should move it to MitM.

I'm not certain. All "pure math" (and ultimately all physics) concepts belong to MitM, but I can in theory imagine gadgets based on more game-specific ideas...

[richardmarcus]

I still think that having an alias instead of the full URI would have advantages in the future but this wasn't meant as a crucial issue so we can go with the proposed format concept. I would just make a few structural changes for simpler serialization:

{
  "type": "mmtdecl",
  "detail": {
  "name" : "A"
  "def" : {
    "DPath": ""
    "Theory": ""
    "op": "tuple"
    "args": ["x","y","z"]
  }
}
}

or

{
  "type": "mmtdecl",
  "name" : "A"
  "def" : {
    "DPath": ""
    "Theory": ""
    "op": "tuple"
    "args": ["x","y","z"]
  }
}

The bigger part will be to adapt the server accordingly and make sure that scrolls work again. The Unity side only needs minor adaptions. I think the easiest way to test the server would just be to assume a dummy input (e.g. (0,0,0) (0,1,0) (0,1,1) etc).
How complete is the rework of the server + mmt-scroll- application? Do we need a separate issue for this?

[Jazzpirate]

I neither see how that as a simplification, nor what the semantics of / idea behind either of those is... why does the definiens of a declaration (i.e. a term) have a DPath and a Theory? Only URIs have/need DPath and Theory components, i.e. individual symbols...

[ComFreek]

For JSON (de)serialization of "inductive" class hierarchies, it seems one can build this very easily on top of the library JSON.NET for C#. Here are some pointers:

• https://stackoverflow.com/questions/11099466/using-a-custom-type-discriminator-to-tell-json-net-which-type-of-a-class-hierarc
• https://github.com/manuc66/JsonSubTypes
• https://github.com/dmitry-bym/JsonKnownTypes

Key words are: json.net subtypes, discriminator, TypeNameHandling

The repo behind the second link seems well-maintained. With that library one can do:

[JsonConverter(typeof(JsonSubtypes), "Kind")]
public interface IAnimal
{
    string Kind { get; }
}

public class Dog : IAnimal
{
    public string Kind { get; } = "Dog";
    public string Breed { get; set; }
}

public class Cat : IAnimal {
    public string Kind { get; } = "Cat";
    public bool Declawed { get; set;}
}

do get JSONs like {"Kind": "Dog", "Breed": "Terrier"} and {"Kind": "Cat", "Declawed": false}.
This should straightforwardly be adaptable to our OMDoc/MMT class hierarchy.

[richardmarcus]

Apart from that, we shouldn't make the language more difficult just because Unity sucks at handling JSON... or, really, because C# doesn't have nice pattern matching ;)

That sounds like we shouldn't use complicated URIs in the format just because MMT doesn't have nice URI aliasing. But I guess there is nothing wrong with using archive URLs in persistent identifiers :)

I don't understand the difference between Def and Def2 though, this looks like there might be another misunderstanding?

one uses a string and one uses an object of class OP (with using a single string for URI we will avoid this in this case)

Furthermore, quote Unity manual:
"If you don’t know the type of an object ahead of time, deserialize the JSON into a class or struct that contains “common” fields, and then use the values of those fields to work out what actual type you want. Then deserialize a second time into that type."

that seems more convenient than duplicating the whole class structure, tbh ;)

This îs the same what I have described, it relies on duplicating the class structure.

1. Deserialize into class with common fields --> based on DeciderClass { public string type} (we could use Request for this)
2. Depending on type, deserialize based on Request or Request1

[richardmarcus]

For JSON (de)serialization of "inductive" class hierarchies, it seems one can build this very easily on top of the library JSON.NET for C#.

do get JSONs like {"Kind": "Dog", "Breed": "Terrier"} and {"Kind": "Cat", "Declawed": false}.
This should straightforwardly be adaptable to our OMDoc/MMT class hierarchy.

This sounds interesting. Big question is if we can also deserialize these JSONs based on IAnimal and get the correct animal object

[richardmarcus]

This sounds interesting. Big question is if we can also deserialize these JSONs based on IAnimal and get the correct animal object

The answer seems to be yes, they use a custom registration process, which is a lot better than doing this with the method Unity proposes.

var settings = new JsonSerializerSettings();
settings.Converters.Add(JsonSubtypesConverterBuilder
    .Of(typeof(Animal), "Type") // type property is only defined here
    .RegisterSubtype(typeof(Cat), AnimalType.Cat)
    .RegisterSubtype(typeof(Dog), AnimalType.Dog)
    .SerializeDiscriminatorProperty() // ask to serialize the type property
    .Build());

[Jazzpirate]

That sounds like we shouldn't use complicated URIs in the format just because MMT doesn't have nice URI aliasing. But I guess there is nothing wrong with using archive URLs in persistent identifiers :)

They're not complicated. In fact, they are the simplest URI specification that does what we need it to do and that scales with the kind of module system that MMT offers - and FrameIT by extension uses. Believe me, anything simpler will ultimately cause more problems; e.g. with name clashes and modularity on the theory-side.

one uses a string and one uses an object of class OP (with using a single string for URI we will avoid this in this case)

Just in case this isn't already obsolete by Navid's library suggestion: What is this "Op" class? Is it supposed to be OMA? If so, I would have thought that the idea behind deserialization classes is to have one generic class "MMTTerm" that takes care of further deserializing either OMA or OMS, in which case we have precisely one "mmtdecl"-class with a "def" field of class "MMTTerm"...

[richardmarcus]

Just in case this isn't already obsolete by Navid's library suggestion: What is this "Op" class? Is it supposed to be OMA? If so, I would have thought that the idea behind deserialization classes is to have one generic class "MMTTerm" that takes care of further deserializing either OMA or OMS, in which case we have precisely one "mmtdecl"-class with a "def" field of class "MMTTerm"...

You introduced op: a JSON encoding of a term, which seems to bei either an OMS or a string.
You can't have a generic class for deserialization without a library like the one Navid suggested...

[Jazzpirate]

You introduced op: a JSON encoding of a term, which seems to bei either an OMS or a string.
You can't have a generic class for deserialization without a library like the one Navid suggested...

ah, okay - well then to clarify: "op" is a field in OMA, and is a JSON encoding of a term. A term is either an OMA or an OMS. An OMS is a string (or - alternatively - an object with DPath, Theory and name, but a string will do), an OMA is an object with "op" and "args"-fields.

So if your class structure reflects the JSON scheme, then "op" shouldn't be a class. "op" is just a field name in an OMA; the corresponding class would be "Term" - because the same applies to the "args" field. Since "args" is a list of terms, each one of those can be an OMS (string) or an OMA (json-object) ;)

[richardmarcus]

Yes but when the op field is an object with DPath, Theory and name as we have assumed in the examples above, it must be a class (i.e. one that consists of attributes DPath, Theory and name)
And if we just should name the class differently, then it should have the same name in the JSON structure.

By the way, can you think of an example where we need to have an OMA in args?

[Jazzpirate]

Yes but when the op field is an object with DPath, Theory and name as we have assumed in the examples above, it must be a class (i.e. one that consists of attributes DPath, Theory and name)

The op field is a Term. A Term can either be an OMA or an OMS. The same applies to all elements of the arg list. However we handle the arg list, the op field needs to be handled the same way. So I'm almost sure that unless you want to tell me you need to introduce a separate "OMA"-class for every possible arity and permutation of OMAs and OMSs in the arg-list, then you don't need to introduce separate classes for op either.

Otherwise, think of "op" as simply the head of the "arg"-list, if that helps...?

And if we just should name the class differently, then it should have the same name in the JSON structure.

The class names should reflect the thing they represent. "op" is a term, hence I recommend it is an element of type/class "term". The name of the field and the type of the field are separate things, though.

By the way, can you think of an example where we need to have an OMA in args?

As soon as you have "higher-order" scrolls that yield / require functions this will be the case. Obviously, any application-of-an-application can be uncurried via "helper constants" such that it is an OMS applied to several arguments, but guaranteeing that will massively restrict the way things can be formalized in MMT in order to be usable in FrameIT - that we should not do if we want FrameIT to scale with MitM, which we definitely want.

[richardmarcus]

Hmm, your format seems to be recursive then, I am not sure if it is possible to deserialize something like that...thinking...

[Jazzpirate]

Hmm, your format seems to be recursive then, I am not sure if it is possible to deserialize something like that...thinking...

Yes, it definitely is! :) Logical languages usually are recursive. And JSON is particularly useful precisely to represent recursive syntaxes, so I'd be really surprised if any semi-proper JSON implementation can't handle recursive datastructures.

Apparently Unity can't do that properly, but then I definitely recommend switching to a proper JSON library...

[richardmarcus]

Well, that explains why I was struggling with the term/op definition. I have never seen recursive datastructures in C# at all, so it never occured to me that is was meant like this... investigating....

[richardmarcus]

I did some tests with https://github.com/manuc66/JsonSubTypes and JSON.NET.
JSON.NET alone probably already solves all our problems if we use generic objects.

public class OMA { public object op; public List<object> args; }

public class Request { public string type = "mmtdecl"; public object def; }

This should suffice if we also use generic strings instead of OMS.
Only issue with that is that for deserialization, we need to do something hacky like
if((result.def as OMA).op!=null) { //OMA handling} else { //OMS handling}
but I guess that would be ok.

• If we want also want to add an additional OMS class with three strings, we need another if

• If we do not want to use generic strings instead of OMS at all, we need a different OMS class and the JSON would become
  "op": {"text": "tuple"} instead of "op": "tuple"

• If we want subclasses in C#, we need to add an discriminator attribute type into the MMTTerm class for the JsonSubTypes add-on

I would probably prefer to use the basic variant without an OMS class. This way, we are close to the original format, except that we use a single string to represent OMS and have a JSON object{ type, def} instead of an JSON array with these 2 elements.

[Jazzpirate]

I don't have strong opinions about C#-implementations. Using strings for OMSs is entirely fine with me.

and have a JSON object{ type, def} instead of an JSON array with these 2 elements.

This I don't understand...?

[richardmarcus]

Your original format specified

Requests are JSON Arrays of length 2, the first element is the "kind" of request (as String), the second represents the specifics

[Jazzpirate]

ah. Yeah, might as well be an object. Don't call them "type" and "def" though, please; both terms are heavily connotated with different things in our context ;)

[richardmarcus]

To be precise: we then have this structure, right? (calling it kind and detail now, but detail has a def field)

{
  "kind": "mmtdecl",
  "detail": {
    "name" : "A"
    "def" : {
      OMA / OMS
    }
  }
}

[Jazzpirate]

looks good to me :)

then we can analogously do e.g.

{
  "kind": "fact"
  "detail": {
    "lhs" : OMA / OMS
    "rhs": OMA / OMS
  }
}

...or whatever else we need

[Jazzpirate]

actually, I should add that "OMA / OMS" would actually be "OMA / OMS / Float", since we also have to deal with floating point literals...

[ComFreek]

@richardmarcus I still don't get why you need this hacky if condition. Why doesn't the following work?

[JsonConverter(typeof(JsonSubtypes), "Species")]
public interface ITerm
{
    string Species { get; }
}

public class OMS : ITerm
{
  public string Species {get;} = "OMS";
  public string uri; // possibilitiy: instead use `public MMTURI uri` with another class `MMTURI`
}

public class OMA : ITerm
{
    public string Species {get;} = "OMA";
    public ITerm head {get; set;};
    public List<ITerm> args {get; set;};
}

public class MyFloat : ITerm {
    public string Species { get; } = "Float";
    public float value {get; set;};
}

public class MMTDeclaration {
    public String uri {get; set;};
    public ITerm type {get; set;};
    public ITerm definiens {get; set;};
}

NB: Not sure if all those {get;set;}s are actually necessary. Possibly you still need this subtype registering you showed before.

NB2: Did an edit.

[richardmarcus]

With subclasses we don't need hacky ifs but we need to add additonal identifier strings into the JSON.
Current approach would use generic objects.

[kohlhase]

I have not followed all of the discussion. But it seems to me that you may be re-invending the wheel. There IS a JSON encoding of OpenMath that is standardized. If this is at all similar, then that should be used.
SEe https://omjson.kwarc.info/ if we do not use it who will.
At the best, a C# library for that JSON would come out of FrameIT.

[Jazzpirate]

If this is at all similar, then that should be used.

It's mostly not. We could "carve out" the fragment that we actually need (i.e. OMA, OMID and OMfloat), leave away all the "attr", "base" etc. fields that we don't need and add notions for declarations and facts, but then we basically end up with what we have up there anyway - and obviously omjson has the same "problems" from the point of view of C#/Richard since it's also a recursive grammar.

[ComFreek]

I have refactored the server. Below is the output for a request to /scroll/list: it shows the OppositeLen scroll.

@richardmarcus Please tell me if it looks good. In particular, I guess SOMS, SOMA etc. should get different names.

[
    {
        "problemTheory": "http://mathhub.info/FrameIT/frameworld?OppositeLen_Problem",
        "solutionTheory": "http://mathhub.info/FrameIT/frameworld?OppositeLen_Solution",
        "label": "OppositeLen",
        "description": "Given a triangle ABC right angled at C, the distance AB can be computed from the angle at B and the distance BC",
        "declarations": [
            {
                "uri": "http://mathhub.info/FrameIT/frameworld?OppositeLen_Problem?pA",
                "tp": {
                    "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point",
                    "kind": "SOMS"
                },
                "df": null
            },
            {
                "uri": "http://mathhub.info/FrameIT/frameworld?OppositeLen_Problem?pB",
                "tp": {
                    "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point",
                    "kind": "SOMS"
                },
                "df": null
            },
            {
                "uri": "http://mathhub.info/FrameIT/frameworld?OppositeLen_Problem?pC",
                "tp": {
                    "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point",
                    "kind": "SOMS"
                },
                "df": null
            },
            {
                "uri": "http://mathhub.info/FrameIT/frameworld?OppositeLen_Problem?pdistBC_v",
                "tp": {
                    "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit",
                    "kind": "SOMS"
                },
                "df": null
            },
            {
                "uri": "http://mathhub.info/FrameIT/frameworld?OppositeLen_Problem?pdistBC",
                "tp": {
                    "applicant": {
                        "uri": "http://mathhub.info/FrameIT/frameworld?DistanceFact?distanceFact",
                        "kind": "SOMS"
                    },
                    "arguments": [
                        {
                            "uri": "http://mathhub.info/FrameIT/frameworld?OppositeLen_Problem?pB",
                            "kind": "SOMS"
                        },
                        {
                            "uri": "http://mathhub.info/FrameIT/frameworld?OppositeLen_Problem?pC",
                            "kind": "SOMS"
                        },
                        {
                            "uri": "http://mathhub.info/FrameIT/frameworld?OppositeLen_Problem?pdistBC_v",
                            "kind": "SOMS"
                        }
                    ],
                    "kind": "SOMA"
                },
                "df": null
            },
            {
                "uri": "http://mathhub.info/FrameIT/frameworld?OppositeLen_Problem?pangleABC_v",
                "tp": {
                    "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit",
                    "kind": "SOMS"
                },
                "df": null
            },
            {
                "uri": "http://mathhub.info/FrameIT/frameworld?OppositeLen_Problem?pangleABC",
                "tp": {
                    "applicant": {
                        "uri": "http://mathhub.info/FrameIT/frameworld?AngleFact?angleFact",
                        "kind": "SOMS"
                    },
                    "arguments": [
                        {
                            "uri": "http://mathhub.info/FrameIT/frameworld?OppositeLen_Problem?pA",
                            "kind": "SOMS"
                        },
                        {
                            "uri": "http://mathhub.info/FrameIT/frameworld?OppositeLen_Problem?pB",
                            "kind": "SOMS"
                        },
                        {
                            "uri": "http://mathhub.info/FrameIT/frameworld?OppositeLen_Problem?pC",
                            "kind": "SOMS"
                        },
                        {
                            "uri": "http://mathhub.info/FrameIT/frameworld?OppositeLen_Problem?pangleABC_v",
                            "kind": "SOMS"
                        }
                    ],
                    "kind": "SOMA"
                },
                "df": null
            },
            {
                "uri": "http://mathhub.info/FrameIT/frameworld?OppositeLen_Problem?pangleBCA",
                "tp": {
                    "applicant": {
                        "uri": "http://mathhub.info/FrameIT/frameworld?AngleFact?angleFact",
                        "kind": "SOMS"
                    },
                    "arguments": [
                        {
                            "uri": "http://mathhub.info/FrameIT/frameworld?OppositeLen_Problem?pB",
                            "kind": "SOMS"
                        },
                        {
                            "uri": "http://mathhub.info/FrameIT/frameworld?OppositeLen_Problem?pC",
                            "kind": "SOMS"
                        },
                        {
                            "uri": "http://mathhub.info/FrameIT/frameworld?OppositeLen_Problem?pA",
                            "kind": "SOMS"
                        },
                        {
                            "float": 90.0,
                            "kind": "SFloatingPoint"
                        }
                    ],
                    "kind": "SOMA"
                },
                "df": null
            }
        ]
    }
]

[richardmarcus]

A few things that i noticed but not sure about them:

• the labels for the scroll facts are missing (I think they were supposed to be sent in this kind of request), also How to visualize scrolls in-game (SVG/MathML/...)? #18 and Scroll assignment communication #24 might be relevant
• better readability with kind first?,
• names: we wanted to follow the naming of https://omjson.kwarc.info/ , so I guess just OMA would be correct?
• does it make sense to follow this structure?:

{
  "kind": "scroll"
  "detail": {
 
  }
}

• a bit confused about "df": null

[ComFreek]

@richardmarcus

• I added labels. By default they are just the declaration name from the formalization, but you can override this behavior in scrolls by declaring myFact : ... | meta ?http://mathhub.info/FrameIT/frameworld?ScrollMeta?factLabel "new label"

• I don't think I can control where "kind" appears with the JSON library (circe) I am using. Machines reading that JSON shouldn't care anyway.

• Fixed in accordance to OpenMath JSON spec.

• I would say it doesn't make sense to have {"kind": "scroll", "detail": ...}. At all endpoints you should know what you expect. The only place where you cannot is with recursive grammars, hence there we add this kind metadata.

• "df": null says the fact declaration doesn't have a definiens. Probably all facts have no definiens, but I am not sure. You can ignore it for now.

New sample output of the list of all scrolls: https://pastebin.com/BzUSRfpL

[ComFreek]

The communication format has finally been settled to great extent. The implementation is done in the server component, the game engine component is being worked on by @SESch93.
As the format is settled, this issue is settled, too 😄