Add syntax for constructing and eliminating sum type values

[shonfeder]

Closes #1092

This followup to #1089 adds two more additions to our syntax for sum types, following the design proposed in #1062.

New additions to the IR:

• QuintMatch, representing match expressions for eliminating variants of a sum type.
• QuintVaraint, representing a value of a sum type. This just pairs a label with a value.

Additionally, as per RFC001, parsing a sum-type declaration generates constructors for each variant.

A number of minor fixes needed to be made along the way.

Key concepts

Match expressions are represented as associations of variant labels and lambdas that can be applied to the argument of a variant. E.g.,

match x {A => e1 | B(v) => e2 }

is represented as (in pseudo code)

{ expr: x,
, cases: [ ('A', (()) => e1)
         , ('B', (v) => e2)
         ]
}

A variant value is basically just a tuple pairing a label with the associated expression (but uses an object to match the rest or our IR).

Reviewing

• Reviewing by commit, and skipping the generated stuff, is probably best!
• This is currently branched off of Fix non-exhaustive switches #1092, and it will be a lot smaller once that is merged in.

• Tests added for any new code
• [-] Documentation added for any new functionality
• [-] Entries added to the respective CHANGELOG.md for any new functionality
• [-] Feature table on README.md updated for any listed functionality

[konnov]

Left a comment on the extension of QuintEx, which IMO does not align with the current IR design. In the future, we may want to introduce high-level IR, e.g., HighQuintEx that expresses the special operators of QuintEx via case distinction.

[konnov]

We probably have different opinions on how the Quint IR should look like. So far, we have managed to keep the number of cases in QuintEx at minimum. This required us to introduce "special" low-level operators like Rec(...) and field(...) instead of having distinct cases in the IR. Although the normal users should not use these operators, they simplify IR manipulation at large.

Just to stress here, I am not arguing that a high-level IR is worse than a low-level IR, it is just that the current IR is minimal and low-level.

Given the above reasoning, I am proposing to introduce two new "special" operators instead of introducing two new cases of QuintEx, namely:

// Construct a variant of a sum type, where `label` carries the name of the label to be used in the type.
variant(label: str, payload: a): { label(a) | b }
// Match an expression with one of the labels `label_1`, ..., `label_n`.
// Process each case with the operators `f_1`, ..., `f_n`, respectively.
match(expr: a, label_1: str, f_1: (...) => ..., ..., label_n: str, f_n: (...) => ...): b

Since we are already processing records and tuples in a special way, I don't see why we could not do the same with sum types. The only big difference here is that match is a higher-order operator.

[shonfeder]

In general:

we have managed to keep the number of cases in QuintEx at minimum. This required us to introduce "special" low-level operators like Rec(...) and field(...) instead of having distinct cases in the IR. Although the normal users should not use these operators, they simplify IR manipulation at large.

But what is the gain here? I've enumerated some of the costs here:

• https://github.com/informalsystems/quint/blob/65f4877aba142b3c7f5538920bb568a69c3f8244/doc/rfcs/rfc001-sum-types/rfc001-sum-types.org#drop-the-exotic-operators
• Introduce stronger lexical rules for identifiers #1081

In the case of these kind of special constructs, any savings on the cases on QuintEx are paid for directly in the number of cases in the operator application logic, only we lose structure along the way and up having to perform unnecessarily validations and computations to reconstruct that lost data.

This PR is meant in part to show the benefit of dropping these exotic operator in favor a richer and more helpful representation in the IR.

But if you could help me understand where we actually see simplifications instead of complexity, that could help me move past my aversion here.

In particular:

Wouldn't adding the varaiant operator require support for open rows in sum-types, which we agreed (as per your preference) we did not want to expose in #1062?

We will need special cases for most operator applications to handle match, but we will lose the typing info and structure provided here.

[shonfeder]

I talked thru the pros and cons of our current approach vs. a richer representation in the ir with @bugarela. I’m still of the opinion that the current approach is worse for most Americans d the most important purposes than a more structured representation, but I see the trade offs clearer now, and am fine with implementing this using the exotic operators. I’ll make a new pr, since this will be a very different approach and there are lots of merge conflicts here anyhow.