From fe8f55a8802742a304fcefdbd66ee09938be5a33 Mon Sep 17 00:00:00 2001 From: Shon Feder Date: Wed, 4 Oct 2023 23:48:35 -0400 Subject: [PATCH] Replace unsupported union match with sum match --- quint/src/generated/Quint.g4 | 12 +- quint/src/graphics.ts | 2 +- quint/src/ir/IRprinting.ts | 4 +- quint/src/ir/quintIr.ts | 4 +- quint/src/ir/quintTypes.ts | 4 +- quint/src/names/base.ts | 4 +- quint/src/parsing/ToIrListener.ts | 174 ++++++++++++------ quint/src/runtime/impl/compilerImpl.ts | 2 + quint/test/ir/IRprinting.test.ts | 4 +- .../test/parsing/quintParserFrontend.test.ts | 24 +-- quint/testFixture/SuperSpec.json | 2 +- quint/testFixture/SuperSpec.qnt | 10 - quint/testFixture/_1025importeeWithError.json | 2 +- 13 files changed, 148 insertions(+), 100 deletions(-) diff --git a/quint/src/generated/Quint.g4 b/quint/src/generated/Quint.g4 index 7f8a3d101..9e4b25d3d 100644 --- a/quint/src/generated/Quint.g4 +++ b/quint/src/generated/Quint.g4 @@ -57,8 +57,7 @@ typeDef | 'type' typeName=qualId '=' '|'? typeSumVariant ('|' typeSumVariant)* # typeSumDef ; -// A single variant case in a sum type definition. -// +// A single variant case in a sum type definition or match statement. // E.g., `A(t)` or `A`. typeSumVariant : sumLabel=simpleId["variant label"] ('(' type ')')? ; @@ -157,8 +156,7 @@ expr: // apply a built-in operator via the dot notation | expr OR expr # or | expr IFF expr # iff | expr IMPLIES expr # implies - | expr MATCH - ('|' STRING ':' parameter '=>' expr)+ # match + | matchSumExpr # match | 'all' '{' expr (',' expr)* ','? '}' # actionAll | 'any' '{' expr (',' expr)* ','? '}' # actionAny | ( qualId | INT | BOOL | STRING) # literalOrId @@ -176,6 +174,12 @@ expr: // apply a built-in operator via the dot notation | '{' expr '}' # braces ; +// match e { A(a) => e1 | B => e2 | C(_)} +matchSumExpr: MATCH expr '{' '|'? matchCase+=matchSumCase ('|' matchCase+=matchSumCase)* '}' ; +matchSumCase: (variantMatch=matchSumVariant | wildCardMatch='_') '=>' expr ; +matchSumVariant + : (variantLabel=simpleId["variant label"]) ('(' (variantParam=simpleId["match case parameter"] | '_') ')')? ; + // A probing rule for REPL. // Note that a top-level declaration has priority over an expression. // For example, see: https://github.com/informalsystems/quint/issues/394 diff --git a/quint/src/graphics.ts b/quint/src/graphics.ts index b933dd1a6..74f5e9bf7 100644 --- a/quint/src/graphics.ts +++ b/quint/src/graphics.ts @@ -187,7 +187,7 @@ export function prettyQuintType(type: QuintType): Doc { return group([text('{ '), prettyRow(type.fields), text('}')]) } case 'sum': { - return group([text('{ '), prettySumRow(type.fields), text('}')]) + return prettySumRow(type.fields) } case 'union': { const records = type.records.map(rec => { diff --git a/quint/src/ir/IRprinting.ts b/quint/src/ir/IRprinting.ts index d7df7c8f2..c79810555 100644 --- a/quint/src/ir/IRprinting.ts +++ b/quint/src/ir/IRprinting.ts @@ -13,7 +13,7 @@ */ import { OpQualifier, QuintDeclaration, QuintDef, QuintEx, QuintModule, isAnnotatedDef } from './quintIr' -import { QuintSumType, QuintType, Row, RowField, isTheUnit } from './quintTypes' +import { QuintSumType, QuintType, Row, RowField, isUnitType } from './quintTypes' import { TypeScheme } from '../types/base' import { typeSchemeToString } from '../types/printing' @@ -218,7 +218,7 @@ export function rowToString(r: Row): string { export function sumToString(s: QuintSumType): string { return s.fields.fields .map((f: RowField) => { - if (isTheUnit(f.fieldType)) { + if (isUnitType(f.fieldType)) { return `| ${f.fieldName}` } else { return `| ${f.fieldName}(${typeToString(f.fieldType)})` diff --git a/quint/src/ir/quintIr.ts b/quint/src/ir/quintIr.ts index a049b6d9d..7700f9aee 100644 --- a/quint/src/ir/quintIr.ts +++ b/quint/src/ir/quintIr.ts @@ -131,7 +131,7 @@ export function isQuintBuiltin(app: QuintApp): app is QuintBuiltinApp { } // This should be the source of truth for all builtin opcodes -const builtinOpCodes = [ +export const builtinOpCodes = [ 'List', 'Map', 'Rec', @@ -187,6 +187,7 @@ const builtinOpCodes = [ 'length', 'map', 'mapBy', + 'match', 'mustChange', 'neq', 'next', @@ -217,6 +218,7 @@ const builtinOpCodes = [ 'tuples', 'union', 'unionMatch', + 'variant', 'weakFair', 'with', ] as const diff --git a/quint/src/ir/quintTypes.ts b/quint/src/ir/quintTypes.ts index 065a41446..2a08553e4 100644 --- a/quint/src/ir/quintTypes.ts +++ b/quint/src/ir/quintTypes.ts @@ -75,7 +75,7 @@ export interface QuintRecordType extends WithOptionalId { } // A value of the unit type, i.e. an empty record -export function unitValue(id: bigint): QuintRecordType { +export function unitType(id: bigint): QuintRecordType { return { id, kind: 'rec', @@ -83,7 +83,7 @@ export function unitValue(id: bigint): QuintRecordType { } } -export function isTheUnit(r: QuintType): Boolean { +export function isUnitType(r: QuintType): Boolean { return r.kind === 'rec' && r.fields.kind === 'row' && r.fields.fields.length === 0 && r.fields.other.kind === 'empty' } diff --git a/quint/src/names/base.ts b/quint/src/names/base.ts index 248e046fa..5da5f2cab 100644 --- a/quint/src/names/base.ts +++ b/quint/src/names/base.ts @@ -12,7 +12,7 @@ * @module */ -import { QuintDef, QuintExport, QuintImport, QuintInstance, QuintLambdaParameter } from '../ir/quintIr' +import { QuintDef, QuintExport, QuintImport, QuintInstance, QuintLambdaParameter, builtinOpCodes } from '../ir/quintIr' import { QuintType } from '../ir/quintTypes' /** @@ -232,4 +232,6 @@ export const builtinNames = [ 'ite', 'cross', 'difference', + 'match', + 'variant', ] diff --git a/quint/src/parsing/ToIrListener.ts b/quint/src/parsing/ToIrListener.ts index cb85eed3f..b3ef0b5fc 100644 --- a/quint/src/parsing/ToIrListener.ts +++ b/quint/src/parsing/ToIrListener.ts @@ -5,22 +5,26 @@ import { QuintListener } from '../generated/QuintListener' import { OpQualifier, QuintApp, + QuintBuiltinApp, QuintDeclaration, QuintDef, QuintEx, + QuintLambda, QuintLambdaParameter, QuintLet, QuintModule, QuintName, QuintOpDef, + QuintStr, } from '../ir/quintIr' -import { ConcreteFixedRow, QuintSumType, QuintType, Row, RowField, unitValue } from '../ir/quintTypes' +import { ConcreteFixedRow, QuintSumType, QuintType, Row, RowField, isUnitType, unitType } from '../ir/quintTypes' import { strict as assert } from 'assert' import { ErrorMessage, Loc } from './quintParserFrontend' import { compact, zipWith } from 'lodash' import { Maybe, just, none } from '@sweet-monads/maybe' import { TerminalNode } from 'antlr4ts/tree/TerminalNode' import { QuintTypeDef } from '../ir/quintIr' +import { zip } from '../../test/util' /** * An ANTLR4 listener that constructs QuintIr objects out of the abstract @@ -373,44 +377,69 @@ export class ToIrListener implements QuintListener { // type T = | A | B(t1) | C(t2) exitTypeSumDef(ctx: p.TypeSumDefContext) { const name = ctx._typeName!.text! - const defId = this.idGen.nextId() - this.sourceMap.set(defId, this.loc(ctx)) - - const typeId = this.idGen.nextId() - this.sourceMap.set(typeId, this.loc(ctx)) + const id = this.getId(ctx) + // Build the type declaraion const fields: RowField[] = popMany(this.variantStack, this.variantStack.length) const row: ConcreteFixedRow = { kind: 'row', fields, other: { kind: 'empty' } } - const type: QuintSumType = { id: defId, kind: 'sum', fields: row } - + const type: QuintSumType = { id, kind: 'sum', fields: row } const def: QuintTypeDef = { - id: defId, + id: id, name, kind: 'typedef', type, } - this.declarationStack.push(def) + // Generate all the variant constructors + // a variant constructor is an operator that injects an exprssion + // into the sum type by wrapping it in a label + const constructors: QuintOpDef[] = zip(fields, ctx.typeSumVariant()).map( + ([{ fieldName, fieldType }, variantCtx]) => { + // Mangle the parameter name to avoid clashes + // This shouldn't be visible to users + const paramName = `__${fieldName}Param` + + let params: QuintLambdaParameter[] + let expr: QuintEx + let qualifier: OpQualifier + + if (isUnitType(fieldType)) { + // The nullary variant constructor is actual + // variant pairint a label with the unit. + params = [] + expr = unitValue(this.getId(variantCtx._sumLabel)) + // Its a `val` cause it takes no arguments + qualifier = 'val' + } else { + // Oherwise we will build constructor that takes one parameter + // and wraps it in a `variaint` + params = [{ id: this.getId(variantCtx.type()!), name: paramName }] + expr = { kind: 'name', name: paramName, id: this.getId(variantCtx._sumLabel) } + qualifier = 'def' + } + const label: QuintStr = { id: this.getId(variantCtx), kind: 'str', value: fieldName } + const variant: QuintBuiltinApp = { + id: this.getId(variantCtx), + kind: 'app', + opcode: 'variant', + args: [label, expr], + } + const lam: QuintLambda = { id: this.getId(variantCtx), kind: 'lambda', params, qualifier, expr: variant } + return { id: this.getId(variantCtx), kind: 'def', name: fieldName, qualifier, expr: lam } + } + ) + + this.declarationStack.push(def, ...constructors) } exitTypeSumVariant(ctx: p.TypeSumVariantContext) { const fieldName = ctx._sumLabel!.text! const poppedType = this.popType().value - - let fieldType: QuintType - // Check if we have an accompanying type, and if not, then synthesize the // unit type. - // - // I.e., we interpert a variant `A` as `A({})`. - if (poppedType === undefined) { - const id = this.idGen.nextId() - this.sourceMap.set(id, this.loc(ctx)) - fieldType = unitValue(id) - } else { - fieldType = poppedType - } - + // const poppedType = this.popType().value + // I.e., we interpret a variant `A` as `A({})`. + const fieldType: QuintType = poppedType ? poppedType : unitType(this.getId(ctx)) this.variantStack.push({ fieldName, fieldType }) } @@ -887,45 +916,68 @@ export class ToIrListener implements QuintListener { } // if (p) e1 else e2 - exitIfElse(ctx: any) { + exitIfElse(ctx: p.IfElseContext) { const args = popMany(this.exprStack, 3) this.pushApplication(ctx, 'ite', args) } - // entry match - // | "Cat": cat => cat.name != "" - // | "Dog": dog => dog.year > 0 - exitMatch(ctx: p.MatchContext) { - const options = ctx.STRING().map(opt => opt.text.slice(1, -1)) - const noptions = options.length - // expressions in the right-hand sides, e.g., dog.year > 0 - const rhsExprs = popMany(this.exprStack, noptions) - // parameters in the right-hand side - const params = popMany(this.paramStack, noptions) - // matched expressionm e.g., entry - const exprToMatch = popMany(this.exprStack, 1)![0] - const matchArgs: QuintEx[] = [exprToMatch] - // push the tag value and the corresponding lambda in matchArgs - for (let i = 0; i < noptions; i++) { - const tagId = this.getId(ctx) - const tag: QuintEx = { - id: tagId, - kind: 'str', - value: options[i], - } - const lamId = this.getId(ctx) - const lam: QuintEx = { - id: lamId, - kind: 'lambda', - params: [params[i]], - qualifier: 'def', - expr: rhsExprs[i], + // match expr { + // | Variant1(var1) => expr1 + // | Variantk(_) => exprk // a hole in the payload + // | ... + // | Variantn(varn) => exprn + // | _ => exprm // A wildcard match, acting as a catchall + // } + // + // The above is represented in the UFC using an exotic `match` operator of the form + // + // match(epxr, label1, (var1) => expr1, ..., labeln, (varn) => exprn, "_", (_) => exprm) + exitMatchSumExpr(ctx: p.MatchSumExprContext) { + const matchId = this.getId(ctx) + // We will have one expression for each match case, plus the + const exprs = popMany(this.exprStack, ctx._matchCase.length + 1) + // The first expression is the one we are matching on + // the syntax rules ensure that at least this expression is given + const expr = exprs.shift()! + const gatherCase: ( + acc: (QuintStr | QuintLambda)[], + matchCase: [QuintEx, p.MatchSumCaseContext] + ) => (QuintStr | QuintLambda)[] = (acc, [caseExpr, caseCtx]) => { + const caseId = this.getId(caseCtx) + let label: string + let params: QuintLambdaParameter[] + if (caseCtx._wildCardMatch) { + // a wildcard case: _ => expr + label = '_' + params = [] + } else if (caseCtx._variantMatch) { + const variant = caseCtx._variantMatch + let name: string + if (variant._variantParam) { + name = variant._variantParam.text + } else { + // We either have a hole or no param specified, in which case our lambda only needs a hole + name = '_' + } + label = variant._variantLabel.text + params = [{ name, id: this.getId(variant) }] + } else { + throw new Error('impossible: either _wildCardMatch or _variantMatch must be present') } - matchArgs.push(tag) - matchArgs.push(lam) + const labelStr: QuintStr = { id: caseId, kind: 'str', value: label } + const elim: QuintLambda = { id: caseId, kind: 'lambda', qualifier: 'def', expr: caseExpr, params } + return acc.concat([labelStr, elim]) + } + + // after shifting off the match expr, the remaing exprs are in each case + const cases: (QuintStr | QuintLambda)[] = zip(exprs, ctx._matchCase).reduce(gatherCase, []) + const matchExpr: QuintBuiltinApp = { + id: matchId, + kind: 'app', + opcode: 'match', + args: [expr].concat(cases), } - // construct the match expression and push it in exprStack - this.pushApplication(ctx, 'unionMatch', matchArgs) + this.exprStack.push(matchExpr) } /** ******************* translate types ********************************/ @@ -1238,3 +1290,13 @@ function popMany(stack: T[], n: number): T[] { function getDocText(doc: TerminalNode[]): string { return doc.map(l => l.text.slice(4, -1)).join('\n') } + +// Helper to construct an empty record (the unit value) +function unitValue(id: bigint): QuintBuiltinApp { + return { + id, + kind: 'app', + opcode: 'Rec', + args: [], + } +} diff --git a/quint/src/runtime/impl/compilerImpl.ts b/quint/src/runtime/impl/compilerImpl.ts index 1e7b733f1..32feaf506 100644 --- a/quint/src/runtime/impl/compilerImpl.ts +++ b/quint/src/runtime/impl/compilerImpl.ts @@ -919,6 +919,8 @@ export class CompilerVisitor implements IRVisitor { // builtin operators that are not handled by REPL case 'unionMatch': + case 'variant': // TODO: https://github.com/informalsystems/quint/issues/1033 + case 'match': // TODO: https://github.com/informalsystems/quint/issues/1033 case 'orKeep': case 'mustChange': case 'weakFair': diff --git a/quint/test/ir/IRprinting.test.ts b/quint/test/ir/IRprinting.test.ts index 8cbee1b85..1389cfbb7 100644 --- a/quint/test/ir/IRprinting.test.ts +++ b/quint/test/ir/IRprinting.test.ts @@ -9,7 +9,7 @@ import { typeToString, } from '../../src/ir/IRprinting' import { toScheme } from '../../src/types/base' -import { QuintSumType, unitValue } from '../../src' +import { QuintSumType, unitType } from '../../src' describe('moduleToString', () => { const quintModule = buildModuleWithDecls(['var S: Set[int]', 'val f = S.filter(x => x + 1)']) @@ -241,7 +241,7 @@ describe('typeToString', () => { kind: 'row', fields: [ { fieldName: 'A', fieldType: { kind: 'int', id: 0n } }, - { fieldName: 'B', fieldType: unitValue(0n) }, + { fieldName: 'B', fieldType: unitType(0n) }, ], other: { kind: 'empty' }, }, diff --git a/quint/test/parsing/quintParserFrontend.test.ts b/quint/test/parsing/quintParserFrontend.test.ts index d2fe46df8..224ea4c21 100644 --- a/quint/test/parsing/quintParserFrontend.test.ts +++ b/quint/test/parsing/quintParserFrontend.test.ts @@ -15,7 +15,6 @@ import { right } from '@sweet-monads/either' import { newIdGenerator } from '../../src/idGenerator' import { collectIds } from '../util' import { fileSourceResolver } from '../../src/parsing/sourceResolver' -import { isTheUnit } from '../../src' // read a Quint file from the test data directory function readQuint(name: string): string { @@ -131,24 +130,11 @@ describe('parsing', () => { }) it('parses sum types', () => { - const mod = ` - module SumTypes { - type T = - | A - | B(int) - } - ` - const result = parsePhase1fromText(newIdGenerator(), mod, 'test') - assert(result.isRight()) - const typeDef = result.value.modules[0].declarations[0] - assert(typeDef.kind === 'typedef') - const sumType = typeDef.type! - assert(sumType.kind === 'sum') - const [variantA, variantB] = sumType.fields.fields - assert(variantA.fieldName === 'A') - assert(isTheUnit(variantA.fieldType)) - assert(variantB.fieldName === 'B') - assert(variantB.fieldType.kind === 'int') + parseAndCompare('_1043sumTypeDecl') + }) + + it('parses match expressions', () => { + parseAndCompare('_1044matchExpression') }) }) diff --git a/quint/testFixture/SuperSpec.json b/quint/testFixture/SuperSpec.json index dda01e30c..d53360132 100644 --- a/quint/testFixture/SuperSpec.json +++ b/quint/testFixture/SuperSpec.json @@ -1 +1 @@ -{"stage":"parsing","warnings":[],"modules":[{"id":3,"name":"M1","declarations":[{"id":2,"kind":"def","name":"foo","qualifier":"val","expr":{"id":1,"kind":"int","value":4}}]},{"id":6,"name":"M2","declarations":[{"id":5,"kind":"def","name":"bar","qualifier":"val","expr":{"id":4,"kind":"int","value":4}}]},{"id":11,"name":"Proto","declarations":[{"kind":"var","name":"x","typeAnnotation":{"id":9,"kind":"int"},"id":10},{"kind":"const","name":"N","typeAnnotation":{"id":7,"kind":"int"},"id":8}]},{"id":523,"name":"withConsts","declarations":[{"id":102,"kind":"def","name":"pow_2_to_3","qualifier":"val","expr":{"id":101,"kind":"app","opcode":"ipow","args":[{"id":99,"kind":"int","value":2},{"id":100,"kind":"int","value":3}]}},{"id":105,"kind":"def","name":"uminus","qualifier":"val","expr":{"id":104,"kind":"app","opcode":"iuminus","args":[{"id":103,"kind":"int","value":100}]}},{"id":109,"kind":"def","name":"gt_2_to_3","qualifier":"val","expr":{"id":108,"kind":"app","opcode":"igt","args":[{"id":106,"kind":"int","value":2},{"id":107,"kind":"int","value":3}]}},{"id":113,"kind":"def","name":"ge_2_to_3","qualifier":"val","expr":{"id":112,"kind":"app","opcode":"igte","args":[{"id":110,"kind":"int","value":2},{"id":111,"kind":"int","value":3}]}},{"id":117,"kind":"def","name":"lt_2_to_3","qualifier":"val","expr":{"id":116,"kind":"app","opcode":"ilt","args":[{"id":114,"kind":"int","value":2},{"id":115,"kind":"int","value":3}]}},{"id":121,"kind":"def","name":"le_2_to_3","qualifier":"val","expr":{"id":120,"kind":"app","opcode":"ilte","args":[{"id":118,"kind":"int","value":2},{"id":119,"kind":"int","value":3}]}},{"id":125,"kind":"def","name":"eqeq_2_to_3","qualifier":"val","expr":{"id":124,"kind":"app","opcode":"eq","args":[{"id":122,"kind":"int","value":2},{"id":123,"kind":"int","value":3}]}},{"id":129,"kind":"def","name":"ne_2_to_3","qualifier":"val","expr":{"id":128,"kind":"app","opcode":"neq","args":[{"id":126,"kind":"int","value":2},{"id":127,"kind":"int","value":3}]}},{"kind":"const","name":"N","typeAnnotation":{"id":12,"kind":"int"},"id":13},{"id":135,"kind":"def","name":"VeryTrue","qualifier":"val","expr":{"id":134,"kind":"app","opcode":"eq","args":[{"id":132,"kind":"app","opcode":"iadd","args":[{"id":130,"kind":"int","value":2},{"id":131,"kind":"int","value":2}]},{"id":133,"kind":"int","value":4}]}},{"id":139,"kind":"def","name":"nat_includes_one","qualifier":"val","expr":{"id":138,"kind":"app","opcode":"in","args":[{"id":136,"kind":"int","value":1},{"id":137,"kind":"name","name":"Nat"}]}},{"id":151,"kind":"def","name":"withType","qualifier":"val","expr":{"id":150,"kind":"app","opcode":"Set","args":[{"id":148,"kind":"int","value":1},{"id":149,"kind":"int","value":2}]},"typeAnnotation":{"id":147,"kind":"set","elem":{"id":146,"kind":"int"}}},{"id":152,"kind":"typedef","name":"PROC"},{"kind":"var","name":"n","typeAnnotation":{"id":157,"kind":"int"},"id":158},{"kind":"const","name":"S","typeAnnotation":{"id":15,"kind":"set","elem":{"id":14,"kind":"int"}},"id":16},{"id":160,"kind":"def","name":"magicNumber","qualifier":"pureval","expr":{"id":159,"kind":"int","value":42}},{"kind":"const","name":"MySet","typeAnnotation":{"id":18,"kind":"set","elem":{"id":17,"kind":"int"}},"id":19},{"kind":"var","name":"k","typeAnnotation":{"id":197,"kind":"int"},"id":198},{"id":219,"kind":"def","name":"test_and","qualifier":"val","expr":{"id":218,"kind":"app","opcode":"and","args":[{"id":216,"kind":"bool","value":false},{"id":217,"kind":"bool","value":true}]}},{"kind":"const","name":"MySeq","typeAnnotation":{"id":21,"kind":"list","elem":{"id":20,"kind":"bool"}},"id":22},{"id":223,"kind":"def","name":"test_or","qualifier":"val","expr":{"id":222,"kind":"app","opcode":"or","args":[{"id":220,"kind":"bool","value":false},{"id":221,"kind":"bool","value":true}]}},{"id":227,"kind":"def","name":"test_implies","qualifier":"val","expr":{"id":226,"kind":"app","opcode":"implies","args":[{"id":224,"kind":"bool","value":false},{"id":225,"kind":"bool","value":true}]}},{"id":256,"kind":"def","name":"test_block_and","qualifier":"val","expr":{"id":255,"kind":"app","opcode":"and","args":[{"id":252,"kind":"bool","value":false},{"id":253,"kind":"bool","value":true},{"id":254,"kind":"bool","value":false}]}},{"kind":"const","name":"MyFun","typeAnnotation":{"id":25,"kind":"fun","arg":{"id":23,"kind":"int"},"res":{"id":24,"kind":"str"}},"id":26},{"id":261,"kind":"def","name":"test_action_and","qualifier":"action","expr":{"id":260,"kind":"app","opcode":"actionAll","args":[{"id":257,"kind":"bool","value":false},{"id":258,"kind":"bool","value":true},{"id":259,"kind":"bool","value":false}]}},{"id":266,"kind":"def","name":"test_block_or","qualifier":"val","expr":{"id":265,"kind":"app","opcode":"or","args":[{"id":262,"kind":"bool","value":false},{"id":263,"kind":"bool","value":true},{"id":264,"kind":"bool","value":false}]}},{"id":271,"kind":"def","name":"test_action_or","qualifier":"action","expr":{"id":270,"kind":"app","opcode":"actionAny","args":[{"id":267,"kind":"bool","value":false},{"id":268,"kind":"bool","value":true},{"id":269,"kind":"bool","value":false}]}},{"id":276,"kind":"def","name":"test_ite","qualifier":"val","expr":{"id":275,"kind":"app","opcode":"ite","args":[{"id":272,"kind":"bool","value":true},{"id":273,"kind":"int","value":1},{"id":274,"kind":"int","value":0}]}},{"kind":"var","name":"f1","typeAnnotation":{"id":292,"kind":"fun","arg":{"id":290,"kind":"str"},"res":{"id":291,"kind":"int"}},"id":293},{"id":301,"kind":"def","name":"MyOper","qualifier":"def","expr":{"id":301,"kind":"lambda","params":[{"id":298,"name":"a"},{"id":299,"name":"b"}],"qualifier":"def","expr":{"id":300,"kind":"int","value":1}}},{"id":313,"kind":"def","name":"oper_in","qualifier":"val","expr":{"id":312,"kind":"app","opcode":"in","args":[{"id":310,"kind":"int","value":1},{"id":311,"kind":"app","opcode":"Set","args":[]}]}},{"kind":"const","name":"MyFunFun","typeAnnotation":{"id":31,"kind":"fun","arg":{"id":29,"kind":"fun","arg":{"id":27,"kind":"int"},"res":{"id":28,"kind":"str"}},"res":{"id":30,"kind":"bool"}},"id":32},{"kind":"const","name":"MyOperator","typeAnnotation":{"id":36,"kind":"oper","args":[{"id":33,"kind":"int"},{"id":34,"kind":"str"}],"res":{"id":35,"kind":"bool"}},"id":37},{"id":378,"kind":"def","name":"one","qualifier":"val","expr":{"id":377,"kind":"app","opcode":"head","args":[{"id":376,"kind":"app","opcode":"List","args":[{"id":374,"kind":"int","value":1},{"id":375,"kind":"int","value":2}]}]}},{"id":383,"kind":"def","name":"test_tuple","qualifier":"val","expr":{"id":382,"kind":"app","opcode":"Tup","args":[{"id":379,"kind":"int","value":1},{"id":380,"kind":"int","value":2},{"id":381,"kind":"int","value":3}]}},{"id":388,"kind":"def","name":"test_tuple2","qualifier":"val","expr":{"id":387,"kind":"app","opcode":"Tup","args":[{"id":384,"kind":"int","value":1},{"id":385,"kind":"int","value":2},{"id":386,"kind":"int","value":3}]}},{"id":392,"kind":"def","name":"test_pair","qualifier":"val","expr":{"id":391,"kind":"app","opcode":"Tup","args":[{"id":389,"kind":"int","value":4},{"id":390,"kind":"int","value":5}]}},{"id":397,"kind":"def","name":"test_list","qualifier":"val","expr":{"id":396,"kind":"app","opcode":"List","args":[{"id":393,"kind":"int","value":1},{"id":394,"kind":"int","value":2},{"id":395,"kind":"int","value":3}]}},{"id":402,"kind":"def","name":"test_list2","qualifier":"val","expr":{"id":401,"kind":"app","opcode":"List","args":[{"id":398,"kind":"int","value":1},{"id":399,"kind":"int","value":2},{"id":400,"kind":"int","value":3}]}},{"id":409,"kind":"def","name":"test_list_nth","qualifier":"val","expr":{"id":408,"kind":"app","opcode":"nth","args":[{"id":406,"kind":"app","opcode":"List","args":[{"id":403,"kind":"int","value":2},{"id":404,"kind":"int","value":3},{"id":405,"kind":"int","value":4}]},{"id":407,"kind":"int","value":2}]}},{"id":415,"kind":"def","name":"test_record","qualifier":"val","expr":{"id":414,"kind":"app","opcode":"Rec","args":[{"id":411,"kind":"str","value":"name"},{"id":410,"kind":"str","value":"igor"},{"id":413,"kind":"str","value":"year"},{"id":412,"kind":"int","value":1981}]}},{"kind":"const","name":"MyOperatorWithComma","typeAnnotation":{"id":41,"kind":"oper","args":[{"id":38,"kind":"int"},{"id":39,"kind":"str"}],"res":{"id":40,"kind":"bool"}},"id":42},{"id":421,"kind":"def","name":"test_record2","qualifier":"val","expr":{"id":420,"kind":"app","opcode":"Rec","args":[{"id":416,"kind":"str","value":"name"},{"id":417,"kind":"str","value":"igor"},{"id":418,"kind":"str","value":"year"},{"id":419,"kind":"int","value":1981}]}},{"id":434,"kind":"def","name":"test_set","qualifier":"val","expr":{"id":433,"kind":"app","opcode":"Set","args":[{"id":430,"kind":"int","value":1},{"id":431,"kind":"int","value":2},{"id":432,"kind":"int","value":3}]}},{"id":463,"kind":"def","name":"in_2_empty","qualifier":"val","expr":{"id":462,"kind":"app","opcode":"in","args":[{"id":460,"kind":"int","value":2},{"id":461,"kind":"app","opcode":"Set","args":[]}]}},{"id":467,"kind":"def","name":"subseteq_empty","qualifier":"val","expr":{"id":466,"kind":"app","opcode":"subseteq","args":[{"id":464,"kind":"app","opcode":"Set","args":[]},{"id":465,"kind":"app","opcode":"Set","args":[]}]}},{"kind":"const","name":"MyTuple","typeAnnotation":{"id":46,"kind":"tup","fields":{"kind":"row","fields":[{"fieldName":"0","fieldType":{"id":43,"kind":"int"}},{"fieldName":"1","fieldType":{"id":44,"kind":"bool"}},{"fieldName":"2","fieldType":{"id":45,"kind":"str"}}],"other":{"kind":"empty"}}},"id":47},{"id":476,"kind":"def","name":"powersets","qualifier":"val","expr":{"id":475,"kind":"app","opcode":"in","args":[{"id":469,"kind":"app","opcode":"Set","args":[{"id":468,"kind":"int","value":1}]},{"id":474,"kind":"app","opcode":"powerset","args":[{"id":473,"kind":"app","opcode":"Set","args":[{"id":470,"kind":"int","value":1},{"id":471,"kind":"int","value":2},{"id":472,"kind":"int","value":3}]}]}]}},{"id":489,"kind":"typedef","name":"INT_SET","type":{"id":488,"kind":"set","elem":{"id":487,"kind":"int"}}},{"id":490,"kind":"typedef","name":"UNINTERPRETED_TYPE"},{"id":502,"kind":"typedef","name":"ENTRY_TYPE","type":{"id":501,"kind":"union","tag":"tag","records":[{"tagValue":"Cat","fields":{"kind":"row","fields":[{"fieldName":"name","fieldType":{"id":496,"kind":"str"}},{"fieldName":"year","fieldType":{"id":497,"kind":"int"}}],"other":{"kind":"empty"}}},{"tagValue":"Date","fields":{"kind":"row","fields":[{"fieldName":"day","fieldType":{"id":498,"kind":"int"}},{"fieldName":"month","fieldType":{"id":499,"kind":"int"}},{"fieldName":"year","fieldType":{"id":500,"kind":"int"}}],"other":{"kind":"empty"}}}]}},{"kind":"const","name":"MyTupleWithComma","typeAnnotation":{"id":51,"kind":"tup","fields":{"kind":"row","fields":[{"fieldName":"0","fieldType":{"id":48,"kind":"int"}},{"fieldName":"1","fieldType":{"id":49,"kind":"bool"}},{"fieldName":"2","fieldType":{"id":50,"kind":"str"}}],"other":{"kind":"empty"}}},"id":52},{"kind":"const","name":"MyRecord","typeAnnotation":{"id":56,"kind":"rec","fields":{"kind":"row","fields":[{"fieldName":"i","fieldType":{"id":53,"kind":"int"}},{"fieldName":"b","fieldType":{"id":54,"kind":"bool"}},{"fieldName":"s","fieldType":{"id":55,"kind":"str"}}],"other":{"kind":"empty"}}},"id":57},{"kind":"const","name":"MyRecordWithComma","typeAnnotation":{"id":61,"kind":"rec","fields":{"kind":"row","fields":[{"fieldName":"i","fieldType":{"id":58,"kind":"int"}},{"fieldName":"b","fieldType":{"id":59,"kind":"bool"}},{"fieldName":"s","fieldType":{"id":60,"kind":"str"}}],"other":{"kind":"empty"}}},"id":62},{"kind":"const","name":"MyUnion","typeAnnotation":{"id":67,"kind":"union","tag":"tag","records":[{"tagValue":"circle","fields":{"kind":"row","fields":[{"fieldName":"radius","fieldType":{"id":63,"kind":"int"}}],"other":{"kind":"empty"}}},{"tagValue":"rectangle","fields":{"kind":"row","fields":[{"fieldName":"width","fieldType":{"id":64,"kind":"int"}},{"fieldName":"height","fieldType":{"id":65,"kind":"int"}}],"other":{"kind":"empty"}}},{"tagValue":"dog","fields":{"kind":"row","fields":[{"fieldName":"name","fieldType":{"id":66,"kind":"str"}}],"other":{"kind":"empty"}}}]},"id":68},{"kind":"const","name":"MyUnionWithComma","typeAnnotation":{"id":73,"kind":"union","tag":"tag","records":[{"tagValue":"circle","fields":{"kind":"row","fields":[{"fieldName":"radius","fieldType":{"id":69,"kind":"int"}}],"other":{"kind":"empty"}}},{"tagValue":"rectangle","fields":{"kind":"row","fields":[{"fieldName":"width","fieldType":{"id":70,"kind":"int"}},{"fieldName":"height","fieldType":{"id":71,"kind":"int"}}],"other":{"kind":"empty"}}},{"tagValue":"dog","fields":{"kind":"row","fields":[{"fieldName":"name","fieldType":{"id":72,"kind":"str"}}],"other":{"kind":"empty"}}}]},"id":74},{"kind":"var","name":"i","typeAnnotation":{"id":75,"kind":"int"},"id":76},{"kind":"var","name":"j","typeAnnotation":{"id":77,"kind":"bool"},"id":78},{"id":82,"kind":"def","name":"add_1_to_2","qualifier":"val","expr":{"id":81,"kind":"app","opcode":"iadd","args":[{"id":79,"kind":"int","value":1},{"id":80,"kind":"int","value":2}]}},{"id":86,"kind":"def","name":"sub_1_to_2","qualifier":"val","expr":{"id":85,"kind":"app","opcode":"isub","args":[{"id":83,"kind":"int","value":1},{"id":84,"kind":"int","value":2}]}},{"id":90,"kind":"def","name":"mul_2_to_3","qualifier":"val","expr":{"id":89,"kind":"app","opcode":"imul","args":[{"id":87,"kind":"int","value":2},{"id":88,"kind":"int","value":3}]}},{"id":94,"kind":"def","name":"div_2_to_3","qualifier":"val","expr":{"id":93,"kind":"app","opcode":"idiv","args":[{"id":91,"kind":"int","value":2},{"id":92,"kind":"int","value":3}]}},{"id":98,"kind":"def","name":"mod_2_to_3","qualifier":"val","expr":{"id":97,"kind":"app","opcode":"imod","args":[{"id":95,"kind":"int","value":2},{"id":96,"kind":"int","value":3}]}},{"id":145,"kind":"def","name":"there_is_truth","qualifier":"val","expr":{"id":144,"kind":"app","opcode":"exists","args":[{"id":140,"kind":"name","name":"Bool"},{"id":143,"kind":"lambda","params":[{"id":141,"name":"x"}],"qualifier":"def","expr":{"id":142,"kind":"name","name":"x"}}]}},{"id":156,"kind":"def","name":"withUninterpretedType","qualifier":"val","expr":{"id":155,"kind":"app","opcode":"Set","args":[]},"typeAnnotation":{"id":154,"kind":"set","elem":{"id":153,"kind":"const","name":"PROC"}}},{"id":166,"kind":"def","name":"add","qualifier":"puredef","expr":{"id":166,"kind":"lambda","params":[{"id":161,"name":"x"},{"id":162,"name":"y"}],"qualifier":"puredef","expr":{"id":165,"kind":"app","opcode":"iadd","args":[{"id":163,"kind":"name","name":"x"},{"id":164,"kind":"name","name":"y"}]}}},{"id":171,"kind":"def","name":"ofN","qualifier":"def","expr":{"id":171,"kind":"lambda","params":[{"id":167,"name":"factor"}],"qualifier":"def","expr":{"id":170,"kind":"app","opcode":"imul","args":[{"id":168,"kind":"name","name":"factor"},{"id":169,"kind":"name","name":"n"}]}}},{"id":176,"kind":"def","name":"A","qualifier":"action","expr":{"id":176,"kind":"lambda","params":[{"id":172,"name":"x"}],"qualifier":"action","expr":{"id":175,"kind":"app","opcode":"assign","args":[{"id":174,"kind":"name","name":"n"},{"id":173,"kind":"name","name":"x"}]}}},{"id":180,"kind":"def","name":"B","qualifier":"puredef","expr":{"id":180,"kind":"lambda","params":[{"id":177,"name":"x"}],"qualifier":"puredef","expr":{"id":179,"kind":"app","opcode":"not","args":[{"id":178,"kind":"name","name":"x"}]}}},{"id":190,"kind":"def","name":"H","qualifier":"def","expr":{"id":190,"kind":"lambda","params":[{"id":181,"name":"x"},{"id":182,"name":"y"}],"qualifier":"def","expr":{"id":189,"kind":"app","opcode":"iadd","args":[{"id":187,"kind":"name","name":"x"},{"id":188,"kind":"name","name":"y"}]}},"typeAnnotation":{"id":186,"kind":"oper","args":[{"id":183,"kind":"int"},{"id":184,"kind":"int"}],"res":{"id":185,"kind":"int"}}},{"id":196,"kind":"def","name":"Pol","qualifier":"def","expr":{"id":196,"kind":"lambda","params":[{"id":191,"name":"x"}],"qualifier":"def","expr":{"id":195,"kind":"name","name":"x"}},"typeAnnotation":{"id":194,"kind":"oper","args":[{"id":192,"kind":"var","name":"a"}],"res":{"id":193,"kind":"var","name":"a"}}},{"id":202,"kind":"def","name":"asgn","qualifier":"action","expr":{"id":201,"kind":"app","opcode":"assign","args":[{"id":200,"kind":"name","name":"k"},{"id":199,"kind":"int","value":3}]}},{"id":215,"kind":"def","name":"min","qualifier":"puredef","expr":{"id":215,"kind":"lambda","params":[{"id":203,"name":"x"},{"id":205,"name":"y"}],"qualifier":"puredef","expr":{"id":213,"kind":"app","opcode":"ite","args":[{"id":210,"kind":"app","opcode":"ilt","args":[{"id":208,"kind":"name","name":"x"},{"id":209,"kind":"name","name":"y"}]},{"id":211,"kind":"name","name":"x"},{"id":212,"kind":"name","name":"y"}]}},"typeAnnotation":{"id":214,"kind":"oper","args":[{"id":204,"kind":"int"},{"id":206,"kind":"int"}],"res":{"id":207,"kind":"int"}}},{"id":230,"kind":"def","name":"F","qualifier":"def","expr":{"id":230,"kind":"lambda","params":[{"id":228,"name":"x"}],"qualifier":"def","expr":{"id":229,"kind":"name","name":"x"}}},{"id":289,"kind":"def","name":"test_ite2","qualifier":"def","expr":{"id":289,"kind":"lambda","params":[{"id":277,"name":"x"},{"id":278,"name":"y"}],"qualifier":"def","expr":{"id":288,"kind":"app","opcode":"ite","args":[{"id":281,"kind":"app","opcode":"ilt","args":[{"id":279,"kind":"name","name":"x"},{"id":280,"kind":"int","value":10}]},{"id":284,"kind":"app","opcode":"iadd","args":[{"id":282,"kind":"name","name":"y"},{"id":283,"kind":"int","value":5}]},{"id":287,"kind":"app","opcode":"imod","args":[{"id":285,"kind":"name","name":"y"},{"id":286,"kind":"int","value":5}]}]}}},{"id":297,"kind":"def","name":"funapp","qualifier":"val","expr":{"id":296,"kind":"app","opcode":"get","args":[{"id":294,"kind":"name","name":"f1"},{"id":295,"kind":"str","value":"a"}]}},{"id":305,"kind":"def","name":"oper_app_normal","qualifier":"val","expr":{"id":304,"kind":"app","opcode":"MyOper","args":[{"id":302,"kind":"str","value":"a"},{"id":303,"kind":"int","value":42}]}},{"id":309,"kind":"def","name":"oper_app_ufcs","qualifier":"val","expr":{"id":308,"kind":"app","opcode":"MyOper","args":[{"id":306,"kind":"str","value":"a"},{"id":307,"kind":"int","value":42}]}},{"id":321,"kind":"def","name":"oper_app_dot1","qualifier":"val","expr":{"id":320,"kind":"app","opcode":"filter","args":[{"id":314,"kind":"name","name":"S"},{"id":319,"kind":"lambda","params":[{"id":315,"name":"x"}],"qualifier":"def","expr":{"id":318,"kind":"app","opcode":"igt","args":[{"id":316,"kind":"name","name":"x"},{"id":317,"kind":"int","value":10}]}}]}},{"id":359,"kind":"def","name":"oper_app_dot4","qualifier":"val","expr":{"id":358,"kind":"app","opcode":"filter","args":[{"id":354,"kind":"name","name":"S"},{"id":357,"kind":"lambda","params":[{"id":355,"name":"_"}],"qualifier":"def","expr":{"id":356,"kind":"bool","value":true}}]}},{"id":367,"kind":"def","name":"f","qualifier":"val","expr":{"id":366,"kind":"app","opcode":"mapBy","args":[{"id":360,"kind":"name","name":"S"},{"id":365,"kind":"lambda","params":[{"id":361,"name":"x"}],"qualifier":"def","expr":{"id":364,"kind":"app","opcode":"iadd","args":[{"id":362,"kind":"name","name":"x"},{"id":363,"kind":"int","value":1}]}}]}},{"id":373,"kind":"def","name":"set_difference","qualifier":"val","expr":{"id":372,"kind":"app","opcode":"exclude","args":[{"id":368,"kind":"name","name":"S"},{"id":371,"kind":"app","opcode":"Set","args":[{"id":369,"kind":"int","value":3},{"id":370,"kind":"int","value":4}]}]}},{"id":429,"kind":"def","name":"test_record3","qualifier":"val","expr":{"id":428,"kind":"app","opcode":"with","args":[{"id":427,"kind":"app","opcode":"with","args":[{"id":426,"kind":"name","name":"test_record"},{"id":423,"kind":"str","value":"name"},{"id":422,"kind":"str","value":"quint"}]},{"id":425,"kind":"str","value":"year"},{"id":424,"kind":"int","value":2023}]}},{"id":445,"kind":"def","name":"rec_field","qualifier":"val","expr":{"id":444,"kind":"let","opdef":{"id":440,"kind":"def","name":"my_rec","qualifier":"val","expr":{"id":439,"kind":"app","opcode":"Rec","args":[{"id":436,"kind":"str","value":"a"},{"id":435,"kind":"int","value":1},{"id":438,"kind":"str","value":"b"},{"id":437,"kind":"str","value":"foo"}]}},"expr":{"id":443,"kind":"app","opcode":"field","args":[{"id":441,"kind":"name","name":"my_rec"},{"id":442,"kind":"str","value":"a"}]}}},{"id":454,"kind":"def","name":"tup_elem","qualifier":"val","expr":{"id":453,"kind":"let","opdef":{"id":449,"kind":"def","name":"my_tup","qualifier":"val","expr":{"id":448,"kind":"app","opcode":"Tup","args":[{"id":446,"kind":"str","value":"a"},{"id":447,"kind":"int","value":3}]}},"expr":{"id":452,"kind":"app","opcode":"item","args":[{"id":450,"kind":"name","name":"my_tup"},{"id":451,"kind":"int","value":2}]}}},{"id":459,"kind":"def","name":"isEmpty","qualifier":"def","expr":{"id":459,"kind":"lambda","params":[{"id":455,"name":"s"}],"qualifier":"def","expr":{"id":458,"kind":"app","opcode":"eq","args":[{"id":456,"kind":"name","name":"s"},{"id":457,"kind":"app","opcode":"List","args":[]}]}}},{"id":480,"kind":"assume","name":"positive","assumption":{"id":479,"kind":"app","opcode":"igt","args":[{"id":477,"kind":"name","name":"N"},{"id":478,"kind":"int","value":0}]}},{"id":484,"kind":"assume","name":"_","assumption":{"id":483,"kind":"app","opcode":"neq","args":[{"id":481,"kind":"name","name":"N"},{"id":482,"kind":"int","value":0}]}},{"id":485,"kind":"import","defName":"foo","protoName":"M1"},{"id":486,"kind":"import","defName":"*","protoName":"M2"},{"kind":"var","name":"S1","typeAnnotation":{"id":491,"kind":"const","name":"INT_SET"},"id":492},{"id":495,"kind":"instance","qualifiedName":"Inst1","protoName":"Proto","overrides":[[{"id":494,"name":"N"},{"id":493,"kind":"name","name":"N"}]],"identityOverride":false},{"id":522,"kind":"def","name":"isValid","qualifier":"def","expr":{"id":522,"kind":"lambda","params":[{"id":503,"name":"entry"}],"qualifier":"def","expr":{"id":521,"kind":"app","opcode":"unionMatch","args":[{"id":504,"kind":"name","name":"entry"},{"id":517,"kind":"str","value":"Cat"},{"id":518,"kind":"lambda","params":[{"id":505,"name":"cat"}],"qualifier":"def","expr":{"id":510,"kind":"app","opcode":"neq","args":[{"id":508,"kind":"app","opcode":"field","args":[{"id":506,"kind":"name","name":"cat"},{"id":507,"kind":"str","value":"name"}]},{"id":509,"kind":"str","value":""}]}},{"id":519,"kind":"str","value":"Date"},{"id":520,"kind":"lambda","params":[{"id":511,"name":"date"}],"qualifier":"def","expr":{"id":516,"kind":"app","opcode":"igt","args":[{"id":514,"kind":"app","opcode":"field","args":[{"id":512,"kind":"name","name":"date"},{"id":513,"kind":"str","value":"year"}]},{"id":515,"kind":"int","value":0}]}}]}}},{"id":237,"kind":"def","name":"G","qualifier":"val","expr":{"id":237,"kind":"lambda","params":[{"id":231,"name":"x"}],"qualifier":"val","expr":{"id":236,"kind":"app","opcode":"and","args":[{"id":233,"kind":"app","opcode":"F","args":[{"id":232,"kind":"name","name":"x"}]},{"id":235,"kind":"app","opcode":"not","args":[{"id":234,"kind":"name","name":"x"}]}]}}},{"id":244,"kind":"def","name":"test_and_arg","qualifier":"val","expr":{"id":244,"kind":"lambda","params":[{"id":238,"name":"x"}],"qualifier":"val","expr":{"id":243,"kind":"app","opcode":"and","args":[{"id":240,"kind":"app","opcode":"F","args":[{"id":239,"kind":"name","name":"x"}]},{"id":242,"kind":"app","opcode":"not","args":[{"id":241,"kind":"name","name":"x"}]}]}}},{"id":251,"kind":"def","name":"test_or_arg","qualifier":"val","expr":{"id":251,"kind":"lambda","params":[{"id":245,"name":"x"}],"qualifier":"val","expr":{"id":250,"kind":"app","opcode":"or","args":[{"id":247,"kind":"app","opcode":"F","args":[{"id":246,"kind":"name","name":"x"}]},{"id":249,"kind":"app","opcode":"not","args":[{"id":248,"kind":"name","name":"x"}]}]}}},{"id":341,"kind":"def","name":"tuple_sum","qualifier":"val","expr":{"id":340,"kind":"app","opcode":"map","args":[{"id":324,"kind":"app","opcode":"tuples","args":[{"id":322,"kind":"name","name":"S"},{"id":323,"kind":"name","name":"MySet"}]},{"id":339,"kind":"lambda","params":[{"id":330,"name":"quintTupledLambdaParam330"}],"qualifier":"def","expr":{"id":335,"kind":"let","opdef":{"id":326,"kind":"def","name":"mys","qualifier":"pureval","expr":{"id":336,"kind":"app","opcode":"item","args":[{"id":337,"kind":"name","name":"quintTupledLambdaParam330"},{"id":338,"kind":"int","value":2}]}},"expr":{"id":331,"kind":"let","opdef":{"id":325,"kind":"def","name":"s","qualifier":"pureval","expr":{"id":332,"kind":"app","opcode":"item","args":[{"id":333,"kind":"name","name":"quintTupledLambdaParam330"},{"id":334,"kind":"int","value":1}]}},"expr":{"id":329,"kind":"app","opcode":"iadd","args":[{"id":327,"kind":"name","name":"s"},{"id":328,"kind":"name","name":"mys"}]}}}}]}},{"id":353,"kind":"def","name":"oper_nondet","qualifier":"action","expr":{"id":352,"kind":"let","opdef":{"id":344,"kind":"def","name":"x","qualifier":"nondet","expr":{"id":343,"kind":"app","opcode":"oneOf","args":[{"id":342,"kind":"name","name":"S"}]}},"expr":{"id":351,"kind":"app","opcode":"actionAll","args":[{"id":347,"kind":"app","opcode":"igt","args":[{"id":345,"kind":"name","name":"x"},{"id":346,"kind":"int","value":10}]},{"id":350,"kind":"app","opcode":"assign","args":[{"id":349,"kind":"name","name":"k"},{"id":348,"kind":"name","name":"x"}]}]}}}]}],"table":{"142":{"id":141,"name":"x","kind":"param"},"153":{"id":152,"kind":"typedef","name":"PROC"},"163":{"id":161,"name":"x","kind":"param"},"164":{"id":162,"name":"y","kind":"param"},"168":{"id":167,"name":"factor","kind":"param"},"169":{"kind":"var","name":"n","typeAnnotation":{"id":157,"kind":"int"},"id":158},"173":{"id":172,"name":"x","kind":"param"},"174":{"kind":"var","name":"n","typeAnnotation":{"id":157,"kind":"int"},"id":158},"178":{"id":177,"name":"x","kind":"param"},"187":{"id":181,"name":"x","kind":"param"},"188":{"id":182,"name":"y","kind":"param"},"195":{"id":191,"name":"x","kind":"param"},"200":{"kind":"var","name":"k","typeAnnotation":{"id":197,"kind":"int"},"id":198},"208":{"id":203,"name":"x","kind":"param"},"209":{"id":205,"name":"y","kind":"param"},"211":{"id":203,"name":"x","kind":"param"},"212":{"id":205,"name":"y","kind":"param"},"229":{"id":228,"name":"x","kind":"param"},"232":{"id":231,"name":"x","kind":"param"},"233":{"id":230,"kind":"def","name":"F","qualifier":"def","expr":{"id":230,"kind":"lambda","params":[{"id":228,"name":"x"}],"qualifier":"def","expr":{"id":229,"kind":"name","name":"x"}},"depth":0},"234":{"id":231,"name":"x","kind":"param"},"239":{"id":238,"name":"x","kind":"param"},"240":{"id":230,"kind":"def","name":"F","qualifier":"def","expr":{"id":230,"kind":"lambda","params":[{"id":228,"name":"x"}],"qualifier":"def","expr":{"id":229,"kind":"name","name":"x"}},"depth":0},"241":{"id":238,"name":"x","kind":"param"},"246":{"id":245,"name":"x","kind":"param"},"247":{"id":230,"kind":"def","name":"F","qualifier":"def","expr":{"id":230,"kind":"lambda","params":[{"id":228,"name":"x"}],"qualifier":"def","expr":{"id":229,"kind":"name","name":"x"}},"depth":0},"248":{"id":245,"name":"x","kind":"param"},"279":{"id":277,"name":"x","kind":"param"},"282":{"id":278,"name":"y","kind":"param"},"285":{"id":278,"name":"y","kind":"param"},"294":{"kind":"var","name":"f1","typeAnnotation":{"id":292,"kind":"fun","arg":{"id":290,"kind":"str"},"res":{"id":291,"kind":"int"}},"id":293},"304":{"id":301,"kind":"def","name":"MyOper","qualifier":"def","expr":{"id":301,"kind":"lambda","params":[{"id":298,"name":"a"},{"id":299,"name":"b"}],"qualifier":"def","expr":{"id":300,"kind":"int","value":1}},"depth":0},"308":{"id":301,"kind":"def","name":"MyOper","qualifier":"def","expr":{"id":301,"kind":"lambda","params":[{"id":298,"name":"a"},{"id":299,"name":"b"}],"qualifier":"def","expr":{"id":300,"kind":"int","value":1}},"depth":0},"314":{"kind":"const","name":"S","typeAnnotation":{"id":15,"kind":"set","elem":{"id":14,"kind":"int"}},"id":16},"316":{"id":315,"name":"x","kind":"param"},"322":{"kind":"const","name":"S","typeAnnotation":{"id":15,"kind":"set","elem":{"id":14,"kind":"int"}},"id":16},"323":{"kind":"const","name":"MySet","typeAnnotation":{"id":18,"kind":"set","elem":{"id":17,"kind":"int"}},"id":19},"327":{"id":325,"kind":"def","name":"s","qualifier":"pureval","expr":{"id":332,"kind":"app","opcode":"item","args":[{"id":333,"kind":"name","name":"quintTupledLambdaParam330"},{"id":334,"kind":"int","value":1}]},"depth":1},"328":{"id":326,"kind":"def","name":"mys","qualifier":"pureval","expr":{"id":336,"kind":"app","opcode":"item","args":[{"id":337,"kind":"name","name":"quintTupledLambdaParam330"},{"id":338,"kind":"int","value":2}]},"depth":1},"333":{"id":330,"name":"quintTupledLambdaParam330","kind":"param"},"337":{"id":330,"name":"quintTupledLambdaParam330","kind":"param"},"342":{"kind":"const","name":"S","typeAnnotation":{"id":15,"kind":"set","elem":{"id":14,"kind":"int"}},"id":16},"345":{"id":344,"kind":"def","name":"x","qualifier":"nondet","expr":{"id":343,"kind":"app","opcode":"oneOf","args":[{"id":342,"kind":"name","name":"S"}]},"depth":1},"348":{"id":344,"kind":"def","name":"x","qualifier":"nondet","expr":{"id":343,"kind":"app","opcode":"oneOf","args":[{"id":342,"kind":"name","name":"S"}]},"depth":1},"349":{"kind":"var","name":"k","typeAnnotation":{"id":197,"kind":"int"},"id":198},"354":{"kind":"const","name":"S","typeAnnotation":{"id":15,"kind":"set","elem":{"id":14,"kind":"int"}},"id":16},"360":{"kind":"const","name":"S","typeAnnotation":{"id":15,"kind":"set","elem":{"id":14,"kind":"int"}},"id":16},"362":{"id":361,"name":"x","kind":"param"},"368":{"kind":"const","name":"S","typeAnnotation":{"id":15,"kind":"set","elem":{"id":14,"kind":"int"}},"id":16},"426":{"id":415,"kind":"def","name":"test_record","qualifier":"val","expr":{"id":414,"kind":"app","opcode":"Rec","args":[{"id":411,"kind":"str","value":"name"},{"id":410,"kind":"str","value":"igor"},{"id":413,"kind":"str","value":"year"},{"id":412,"kind":"int","value":1981}]},"depth":0},"441":{"id":440,"kind":"def","name":"my_rec","qualifier":"val","expr":{"id":439,"kind":"app","opcode":"Rec","args":[{"id":436,"kind":"str","value":"a"},{"id":435,"kind":"int","value":1},{"id":438,"kind":"str","value":"b"},{"id":437,"kind":"str","value":"foo"}]},"depth":1},"450":{"id":449,"kind":"def","name":"my_tup","qualifier":"val","expr":{"id":448,"kind":"app","opcode":"Tup","args":[{"id":446,"kind":"str","value":"a"},{"id":447,"kind":"int","value":3}]},"depth":1},"456":{"id":455,"name":"s","kind":"param"},"477":{"kind":"const","name":"N","typeAnnotation":{"id":12,"kind":"int"},"id":13},"481":{"kind":"const","name":"N","typeAnnotation":{"id":12,"kind":"int"},"id":13},"491":{"id":489,"kind":"typedef","name":"INT_SET","type":{"id":488,"kind":"set","elem":{"id":487,"kind":"int"}}},"493":{"kind":"const","name":"N","typeAnnotation":{"id":12,"kind":"int"},"id":13},"494":{"kind":"const","name":"N","typeAnnotation":{"id":7,"kind":"int"},"id":493,"importedFrom":{"id":495,"kind":"instance","qualifiedName":"Inst1","protoName":"Proto","overrides":[[{"id":494,"name":"N"},{"id":493,"kind":"name","name":"N"}]],"identityOverride":false},"hidden":true,"namespaces":["Inst1","withConsts"]},"504":{"id":503,"name":"entry","kind":"param"},"506":{"id":505,"name":"cat","kind":"param"},"512":{"id":511,"name":"date","kind":"param"}}} \ No newline at end of file +{"stage":"parsing","warnings":[],"errors":[{"explanation":"extraneous input 'match' expecting {'}', 'const', 'var', 'assume', 'type', 'val', 'def', 'pure', 'action', 'run', 'temporal', 'import', 'export', DOCCOMMENT}","locs":[{"source":"mocked_path/testFixture/SuperSpec.qnt","start":{"line":233,"col":10,"index":5236},"end":{"line":233,"col":14,"index":5240}}]}]} \ No newline at end of file diff --git a/quint/testFixture/SuperSpec.qnt b/quint/testFixture/SuperSpec.qnt index ff7489cf2..c35e56005 100644 --- a/quint/testFixture/SuperSpec.qnt +++ b/quint/testFixture/SuperSpec.qnt @@ -226,14 +226,4 @@ module withConsts { // create an instance of Proto by using '*' // import Proto(*) as Inst2 - - // Match - type ENTRY_TYPE = - | { tag: "Cat", name: str, year: int } - | { tag: "Date", day: int, month: int, year: int } - - def isValid(entry) = - entry match - | "Cat": cat => cat.name != "" - | "Date": date => date.year > 0 } diff --git a/quint/testFixture/_1025importeeWithError.json b/quint/testFixture/_1025importeeWithError.json index 1b8d2045f..4027490ae 100644 --- a/quint/testFixture/_1025importeeWithError.json +++ b/quint/testFixture/_1025importeeWithError.json @@ -1 +1 @@ -{"stage":"parsing","warnings":[],"errors":[{"explanation":"mismatched input '}' expecting {'{', 'nondet', 'val', 'def', 'pure', 'action', 'run', 'temporal', '[', 'all', 'any', 'if', '_', STRING, BOOL, INT, 'and', 'or', 'iff', 'implies', 'Set', 'List', 'Map', '-', '(', IDENTIFIER}","locs":[{"source":"mocked_path/testFixture/_1025importeeWithError.qnt","start":{"line":3,"col":0,"index":45},"end":{"line":3,"col":0,"index":45}}]}]} \ No newline at end of file +{"stage":"parsing","warnings":[],"errors":[{"explanation":"mismatched input '}' expecting {'{', 'nondet', 'val', 'def', 'pure', 'action', 'run', 'temporal', '[', 'all', 'any', 'if', '_', STRING, BOOL, INT, 'and', 'or', 'iff', 'implies', 'Set', 'List', 'Map', 'match', '-', '(', IDENTIFIER}","locs":[{"source":"mocked_path/testFixture/_1025importeeWithError.qnt","start":{"line":3,"col":0,"index":45},"end":{"line":3,"col":0,"index":45}}]}]} \ No newline at end of file