JSON IR has no type information

[craft095]

Description

I wanted to use JSON IR as input format to Apalache. In order to understand how to encode specification (and copy-paste standard modules blocks) I generated IR with following command line:

java -jar apalache.jar --write-intermediate=true parse M0.tla

However, the resulting 00_OutSanyParser.json contains no type information. I tried typecheck instead of parse, it contains type information, but it also obfuscates information about standard modules, which I planned to re-use in my JSONs.

Input specification

---- MODULE M0 ----

CONSTANT 
    \* @type: Set(Int);
    MySet

====

Generated JSON IR

{
  "name": "ApalacheIR",
  "version": "1.0",
  "description": "https://apalache.informal.systems/docs/adr/005adr-json.html",
  "modules": [
    {
      "kind": "TlaModule",
      "name": "00_OutSanyParser",
      "declarations": [
        {
          "source": {
            "filename": "M0",
            "from": {
              "line": 5,
              "column": 5
            },
            "to": {
              "line": 5,
              "column": 9
            }
          },
          "type": "Untyped",
          "kind": "TlaConstDecl",
          "name": "MySet"
        }
      ]
    }
  ]
}

System information

• Apalache version: 0.28.0
• OS: Windows 10
• JDK version: openjdk 18.0.2

[shonfeder]

Thanks for the report @craft095. Our parsing phase indeed doesn't interact with the type checking or inference.

FYI, you can get the output from parsing or typechecking a bit easier via the --output flag. E.g.,

apalache-mc typecheck --output=m0.json M0.tla
cat m0.json

This is not a bug with the parsing command, afaict. But it sounds like you have a separate concern w/r/t how standard module values are dealt with in the JSON ir? Could you elaborate on that concern?

[shonfeder]

I wonder if this should be viewed as a documentation bug? We could add a note in the CLI doc for parse like Parse a TLA+ specification and quit (ignores any typing annotations)

[craft095]

Thanks @shonfeder ! I want to generate IR for TLA+ specifications and I more or less understand how to generate my own content, but I hoped that I can re-use IR of standard modules. Is there a way to get IR of standard modules with type annotations inside?

[shonfeder]

To be sure that we can direct our advice and investigations in the right direction, I think it would help for us to be able to discuss in some concrete terms.

Currently, given the following spec that uses some standard modules

------------------- MODULE TestIR -----------------------
EXTENDS Naturals, FiniteSets

Foo == 1 + 1
Bar == Cardinality({1, 2, 3})

============================================================

We obtain the following JSON serialization of the IR via apalche-mc typecheck --output=testir.json TestIR.tla:

{
  "name": "ApalacheIR",
  "version": "1.0",
  "description": "https://apalache.informal.systems/docs/adr/005adr-json.html",
  "modules": [
    {
      "kind": "TlaModule",
      "name": "testir",
      "declarations": [
        {
          "source": "UNKNOWN",
          "type": "(() => Int)",
          "kind": "TlaOperDecl",
          "name": "Foo",
          "formalParams": [
            
          ],
          "isRecursive": false,
          "body": {
            "source": "UNKNOWN",
            "type": "Int",
            "kind": "OperEx",
            "oper": "PLUS",
            "args": [
              {
                "source": "UNKNOWN",
                "type": "Int",
                "kind": "ValEx",
                "value": {
                  "kind": "TlaInt",
                  "value": 1
                }
              },
              {
                "source": "UNKNOWN",
                "type": "Int",
                "kind": "ValEx",
                "value": {
                  "kind": "TlaInt",
                  "value": 1
                }
              }
            ]
          }
        },
        {
          "source": "UNKNOWN",
          "type": "(() => Int)",
          "kind": "TlaOperDecl",
          "name": "Bar",
          "formalParams": [
            
          ],
          "isRecursive": false,
          "body": {
            "source": "UNKNOWN",
            "type": "Int",
            "kind": "OperEx",
            "oper": "FiniteSets!Cardinality",
            "args": [
              {
                "source": "UNKNOWN",
                "type": "Set(Int)",
                "kind": "OperEx",
                "oper": "SET_ENUM",
                "args": [
                  {
                    "source": "UNKNOWN",
                    "type": "Int",
                    "kind": "ValEx",
                    "value": {
                      "kind": "TlaInt",
                      "value": 1
                    }
                  },
                  {
                    "source": "UNKNOWN",
                    "type": "Int",
                    "kind": "ValEx",
                    "value": {
                      "kind": "TlaInt",
                      "value": 2
                    }
                  },
                  {
                    "source": "UNKNOWN",
                    "type": "Int",
                    "kind": "ValEx",
                    "value": {
                      "kind": "TlaInt",
                      "value": 3
                    }
                  }
                ]
              }
            ]
          }
        }
      ]
    }
  ]
}

As you can see, it includes typed representations of the use of standard module operators (tho given in terms of the Apalache internalized equivalents.

Could you use this minimal example, or perhaps your own MWE, to show what kind of information you are missing, and what you would like to have available instead?

It would probably also help if you can provide a description of the end result you are after, as it's possible we can help come up with an alternative method or some additional considerations once we understand the ultimate aim.

Thanks! :D

[craft095]

@shonfeder, thank you! Your example made it clear to me how to obtain what I want: typed IR for standard modules like Bags or TLC:

---- MODULE M0 ----
EXTENDS TLC
====

Then I can obtain IR with apalche-mc typecheck --output=testir.json M0.tla and copy-paste it in every specification, which needs this standard module.

Context: I am generating test cases for TLC and to verify their results I generate also equivalent test cases for Apalache. Apalache and TLC share the same parser SANY, which is a problem, because I need some level of independence. So I am going to generate IR instead of TLA+ code to bypass SANY.

[shonfeder]

Apalache and TLC share the same parser SANY, which is a problem, because I need some level of independence. So I am going to generate IR instead of TLA+ code to bypass SANY.

That's quite clever! Good thinking there :D

Glad we found a solution! :tada: