Support conversion of sum types in Apalache

[shonfeder]

No description provided.

[thpani]

This is pending on sum types in Quint, right?

[shonfeder]

Correct!

[shonfeder]

I've hit a snag that will require a bit of redesign on either the Apalache conversion side or the quint IR processing:

Given a type declaration like E in

  type F = | A
  type E = | X(F)

The declaration is stored in the IR like so:

        "15": {
            "id": 15,
            "name": "E",
            "kind": "typedef",
            "type": {
                "id": 15,
                "kind": "sum",
                "fields": {
                    "kind": "row",
                    "fields": [
                        {
                            "fieldName": "X",
                            "fieldType": {
                                "id": 14,
                                "kind": "const",
                                "name": "F"
                            }
                        }
                    ],
                    "other": { "kind": "empty" }
                }
            }
        },

The snag, for our purposes, is that F is not expanded and inlined, but merely noted as a type constant, together with the id with which we can retrieve the declaration in the lookup table.

Our assumption in the quint conversion so far is that we don't need to take account of defined types, and so type constants like this encountered in the IR are just mapped to abstract types in Apalache. As a result, when trying to construct variant application live variant("X", A), representing the construct for the A variant of F, we get a unification failure, since the type of the operand is given as the concrete sum type | A while apalache only allows the (incorrectly abstract) type constant F as an argument to X.

We have two clear options, afaict:

1. We can make the Apalache conversion take account if type declarations during conversion. This will mean we don't require any change on the quint side, but will increase the complexity of the apalache conversion code, and make for an even tighter coupling, requiring more updates on the apalache side if we change how we are representing these things in quint.
3. We can do a pass on the quint side that inlines all type constants before exporting the IR.

WDYT, @thpani, @bugarela? Any other options come to mind?

[konnov]

I've hit a snag that will require a bit of redesign on either the Apalache conversion side or the quint IR processing...

We should have hit the same issue with other data types earlier. Maybe @thpani remembers how it was dealt with

[bugarela]

We can do a pass on the quint side that inlines all type constants before exporting the IR.

We already have that, see aliasInliner.ts. Perhaps we have to change something there for the inliner to work for sum types as well.

[shonfeder]

@bugarela I'll look into that! Thanks :)

[shonfeder]

Ahhh.. my debugging here is probably very off. I had been assuming that what Apalache gets is essentially the same as the output of typecheck. But I now see that verifySpec has been made to do a bunch of additional things -- changing the contents of a spec, doing additional analysis, additional flattening etc.

I'll have to figure out how to inspect what what is going on there and revise my hypothesis about why we are getting the failure.

Taking a step back, here is what is not working as I'd expect:

Given

  type S = | A
  type T = | B(S)

Apalache conversion is failing with this error from the builder:

  > Input was not a valid representation of the QuintIR: Conversion failed while building operator definition `QuintOpDef(27,B,def,QuintLambda(26,List(QuintLambdaParameter(23,__BParam_26)),def,QuintApp(25,variant,List(QuintStr(22,B), QuintName(24,__BParam_26)))))`: Operator Variants!Variant cannot be applied to arguments of types (Str, A({  })) E@07:33:44.752

And it is failing during this type comparison:

>>>> Comparing types: A({  }) S

Which, if everything were working as expected, would be the same, by definition.

[thpani]

Ahhh.. my debugging here is probably very off. I had been assuming that what Apalache gets is essentially the same as the output of typecheck. But I now see that verifySpec has been made to do a bunch of additional things -- changing the contents of a spec, doing additional analysis, additional flattening etc.

I'll have to figure out how to inspect what what is going on there and revise my hypothesis about why we are getting the failure.

Yeah... there's some flattening happening between typecheck and handing off to Apalache.

I usually just added a call to outputResult inside verifySpec (also, don't be surprised, outputResult calls process.exit() 😄).

[thpani]

We already have that, see aliasInliner.ts. Perhaps we have to change something there for the inliner to work for sum types as well.

Just for context: we also have some Quint type flattening logic in Apalache – I'm actually not sure how much overlap there is, but in the current case I think it makes sense to add to aliasInliner.ts in Quint, if necessary.

[shonfeder]

Thanks for the pointer, @thpani! I don't see any flattening of the relevant sort in the type converter: it is able to do direct conversion without any access to the lookup tables. So I suspect the error is that I neglected to wire in some required visitor method somewhere along the way :)