diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 297133c57..0bf8e65c0 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -82,6 +82,97 @@ FP code in this language, so we keep the balance between readability and FPness. When the idiomatic JavaScript code is shorter and clearer than equivalent FP code, we write the idiomatic JavaScript code. +### Ensure exhaustive matches + +The type system should help us keep the code base maintainable. But when +`switch` statements and conditionals are used purely for side effects, we can +lose the advantage of exhaustivness checking. Here's an example: + +Assume we have a type `T` + +```typescript +type T = 'a' | 'b' | 'c' +``` + +We should structure our program such that + +- we can be sure every alternative is considered (as needed), and +- whenever a new alternative is added to this type, the type system will warn us + about all the places we need to account for the new kind of data. + +If we use `T` with a `switch` or `if`/`then` statement that *returns values*, +this indispensable help is ensured. E.g., if we try to write the following: + +```typescript +function f(x:T): Number { + switch x { + case 'a': + return 0 + case 'b': + return 1 + } +} +``` + +we will end up with a type error, because the annotation on `f` promises it will +return a `Number`, but it might in fact return `undefined` since we are not +handling `c`. + +However, if we are only using side effects in the switch, we lose this check! + +```typescript +function f(x:T): Number { + let n = -1 + switch x { + case 'a': + n = 0 + break + case 'b': + n = 1 + break + } + return ret +} +``` + +Now the typechecker sees that we will be returning a number no matter what +happens, even if none of our cases are hit, and we will not get a warning on the +omitted check for `c`, or for any other data added to this type in the future. + +Now, sometimes this kind of catch-all default is what we want, but we should be +very careful in relying on it, because it creates blind spots. As a rule, we +should only allow cath-all defaults when the computation we are performing +**must** be invariant under any expansion of the domain we are computing from. + +For all other cases, we can avoid these typechecking blind spots by following two guidelines: + +1. Prefer passing data by returning values whenever, and avoid needless mutable + assignments. +2. When switches need to be used for side effects, provide a default that + calls `unreachable` on the expression to ensure all cases are handled: + + ```typescript + import { unreachable } from './util' + + function f(x:T): Number { + let n = -1 + switch x { + case 'a': + n = 0 + break + case 'b': + n = 1 + break + default: + unreachable(x) + } + return ret + } + ``` + + Now the type checker will warn us that we aren't accounting for `c` (or any + additional alternatives added down the line). + ### Using Either TODO @@ -186,7 +277,7 @@ executable and the VSCode plugin. This will trigger the release and publication of the package to npm and GitHub. - + ### VSCode Plugin #### Prerequisites @@ -207,10 +298,9 @@ executable and the VSCode plugin. - Run `vsce publish` - requires access to https://dev.azure.com/informalsystems/ - which allows creating the required PAT (see - https://code.visualstudio.com/api/working-with-extensions/publishing-extension) + https://code.visualstudio.com/api/working-with-extensions/publishing-extension) - Use the web interface - Run `vsce package` to produce a the `.visx` archive - Navigate to https://marketplace.visualstudio.com/manage/publishers/informal, and click the `...` visible when hovering over `Quint` to upload the archive. - diff --git a/doc/adr007-flattening.md b/doc/adr007-flattening.md new file mode 100644 index 000000000..df568800a --- /dev/null +++ b/doc/adr007-flattening.md @@ -0,0 +1,276 @@ +# ADR007: Flattening + +| Revision | Date | Author | +| :------- | :--------- | :--------------- | +| 1 | 2023-08-01 | Gabriela Moreira | + +## 1. Summary + +This document describes a new strategy for flattening modules, that is, replacing imports, instances and exports with the actual definitions. This is a necessary step for compilation and integration with apalache, since both the compiler and apalache cannnot handle imports, instances and exports. + +## 2. Context + +Our current strategy for flattening has intrinsic problems, and some issues that popped up cannot really be solved with the current approach. The first of those issues, and perhaps the one that better flags the problem in the current implementation, is [Flatenning breaks when importing by name a definition that depends on others #836](https://github.com/informalsystems/quint/issues/836). + +The existing flattener takes import/instance/export statements and replaces them with a copy of the definitions from that module, assigning new ids to those definitions and its inner IR components and adding namespaces when necessary. With this, there are two possible scenarios: + +1. All imports, instances and exports include all definitions (i.e. there is no `import A.foo`). In this case, we will end up with a module with all of the definitions from all used modules. +2. There is some statement refering to a specific definition like `import A.foo`. In this case, the other definitions from `A` won't be copied, and if `foo` depends on something else, the flattened module won't be valid. + +Therefore, it is clear that we need some way of looking into the dependencies of definitions when copying them over, both to avoid (1) by copying only the necessary definitions, and to avoid (2) and ensure the flattened module has all the definitions it needs. + +In addition to that, even though this solution is an exaggeration that generates new ids for all definitions it copies, it still has problems with instances. + +See all known problems in [#1071](https://github.com/informalsystems/quint/issues/1071) + +## 3. Options + +I spent three weeks working on a proof of concept for a new flattener, which is described in this document. During this time, I tried a lot of different combinations of strategies, and none of them were sufficient to make our existing integration tests pass. The requirements I followed to pick solutions was something like these: + +1. We need to recurse over definitions being copied to the flattened module until we get all of its dependencies. +2. We need to have different ids for definitions in different instances, so they can assume different values during evaluation. +3. The final flattened module needs to have proper names (i.e. be name resolvable), so Apalache can work with it. + +So if there is something that is somehow viable outside of these requirements, I probably didn't consider it. + +## 4. Solution + +The solution proposed here is a new flattening architecture, which is described in detail in the following sections. The main idea is to have a new flattener that is run twice, with an instance flattener in between. The new flattening procedures require additional information for each definition, so we also propose changes to the name collector in order to gather this information. Therefore, we propose: + +1. Changes to name collection, during name resolution +2. Introduction of an instance flattener +3. Changes to the flattener strategy + +One important thing to notice is that imports, instances and exports are resolved by the name resolver, and that is where any missing or conflicting name errors are flagged. Flattening assumes all names are present and not conflicting, and the solution proposes a lot of manipulations that rely on this assumption. + +To achieve this scenario, we propose: +We describe each change in detail in separate sections below. + +### 4.1 Changes to name collection + +This section explains the proposed changes to name collection. These changes do not affect name resolution itself, but collect additional metadata, to be used later in flattening: + +1. Keep full quint definitions in the lookup table +2. Collect flattened namespaces from import/export/instance statements (adds `namespaces` field) +3. Back-reference the import/export/instance statement that created a definition (adds `importedFrom` field) + +We explain each of the changes in detail in the following subsections. + +#### `LookupTable` with full quint definitions + +Our current lookup table only stores a projection of the quint definition: id (called reference), name and type annotation (if present). There is no strong reason for that, only a premature optimization and the fact that the lookup table values might also be lambda parameters, which are not quint definitions. + +In flattening, we need to manipulate and reorganize definitions, and it is much better for performance and readability if the full definitions are in the lookup table, as opposed to having to scan the modules for a definition. + +Therefore, we change the lookup table to have either a `QuintDef` or a `QuintLambdaParam` as its value, as well as two additional fields (`namespaces` and `importedFrom`) described below. + +#### Collect flattened namespaces from import/export/instance statements (`namespaces`) + +When flattening a definition that originates from an import/export/instance statement, we may need to – _only during flattening_ – prefix it with a namespace in order to refer to it uniquely in the flattened module. +This section describes how to accumulate this namespace information during name collection. It is stored in a fresh `namespaces` field, for each definition in the lookup table. + +##### Namespaces for imports + +Imports are the simplest scenario, since they only copy definitions, possibly adding a namespace to them: +1. `import A.*`, `import A.foo` don't add namespaces +2. `import A` adds `A` namespace +3. `import A as MyA` adds `MyA` namespace + +##### Namespaces for instances + +For instances, we need to ensure uniqueness, since the same names in the instanced module can assume different values if the constants are different. Therefore, we add `this.currentModuleName` to the namespace, differentiating possible instances with the same name from different modules. For the following cases, suppose the statements are inside the `myModule` module. +1. `import A(N=1).*` adds a `myModule::A` namespace + - `myModule` is added to differentiate definitions of this instance from definitions from a similar instance in another module (e.g. `module otherModule { import A(N=2).* }` would have namespace `otherModule::A`) + - `A` is added to keep consistency with the qualified instance scenario (next item), where the qualifier is necessary. In case of no qualifier (this item), we shouldn't need to add `A`, but having the definitions from `A` namespaced like `myModule::foo` can cause confusion (for us developers while testing and debugging). `myModule::A::foo` is clearer and more consistent with the qualified instance scenario. +2. `import A(N=1) as A1` adds a `myModule::A1` namespace + - `myModule` is added for the same reason as in (1). + - `A1` is added to differentiate definitions of this instance from definitions from a similar instance in the same module (e.g. `import A(N=2) as A2` would have namespace `myModule::A2`) + +##### Namespaces for exports + +Exports have a particularity: they can remove namespaces. Consider the example: +```bluespec +module A { + const N: int + val a = N +} + +module B { + import A(N=1) as A1 + export A1.* +} +``` + +In this example, `export A1.*` is taking the definitions from `A1` and making them available without any additional namespaces. + +This scenario is tricky and, as discussed in a Quint meeting, we could not support it in the first version. Current flattening does support this, but it is not able to distinguish different instances, so problems arise. We are not sure how useful and clear this scenario is for users. + +So, exports that change the namespaces of the previously imported definitions are not supported in the first version of the new flattener. We should raise a proper error when an export like that is found. The example above could be rewritten as: +```bluespec +module A { + const N: int + val a = N +} + +module B { + import A(N=1) as A1 + export A1 +} +``` + +Currently, this prevents us from using `A1` without a namespace, since we can't write an export for `import A(N=1).*`. @konnov suggested the introduction of `export *` for this end, which is still in consideration. + +#### Back-reference the import/export/instance statement that created a definition (`importedFrom`) + +We add a reference to the import/export/instance statement that created a definition, also gathered during name collection, in the new `importedFrom` field. Used in flattening to distinguish definitions that come from instances from definitions that come from imports/exports. + +### 4.2 Instance Flattener + +The instance flattener gets rid of instances, which is the most complicated part of flattening. We cannot use the same id for the same definition of different instances, as they might assume different values[^1]. + +Each instance statement is replaced with an import statement and generates a new module. The new module has the constants replaced with `pure val` definitions (from the overrides in the instance statement), and all its names are fully-qualified, constructed with the previously defined namespace algorithm. The new import statement, replacing the instance statement, is a unqualified import of the new module. + +The names in the module containing the instance statement also have to be updated with a namespace, since they might refer to definitions that now include a namespace. We look at each name in the module and, if it refers to a definition that comes from an instance, (that is, its `importFrom` field has an instance), then we replace the name with a namespaced version of it (using the `namespaces` field). For this to work properly, any existing `import` and `export` statements should have been flattened before the instance flattener is run, ensuring that the definitions referred to by these names already have their proper namespaces. + +All of this tinkering on names and the addition of a matching import statement makes it so the module outputted by the instance flattener can be name resolved. The name resolution of this module will produce a lookup table where the names referring to instances point to the new modules (produced for each instance), which are no longer instances. Therefore, after instance flattening, we have instance-less modules and their corresponding lookup table. + +#### Example + +Take this module as example, where `A` is instanced twice with the same name: +```bluespec +module A { + const N: int // id 1 + val a = N // id 2 +} + +module B { + import A(N=1) as A1 + val b = A1::a // id 3 +} + +module C { + import A(N=0) as A1 + val C = A1::a // id 4 +} +``` + +The instance flattener will create two new modules: `B::A1` and `C::A1`, with new ids for the definitions inside it. +```bluespec +module A { + const N: int // id 1 + val a = N // id 2 +} + +module B::A1 { + pure val B::A1::N = 1 // id 5 + pure val B::A1::a = B::A1::N // id 6 +} + +module C::A1 { + pure val C::A1::N = 0 // id 7 + pure val C::A1::a = C::A1::N // id 8 +} + +module B { + import B::A1.* + val b = B::A1::a // id 3 +} + +module C { + import C::A1.* + val c = C::A1::a // id 4 +} +``` + +Lookup table before instance flattening: +```mermaid +graph BT + 1["(1) const N: int"] + 2["(2) val a = N"] --> 1 + 3["(3) val b = A1::a"] --> 2 + 4["(4) val c = A1::a"] --> 2 +``` + +After instance flattening, there are two independent sub-trees, since both instances are completely independent of each other: +```mermaid +graph BT + 1["(1) const N: int"] + 2["(2) val a = N"] --> 1 + 3["(3) val b = B::A1::a"] --> 6 + 4["(4) val c = C::A1::a"] --> 8 + 5["(5) pure val B::A1::N = 1"] + 6["(6) pure val B::A1::a = B::A1::N"] --> 5 + 7["(7) pure val C::A1::N = 0"] + 8["(8) pure val C::A1::a = C::A1::N"] --> 7 +``` + +This solution relies mostly in name manipulation: we change the names and let the name resolver restructure the lookup table. In theory, we could keep the original names for the definitions inside the new modules, as long as we properly manipulate the lookup table to have the names related to that instance pointing to the names inside that module. I time-boxed some time to try this and I couldn't do it. The name manipulation solution has a significant cognitive advantage: it is much easier to understand and debug names (which can be pretty-printed) than ids and pointers (that is, the lookup table). As this is already a complex solution, I believe that it makes sense to prioritize the reduction of cognitive load. + +##### Override expressions + +In an instance statement like `import A(N=e).*`, `e` might depend on expressions defined in the current module. In this case, we need to ensure that the dependencies of `e` are copied to the new module created for the instance, otherwise `pure val myModule::A::N = e` won't resolve. To accomplish this, we use the actual `Flattener` (described below) to inspect only the expressions in the overrides and find any definitions they might depend on. + +### Flattener + +The flattener adds missing definitions to a module by recursively fetching the lookup table and copying the referenced definition, then looking into that definition for any other names and doing the same. A missing definition is a definition that is referred to by a name in the module, but is not present in that module (because it comes from an import, instance or export statement). + +When adding a missing definition, if that definitions carries a namespace, we actually need to do a "deep" procedure to add that name to not only the definition name, but also to every other name appearing in it's body. This includes adding the namespace to lambda parameters and nested definitions (even though they cannot be referred), so flattening doesn't create name conflicts with them. + +This deep namespace-adding procedure is already done in the current implementation of flattening (see [`addNamespaceToDef`](https://github.com/informalsystems/quint/blob/main/quint/src/flattening.ts#L276C4-L276C4)), with the only difference being that we don't want to generate new ids in this case (we only create new ids in the Instance Flattener). + +### Flattening imports/exports and instances + +Our proposed architecture sandwiches one run of the instance flattener (to flatten instances) between two runs of the flattener (to flatten imports/exports): + +1. First round of flattening: flattens all imports and exports, leaving us with only instances. +2. Instance Flattener: turns instance statements into imports (and adds a fresh module for each instance) +3. Second round of flattening: flattens the remaining imports created by the Instance Flattener + +We use the `importedFrom` field, introduced above, to choose the appropriate step for each definition. + +### Overall flattening process + +The flattening process is run completely for each module before proceeding to flatten the next module. The modules are assumed to be topologically sorted. The need for running this by module is that we do remove the import statements after we resolve all dependencies, but we can only ensure that all dependencies were flattened if the depending modules were completely flattened before. + +The whole flattening process consists of the following steps: +1. Run the Flattener, ignoring definitions that come from instances +2. Remove `import` and `export` statements +3. Run the Instance Flattener +4. Resolve names for the module and its dependencies, obtaining a new lookup table + - In theory, we should be able to manipulate the lookup table while flattening and avoid this step. However, I believe that would be significantly complex to write and maintain, while I see no outstanding drawbacks in running this step. +5. With the new table and modules, run the Flattener again, this time for all definitions +6. Resolve names again for all modules (using the flattened version for those that are already flattened, and the original version for those that are not). The resulting table is used as the starting point of flattening for the next module, or returned as the final table if this is the last one. + - We might be able to manipulate the table inside the flattener so this is not necessary, but it is not obvious how to do that. I believe that the only reason we have to run this now is to update the `importFrom` and `namespaces` fields of definitions coming from instances, since the Instance Flattener replaced instance statements with import statements, and the `importFrom` and `namespaces` fields of the related definitions have to be updated. I have not validated this hypothesis yet. +7. Sort names topologically, since the added definitions might be out of order. + - We might also avoid doing this if we add the new definitions in a proper order. + +### [Discussion] `FlatModule` and `FlatDef` types + +I have not tried this in the proof of concept, but I believe we need to improve our nomenclature and types. This is what we currently use: +- An IR definition (`QuintDef`) is any top level definition, including vars, consts, imports, etc. +- A flat definition (`FlatDef`) is a definition that is not a import, instance or export. All flat definitions have a `.name` field. +- A flat module (`FlatModule`) is a module with only flat definitions +- A definition in the lookup table (`Definition`) is any `QuintDef` or a `QuintLambdaParameter` +- Sometimes, we call `QuintDef` by 'unit' (in the parser and parsing functions such as `parseExprOrUnit`) + +I think we should do something like: +- Call this high level definitions that encapsulate everything as 'declarations'. +- `QuintModule` has a list of 'declarations'. +- `QuintDef` should refer only to flat definitions, that is, everything but imports, instances and exports. Those will always have a `.name` field. +- `FlatModule` has a list of `QuintDef`. + +## Implementation plan + +1. Extract the deep namespace-adding procedure from the current flattener, adding an option to choose whether to generate new ids. +2. Change the lookup table data structure to store the whole `QuintDef` or `QuintLambdaParameter` in its values. + - This will break integration with apalache. To avoid that, we should either: + 1. Cleanup the produced lookup table in the JSON output so it contains a field called `reference` in the values + 2. Release an apalache version that accepts a lookup table with `id` fields in the values. + - This also requires a simple update to the `typeAliasInliner`, which now has to operate over different values in the lookup table. +3. Implement the new Flattener +4. Implement the Instance Flattener +5. Use the new flattening process to flatten modules before compiling +6. Make the new flattening process to be done incrementally[^2] + +[^1]: In theory, we could use the same id and save some computation for `pure` definitions that don't depend on constants, but that's "future work" :). +[^2]: If it is not a performance issue right now, this is not a priority. It is not super obvious how to do that and it is not covered by the proof of concept. diff --git a/examples/.scripts/run-example.sh b/examples/.scripts/run-example.sh index 268879b89..77e66abe2 100755 --- a/examples/.scripts/run-example.sh +++ b/examples/.scripts/run-example.sh @@ -55,7 +55,7 @@ result () { printf "https://github.com/informalsystems/quint/pull/1023" elif [[ "$file" == "cosmwasm/zero-to-hero/vote.qnt" && "$cmd" == "verify" ]] ; then printf "https://github.com/informalsystems/quint/issues/693" - elif [[ "$file" == "language-features/option.qnt" && ( "$cmd" == "test" || "$cmd" == "verify" ) ]] ; then + elif [[ "$file" == "language-features/option.qnt" && "$cmd" == "verify" ]] ; then printf "https://github.com/informalsystems/quint/issues/244" elif [[ "$file" == "language-features/tuples.qnt" && "$cmd" == "verify" ]] ; then printf "https://github.com/informalsystems/apalache/issues/2670" diff --git a/examples/README.md b/examples/README.md index 3f7d993bc..3278c338e 100644 --- a/examples/README.md +++ b/examples/README.md @@ -76,7 +76,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: | :x:https://github.com/informalsystems/quint/issues/244 | :x:https://github.com/informalsystems/quint/issues/244 | +| [language-features/option.qnt](./language-features/option.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:https://github.com/informalsystems/quint/issues/244 | | [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: | :x:https://github.com/informalsystems/apalache/issues/2670 | diff --git a/examples/spells/basicSpells.qnt b/examples/spells/basicSpells.qnt index 32747e0f6..40764b81b 100644 --- a/examples/spells/basicSpells.qnt +++ b/examples/spells/basicSpells.qnt @@ -123,4 +123,21 @@ module basicSpells { assert(Map(3 -> 4, 7 -> 8) == Map(3 -> 4, 5 -> 6, 7 -> 8).mapRemove(5)), assert(Map() == Map().mapRemove(3)), } -} \ No newline at end of file + + /// Removes a set of map entries. + /// + /// - @param __map a map to remove entries from + /// - @param __keys a set of keys for entries to remove from the map + /// - @returns a new map that contains all entries of __map + /// that do not have a key in __keys + pure def mapRemoveAll(__map: a -> b, __keys: Set[a]): a -> b = { + __map.keys().exclude(__keys).mapBy(__k => __map.get(__k)) + } + + run mapRemoveAllTest = + val m = Map(3 -> 4, 5 -> 6, 7 -> 8) + all { + assert(m.mapRemoveAll(Set(5, 7)) == Map(3 -> 4)), + assert(m.mapRemoveAll(Set(5, 99999)) == Map(3 -> 4, 7 -> 8)), + } +} diff --git a/quint/src/cliCommands.ts b/quint/src/cliCommands.ts index 3c912574e..9d0bb8f7e 100644 --- a/quint/src/cliCommands.ts +++ b/quint/src/cliCommands.ts @@ -513,34 +513,21 @@ export async function runSimulator(prev: TypecheckedStage): Promise walkEffect(visitor, e)) - walkEffect(visitor, effect.result) + effect.params.forEach(e => walkEffect(visitor, e)) + walkEffect(visitor, effect.result) - if (visitor.exitArrow) { - visitor.exitArrow(effect) + if (visitor.exitArrow) { + visitor.exitArrow(effect) + } } - } + break + default: + unreachable(effect) } } diff --git a/quint/src/effects/builtinSignatures.ts b/quint/src/effects/builtinSignatures.ts index ae8f3b2ae..348352ec1 100644 --- a/quint/src/effects/builtinSignatures.ts +++ b/quint/src/effects/builtinSignatures.ts @@ -15,6 +15,7 @@ import { ComponentKind, Effect, EffectComponent, EffectScheme, Entity, Signature, effectNames, toScheme } from './base' import { parseEffectOrThrow } from './parser' import { range, times } from 'lodash' +import { QuintBuiltinOpcode } from '../ir/quintIr' export function getSignatures(): Map { return new Map(fixedAritySignatures.concat(multipleAritySignatures)) @@ -227,7 +228,7 @@ const otherOperators = [ }, ] -const multipleAritySignatures: [string, Signature][] = [ +const multipleAritySignatures: [QuintBuiltinOpcode, Signature][] = [ ['List', standardPropagation], ['Set', standardPropagation], ['Map', standardPropagation], diff --git a/quint/src/effects/modeChecker.ts b/quint/src/effects/modeChecker.ts index 5eee00069..30847e9b7 100644 --- a/quint/src/effects/modeChecker.ts +++ b/quint/src/effects/modeChecker.ts @@ -18,6 +18,7 @@ import { qualifierToString } from '../ir/IRprinting' import { IRVisitor, walkDefinition } from '../ir/IRVisitor' import { QuintError } from '../quintError' import { OpQualifier, QuintDef, QuintInstance, QuintOpDef } from '../ir/quintIr' +import { unreachable } from '../util' import { ArrowEffect, ComponentKind, EffectScheme, Entity, entityNames, stateVariables } from './base' import { effectToString, entityToString } from './printing' @@ -247,26 +248,34 @@ function paramEntitiesByEffect(effect: ArrowEffect): Map { switch (p.kind) { - case 'concrete': { - p.components.forEach(c => { - const existing = entitiesByComponentKind.get(c.kind) || [] - entitiesByComponentKind.set(c.kind, concatEntity(existing, c.entity)) - }) - break - } - case 'arrow': { - const nested = paramEntitiesByEffect(p) - nested.forEach((entities, kind) => { - const existing = entitiesByComponentKind.get(kind) || [] - entitiesByComponentKind.set(kind, entities.reduce(concatEntity, existing)) - }) - if (p.result.kind === 'concrete') { - p.result.components.forEach(c => { + case 'concrete': + { + p.components.forEach(c => { const existing = entitiesByComponentKind.get(c.kind) || [] entitiesByComponentKind.set(c.kind, concatEntity(existing, c.entity)) }) } - } + break + case 'arrow': + { + const nested = paramEntitiesByEffect(p) + nested.forEach((entities, kind) => { + const existing = entitiesByComponentKind.get(kind) || [] + entitiesByComponentKind.set(kind, entities.reduce(concatEntity, existing)) + }) + if (p.result.kind === 'concrete') { + p.result.components.forEach(c => { + const existing = entitiesByComponentKind.get(c.kind) || [] + entitiesByComponentKind.set(c.kind, concatEntity(existing, c.entity)) + }) + } + } + break + case 'variable': + // Nothing to gather + break + default: + unreachable(p) } }) diff --git a/quint/src/effects/simplification.ts b/quint/src/effects/simplification.ts index 3aaac58ee..4f9242d0f 100644 --- a/quint/src/effects/simplification.ts +++ b/quint/src/effects/simplification.ts @@ -13,6 +13,7 @@ */ import isEqual from 'lodash.isequal' +import { unreachable } from '../util' import { ConcreteEffect, Effect, Entity, StateVariable } from './base' /** @@ -57,35 +58,35 @@ export function simplify(e: Effect): Effect { * Otherwise, the entity without change. */ export function flattenUnions(entity: Entity): Entity { - switch (entity.kind) { - case 'union': { - const unionEntities: Entity[] = [] - const vars: StateVariable[] = [] - const flattenEntities = entity.entities.map(v => flattenUnions(v)) - flattenEntities.forEach(v => { - switch (v.kind) { - case 'variable': - unionEntities.push(v) - break - case 'concrete': - vars.push(...v.stateVariables) - break - case 'union': - unionEntities.push(...v.entities) - break - } - }) - - if (unionEntities.length > 0) { - const entities = - vars.length > 0 ? unionEntities.concat({ kind: 'concrete', stateVariables: vars }) : unionEntities - return entities.length > 1 ? { kind: 'union', entities: entities } : entities[0] - } else { - return { kind: 'concrete', stateVariables: vars } + if (entity.kind == 'union') { + const unionEntities: Entity[] = [] + const vars: StateVariable[] = [] + const flattenEntities = entity.entities.map(v => flattenUnions(v)) + flattenEntities.map(v => { + switch (v.kind) { + case 'variable': + unionEntities.push(v) + break + case 'concrete': + vars.push(...v.stateVariables) + break + case 'union': + unionEntities.push(...v.entities) + break + default: + unreachable(v) } + }) + + if (unionEntities.length > 0) { + const entities = + vars.length > 0 ? unionEntities.concat({ kind: 'concrete', stateVariables: vars }) : unionEntities + return entities.length > 1 ? { kind: 'union', entities: entities } : entities[0] + } else { + return { kind: 'concrete', stateVariables: vars } } - default: - return entity + } else { + return entity } } diff --git a/quint/src/ir/IRTransformer.ts b/quint/src/ir/IRTransformer.ts index 0d1c16502..13faea040 100644 --- a/quint/src/ir/IRTransformer.ts +++ b/quint/src/ir/IRTransformer.ts @@ -15,6 +15,7 @@ import * as ir from './quintIr' import * as t from './quintTypes' +import { unreachable } from '../util' export class IRTransformer { enterModule?: (module: ir.QuintModule) => ir.QuintModule @@ -81,6 +82,8 @@ export class IRTransformer { exitTupleType?: (type: t.QuintTupleType) => t.QuintTupleType enterRecordType?: (type: t.QuintRecordType) => t.QuintRecordType exitRecordType?: (type: t.QuintRecordType) => t.QuintRecordType + enterSumType?: (type: t.QuintSumType) => t.QuintSumType + exitSumType?: (type: t.QuintSumType) => t.QuintSumType enterUnionType?: (type: t.QuintUnionType) => t.QuintUnionType exitUnionType?: (type: t.QuintUnionType) => t.QuintUnionType @@ -247,6 +250,18 @@ export function transformType(transformer: IRTransformer, type: t.QuintType): t. newType = transformer.exitUnionType(newType) } break + + case 'sum': + if (transformer.enterSumType) { + newType = transformer.enterSumType(newType) + } + if (transformer.exitSumType) { + newType = transformer.exitSumType(newType) + } + break + + default: + unreachable(newType) } if (transformer.exitType) { @@ -346,6 +361,8 @@ export function transformDefinition(transformer: IRTransformer, def: ir.QuintDef newDef = transformer.exitAssume(newDef) } break + default: + unreachable(newDef) } if (transformer.exitDef) { newDef = transformer.exitDef(newDef) @@ -410,26 +427,30 @@ function transformExpression(transformer: IRTransformer, expr: ir.QuintEx): ir.Q newExpr = transformer.exitLambda(newExpr) } break - case 'let': { - if (transformer.enterLet) { - newExpr = transformer.enterLet(newExpr) - } - - const opdef = transformDefinition(transformer, newExpr.opdef) - if (opdef.kind !== 'def') { - // This should only happen if we write a bad transformer. Should never - // be a user facing issue. - throw new Error('Let operator definition transformed into non-operator definition') - } - - newExpr.opdef = opdef - newExpr.expr = transformExpression(transformer, newExpr.expr) - - if (transformer.exitLet) { - newExpr = transformer.exitLet(newExpr) + case 'let': + { + if (transformer.enterLet) { + newExpr = transformer.enterLet(newExpr) + } + + const opdef = transformDefinition(transformer, newExpr.opdef) + if (opdef.kind !== 'def') { + // This should only happen if we write a bad transformer. Should never + // be a user facing issue. + throw new Error('Let operator definition transformed into non-operator definition') + } + + newExpr.opdef = opdef + newExpr.expr = transformExpression(transformer, newExpr.expr) + + if (transformer.exitLet) { + newExpr = transformer.exitLet(newExpr) + } } break - } + + default: + unreachable(newExpr) } if (transformer.exitExpr) { diff --git a/quint/src/ir/IRVisitor.ts b/quint/src/ir/IRVisitor.ts index 280c2cc62..3cd17870d 100644 --- a/quint/src/ir/IRVisitor.ts +++ b/quint/src/ir/IRVisitor.ts @@ -15,6 +15,7 @@ import * as ir from './quintIr' import * as t from './quintTypes' +import { unreachable } from '../util' /** * Interface to be implemented by visitor classes. @@ -81,6 +82,8 @@ export interface IRVisitor { exitTupleType?: (_type: t.QuintTupleType) => void enterRecordType?: (_type: t.QuintRecordType) => void exitRecordType?: (_type: t.QuintRecordType) => void + enterSumType?: (_type: t.QuintSumType) => void + exitSumType?: (_type: t.QuintSumType) => void enterUnionType?: (_type: t.QuintUnionType) => void exitUnionType?: (_type: t.QuintUnionType) => void @@ -242,6 +245,14 @@ export function walkType(visitor: IRVisitor, type: t.QuintType): void { visitor.exitUnionType(type) } break + + case 'sum': + visitor.enterSumType?.(type) + visitor.exitSumType?.(type) + break + + default: + unreachable(type) } if (visitor.exitType) { @@ -393,6 +404,8 @@ function walkExpression(visitor: IRVisitor, expr: ir.QuintEx): void { visitor.exitLet(expr) } break + default: + unreachable(expr) } if (visitor.exitExpr) { @@ -432,6 +445,9 @@ function walkRow(visitor: IRVisitor, r: t.Row) { if (visitor.exitEmptyRow) { visitor.exitEmptyRow(r) } + break + default: + unreachable(r) } if (visitor.exitRow) { visitor.exitRow(r) diff --git a/quint/src/ir/quintIr.ts b/quint/src/ir/quintIr.ts index 0caa3e010..608c8e0a0 100644 --- a/quint/src/ir/quintIr.ts +++ b/quint/src/ir/quintIr.ts @@ -116,6 +116,113 @@ export interface QuintApp extends WithId { args: QuintEx[] } +/** A subtype of `QuintApp` covering all quint builtin operators */ +export interface QuintBuiltinApp extends QuintApp { + /** The name of the builtin being applied */ + opcode: QuintBuiltinOpcode +} + +/** A type guard to narrow the type of a `QuintApp` to a `QuintBuiltinApp` + * + * See https://stackoverflow.com/a/61129291 + */ +export function isQuintBuiltin(app: QuintApp): app is QuintBuiltinApp { + return builtinOpCodes.includes(app.opcode as QuintBuiltinOpcode) +} + +// This should be the source of truth for all builtin opcodes +const builtinOpCodes = [ + 'List', + 'Map', + 'Rec', + 'Set', + 'Tup', + 'actionAll', + 'actionAny', + 'allLists', + 'always', + 'and', + 'append', + 'assert', + 'assign', + 'chooseSome', + 'concat', + 'contains', + 'enabled', + 'eq', + 'eventually', + 'exclude', + 'exists', + 'fail', + 'field', + 'fieldNames', + 'filter', + 'flatten', + 'fold', + 'foldl', + 'foldr', + 'forall', + 'get', + 'head', + 'iadd', + 'idiv', + 'iff', + 'igt', + 'igte', + 'ilt', + 'ilte', + 'imod', + 'implies', + 'imul', + 'in', + 'indices', + 'intersect', + 'ipow', + 'isFinite', + 'isub', + 'ite', + 'item', + 'iuminus', + 'keys', + 'length', + 'map', + 'mapBy', + 'mustChange', + 'neq', + 'next', + 'not', + 'nth', + 'oneOf', + 'or', + 'orKeep', + 'powerset', + 'put', + 'q::test', + 'q::testOnce', + 'range', + 'replaceAt', + 'reps', + 'select', + 'set', + 'setBy', + 'setOfMaps', + 'setToMap', + 'size', + 'slice', + 'strongFair', + 'subseteq', + 'tail', + 'then', + 'to', + 'tuples', + 'union', + 'unionMatch', + 'weakFair', + 'with', +] as const + +export type QuintBuiltinOpcode = (typeof builtinOpCodes)[number] + export interface QuintLambdaParameter extends WithId { /** The name of the formal parameter */ name: string diff --git a/quint/src/names/base.ts b/quint/src/names/base.ts index 84ccdd9b6..104e8df20 100644 --- a/quint/src/names/base.ts +++ b/quint/src/names/base.ts @@ -147,10 +147,6 @@ export const builtinNames = [ 'enabled', 'weakFair', 'strongFair', - 'guarantees', - 'existsConst', - 'forallConst', - 'chooseConst', 'Bool', 'Int', 'Nat', diff --git a/quint/src/runtime/impl/compilerImpl.ts b/quint/src/runtime/impl/compilerImpl.ts index 930ece9f1..320e0c825 100644 --- a/quint/src/runtime/impl/compilerImpl.ts +++ b/quint/src/runtime/impl/compilerImpl.ts @@ -36,6 +36,7 @@ import { RuntimeValue, rv } from './runtimeValue' import { ErrorCode } from '../../quintError' import { lastTraceName } from '../compile' +import { unreachable } from '../../util' const specialNames = ['q::input', 'q::runResult', 'q::nruns', 'q::nsteps', 'q::init', 'q::next', 'q::inv'] @@ -364,6 +365,10 @@ export class CompilerVisitor implements IRVisitor { case 'str': this.compStack.push(mkConstComputable(rv.mkStr(expr.value))) + break + + default: + unreachable(expr) } } @@ -387,514 +392,519 @@ export class CompilerVisitor implements IRVisitor { } exitApp(app: ir.QuintApp) { - switch (app.opcode) { - case 'next': { - const register = this.compStack.pop() - if (register) { - const name = (register as Register).name - const nextvar = this.contextGet(name, ['nextvar']) - this.compStack.push(nextvar ?? fail) - } else { - this.errorTracker.addCompileError(app.id, 'Operator next(...) needs one argument') - this.compStack.push(fail) - } - break - } - - case 'assign': - this.translateAssign(app.id) - break - - case 'eq': - this.applyFun(app.id, 2, (x, y) => just(rv.mkBool(x.equals(y)))) - break - - case 'neq': - this.applyFun(app.id, 2, (x, y) => just(rv.mkBool(!x.equals(y)))) - break - - // conditional - case 'ite': - this.translateIfThenElse(app.id) - break - - // Booleans - case 'not': - this.applyFun(app.id, 1, p => just(rv.mkBool(!p.toBool()))) - break - - case 'and': - // a conjunction over expressions is lazy - this.translateBoolOp(app, just(rv.mkBool(true)), (_, r) => (!r ? just(rv.mkBool(false)) : none())) - break - - case 'actionAll': - this.translateAllOrThen(app) - break - - case 'or': - // a disjunction over expressions is lazy - this.translateBoolOp(app, just(rv.mkBool(false)), (_, r) => (r ? just(rv.mkBool(true)) : none())) - break - - case 'actionAny': - this.translateOrAction(app) - break - - case 'implies': - // an implication is lazy - this.translateBoolOp(app, just(rv.mkBool(false)), (n, r) => (n == 0 && !r ? just(rv.mkBool(true)) : none())) - break - - case 'iff': - this.applyFun(app.id, 2, (p, q) => just(rv.mkBool(p.toBool() === q.toBool()))) - break - - // integers - case 'iuminus': - this.applyFun(app.id, 1, n => just(rv.mkInt(-n.toInt()))) - break - - case 'iadd': - this.applyFun(app.id, 2, (p, q) => just(rv.mkInt(p.toInt() + q.toInt()))) - break - - case 'isub': - this.applyFun(app.id, 2, (p, q) => just(rv.mkInt(p.toInt() - q.toInt()))) - break - - case 'imul': - this.applyFun(app.id, 2, (p, q) => just(rv.mkInt(p.toInt() * q.toInt()))) - break - - case 'idiv': - this.applyFun(app.id, 2, (p, q) => { - if (q.toInt() !== 0n) { - return just(rv.mkInt(p.toInt() / q.toInt())) - } else { - this.errorTracker.addRuntimeError(app.id, 'Division by zero') - return none() - } - }) - break - - case 'imod': - this.applyFun(app.id, 2, (p, q) => just(rv.mkInt(p.toInt() % q.toInt()))) - break - - case 'ipow': - this.applyFun(app.id, 2, (p, q) => { - if (q.toInt() == 0n && p.toInt() == 0n) { - this.errorTracker.addRuntimeError(app.id, '0^0 is undefined') - } else if (q.toInt() < 0n) { - this.errorTracker.addRuntimeError(app.id, 'i^j is undefined for j < 0') - } else { - return just(rv.mkInt(p.toInt() ** q.toInt())) - } - return none() - }) - break - - case 'igt': - this.applyFun(app.id, 2, (p, q) => just(rv.mkBool(p.toInt() > q.toInt()))) - break - - case 'ilt': - this.applyFun(app.id, 2, (p, q) => just(rv.mkBool(p.toInt() < q.toInt()))) - break - - case 'igte': - this.applyFun(app.id, 2, (p, q) => just(rv.mkBool(p.toInt() >= q.toInt()))) - break - - case 'ilte': - this.applyFun(app.id, 2, (p, q) => just(rv.mkBool(p.toInt() <= q.toInt()))) - break - - case 'Tup': - // Construct a tuple from an array of values - this.applyFun(app.id, app.args.length, (...values: RuntimeValue[]) => just(rv.mkTuple(values))) - break - - case 'item': - // Access a tuple: tuples are 1-indexed, that is, _1, _2, etc. - this.applyFun(app.id, 2, (tuple, idx) => this.getListElem(app.id, tuple.toList(), Number(idx.toInt()) - 1)) - break - - case 'tuples': - // Construct a cross product - this.applyFun(app.id, app.args.length, (...sets: RuntimeValue[]) => just(rv.mkCrossProd(sets))) - break - - case 'List': - // Construct a list from an array of values - this.applyFun(app.id, app.args.length, (...values: RuntimeValue[]) => just(rv.mkList(values))) - break - - case 'range': - this.applyFun(app.id, 2, (start, end) => { - const [s, e] = [Number(start.toInt()), Number(end.toInt())] - if (s <= e) { - const arr: RuntimeValue[] = [] - for (let i = s; i < e; i++) { - arr.push(rv.mkInt(BigInt(i))) + if (!ir.isQuintBuiltin(app)) { + this.applyUserDefined(app) + } else { + switch (app.opcode) { + case 'next': + { + const register = this.compStack.pop() + if (register) { + const name = (register as Register).name + const nextvar = this.contextGet(name, ['nextvar']) + this.compStack.push(nextvar ?? fail) + } else { + this.errorTracker.addCompileError(app.id, 'Operator next(...) needs one argument') + this.compStack.push(fail) } - return just(rv.mkList(arr)) - } else { - this.errorTracker.addRuntimeError(app.id, `range(${s}, ${e}) is out of bounds`) - return none() } - }) - break - - case 'nth': - // Access a list - this.applyFun(app.id, 2, (list, idx) => this.getListElem(app.id, list.toList(), Number(idx.toInt()))) - break - - case 'replaceAt': - this.applyFun(app.id, 3, (list, idx, value) => - this.updateList(app.id, list.toList(), Number(idx.toInt()), value) - ) - break - - case 'head': - this.applyFun(app.id, 1, list => this.getListElem(app.id, list.toList(), 0)) - break - - case 'tail': - this.applyFun(app.id, 1, list => { - const l = list.toList() - if (l.size > 0) { - return this.sliceList(app.id, l, 1, l.size) - } else { - this.errorTracker.addRuntimeError(app.id, 'Applied tail to an empty list') - return none() - } - }) - break - - case 'slice': - this.applyFun(app.id, 3, (list, start, end) => { - const [l, s, e] = [list.toList(), Number(start.toInt()), Number(end.toInt())] - if (s >= 0 && s <= l.size && e <= l.size && e >= s) { - return this.sliceList(app.id, l, s, e) - } else { - this.errorTracker.addRuntimeError(app.id, `slice(..., ${s}, ${e}) applied to a list of size ${l.size}`) - return none() - } - }) - break - - case 'length': - this.applyFun(app.id, 1, list => just(rv.mkInt(BigInt(list.toList().size)))) - break - - case 'append': - this.applyFun(app.id, 2, (list, elem) => just(rv.mkList(list.toList().push(elem)))) - break - - case 'concat': - this.applyFun(app.id, 2, (list1, list2) => just(rv.mkList(list1.toList().concat(list2.toList())))) - break - - case 'indices': - this.applyFun(app.id, 1, list => just(rv.mkInterval(0n, BigInt(list.toList().size - 1)))) - break - - case 'Rec': - // Construct a record - this.applyFun(app.id, app.args.length, (...values: RuntimeValue[]) => { - const keys = values.filter((e, i) => i % 2 === 0).map(k => k.toStr()) - const map: OrderedMap = keys.reduce((map, key, i) => { - const v = values[2 * i + 1] - return v ? map.set(key, v) : map - }, OrderedMap()) - return just(rv.mkRecord(map)) - }) - break - - case 'field': - // Access a record via the field name - this.applyFun(app.id, 2, (rec, fieldName) => { - const name = fieldName.toStr() - const fieldValue = rec.toOrderedMap().get(name) - if (fieldValue) { - return just(fieldValue) - } else { - this.errorTracker.addRuntimeError(app.id, `Accessing a missing record field ${name}`) - return none() - } - }) - break - - case 'fieldNames': - this.applyFun(app.id, 1, rec => { - const keysAsRuntimeValues = rec - .toOrderedMap() - .keySeq() - .map(key => rv.mkStr(key)) - return just(rv.mkSet(keysAsRuntimeValues)) - }) - break - - case 'with': - // update a record - this.applyFun(app.id, 3, (rec, fieldName, fieldValue) => { - const oldMap = rec.toOrderedMap() - const key = fieldName.toStr() - if (oldMap.has(key)) { - const newMap = rec.toOrderedMap().set(key, fieldValue) - return just(rv.mkRecord(newMap)) - } else { - this.errorTracker.addRuntimeError(app.id, `Called 'with' with a non-existent key ${key}`) + break + + case 'assign': + this.translateAssign(app.id) + break + + case 'eq': + this.applyFun(app.id, 2, (x, y) => just(rv.mkBool(x.equals(y)))) + break + + case 'neq': + this.applyFun(app.id, 2, (x, y) => just(rv.mkBool(!x.equals(y)))) + break + + // conditional + case 'ite': + this.translateIfThenElse(app.id) + break + + // Booleans + case 'not': + this.applyFun(app.id, 1, p => just(rv.mkBool(!p.toBool()))) + break + + case 'and': + // a conjunction over expressions is lazy + this.translateBoolOp(app, just(rv.mkBool(true)), (_, r) => (!r ? just(rv.mkBool(false)) : none())) + break + + case 'actionAll': + this.translateAllOrThen(app) + break + + case 'or': + // a disjunction over expressions is lazy + this.translateBoolOp(app, just(rv.mkBool(false)), (_, r) => (r ? just(rv.mkBool(true)) : none())) + break + + case 'actionAny': + this.translateOrAction(app) + break + + case 'implies': + // an implication is lazy + this.translateBoolOp(app, just(rv.mkBool(false)), (n, r) => (n == 0 && !r ? just(rv.mkBool(true)) : none())) + break + + case 'iff': + this.applyFun(app.id, 2, (p, q) => just(rv.mkBool(p.toBool() === q.toBool()))) + break + + // integers + case 'iuminus': + this.applyFun(app.id, 1, n => just(rv.mkInt(-n.toInt()))) + break + + case 'iadd': + this.applyFun(app.id, 2, (p, q) => just(rv.mkInt(p.toInt() + q.toInt()))) + break + + case 'isub': + this.applyFun(app.id, 2, (p, q) => just(rv.mkInt(p.toInt() - q.toInt()))) + break + + case 'imul': + this.applyFun(app.id, 2, (p, q) => just(rv.mkInt(p.toInt() * q.toInt()))) + break + + case 'idiv': + this.applyFun(app.id, 2, (p, q) => { + if (q.toInt() !== 0n) { + return just(rv.mkInt(p.toInt() / q.toInt())) + } else { + this.errorTracker.addRuntimeError(app.id, 'Division by zero') + return none() + } + }) + break + + case 'imod': + this.applyFun(app.id, 2, (p, q) => just(rv.mkInt(p.toInt() % q.toInt()))) + break + + case 'ipow': + this.applyFun(app.id, 2, (p, q) => { + if (q.toInt() == 0n && p.toInt() == 0n) { + this.errorTracker.addRuntimeError(app.id, '0^0 is undefined') + } else if (q.toInt() < 0n) { + this.errorTracker.addRuntimeError(app.id, 'i^j is undefined for j < 0') + } else { + return just(rv.mkInt(p.toInt() ** q.toInt())) + } return none() - } - }) - break - - case 'Set': - // Construct a set from an array of values. - this.applyFun(app.id, app.args.length, (...values: RuntimeValue[]) => just(rv.mkSet(values))) - break - - case 'powerset': - this.applyFun(app.id, 1, (baseset: RuntimeValue) => just(rv.mkPowerset(baseset))) - break - - case 'contains': - this.applyFun(app.id, 2, (set, value) => just(rv.mkBool(set.contains(value)))) - break - - case 'in': - this.applyFun(app.id, 2, (value, set) => just(rv.mkBool(set.contains(value)))) - break - - case 'subseteq': - this.applyFun(app.id, 2, (l, r) => just(rv.mkBool(l.isSubset(r)))) - break - - case 'union': - this.applyFun(app.id, 2, (l, r) => just(rv.mkSet(l.toSet().union(r.toSet())))) - break - - case 'intersect': - this.applyFun(app.id, 2, (l, r) => just(rv.mkSet(l.toSet().intersect(r.toSet())))) - break - - case 'exclude': - this.applyFun(app.id, 2, (l, r) => just(rv.mkSet(l.toSet().subtract(r.toSet())))) - break - - case 'size': - this.applyFun(app.id, 1, set => set.cardinality().map(rv.mkInt)) - break - - case 'isFinite': - // at the moment, we support only finite sets, so just return true - this.applyFun(app.id, 1, _set => just(rv.mkBool(true))) - break - - case 'to': - this.applyFun(app.id, 2, (i, j) => just(rv.mkInterval(i.toInt(), j.toInt()))) - break + }) + break + + case 'igt': + this.applyFun(app.id, 2, (p, q) => just(rv.mkBool(p.toInt() > q.toInt()))) + break + + case 'ilt': + this.applyFun(app.id, 2, (p, q) => just(rv.mkBool(p.toInt() < q.toInt()))) + break + + case 'igte': + this.applyFun(app.id, 2, (p, q) => just(rv.mkBool(p.toInt() >= q.toInt()))) + break + + case 'ilte': + this.applyFun(app.id, 2, (p, q) => just(rv.mkBool(p.toInt() <= q.toInt()))) + break + + case 'Tup': + // Construct a tuple from an array of values + this.applyFun(app.id, app.args.length, (...values: RuntimeValue[]) => just(rv.mkTuple(values))) + break + + case 'item': + // Access a tuple: tuples are 1-indexed, that is, _1, _2, etc. + this.applyFun(app.id, 2, (tuple, idx) => this.getListElem(app.id, tuple.toList(), Number(idx.toInt()) - 1)) + break + + case 'tuples': + // Construct a cross product + this.applyFun(app.id, app.args.length, (...sets: RuntimeValue[]) => just(rv.mkCrossProd(sets))) + break + + case 'List': + // Construct a list from an array of values + this.applyFun(app.id, app.args.length, (...values: RuntimeValue[]) => just(rv.mkList(values))) + break + + case 'range': + this.applyFun(app.id, 2, (start, end) => { + const [s, e] = [Number(start.toInt()), Number(end.toInt())] + if (s <= e) { + const arr: RuntimeValue[] = [] + for (let i = s; i < e; i++) { + arr.push(rv.mkInt(BigInt(i))) + } + return just(rv.mkList(arr)) + } else { + this.errorTracker.addRuntimeError(app.id, `range(${s}, ${e}) is out of bounds`) + return none() + } + }) + break - case 'fold': - this.applyFold(app.id, 'fwd') - break + case 'nth': + // Access a list + this.applyFun(app.id, 2, (list, idx) => this.getListElem(app.id, list.toList(), Number(idx.toInt()))) + break - case 'foldl': - this.applyFold(app.id, 'fwd') - break + case 'replaceAt': + this.applyFun(app.id, 3, (list, idx, value) => + this.updateList(app.id, list.toList(), Number(idx.toInt()), value) + ) + break - case 'foldr': - this.applyFold(app.id, 'rev') - break + case 'head': + this.applyFun(app.id, 1, list => this.getListElem(app.id, list.toList(), 0)) + break - case 'flatten': - this.applyFun(app.id, 1, set => { - // unpack the sets from runtime values - const setOfSets = set.toSet().map(e => e.toSet()) - // and flatten the set of sets via immutable-js - return just(rv.mkSet(setOfSets.flatten(1) as Set)) - }) - break + case 'tail': + this.applyFun(app.id, 1, list => { + const l = list.toList() + if (l.size > 0) { + return this.sliceList(app.id, l, 1, l.size) + } else { + this.errorTracker.addRuntimeError(app.id, 'Applied tail to an empty list') + return none() + } + }) + break - case 'get': - // Get a map value - this.applyFun(app.id, 2, (map, key) => { - const value = map.toMap().get(key.normalForm()) - if (value) { - return just(value) - } else { - // Should we print the key? It may be a complex expression. - this.errorTracker.addRuntimeError(app.id, "Called 'get' with a non-existing key") - return none() - } - }) - break + case 'slice': + this.applyFun(app.id, 3, (list, start, end) => { + const [l, s, e] = [list.toList(), Number(start.toInt()), Number(end.toInt())] + if (s >= 0 && s <= l.size && e <= l.size && e >= s) { + return this.sliceList(app.id, l, s, e) + } else { + this.errorTracker.addRuntimeError(app.id, `slice(..., ${s}, ${e}) applied to a list of size ${l.size}`) + return none() + } + }) + break + + case 'length': + this.applyFun(app.id, 1, list => just(rv.mkInt(BigInt(list.toList().size)))) + break + + case 'append': + this.applyFun(app.id, 2, (list, elem) => just(rv.mkList(list.toList().push(elem)))) + break + + case 'concat': + this.applyFun(app.id, 2, (list1, list2) => just(rv.mkList(list1.toList().concat(list2.toList())))) + break + + case 'indices': + this.applyFun(app.id, 1, list => just(rv.mkInterval(0n, BigInt(list.toList().size - 1)))) + break + + case 'Rec': + // Construct a record + this.applyFun(app.id, app.args.length, (...values: RuntimeValue[]) => { + const keys = values.filter((e, i) => i % 2 === 0).map(k => k.toStr()) + const map: OrderedMap = keys.reduce((map, key, i) => { + const v = values[2 * i + 1] + return v ? map.set(key, v) : map + }, OrderedMap()) + return just(rv.mkRecord(map)) + }) + break + + case 'field': + // Access a record via the field name + this.applyFun(app.id, 2, (rec, fieldName) => { + const name = fieldName.toStr() + const fieldValue = rec.toOrderedMap().get(name) + if (fieldValue) { + return just(fieldValue) + } else { + this.errorTracker.addRuntimeError(app.id, `Accessing a missing record field ${name}`) + return none() + } + }) + break + + case 'fieldNames': + this.applyFun(app.id, 1, rec => { + const keysAsRuntimeValues = rec + .toOrderedMap() + .keySeq() + .map(key => rv.mkStr(key)) + return just(rv.mkSet(keysAsRuntimeValues)) + }) + break + + case 'with': + // update a record + this.applyFun(app.id, 3, (rec, fieldName, fieldValue) => { + const oldMap = rec.toOrderedMap() + const key = fieldName.toStr() + if (oldMap.has(key)) { + const newMap = rec.toOrderedMap().set(key, fieldValue) + return just(rv.mkRecord(newMap)) + } else { + this.errorTracker.addRuntimeError(app.id, `Called 'with' with a non-existent key ${key}`) + return none() + } + }) + break + + case 'Set': + // Construct a set from an array of values. + this.applyFun(app.id, app.args.length, (...values: RuntimeValue[]) => just(rv.mkSet(values))) + break + + case 'powerset': + this.applyFun(app.id, 1, (baseset: RuntimeValue) => just(rv.mkPowerset(baseset))) + break + + case 'contains': + this.applyFun(app.id, 2, (set, value) => just(rv.mkBool(set.contains(value)))) + break + + case 'in': + this.applyFun(app.id, 2, (value, set) => just(rv.mkBool(set.contains(value)))) + break + + case 'subseteq': + this.applyFun(app.id, 2, (l, r) => just(rv.mkBool(l.isSubset(r)))) + break + + case 'union': + this.applyFun(app.id, 2, (l, r) => just(rv.mkSet(l.toSet().union(r.toSet())))) + break + + case 'intersect': + this.applyFun(app.id, 2, (l, r) => just(rv.mkSet(l.toSet().intersect(r.toSet())))) + break + + case 'exclude': + this.applyFun(app.id, 2, (l, r) => just(rv.mkSet(l.toSet().subtract(r.toSet())))) + break + + case 'size': + this.applyFun(app.id, 1, set => set.cardinality().map(rv.mkInt)) + break + + case 'isFinite': + // at the moment, we support only finite sets, so just return true + this.applyFun(app.id, 1, _set => just(rv.mkBool(true))) + break + + case 'to': + this.applyFun(app.id, 2, (i, j) => just(rv.mkInterval(i.toInt(), j.toInt()))) + break + + case 'fold': + this.applyFold(app.id, 'fwd') + break + + case 'foldl': + this.applyFold(app.id, 'fwd') + break + + case 'foldr': + this.applyFold(app.id, 'rev') + break + + case 'flatten': + this.applyFun(app.id, 1, set => { + // unpack the sets from runtime values + const setOfSets = set.toSet().map(e => e.toSet()) + // and flatten the set of sets via immutable-js + return just(rv.mkSet(setOfSets.flatten(1) as Set)) + }) + break + + case 'get': + // Get a map value + this.applyFun(app.id, 2, (map, key) => { + const value = map.toMap().get(key.normalForm()) + if (value) { + return just(value) + } else { + // Should we print the key? It may be a complex expression. + this.errorTracker.addRuntimeError(app.id, "Called 'get' with a non-existing key") + return none() + } + }) + break + + case 'set': + // Update a map value + this.applyFun(app.id, 3, (map, key, newValue) => { + const normalKey = key.normalForm() + const asMap = map.toMap() + if (asMap.has(normalKey)) { + const newMap = asMap.set(normalKey, newValue) + return just(rv.fromMap(newMap)) + } else { + this.errorTracker.addRuntimeError(app.id, "Called 'set' with a non-existing key") + return none() + } + }) + break - case 'set': - // Update a map value - this.applyFun(app.id, 3, (map, key, newValue) => { - const normalKey = key.normalForm() - const asMap = map.toMap() - if (asMap.has(normalKey)) { + case 'put': + // add a value to a map + this.applyFun(app.id, 3, (map, key, newValue) => { + const normalKey = key.normalForm() + const asMap = map.toMap() const newMap = asMap.set(normalKey, newValue) return just(rv.fromMap(newMap)) - } else { - this.errorTracker.addRuntimeError(app.id, "Called 'set' with a non-existing key") - return none() - } - }) - break - - case 'put': - // add a value to a map - this.applyFun(app.id, 3, (map, key, newValue) => { - const normalKey = key.normalForm() - const asMap = map.toMap() - const newMap = asMap.set(normalKey, newValue) - return just(rv.fromMap(newMap)) - }) - break - - case 'setBy': { - // Update a map value via a lambda - const fun = this.compStack.pop() ?? fail - this.applyFun(app.id, 2, (map, key) => { - const normalKey = key.normalForm() - const asMap = map.toMap() - if (asMap.has(normalKey)) { - return fun.eval([just(asMap.get(normalKey))]).map(newValue => { - const newMap = asMap.set(normalKey, newValue as RuntimeValue) - return rv.fromMap(newMap) - }) - } else { - this.errorTracker.addRuntimeError(app.id, "Called 'setBy' with a non-existing key") - return none() - } - }) - break - } - - case 'keys': - // map keys as a set - this.applyFun(app.id, 1, map => { - return just(rv.mkSet(map.toMap().keys())) - }) - break - - case 'oneOf': - this.applyOneOf(app.id) - break - - case 'exists': - this.mapLambdaThenReduce(app.id, set => rv.mkBool(set.find(([result, _]) => result.toBool()) !== undefined)) - break - - case 'forall': - this.mapLambdaThenReduce(app.id, set => rv.mkBool(set.find(([result, _]) => !result.toBool()) === undefined)) - break - - case 'map': - this.mapLambdaThenReduce(app.id, array => rv.mkSet(array.map(([result, _]) => result))) - break - - case 'filter': - this.mapLambdaThenReduce(app.id, arr => rv.mkSet(arr.filter(([r, _]) => r.toBool()).map(([_, e]) => e))) - break - - case 'select': - this.mapLambdaThenReduce(app.id, arr => rv.mkList(arr.filter(([r, _]) => r.toBool()).map(([_, e]) => e))) - break - - case 'mapBy': - this.mapLambdaThenReduce(app.id, arr => rv.mkMap(arr.map(([v, k]) => [k, v]))) - break - - case 'Map': - this.applyFun(app.id, app.args.length, (...pairs: any[]) => just(rv.mkMap(pairs))) - break - - case 'setToMap': - this.applyFun(app.id, 1, (set: RuntimeValue) => - just( - rv.mkMap( - set.toSet().map(p => { - const arr = p.toList().toArray() - return [arr[0], arr[1]] + }) + break + + case 'setBy': { + // Update a map value via a lambda + const fun = this.compStack.pop() ?? fail + this.applyFun(app.id, 2, (map, key) => { + const normalKey = key.normalForm() + const asMap = map.toMap() + if (asMap.has(normalKey)) { + return fun.eval([just(asMap.get(normalKey))]).map(newValue => { + const newMap = asMap.set(normalKey, newValue as RuntimeValue) + return rv.fromMap(newMap) }) + } else { + this.errorTracker.addRuntimeError(app.id, "Called 'setBy' with a non-existing key") + return none() + } + }) + break + } + + case 'keys': + // map keys as a set + this.applyFun(app.id, 1, map => { + return just(rv.mkSet(map.toMap().keys())) + }) + break + + case 'oneOf': + this.applyOneOf(app.id) + break + + case 'exists': + this.mapLambdaThenReduce(app.id, set => rv.mkBool(set.find(([result, _]) => result.toBool()) !== undefined)) + break + + case 'forall': + this.mapLambdaThenReduce(app.id, set => rv.mkBool(set.find(([result, _]) => !result.toBool()) === undefined)) + break + + case 'map': + this.mapLambdaThenReduce(app.id, array => rv.mkSet(array.map(([result, _]) => result))) + break + + case 'filter': + this.mapLambdaThenReduce(app.id, arr => rv.mkSet(arr.filter(([r, _]) => r.toBool()).map(([_, e]) => e))) + break + + case 'select': + this.mapLambdaThenReduce(app.id, arr => rv.mkList(arr.filter(([r, _]) => r.toBool()).map(([_, e]) => e))) + break + + case 'mapBy': + this.mapLambdaThenReduce(app.id, arr => rv.mkMap(arr.map(([v, k]) => [k, v]))) + break + + case 'Map': + this.applyFun(app.id, app.args.length, (...pairs: any[]) => just(rv.mkMap(pairs))) + break + + case 'setToMap': + this.applyFun(app.id, 1, (set: RuntimeValue) => + just( + rv.mkMap( + set.toSet().map(p => { + const arr = p.toList().toArray() + return [arr[0], arr[1]] + }) + ) ) ) - ) - break + break - case 'setOfMaps': - this.applyFun(app.id, 2, (dom, rng) => { - return just(rv.mkMapSet(dom, rng)) - }) - break + case 'setOfMaps': + this.applyFun(app.id, 2, (dom, rng) => { + return just(rv.mkMapSet(dom, rng)) + }) + break - case 'then': - this.translateAllOrThen(app) - break + case 'then': + this.translateAllOrThen(app) + break - case 'fail': - this.applyFun(app.id, 1, result => { - return just(rv.mkBool(!result.toBool())) - }) - break + case 'fail': + this.applyFun(app.id, 1, result => { + return just(rv.mkBool(!result.toBool())) + }) + break - case 'assert': - this.applyFun(app.id, 1, cond => { - if (!cond.toBool()) { - this.errorTracker.addRuntimeError(app.id, 'Assertion failed') + case 'assert': + this.applyFun(app.id, 1, cond => { + if (!cond.toBool()) { + this.errorTracker.addRuntimeError(app.id, 'Assertion failed') + return none() + } + return just(cond) + }) + break + + case 'reps': + this.translateReps(app) + break + + case 'q::test': + // the special operator that runs random simulation + this.test(app.id) + break + + case 'q::testOnce': + // the special operator that runs random simulation + this.testOnce(app.id) + break + + // standard unary operators that are not handled by REPL + case 'allLists': + case 'chooseSome': + case 'always': + case 'eventually': + case 'enabled': + this.applyFun(app.id, 1, _ => { + this.errorTracker.addRuntimeError(app.id, `Runtime does not support the built-in operator '${app.opcode}'`) return none() - } - return just(cond) - }) - break - - case 'reps': - this.translateReps(app) - break - - case 'q::test': - // the special operator that runs random simulation - this.test(app.id) - break - - case 'q::testOnce': - // the special operator that runs random simulation - this.testOnce(app.id) - break - - // standard unary operators that are not handled by REPL - case 'allLists': - case 'chooseSome': - case 'always': - case 'eventually': - case 'enabled': - this.applyFun(app.id, 1, _ => { - this.errorTracker.addRuntimeError(app.id, `Runtime does not support the built-in operator '${app.opcode}'`) - return none() - }) - break - - // standard binary operators that are not handled by REPL - case 'orKeep': - case 'mustChange': - case 'weakFair': - case 'strongFair': - this.applyFun(app.id, 2, _ => { - this.errorTracker.addRuntimeError(app.id, `Runtime does not support the built-in operator '${app.opcode}'`) - return none() - }) - break + }) + break + + // builtin operators that are not handled by REPL + case 'unionMatch': + case 'orKeep': + case 'mustChange': + case 'weakFair': + case 'strongFair': + this.applyFun(app.id, 2, _ => { + this.errorTracker.addRuntimeError(app.id, `Runtime does not support the built-in operator '${app.opcode}'`) + return none() + }) + break - default: { - this.applyUserDefined(app) + default: + unreachable(app.opcode) } } } diff --git a/quint/src/types/builtinSignatures.ts b/quint/src/types/builtinSignatures.ts index 96c250bb1..69e83c3f7 100644 --- a/quint/src/types/builtinSignatures.ts +++ b/quint/src/types/builtinSignatures.ts @@ -16,6 +16,7 @@ import { parseTypeOrThrow } from './parser' import { typeNames } from '../ir/quintTypes' import { Signature, TypeScheme } from './base' import { times } from 'lodash' +import { QuintBuiltinOpcode } from '../ir/quintIr' export function getSignatures(): Map { return new Map(fixedAritySignatures.concat(multipleAritySignatures)) @@ -130,7 +131,7 @@ function uniformArgsWithResult(argsType: string, resultType: string): Signature } // TODO: check arity conditions, see issue https://github.com/informalsystems/quint/issues/169 -const multipleAritySignatures: [string, Signature][] = [ +const multipleAritySignatures: [QuintBuiltinOpcode, Signature][] = [ ['List', uniformArgsWithResult('a', 'List[a]')], ['Set', uniformArgsWithResult('a', 'Set[a]')], ['Map', uniformArgsWithResult('(a, b)', 'a -> b')], diff --git a/quint/src/types/substitutions.ts b/quint/src/types/substitutions.ts index 3989c976c..9a22ba2bc 100644 --- a/quint/src/types/substitutions.ts +++ b/quint/src/types/substitutions.ts @@ -15,7 +15,7 @@ import { Either } from '@sweet-monads/either' import { ErrorTree, errorTreeToString } from '../errorTree' import { LookupTable } from '../names/base' -import { QuintType, Row } from '../ir/quintTypes' +import { ConcreteFixedRow, QuintType, Row } from '../ir/quintTypes' import { Constraint } from './base' import { unify, unifyRows } from './constraintSolver' import { substitutionsToString } from './printing' @@ -51,49 +51,44 @@ export function compose(table: LookupTable, s1: Substitutions, s2: Substitutions * given type */ export function applySubstitution(table: LookupTable, subs: Substitutions, t: QuintType): QuintType { - let result = t switch (t.kind) { case 'var': { const sub = subs.find(s => s.name === t.name) if (sub && sub.kind === 'type') { - result = sub.value + return sub.value + } else { + return t } - break } case 'oper': { const arrowParams = t.args.map(ef => applySubstitution(table, subs, ef)) const arrowResult = applySubstitution(table, subs, t.res) - result = { kind: t.kind, args: arrowParams, res: arrowResult, id: t.id } - break + return { kind: t.kind, args: arrowParams, res: arrowResult, id: t.id } } case 'list': case 'set': { - result = { kind: t.kind, elem: applySubstitution(table, subs, t.elem), id: t.id } - break + return { kind: t.kind, elem: applySubstitution(table, subs, t.elem), id: t.id } } case 'fun': { - result = { + return { kind: t.kind, arg: applySubstitution(table, subs, t.arg), res: applySubstitution(table, subs, t.res), id: t.id, } - break } case 'tup': { - result = { kind: t.kind, fields: applySubstitutionToRow(table, subs, t.fields), id: t.id } - break + return { kind: t.kind, fields: applySubstitutionToRow(table, subs, t.fields), id: t.id } } case 'rec': { - result = { + return { kind: t.kind, fields: applySubstitutionToRow(table, subs, t.fields), id: t.id, } - break } case 'union': { - result = { + return { kind: t.kind, tag: t.tag, records: t.records.map(r => { @@ -104,11 +99,22 @@ export function applySubstitution(table: LookupTable, subs: Substitutions, t: Qu }), id: t.id, } - break } - } + case 'sum': + return { + ...t, + // We know this has to end up as a concrete fixed row, since it must + // start as one, and applying substitions cannot result in a wider type + fields: applySubstitutionToRow(table, subs, t.fields) as ConcreteFixedRow, + } - return result + // The basic types have no variables, so cannot + case 'int': + case 'bool': + case 'str': + case 'const': + return t + } } /** diff --git a/quint/src/util.ts b/quint/src/util.ts new file mode 100644 index 000000000..61074beb3 --- /dev/null +++ b/quint/src/util.ts @@ -0,0 +1,29 @@ +/* ---------------------------------------------------------------------------------- + * Copyright (c) Informal Systems 2023. All rights reserved. + * Licensed under the Apache 2.0. + * See License.txt in the project root for license information. + * --------------------------------------------------------------------------------- */ + +/** + * General purpose utilities used within the quint codebase + * + * @author Shon Feder + * + * @module + */ + +/** Add this at the end of a switch statement or if/then sequence to enforce exhaustiveness checking + * + * E.g., + * + * ``` + * switch (foo.bar) { + * case 'bax': ... + * case 'qux': ... + * default: unreachable(foo) + * } + * ``` + * See https://stackoverflow.com/a/39419171 */ +export function unreachable(_: never): never { + throw new Error('impossible: non-exhuastive check should fail during type checking') +} diff --git a/vscode/quint-vscode/CHANGELOG.md b/vscode/quint-vscode/CHANGELOG.md index 3adaab24e..7be020e4a 100644 --- a/vscode/quint-vscode/CHANGELOG.md +++ b/vscode/quint-vscode/CHANGELOG.md @@ -7,6 +7,15 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 ## UNRELEASED +### Added +### Changed +### Deprecated +### Removed +### Fixed +### Security + +## v0.7.0 -- 2023-08-06 + ### Added - Better icons in VSCode outline view (#1024). diff --git a/vscode/quint-vscode/package-lock.json b/vscode/quint-vscode/package-lock.json index 07e0e6045..8c9000b91 100644 --- a/vscode/quint-vscode/package-lock.json +++ b/vscode/quint-vscode/package-lock.json @@ -1,12 +1,12 @@ { "name": "quint-vscode", - "version": "0.6.0", + "version": "0.7.0", "lockfileVersion": 2, "requires": true, "packages": { "": { "name": "quint-vscode", - "version": "0.6.0", + "version": "0.7.0", "hasInstallScript": true, "dependencies": { "vscode-languageclient": "^7.0.0" diff --git a/vscode/quint-vscode/package.json b/vscode/quint-vscode/package.json index 9234725ea..c7b7850aa 100644 --- a/vscode/quint-vscode/package.json +++ b/vscode/quint-vscode/package.json @@ -2,7 +2,7 @@ "name": "quint-vscode", "displayName": "Quint", "description": "Language support for Quint specifications", - "version": "0.6.0", + "version": "0.7.0", "publisher": "informal", "engines": { "vscode": "^1.52.0" @@ -50,7 +50,7 @@ "postinstall": "cd server && npm install && cd ..", "test": "cd server && npm test", "format-check": "npx prettier --check '**/*.ts' && npx eslint '**/*.ts'", - "format": "npx prettier --write '**/*.ts' && npx eslint --fix '**/*.ts'" + "format": "npx prettier --write '**/*.ts' && npx eslint --fix '**/*.ts'" }, "devDependencies": { "@types/mocha": "^8.2.2", @@ -58,7 +58,7 @@ "@typescript-eslint/eslint-plugin": "^5.30.6", "@typescript-eslint/parser": "^5.30.6", "eslint": "^8.27.0", - "eslint-config-prettier": "^8.8.0", + "eslint-config-prettier": "^8.8.0", "eslint-config-recommended": "^4.1.0", "eslint-plugin-import": "^2.26.0", "eslint-plugin-json": "^3.1.0", @@ -66,7 +66,7 @@ "eslint-plugin-promise": "^6.1.1", "eslint-plugin-unused-imports": "^2.0.0", "mocha": "^8.3.2", - "prettier": "2.8.8", + "prettier": "2.8.8", "typescript": "^4.2.3", "@types/vscode": "^1.52.0", "vscode-test": "^1.3.0" diff --git a/vscode/quint-vscode/server/package-lock.json b/vscode/quint-vscode/server/package-lock.json index 6a9602f5b..b0a672147 100644 --- a/vscode/quint-vscode/server/package-lock.json +++ b/vscode/quint-vscode/server/package-lock.json @@ -1,15 +1,15 @@ { "name": "quint-lsp-server", - "version": "0.6.0", + "version": "0.7.0", "lockfileVersion": 2, "requires": true, "packages": { "": { "name": "quint-lsp-server", - "version": "0.6.0", + "version": "0.7.0", "license": "Apache 2.0", "dependencies": { - "@informalsystems/quint": "^0.12.0", + "@informalsystems/quint": "^0.13.0", "vscode-languageserver": "^7.0.0", "vscode-languageserver-textdocument": "^1.0.1", "vscode-uri": "^3.0.7" @@ -477,9 +477,9 @@ "dev": true }, "node_modules/@informalsystems/quint": { - "version": "0.12.0", - "resolved": "https://registry.npmjs.org/@informalsystems/quint/-/quint-0.12.0.tgz", - "integrity": "sha512-K3yxpIvfQs2Oxkly1SIQuCoa8KBgXKxkoaQhTcX5kFOeKcOXnabNALLE5IbTf6tgOcx1fDZAh6/kGu4VLDtivw==", + "version": "0.13.0", + "resolved": "https://registry.npmjs.org/@informalsystems/quint/-/quint-0.13.0.tgz", + "integrity": "sha512-GmBnv+WQZH1BCC0py4mVRt3eSZd6xhbUnfYaBHmeEVYLonO93+XDIWW436vB/k1c8w9ed0oXGxBiN+Z2fXMvDQ==", "dependencies": { "@grpc/grpc-js": "^1.8.14", "@grpc/proto-loader": "^0.7.7", @@ -7109,9 +7109,9 @@ "dev": true }, "@informalsystems/quint": { - "version": "0.12.0", - "resolved": "https://registry.npmjs.org/@informalsystems/quint/-/quint-0.12.0.tgz", - "integrity": "sha512-K3yxpIvfQs2Oxkly1SIQuCoa8KBgXKxkoaQhTcX5kFOeKcOXnabNALLE5IbTf6tgOcx1fDZAh6/kGu4VLDtivw==", + "version": "0.13.0", + "resolved": "https://registry.npmjs.org/@informalsystems/quint/-/quint-0.13.0.tgz", + "integrity": "sha512-GmBnv+WQZH1BCC0py4mVRt3eSZd6xhbUnfYaBHmeEVYLonO93+XDIWW436vB/k1c8w9ed0oXGxBiN+Z2fXMvDQ==", "requires": { "@grpc/grpc-js": "^1.8.14", "@grpc/proto-loader": "^0.7.7", diff --git a/vscode/quint-vscode/server/package.json b/vscode/quint-vscode/server/package.json index 830fa3220..0291fd221 100644 --- a/vscode/quint-vscode/server/package.json +++ b/vscode/quint-vscode/server/package.json @@ -1,7 +1,7 @@ { "name": "quint-lsp-server", "description": "LSP server for Quint in node.", - "version": "0.6.0", + "version": "0.7.0", "author": "Informal Systems", "license": "Apache 2.0", "engines": { @@ -12,7 +12,7 @@ "url": "https://github.com/informalsystems/quint" }, "dependencies": { - "@informalsystems/quint": "^0.12.0", + "@informalsystems/quint": "^0.13.0", "vscode-languageserver": "^7.0.0", "vscode-languageserver-textdocument": "^1.0.1", "vscode-uri": "^3.0.7"