Add syntax for match and variant operators #1206
Conversation
Move helper function into its own private method
This is covered in the example test
This marks our switch to sum types from the union of records. Record unions are not really supported, and we mean to ditch them, so this is a more honest report of the current state of things.
We use it in ToIrListener now, not just in the tests.
Expected goes second. This effects the output.
| return group([text('{ '), prettySumRow(type.fields), text('}')]) | ||
| return prettySumRow(type.fields) |
There was a problem hiding this comment.
This is cleanup from the previous PR adding the sum types. The were wrapped in an extra {...}
quint/src/parsing/ToIrListener.ts
Outdated
| fieldType = poppedType | ||
| } | ||
|
|
||
| // const poppedType = this.popType().value |
There was a problem hiding this comment.
| // const poppedType = this.popType().value | |
| // |
quint/src/parsing/ToIrListener.ts
Outdated
| const labelStr: QuintStr = { id: caseId, kind: 'str', value: label } | ||
| const elim: QuintLambda = { id: caseId, kind: 'lambda', qualifier: 'def', expr: caseExpr, params } | ||
| return [labelStr, elim] | ||
| // return acc.concat([labelStr, elim]) |
There was a problem hiding this comment.
| // return acc.concat([labelStr, elim]) |
There was a problem hiding this comment.
Thanks for catching these!
| @@ -29,3 +30,17 @@ import JSONbig from 'json-bigint' | |||
| export function unreachable(object: never): never { | |||
| throw new Error(`impossible: non-exhuastive check should fail during type checking ${JSONbig.stringify(object)}`) | |||
| } | |||
|
|
|||
| /** A wrapper around lodash zip that ensures all zipped elements are defined | |||
There was a problem hiding this comment.
Ah, I noticed this was moved, but regardless, I didn't know/remember we have this 😄
There was a problem hiding this comment.
It was added in 99910e3 :)
| matchSumExpr: MATCH expr '{' '|'? matchCase+=matchSumCase ('|' matchCase+=matchSumCase)* '}' ; | ||
| matchSumCase: (variantMatch=matchSumVariant | wildCardMatch='_') '=>' expr ; | ||
| matchSumVariant | ||
| : (variantLabel=simpleId["variant label"]) ('(' (variantParam=simpleId["match case parameter"] | '_') ')')? ; |
There was a problem hiding this comment.
How are these labels used? I see they have spaces, so I suppose it's only for error reporting to users? If so, that's really great - we should really use them more.
There was a problem hiding this comment.
Yep, the string arguments are used for error reporting in
quint/quint/src/generated/Quint.g4
Lines 243 to 254 in ba946ad
To produce messages like
>>> {A::B::c: 3}
syntax error: error: [QNT008] Identifiers in a record cannot be qualified with '::'. Found A::B::c.
{A::B::c: 3}
^
>>> type T = A::B(int)
syntax error: error: [QNT008] Identifiers in a variant label cannot be qualified with '::'. Found A::B.
type T = A::B(int)
^
The ANTLR labels like variantLabel and variantParam, on the other hand, are used to provide named accessors for the parsed data on the rhs of the =, used in
quint/quint/src/parsing/ToIrListener.ts
Lines 996 to 1003 in ba946ad
|
Thank you for the careful review! |
Closes #1082
This is an alternative to #1093, based on @konnov's preference to use the
existing convention of encoding language constructs as builtin operators with
special interpretations instead of extending our IR.
It adds support for:
It also includes some fixes and clean up from the last PR on sum types.
A notable alteration:
I am replacing the existing
matchsyntax used for the unsupported record unions with the superseding sum-type syntax agreed upon in #1062. This means a "regression" in ouroptions.qntexample, since this used the partially supported union syntax. However, afaiu, this really just reflects more accurately the state of our support for this kind of construct at the moment.CHANGELOG.mdfor any new functionalityREADME.mdupdated for any listed functionality