From 06c24e76e1cf32acea762f7a523eb33719b9dac2 Mon Sep 17 00:00:00 2001 From: bugarela Date: Fri, 1 Mar 2024 18:16:36 -0300 Subject: [PATCH 1/7] Resolve type applications at the IR level --- quint/src/quintAnalyzer.ts | 17 ++++++++++---- quint/src/types/inferrer.ts | 17 ++------------ quint/src/types/typeApplicationResolution.ts | 24 ++++++++++++++------ 3 files changed, 31 insertions(+), 27 deletions(-) diff --git a/quint/src/quintAnalyzer.ts b/quint/src/quintAnalyzer.ts index e7bc4b7c9..beace6c1f 100644 --- a/quint/src/quintAnalyzer.ts +++ b/quint/src/quintAnalyzer.ts @@ -22,6 +22,7 @@ import { ModeChecker } from './effects/modeChecker' import { QuintError } from './quintError' import { errorTreeToString } from './errorTree' import { MultipleUpdatesChecker } from './effects/MultipleUpdatesChecker' +import { TypeApplicationResolver } from './types/typeApplicationResolution' /* Products from static analysis */ export type AnalysisOutput = { @@ -42,7 +43,7 @@ export type AnalysisResult = [QuintError[], AnalysisOutput] */ export function analyzeModules(lookupTable: LookupTable, quintModules: QuintModule[]): AnalysisResult { const analyzer = new QuintAnalyzer(lookupTable) - quintModules.map(m => analyzer.analyzeDeclarations(m.declarations)) + quintModules.forEach(m => (m.declarations = analyzer.analyzeDeclarations(m.declarations))) return analyzer.getResult() } @@ -75,6 +76,7 @@ export function analyzeInc( * @param previousOutput - The previous analysis output to be used as a starting point. */ class QuintAnalyzer { + private typeApplicationResolver: TypeApplicationResolver private effectInferrer: EffectInferrer private typeInferrer: TypeInferrer private modeChecker: ModeChecker @@ -84,17 +86,20 @@ class QuintAnalyzer { private output: AnalysisOutput = { types: new Map(), effects: new Map(), modes: new Map() } constructor(lookupTable: LookupTable, previousOutput?: AnalysisOutput) { + this.typeApplicationResolver = new TypeApplicationResolver(lookupTable) this.typeInferrer = new TypeInferrer(lookupTable, previousOutput?.types) this.effectInferrer = new EffectInferrer(lookupTable, previousOutput?.effects) this.multipleUpdatesChecker = new MultipleUpdatesChecker() this.modeChecker = new ModeChecker(previousOutput?.modes) } - analyzeDeclarations(decls: QuintDeclaration[]): void { - const [typeErrMap, types] = this.typeInferrer.inferTypes(decls) - const [effectErrMap, effects] = this.effectInferrer.inferEffects(decls) + analyzeDeclarations(decls: QuintDeclaration[]): QuintDeclaration[] { + const resolvedDecls = this.typeApplicationResolver.resolveTypeApplications(decls) + + const [typeErrMap, types] = this.typeInferrer.inferTypes(resolvedDecls) + const [effectErrMap, effects] = this.effectInferrer.inferEffects(resolvedDecls) const updatesErrMap = this.multipleUpdatesChecker.checkEffects([...effects.values()]) - const [modeErrMap, modes] = this.modeChecker.checkModes(decls, effects) + const [modeErrMap, modes] = this.modeChecker.checkModes(resolvedDecls, effects) const errorTrees = [...typeErrMap, ...effectErrMap] @@ -114,6 +119,8 @@ class QuintAnalyzer { effects: new Map([...this.output.effects, ...effects]), modes: new Map([...this.output.modes, ...modes]), } + + return resolvedDecls } getResult(): AnalysisResult { diff --git a/quint/src/types/inferrer.ts b/quint/src/types/inferrer.ts index 1fbfedfd1..a0f349552 100644 --- a/quint/src/types/inferrer.ts +++ b/quint/src/types/inferrer.ts @@ -16,21 +16,17 @@ import { ErrorTree } from '../errorTree' import { walkDeclaration } from '../ir/IRVisitor' import { LookupTable } from '../names/base' -import { QuintDeclaration } from '../ir/quintIr' +import { QuintDeclaration, isDef } from '../ir/quintIr' import { TypeScheme } from './base' import { ConstraintGeneratorVisitor } from './constraintGenerator' import { solveConstraint } from './constraintSolver' import { simplify } from './simplification' -import { TypeApplicationResolver } from './typeApplicationResolution' -import { transformDeclaration, transformLookupDefinition } from '../ir/IRTransformer' export type TypeInferenceResult = [Map, Map] export class TypeInferrer extends ConstraintGeneratorVisitor { - private resolver: TypeApplicationResolver constructor(table: LookupTable, types?: Map) { super(solveConstraint, table, types) - this.resolver = new TypeApplicationResolver(this.table, this.freshVarGenerator) } /** @@ -43,17 +39,8 @@ export class TypeInferrer extends ConstraintGeneratorVisitor { */ inferTypes(declarations: QuintDeclaration[]): TypeInferenceResult { // Resolve all type applications used in expressions in the lookup table - this.table.forEach((def, id) => { - // Don't resolve type definitions, since those should keep their original type variable names - // They are our source of truth for all resolutions - if (def.kind !== 'typedef') { - const resolvedLookupDef = transformLookupDefinition(this.resolver, def) - this.table.set(id, resolvedLookupDef) - } - }) declarations.forEach(decl => { - const resolvedDecl = transformDeclaration(this.resolver, decl) - walkDeclaration(this, resolvedDecl) + walkDeclaration(this, decl) }) const simplifiedTypes = new Map([...this.types.entries()].map(([id, t]) => [id, simplify(t)])) return [this.errors, simplifiedTypes] diff --git a/quint/src/types/typeApplicationResolution.ts b/quint/src/types/typeApplicationResolution.ts index c84ce9474..a20d0a975 100644 --- a/quint/src/types/typeApplicationResolution.ts +++ b/quint/src/types/typeApplicationResolution.ts @@ -14,9 +14,10 @@ import { fail } from 'assert' import { FreshVarGenerator } from '../FreshVarGenerator' + import { typeToString } from '../ir/IRprinting' -import { IRTransformer, transformType } from '../ir/IRTransformer' -import { QuintTypeAlias } from '../ir/quintIr' +import { IRTransformer, transformDeclaration, transformLookupDefinition, transformType } from '../ir/IRTransformer' +import { QuintDeclaration, QuintTypeAlias } from '../ir/quintIr' import { QuintAppType, QuintType, QuintVarType, Row } from '../ir/quintTypes' import { LookupTable } from '../names/base' import { zip } from '../util' @@ -29,13 +30,22 @@ export class TypeApplicationResolver implements IRTransformer { // Lookup table from the parser private table: LookupTable - constructor(table: LookupTable, freshVarGenerator: FreshVarGenerator) { + constructor(table: LookupTable) { this.table = table - this.freshVarGenerator = freshVarGenerator + this.freshVarGenerator = new FreshVarGenerator() + + this.table.forEach((def, id) => { + const resolvedLookupDef = transformLookupDefinition(this, def) + this.table.set(id, resolvedLookupDef) + }) + } + + resolveTypeApplications(decls: QuintDeclaration[]): QuintDeclaration[] { + return decls.map(decl => transformDeclaration(this, decl)) } exitType(t: QuintType): QuintType { - return this.resolveTypeApplications(t) + return this.resolveTypeApplicationsForType(t) } // Transforms `t` by resolving all the type applications in all its sub-terms @@ -46,8 +56,8 @@ export class TypeApplicationResolver implements IRTransformer { // type Bar[x, y] = {i: x, j: y} // // - // resolveTypeApplications(Foo[a, {f: Bar[int, str]}]) = (a, {f: {i: int, j: str}}) - resolveTypeApplications(t: QuintType): QuintType { + // resolveTypeApplicationsForType(Foo[a, {f: Bar[int, str]}]) = (a, {f: {i: int, j: str}}) + private resolveTypeApplicationsForType(t: QuintType): QuintType { const f: (_: QuintType) => QuintType = x => (x.kind !== 'app' ? x : this.resolveTypeApp(x)) return mapType(f, t) } From 44ad95176dda6a01f1703c3886815cf50f6db2b2 Mon Sep 17 00:00:00 2001 From: Shon Feder Date: Fri, 1 Mar 2024 22:36:48 -0500 Subject: [PATCH 2/7] Add regression test for 1391 --- quint/test/flattening/fullFlattener.test.ts | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/quint/test/flattening/fullFlattener.test.ts b/quint/test/flattening/fullFlattener.test.ts index f55422999..6dc0c8c39 100644 --- a/quint/test/flattening/fullFlattener.test.ts +++ b/quint/test/flattening/fullFlattener.test.ts @@ -235,4 +235,19 @@ describe('flattenModules', () => { assertFlattenedModule(text) }) + + // Regression test for https://github.com/informalsystems/quint/issues/1391 + describe('can flatten with polymorphic types between different modules (#802)', () => { + const text = `module A { + type Foo[a] = F(a) + def mapFoo(x: Foo[a], f: a => b): Foo[b] = match x { F(v) => F(f(v)) } + } + + module B { + import A.* + val b: Foo[int] = F("one").mapFoo(_ => 1) + }` + + assertFlattenedModule(text) + }) }) From be70a9ed41ca1294e5022e9a1fda8acc5b758b06 Mon Sep 17 00:00:00 2001 From: Shon Feder Date: Fri, 1 Mar 2024 23:08:40 -0500 Subject: [PATCH 3/7] Resolve type apps in type inference tests --- quint/test/types/inferrer.test.ts | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/quint/test/types/inferrer.test.ts b/quint/test/types/inferrer.test.ts index be12dfcf3..1a1e20976 100644 --- a/quint/test/types/inferrer.test.ts +++ b/quint/test/types/inferrer.test.ts @@ -4,6 +4,7 @@ import { TypeInferenceResult, TypeInferrer } from '../../src/types/inferrer' import { typeSchemeToString } from '../../src/types/printing' import { errorTreeToString } from '../../src/errorTree' import { parseMockedModule } from '../util' +import { TypeApplicationResolver } from '../../src/types/typeApplicationResolution' // Utility used to print update `stringType` values to make // updating the expected values in the following tests less @@ -16,9 +17,12 @@ function _printUpdatedStringTypes(stringTypes: (string | bigint)[][]) { describe('inferTypes', () => { function inferTypesForModules(text: string): TypeInferenceResult { - const { modules, table } = parseMockedModule(text) + const { modules: parsedModules, table } = parseMockedModule(text) + // Type inference assumes all type applications (e.g., `Foo[int, str]`) have been resolved. + const resolver = new TypeApplicationResolver(table) const inferrer = new TypeInferrer(table) + const modules = parsedModules.map(m => ({ ...m, declarations: resolver.resolveTypeApplications(m.declarations) })) return inferrer.inferTypes(modules.flatMap(m => m.declarations)) } From bdabe6433e6f4dfc954e29d91374608bab6ddda1 Mon Sep 17 00:00:00 2001 From: Shon Feder Date: Fri, 1 Mar 2024 23:08:56 -0500 Subject: [PATCH 4/7] Warn about mutations --- quint/src/quintAnalyzer.ts | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/quint/src/quintAnalyzer.ts b/quint/src/quintAnalyzer.ts index beace6c1f..970c7bfc8 100644 --- a/quint/src/quintAnalyzer.ts +++ b/quint/src/quintAnalyzer.ts @@ -37,12 +37,16 @@ export type AnalysisResult = [QuintError[], AnalysisOutput] /** * Analyzes multiple Quint modules and returns the analysis result. * + * NOTE: This is modifies the `lookupTable` and the `quintModules`! + * See XXX for the mutation sites. + * * @param lookupTable - The lookup tables for the modules. * @param quintModules - The Quint modules to be analyzed. * @returns A tuple with a list of errors and the analysis output. */ export function analyzeModules(lookupTable: LookupTable, quintModules: QuintModule[]): AnalysisResult { const analyzer = new QuintAnalyzer(lookupTable) + // XXX: the modules are mutated here. quintModules.forEach(m => (m.declarations = analyzer.analyzeDeclarations(m.declarations))) return analyzer.getResult() } @@ -50,6 +54,9 @@ export function analyzeModules(lookupTable: LookupTable, quintModules: QuintModu /** * Analyzes declarations incrementally and returns the analysis result. * + * NOTE: This is modifies the `lookupTable`! + * See XXX for the mutation sites. + * * @param analysisOutput - The previous analysis output to be used as a starting point. * @param lookupTable - The lookup tables for the modules. * @param declarations - The Quint declarations to be analyzed. @@ -86,6 +93,7 @@ class QuintAnalyzer { private output: AnalysisOutput = { types: new Map(), effects: new Map(), modes: new Map() } constructor(lookupTable: LookupTable, previousOutput?: AnalysisOutput) { + // XXX: the lookUp table is mutated when TypeApplicationResolver is instantiated this.typeApplicationResolver = new TypeApplicationResolver(lookupTable) this.typeInferrer = new TypeInferrer(lookupTable, previousOutput?.types) this.effectInferrer = new EffectInferrer(lookupTable, previousOutput?.effects) @@ -96,6 +104,7 @@ class QuintAnalyzer { analyzeDeclarations(decls: QuintDeclaration[]): QuintDeclaration[] { const resolvedDecls = this.typeApplicationResolver.resolveTypeApplications(decls) + // XXX: the lookUp table is mutated during type inference const [typeErrMap, types] = this.typeInferrer.inferTypes(resolvedDecls) const [effectErrMap, effects] = this.effectInferrer.inferEffects(resolvedDecls) const updatesErrMap = this.multipleUpdatesChecker.checkEffects([...effects.values()]) From 3f7f1d9ae5a55bdbb0bca7eab85a98efcad8bbec Mon Sep 17 00:00:00 2001 From: Shon Feder Date: Fri, 1 Mar 2024 23:53:22 -0500 Subject: [PATCH 5/7] Add error handling for invaild type applications Closes #1390 --- quint/src/quintAnalyzer.ts | 4 +- quint/src/types/typeApplicationResolution.ts | 54 +++++++++++++------- quint/test/types/inferrer.test.ts | 40 +++++++++++++-- 3 files changed, 75 insertions(+), 23 deletions(-) diff --git a/quint/src/quintAnalyzer.ts b/quint/src/quintAnalyzer.ts index 970c7bfc8..32cd723c8 100644 --- a/quint/src/quintAnalyzer.ts +++ b/quint/src/quintAnalyzer.ts @@ -102,7 +102,7 @@ class QuintAnalyzer { } analyzeDeclarations(decls: QuintDeclaration[]): QuintDeclaration[] { - const resolvedDecls = this.typeApplicationResolver.resolveTypeApplications(decls) + const [typAppErrMap, resolvedDecls] = this.typeApplicationResolver.resolveTypeApplications(decls) // XXX: the lookUp table is mutated during type inference const [typeErrMap, types] = this.typeInferrer.inferTypes(resolvedDecls) @@ -110,7 +110,7 @@ class QuintAnalyzer { const updatesErrMap = this.multipleUpdatesChecker.checkEffects([...effects.values()]) const [modeErrMap, modes] = this.modeChecker.checkModes(resolvedDecls, effects) - const errorTrees = [...typeErrMap, ...effectErrMap] + const errorTrees = [...typeErrMap, ...effectErrMap, ...typAppErrMap] // TODO: Type and effect checking should return QuintErrors instead of error trees this.errors.push( diff --git a/quint/src/types/typeApplicationResolution.ts b/quint/src/types/typeApplicationResolution.ts index a20d0a975..9f62ec4a3 100644 --- a/quint/src/types/typeApplicationResolution.ts +++ b/quint/src/types/typeApplicationResolution.ts @@ -12,7 +12,7 @@ * @module */ -import { fail } from 'assert' +import { buildErrorLeaf, buildErrorTree, ErrorTree } from '../errorTree' import { FreshVarGenerator } from '../FreshVarGenerator' import { typeToString } from '../ir/IRprinting' @@ -22,9 +22,12 @@ import { QuintAppType, QuintType, QuintVarType, Row } from '../ir/quintTypes' import { LookupTable } from '../names/base' import { zip } from '../util' import { Substitutions, applySubstitution } from './substitutions' +import assert from 'assert' /** Resolves all type applications in an IR object */ export class TypeApplicationResolver implements IRTransformer { + // Errors found during type application resolution + private errors: Map = new Map() // Fresh variable generator, shared with the TypeInferrer private freshVarGenerator: FreshVarGenerator // Lookup table from the parser @@ -40,8 +43,10 @@ export class TypeApplicationResolver implements IRTransformer { }) } - resolveTypeApplications(decls: QuintDeclaration[]): QuintDeclaration[] { - return decls.map(decl => transformDeclaration(this, decl)) + resolveTypeApplications(decls: QuintDeclaration[]): [Map, QuintDeclaration[]] { + const resolvedDecls = decls.map(decl => transformDeclaration(this, decl)) + const errors = this.errors + return [errors, resolvedDecls] } exitType(t: QuintType): QuintType { @@ -63,26 +68,39 @@ export class TypeApplicationResolver implements IRTransformer { } private resolveTypeApp(t: QuintAppType): QuintType { - if (!t.ctor.id) { - // This should be ensured by parsing - fail( - `invalid IR node: type constructor ${t.ctor.name} in type application ${typeToString(t)} id ${t.id} has no id` - ) - } + // Ensured by parsing + assert(t.id, `invalid IR node: type application ${typeToString(t)} has no id`) + // Ensured by parsing + assert( + t.ctor.id, + `invalid IR node: type constructor ${t.ctor.name} in type application ${typeToString(t)} id ${t.id} has no id` + ) const typeDef = this.table.get(t.ctor.id) - if (!typeDef) { - // This should be ensured by name resolution - fail(`invalid IR reference: type constructor ${t.ctor.name} with id ${t.ctor.id} has no type definition`) - } - - if (typeDef.kind !== 'typedef' || !typeDef.type) { - // This should be ensured by the grammar and by name resolution - fail(`invalid kind looked up for constructor of type application with id ${t.ctor.id} `) - } + // Ensured by name resolution + assert(typeDef, `invalid IR reference: type constructor ${t.ctor.name} with id ${t.ctor.id} has no type definition`) + // Ensured by the grammar and by name resolution + assert( + typeDef.kind === 'typedef' && typeDef.type, + `invalid kind looked up for constructor of type application with id ${t.ctor.id} ` + ) const { params, type } = this.freshTypeFromDef(typeDef as QuintTypeAlias) + // NOTE: Early exit on error + // Check for arity mismatch in type application + if (params.length !== t.args.length) { + const ctorMsg = typeToString(t.ctor) + const typeArgsMsg = t.args.map(typeToString).join(', ') + const manyOrFew = params.length > t.args.length ? 'few' : 'many' + const err = buildErrorLeaf( + `applying type constructor ${ctorMsg} to arguments ${typeArgsMsg}`, + `too ${manyOrFew} arguments supplied: ${ctorMsg} only accepts ${params.length} parameters` + ) + this.errors.set(t.id, err) + return t + } + // Substitute the type `args` for each corresponding fresh variable const subs: Substitutions = zip(params, t.args).map(([param, arg]) => ({ kind: 'type', diff --git a/quint/test/types/inferrer.test.ts b/quint/test/types/inferrer.test.ts index 1a1e20976..a3471cf5d 100644 --- a/quint/test/types/inferrer.test.ts +++ b/quint/test/types/inferrer.test.ts @@ -2,7 +2,7 @@ import { describe, it } from 'mocha' import { assert } from 'chai' import { TypeInferenceResult, TypeInferrer } from '../../src/types/inferrer' import { typeSchemeToString } from '../../src/types/printing' -import { errorTreeToString } from '../../src/errorTree' +import { ErrorTree, errorTreeToString } from '../../src/errorTree' import { parseMockedModule } from '../util' import { TypeApplicationResolver } from '../../src/types/typeApplicationResolution' @@ -22,8 +22,17 @@ describe('inferTypes', () => { // Type inference assumes all type applications (e.g., `Foo[int, str]`) have been resolved. const resolver = new TypeApplicationResolver(table) const inferrer = new TypeInferrer(table) - const modules = parsedModules.map(m => ({ ...m, declarations: resolver.resolveTypeApplications(m.declarations) })) - return inferrer.inferTypes(modules.flatMap(m => m.declarations)) + + // Used to collect errors found during type application + let typeAppErrs: Map = new Map() + const modules = parsedModules.map(m => { + const [errs, declarations] = resolver.resolveTypeApplications(m.declarations) + typeAppErrs = new Map([...typeAppErrs, ...errs]) + return { ...m, declarations } + }) + const [inferenceErrors, inferenceSchemes] = inferrer.inferTypes(modules.flatMap(m => m.declarations)) + const combinedErrors = new Map([...inferenceErrors, ...typeAppErrs]) + return [combinedErrors, inferenceSchemes] } function inferTypesForDefs(defs: string[]): TypeInferenceResult { @@ -445,6 +454,31 @@ Trying to unify ((Ok(bool) | Err(_t5))) => (Ok(bool) | Err(_t5)) and ((Ok(bool) assert.deepEqual(actualErrors, [expectedError]) }) + it('errors when polymorphic types are applied to invalid numbers of arguments', () => { + const defs = [ + 'type Result[ok, err] = Ok(ok) | Err(err)', + `val too_many: Result[a, b, c] = Ok(1)`, + `val too_few: Result[a] = Ok(1)`, + ] + + const [errors] = inferTypesForDefs(defs) + assert.isNotEmpty([...errors.entries()]) + + const actualErrors = [...errors.entries()].map(e => errorTreeToString(e[1])) + const expectedErrors = [ + `Couldn't unify sum and app +Trying to unify (Ok(int) | Err(_t3)) and Result[a, b, c] +`, + `too many arguments supplied: Result only accepts 2 parameters +applying type constructor Result to arguments a, b, c +`, + `too few arguments supplied: Result only accepts 2 parameters +applying type constructor Result to arguments a +`, + ] + assert.deepEqual(actualErrors, expectedErrors) + }) + it('fails when types are not unifiable', () => { const defs = ['def a = 1.map(p => p + 10)'] From 07fbfd0e545037aa685713c755c7f5d4d23d8352 Mon Sep 17 00:00:00 2001 From: Shon Feder Date: Sat, 2 Mar 2024 00:07:42 -0500 Subject: [PATCH 6/7] Fix lints --- quint/src/types/inferrer.ts | 2 +- quint/src/types/typeApplicationResolution.ts | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/quint/src/types/inferrer.ts b/quint/src/types/inferrer.ts index a0f349552..f1bb378a9 100644 --- a/quint/src/types/inferrer.ts +++ b/quint/src/types/inferrer.ts @@ -16,7 +16,7 @@ import { ErrorTree } from '../errorTree' import { walkDeclaration } from '../ir/IRVisitor' import { LookupTable } from '../names/base' -import { QuintDeclaration, isDef } from '../ir/quintIr' +import { QuintDeclaration } from '../ir/quintIr' import { TypeScheme } from './base' import { ConstraintGeneratorVisitor } from './constraintGenerator' import { solveConstraint } from './constraintSolver' diff --git a/quint/src/types/typeApplicationResolution.ts b/quint/src/types/typeApplicationResolution.ts index 9f62ec4a3..7dd83d45e 100644 --- a/quint/src/types/typeApplicationResolution.ts +++ b/quint/src/types/typeApplicationResolution.ts @@ -12,7 +12,7 @@ * @module */ -import { buildErrorLeaf, buildErrorTree, ErrorTree } from '../errorTree' +import { ErrorTree, buildErrorLeaf } from '../errorTree' import { FreshVarGenerator } from '../FreshVarGenerator' import { typeToString } from '../ir/IRprinting' From 862ee0aaac27e48a881b968a9c812a47759f4892 Mon Sep 17 00:00:00 2001 From: Shon Feder Date: Sat, 2 Mar 2024 00:13:18 -0500 Subject: [PATCH 7/7] Update examples --- examples/.scripts/run-example.sh | 2 +- examples/README.md | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/examples/.scripts/run-example.sh b/examples/.scripts/run-example.sh index 4fdbea46b..e64273133 100755 --- a/examples/.scripts/run-example.sh +++ b/examples/.scripts/run-example.sh @@ -61,7 +61,7 @@ result () { elif [[ "$file" == "classic/distributed/TwoPhaseCommit/two_phase_commit_modules.qnt" && "$cmd" =~ (test|verify) ]] ; then printf "https://github.com/informalsystems/quint/issues/1299" elif [[ "$file" == "language-features/option.qnt" && "$cmd" == "verify" ]] ; then - printf "https://github.com/informalsystems/quint/issues/1391" + printf "https://github.com/informalsystems/quint/issues/1393" fi fi } diff --git a/examples/README.md b/examples/README.md index a51536d54..cf82deffe 100644 --- a/examples/README.md +++ b/examples/README.md @@ -86,7 +86,7 @@ listed without any additional command line arguments. | [language-features/lists.qnt](./language-features/lists.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | | [language-features/maps.qnt](./language-features/maps.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | | [language-features/nondetEx.qnt](./language-features/nondetEx.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | -| [language-features/option.qnt](./language-features/option.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:https://github.com/informalsystems/quint/issues/1391 | +| [language-features/option.qnt](./language-features/option.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:https://github.com/informalsystems/quint/issues/1393 | | [language-features/records.qnt](./language-features/records.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | | [language-features/sets.qnt](./language-features/sets.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | | [language-features/tuples.qnt](./language-features/tuples.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |