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 af2f2d8ba..9d0bb8f7e 100644 --- a/quint/src/cliCommands.ts +++ b/quint/src/cliCommands.ts @@ -27,7 +27,7 @@ import { Either, left, right } from '@sweet-monads/either' import { EffectScheme } from './effects/base' import { LookupTable } from './names/base' import { ReplOptions, quintRepl } from './repl' -import { OpQualifier, QuintEx, QuintModule } from './quintIr' +import { OpQualifier, QuintEx, QuintModule } from './ir/quintIr' import { TypeScheme } from './types/base' import lineColumn from 'line-column' import { formatError } from './errorReporter' @@ -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/inferrer.ts b/quint/src/effects/inferrer.ts index 16ec63dd8..0e3adcbe9 100644 --- a/quint/src/effects/inferrer.ts +++ b/quint/src/effects/inferrer.ts @@ -15,8 +15,8 @@ import { Either, left, mergeInMany, right } from '@sweet-monads/either' import { LookupTable } from '../names/base' -import { expressionToString } from '../IRprinting' -import { IRVisitor, walkDefinition } from '../IRVisitor' +import { expressionToString } from '../ir/IRprinting' +import { IRVisitor, walkDefinition } from '../ir/IRVisitor' import { QuintApp, QuintBool, @@ -30,7 +30,7 @@ import { QuintOpDef, QuintStr, QuintVar, -} from '../quintIr' +} from '../ir/quintIr' import { Effect, EffectScheme, Signature, effectNames, toScheme, unify } from './base' import { Substitutions, applySubstitution, compose } from './substitutions' import { Error, ErrorTree, buildErrorLeaf, buildErrorTree, errorTreeToString } from '../errorTree' diff --git a/quint/src/effects/modeChecker.ts b/quint/src/effects/modeChecker.ts index ce143837c..30847e9b7 100644 --- a/quint/src/effects/modeChecker.ts +++ b/quint/src/effects/modeChecker.ts @@ -14,10 +14,11 @@ */ import isEqual from 'lodash.isequal' -import { qualifierToString } from '../IRprinting' -import { IRVisitor, walkDefinition } from '../IRVisitor' +import { qualifierToString } from '../ir/IRprinting' +import { IRVisitor, walkDefinition } from '../ir/IRVisitor' import { QuintError } from '../quintError' -import { OpQualifier, QuintDef, QuintInstance, QuintOpDef } from '../quintIr' +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/flattening.ts b/quint/src/flattening.ts index ce4e22202..877ba771f 100644 --- a/quint/src/flattening.ts +++ b/quint/src/flattening.ts @@ -18,21 +18,19 @@ import { FlatDef, FlatModule, QuintDef, - QuintEx, QuintExport, QuintImport, QuintInstance, QuintModule, - QuintOpDef, - isAnnotatedDef, isFlat, -} from './quintIr' -import { definitionToString } from './IRprinting' -import { ConcreteFixedRow, QuintType, Row } from './quintTypes' +} from './ir/quintIr' +import { definitionToString, moduleToString } from './ir/IRprinting' import { Loc, parsePhase3importAndNameResolution } from './parsing/quintParserFrontend' import { compact, uniqBy } from 'lodash' import { AnalysisOutput } from './quintAnalyzer' import { inlineAliasesInDef, inlineAnalysisOutput, inlineTypeAliases } from './types/aliasInliner' +import { addNamespaceToDefinition } from './ir/namespacer' +import { generateFreshIds } from './ir/idRefresher' /** * Flatten an array of modules, replacing instances, imports and exports with @@ -146,14 +144,15 @@ export function addDefToFlatModule( } class Flatenner { - private idGenerator: IdGenerator private table: LookupTable private currentModuleNames: Set - private sourceMap: Map - private analysisOutput: AnalysisOutput private importedModules: Map private module: QuintModule + private idGenerator: IdGenerator + private sourceMap: Map + private analysisOutput: AnalysisOutput + constructor( idGenerator: IdGenerator, table: LookupTable, @@ -162,7 +161,6 @@ class Flatenner { importedModules: Map, module: QuintModule ) { - this.idGenerator = idGenerator this.table = table this.currentModuleNames = new Set([ // builtin names @@ -171,10 +169,11 @@ class Flatenner { ...compact(module.defs.map(d => (isFlat(d) ? d.name : undefined))), ]) - this.sourceMap = sourceMap - this.analysisOutput = analysisOutput this.importedModules = importedModules this.module = module + this.idGenerator = idGenerator + this.sourceMap = sourceMap + this.analysisOutput = analysisOutput } flattenDef(def: QuintDef): FlatDef[] { @@ -260,233 +259,15 @@ class Flatenner { throw new Error(`Impossible: ${definitionToString(def)} should have been flattened already`) } - if (!isAnnotatedDef(def)) { - return this.addNamespaceToDef(qualifier, def) - } - - const type = this.addNamespaceToType(qualifier, def.typeAnnotation) - const newDef = this.addNamespaceToDef(qualifier, def) - if (!isAnnotatedDef(newDef)) { - throw new Error(`Impossible: transformation should preserve kind`) - } - - return { ...newDef, typeAnnotation: type } - } - - private addNamespaceToDef(name: string | undefined, def: QuintDef): FlatDef { - switch (def.kind) { - case 'def': - return this.addNamespaceToOpDef(name, def) - case 'assume': - return { - ...def, - name: this.namespacedName(name, def.name), - assumption: this.addNamespaceToExpr(name, def.assumption), - id: this.getNewIdWithSameData(def.id), - } - case 'const': - case 'var': - return { ...def, name: this.namespacedName(name, def.name), id: this.getNewIdWithSameData(def.id) } - case 'typedef': - return { - ...def, - name: this.namespacedName(name, def.name), - type: def.type ? this.addNamespaceToType(name, def.type) : undefined, - id: this.getNewIdWithSameData(def.id), - } - case 'instance': - throw new Error(`Instance in ${definitionToString(def)} should have been flatenned already`) - case 'import': - throw new Error(`Import in ${definitionToString(def)} should have been flatenned already`) - case 'export': - throw new Error(`Export in ${definitionToString(def)} should have been flatenned already`) - } - } - - private addNamespaceToOpDef(name: string | undefined, opdef: QuintOpDef): QuintOpDef { - return { - ...opdef, - name: this.namespacedName(name, opdef.name), - expr: this.addNamespaceToExpr(name, opdef.expr), - id: this.getNewIdWithSameData(opdef.id), - } - } - - private addNamespaceToExpr(name: string | undefined, expr: QuintEx): QuintEx { - const id = this.getNewIdWithSameData(expr.id) - - switch (expr.kind) { - case 'name': - if (this.shouldAddNamespace(expr.name)) { - return { ...expr, name: this.namespacedName(name, expr.name), id } - } - - return { ...expr, id } - case 'bool': - case 'int': - case 'str': - return { ...expr, id } - case 'app': { - if (this.shouldAddNamespace(expr.opcode)) { - return { - ...expr, - opcode: this.namespacedName(name, expr.opcode), - args: expr.args.map(arg => this.addNamespaceToExpr(name, arg)), - id, - } - } - - return { - ...expr, - args: expr.args.map(arg => this.addNamespaceToExpr(name, arg)), - id, - } - } - case 'lambda': - return { - ...expr, - params: expr.params.map(param => ({ - name: this.namespacedName(name, param.name), - id: this.getNewIdWithSameData(param.id), - })), - expr: this.addNamespaceToExpr(name, expr.expr), - id, - } - - case 'let': - return { - ...expr, - opdef: this.addNamespaceToOpDef(name, expr.opdef), - expr: this.addNamespaceToExpr(name, expr.expr), - id, - } - } - } - - private addNamespaceToType(name: string | undefined, type: QuintType): QuintType { - const id = type.id ? this.getNewIdWithSameData(type.id) : undefined - - switch (type.kind) { - case 'bool': - case 'int': - case 'str': - case 'var': - return { ...type, id } - case 'const': - return { ...type, name: this.namespacedName(name, type.name), id } - case 'set': - case 'list': - return { ...type, elem: this.addNamespaceToType(name, type.elem), id } - case 'fun': - return { - ...type, - arg: this.addNamespaceToType(name, type.arg), - res: this.addNamespaceToType(name, type.res), - id, - } - case 'oper': - return { - ...type, - args: type.args.map(arg => this.addNamespaceToType(name, arg)), - res: this.addNamespaceToType(name, type.res), - id, - } - case 'tup': - case 'rec': - return { - ...type, - fields: this.addNamespaceToRow(name, type.fields), - id, - } - case 'sum': - return { - ...type, - fields: this.addNamespaceToSumRow(name, type.fields), - id, - } - case 'union': - return { - ...type, - records: type.records.map(record => { - return { - ...record, - fields: this.addNamespaceToRow(name, record.fields), - } - }), - id, - } - } - } + const defWithQualifier = qualifier ? addNamespaceToDefinition(def, qualifier, this.currentModuleNames) : def + const defWithNewId = generateFreshIds(defWithQualifier, this.idGenerator, this.sourceMap, this.analysisOutput) - private addNamespaceToRow(name: string | undefined, row: Row): Row { - if (row.kind !== 'row') { - return row - } - - return { - ...row, - fields: row.fields.map(field => { - return { - ...field, - fieldType: this.addNamespaceToType(name, field.fieldType), - } - }), - } - } - - private addNamespaceToSumRow(name: string | undefined, row: ConcreteFixedRow): ConcreteFixedRow { - return { - ...row, - fields: row.fields.map(field => { - return { - ...field, - fieldType: this.addNamespaceToType(name, field.fieldType), - } - }), - } - } - - private namespacedName(namespace: string | undefined, name: string): string { - return namespace ? `${namespace}::${name}` : name - } - - /** - * Whether a name should be prefixed with the namespace. - * - * @param name the name to be prefixed - * - * @returns false if the name is on the curentModulesName list, true otherwise - */ - private shouldAddNamespace(name: string): boolean { - if (this.currentModuleNames.has(name)) { - return false - } - - return true - } - - private getNewIdWithSameData(id: bigint): bigint { - const newId = this.idGenerator.nextId() - - const type = this.analysisOutput.types.get(id) - const effect = this.analysisOutput.effects.get(id) - const mode = this.analysisOutput.modes.get(id) - const source = this.sourceMap.get(id) - - if (type) { - this.analysisOutput.types.set(newId, type) - } - if (effect) { - this.analysisOutput.effects.set(newId, effect) - } - if (mode) { - this.analysisOutput.modes.set(newId, mode) - } - if (source) { - this.sourceMap.set(newId, source) + if (!isFlat(defWithNewId)) { + // safe cast + throw new Error(`Impossible: updating definitions cannot unflatten a def: ${definitionToString(defWithNewId)}`) } - return newId + return defWithNewId } } @@ -504,6 +285,7 @@ function resolveNamesOrThrow(currentTable: LookupTable, sourceMap: Map e.explanation)}`) }) .unwrap().table diff --git a/quint/src/graphics.ts b/quint/src/graphics.ts index 7d1620239..f0ba52a3b 100644 --- a/quint/src/graphics.ts +++ b/quint/src/graphics.ts @@ -26,13 +26,13 @@ import { textify, } from './prettierimp' -import { QuintDef, QuintEx, isAnnotatedDef } from './quintIr' +import { QuintDef, QuintEx, isAnnotatedDef } from './ir/quintIr' import { ExecutionFrame } from './runtime/trace' import { zerog } from './idGenerator' -import { ConcreteFixedRow, QuintType, Row } from './quintTypes' +import { ConcreteFixedRow, QuintType, Row } from './ir/quintTypes' import { TypeScheme } from './types/base' import { canonicalTypeScheme } from './types/printing' -import { definitionToString, flattenRow, qualifierToString, rowToString } from './IRprinting' +import { definitionToString, flattenRow, qualifierToString, rowToString } from './ir/IRprinting' /** * An abstraction of a Console of bounded text width. diff --git a/quint/src/index.ts b/quint/src/index.ts index 5e7bb46ba..cb0cb5db8 100644 --- a/quint/src/index.ts +++ b/quint/src/index.ts @@ -2,9 +2,9 @@ // // Igor Konnov, Informal Systems, 2021 -export * from './quintTypes' -export * from './quintIr' -export * from './IRprinting' +export * from './ir/quintTypes' +export * from './ir/quintIr' +export * from './ir/IRprinting' export * from './parsing/quintParserFrontend' export * from './effects/base' export * from './effects/printing' @@ -16,7 +16,7 @@ export { produceDocsById, DocumentationEntry } from './docs' export { builtinDocs } from './builtin' export * as Builder from '../test/builders/ir' export { TypeScheme } from './types/base' -export { findExpressionWithId, findTypeWithId, findDefinitionWithId } from './IRFinder' +export { findExpressionWithId, findTypeWithId, findDefinitionWithId } from './ir/IRFinder' export * from './quintAnalyzer' export * from './quintError' export { newIdGenerator, IdGenerator } from './idGenerator' diff --git a/quint/src/IRFinder.ts b/quint/src/ir/IRFinder.ts similarity index 100% rename from quint/src/IRFinder.ts rename to quint/src/ir/IRFinder.ts diff --git a/quint/src/IRTransformer.ts b/quint/src/ir/IRTransformer.ts similarity index 93% rename from quint/src/IRTransformer.ts rename to quint/src/ir/IRTransformer.ts index 0d1c16502..13faea040 100644 --- a/quint/src/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/IRVisitor.ts b/quint/src/ir/IRVisitor.ts similarity index 97% rename from quint/src/IRVisitor.ts rename to quint/src/ir/IRVisitor.ts index 280c2cc62..3cd17870d 100644 --- a/quint/src/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/IRprinting.ts b/quint/src/ir/IRprinting.ts similarity index 98% rename from quint/src/IRprinting.ts rename to quint/src/ir/IRprinting.ts index d63d6e6a0..e838f5528 100644 --- a/quint/src/IRprinting.ts +++ b/quint/src/ir/IRprinting.ts @@ -14,8 +14,8 @@ import { OpQualifier, QuintDef, QuintEx, QuintModule, isAnnotatedDef } from './quintIr' import { EmptyRow, QuintSumType, QuintType, Row, RowField, VarRow, isTheUnit } from './quintTypes' -import { TypeScheme } from './types/base' -import { typeSchemeToString } from './types/printing' +import { TypeScheme } from '../types/base' +import { typeSchemeToString } from '../types/printing' /** * Pretty prints a module diff --git a/quint/src/ir/idRefresher.ts b/quint/src/ir/idRefresher.ts new file mode 100644 index 000000000..246258b08 --- /dev/null +++ b/quint/src/ir/idRefresher.ts @@ -0,0 +1,106 @@ +/* ---------------------------------------------------------------------------------- + * Copyright (c) Informal Systems 2023. All rights reserved. + * Licensed under the Apache 2.0. + * See License.txt in the project root for license information. + * --------------------------------------------------------------------------------- */ + +/** + * Generation of fresh ids for IR components. This is used to generate fresh ids for + * modules generate from instances, enabling them to assume different values in evaluation. + * + * @author Gabriela Moreira + * + * @module + */ + +import { IRTransformer, transformDefinition } from './IRTransformer' +import { IdGenerator } from '../idGenerator' +import { Loc } from '../parsing/quintParserFrontend' +import { AnalysisOutput } from '../quintAnalyzer' +import { QuintDef, QuintEx, QuintLambda } from './quintIr' +import { QuintType } from './quintTypes' + +/** + * Given a QuintDef, generates fresh IDs for all its components using the + * provided IdGenerator. Returns a new QuintDef with the updated IDs. Also extends + * the provided source map and analysis output, such that they contain the respective + * entries under both their old and new IDs. + * + * @param def - The QuintDef to update with fresh IDs. + * @param idGenerator - The IdGenerator to use for generating fresh IDs. + * @param sourceMap - A source map to be updated with sources for the new ids + * (should contain entries for the existing ids) + * @param analysisOutput - An analysis output to be updated with analysis for the new ids + * (should contain entries for the existing ids) + * @returns A new QuintDef with fresh IDs. + */ +export function generateFreshIds( + def: QuintDef, + idGenerator: IdGenerator, + sourceMap: Map, + analysisOutput: AnalysisOutput +): QuintDef { + const transformer = new IdRefresher(idGenerator, sourceMap, analysisOutput) + return transformDefinition(transformer, def) +} + +class IdRefresher implements IRTransformer { + private idGenerator: IdGenerator + private sourceMap: Map + private analysisOutput: AnalysisOutput + + constructor(idGenerator: IdGenerator, sourceMap: Map, analysisOutput: AnalysisOutput) { + this.idGenerator = idGenerator + this.sourceMap = sourceMap + this.analysisOutput = analysisOutput + } + + /* New ID generation */ + + enterDef(def: QuintDef): QuintDef { + return { ...def, id: this.getNewIdWithSameData(def.id) } + } + + enterLambda(expr: QuintLambda): QuintLambda { + return { + ...expr, + params: expr.params.map(p => ({ ...p, id: this.getNewIdWithSameData(p.id) })), + } + } + + enterExpr(expr: QuintEx): QuintEx { + return { ...expr, id: this.getNewIdWithSameData(expr.id) } + } + + enterType(type: QuintType): QuintType { + if (!type.id) { + return type + } + + return { ...type, id: this.getNewIdWithSameData(type.id) } + } + + private getNewIdWithSameData(id: bigint): bigint { + const newId = this.idGenerator.nextId() + + const type = this.analysisOutput.types.get(id) + const effect = this.analysisOutput.effects.get(id) + const mode = this.analysisOutput.modes.get(id) + const source = this.sourceMap.get(id) + + if (type) { + this.analysisOutput.types.set(newId, type) + } + if (effect) { + this.analysisOutput.effects.set(newId, effect) + } + if (mode) { + this.analysisOutput.modes.set(newId, mode) + } + if (source) { + this.sourceMap.set(newId, source) + } + + return newId + } +} diff --git a/quint/src/ir/namespacer.ts b/quint/src/ir/namespacer.ts new file mode 100644 index 000000000..afc39a67a --- /dev/null +++ b/quint/src/ir/namespacer.ts @@ -0,0 +1,89 @@ +/* ---------------------------------------------------------------------------------- + * Copyright (c) Informal Systems 2023. All rights reserved. + * Licensed under the Apache 2.0. + * See License.txt in the project root for license information. + * --------------------------------------------------------------------------------- */ + +/** + * Recursive addition of namespaces into all names in IR components. To be used in flattening + * to manipulate names of copied definitions. + * + * @author Gabriela Moreira + * + * @module + */ + +import { IRTransformer, transformDefinition } from './IRTransformer' +import { QuintApp, QuintDef, QuintLambda, QuintName, isFlat } from './quintIr' +import { QuintConstType } from './quintTypes' + +/** + * Adds a namespace to a QuintDef and the names inside it, preserving a set of names. + * + * @param def - The QuintDef to add the namespace to. + * @param namespace - The namespace to add. + * @param namesToPreserve - A set of names that should not receive the namespace (e.g. builtin names). + * @returns A new QuintDef with the namespace added to its name and all names inside it. + */ +export function addNamespaceToDefinition(def: QuintDef, namespace: string, namesToPreserve: Set): QuintDef { + const updater = new Namespacer(namespace, namesToPreserve) + return transformDefinition(updater, def) +} + +class Namespacer implements IRTransformer { + private namespace: string + private namesToPreserve: Set + + constructor(namespace: string, namesToPreserve: Set) { + this.namespace = namespace + this.namesToPreserve = namesToPreserve + } + + exitDef(def: QuintDef): QuintDef { + // FIXME: The current flattener expects `namesToPreserve` to be ignored for def names. + // In the new flattener, we will need to consider it here as well. + // Also, considering it here makes the interface consistent. + // Uncomment the following line when the new flattener is in place: + // if (isFlat(def) && !this.namesToPreserve.has(def.name)) { + if (isFlat(def)) { + return { ...def, name: namespacedName(this.namespace, def.name) } + } + + return def + } + + exitLambda(expr: QuintLambda): QuintLambda { + return { + ...expr, + params: expr.params.map(p => ({ ...p, name: namespacedName(this.namespace, p.name) })), + } + } + + exitName(expr: QuintName): QuintName { + if (!this.namesToPreserve.has(expr.name)) { + return { ...expr, name: namespacedName(this.namespace, expr.name) } + } + + return expr + } + + exitApp(expr: QuintApp): QuintApp { + if (!this.namesToPreserve.has(expr.opcode)) { + return { ...expr, opcode: namespacedName(this.namespace, expr.opcode) } + } + + return expr + } + + exitConstType(type: QuintConstType): QuintConstType { + if (!this.namesToPreserve.has(type.name)) { + return { ...type, name: namespacedName(this.namespace, type.name) } + } + + return type + } +} + +function namespacedName(namespace: string | undefined, name: string): string { + return namespace ? `${namespace}::${name}` : name +} diff --git a/quint/src/quintIr.ts b/quint/src/ir/quintIr.ts similarity index 85% rename from quint/src/quintIr.ts rename to quint/src/ir/quintIr.ts index 0caa3e010..608c8e0a0 100644 --- a/quint/src/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/quintTypes.ts b/quint/src/ir/quintTypes.ts similarity index 100% rename from quint/src/quintTypes.ts rename to quint/src/ir/quintTypes.ts diff --git a/quint/src/itf.ts b/quint/src/itf.ts index bc1ea501d..95095f016 100644 --- a/quint/src/itf.ts +++ b/quint/src/itf.ts @@ -11,9 +11,9 @@ import { Either, left, merge, right } from '@sweet-monads/either' import { chunk } from 'lodash' -import { QuintApp, QuintStr } from './quintIr' +import { QuintApp, QuintStr } from './ir/quintIr' -import { QuintEx } from './quintIr' +import { QuintEx } from './ir/quintIr' /** The type of IFT traces. * See https://github.com/informalsystems/apalache/blob/main/docs/src/adr/015adr-trace.md */ diff --git a/quint/src/names/base.ts b/quint/src/names/base.ts index 553e5fdaf..104e8df20 100644 --- a/quint/src/names/base.ts +++ b/quint/src/names/base.ts @@ -12,7 +12,7 @@ * @module */ -import { QuintType } from '../quintTypes' +import { QuintType } from '../ir/quintTypes' /** * Possible kinds for definitions @@ -147,10 +147,6 @@ export const builtinNames = [ 'enabled', 'weakFair', 'strongFair', - 'guarantees', - 'existsConst', - 'forallConst', - 'chooseConst', 'Bool', 'Int', 'Nat', diff --git a/quint/src/names/collector.ts b/quint/src/names/collector.ts index bfaad7968..61e9f6506 100644 --- a/quint/src/names/collector.ts +++ b/quint/src/names/collector.ts @@ -12,7 +12,7 @@ * @module */ -import { IRVisitor } from '../IRVisitor' +import { IRVisitor } from '../ir/IRVisitor' import { QuintError } from '../quintError' import { QuintAssume, @@ -24,7 +24,7 @@ import { QuintOpDef, QuintTypeDef, QuintVar, -} from '../quintIr' +} from '../ir/quintIr' import { Definition, DefinitionsByModule, DefinitionsByName, LookupTable, builtinNames, copyNames } from './base' import { moduleNotFoundError, diff --git a/quint/src/names/importErrors.ts b/quint/src/names/importErrors.ts index bd764add0..fba3906c1 100644 --- a/quint/src/names/importErrors.ts +++ b/quint/src/names/importErrors.ts @@ -13,7 +13,7 @@ */ import { QuintError } from '../quintError' -import { QuintExport, QuintImport, QuintInstance, QuintLambdaParameter } from '../quintIr' +import { QuintExport, QuintImport, QuintInstance, QuintLambdaParameter } from '../ir/quintIr' export function selfReferenceError(def: QuintImport | QuintInstance | QuintExport): QuintError { const verb = def.kind === 'instance' ? 'instantiate' : def.kind diff --git a/quint/src/names/resolver.ts b/quint/src/names/resolver.ts index 630268d64..609c633cc 100644 --- a/quint/src/names/resolver.ts +++ b/quint/src/names/resolver.ts @@ -13,9 +13,9 @@ */ import { Either, left, right } from '@sweet-monads/either' -import { IRVisitor, walkModule } from '../IRVisitor' -import { QuintApp, QuintInstance, QuintLambda, QuintLet, QuintModule, QuintName, QuintOpDef } from '../quintIr' -import { QuintConstType } from '../quintTypes' +import { IRVisitor, walkModule } from '../ir/IRVisitor' +import { QuintApp, QuintInstance, QuintLambda, QuintLet, QuintModule, QuintName, QuintOpDef } from '../ir/quintIr' +import { QuintConstType } from '../ir/quintTypes' import { LookupTable, builtinNames } from './base' import { QuintError } from '../quintError' import { NameCollector } from './collector' diff --git a/quint/src/parsing/ToIrListener.ts b/quint/src/parsing/ToIrListener.ts index 6f5961714..0d1aaca9a 100644 --- a/quint/src/parsing/ToIrListener.ts +++ b/quint/src/parsing/ToIrListener.ts @@ -11,14 +11,14 @@ import { QuintModule, QuintName, QuintOpDef, -} from '../quintIr' -import { ConcreteFixedRow, QuintSumType, QuintType, Row, RowField, unitValue } from '../quintTypes' +} from '../ir/quintIr' +import { ConcreteFixedRow, QuintSumType, QuintType, Row, RowField, unitValue } from '../ir/quintTypes' import { strict as assert } from 'assert' import { ErrorMessage, Loc } from './quintParserFrontend' import { compact, zipWith } from 'lodash' import { Maybe, just, none } from '@sweet-monads/maybe' import { TerminalNode } from 'antlr4ts/tree/TerminalNode' -import { QuintTypeDef } from '../quintIr' +import { QuintTypeDef } from '../ir/quintIr' /** * An ANTLR4 listener that constructs QuintIr objects out of the abstract diff --git a/quint/src/parsing/quintParserFrontend.ts b/quint/src/parsing/quintParserFrontend.ts index 9c20f4295..3e4a7e554 100644 --- a/quint/src/parsing/quintParserFrontend.ts +++ b/quint/src/parsing/quintParserFrontend.ts @@ -17,7 +17,7 @@ import { QuintLexer } from '../generated/QuintLexer' import * as p from '../generated/QuintParser' import { QuintListener } from '../generated/QuintListener' -import { IrErrorMessage, QuintDef, QuintEx, QuintModule } from '../quintIr' +import { IrErrorMessage, QuintDef, QuintEx, QuintModule } from '../ir/quintIr' import { IdGenerator } from '../idGenerator' import { ToIrListener } from './ToIrListener' import { LookupTable } from '../names/base' @@ -25,7 +25,7 @@ import { resolveNames } from '../names/resolver' import { QuintError, quintErrorToString } from '../quintError' import { SourceLookupPath, SourceResolver, fileSourceResolver } from './sourceResolver' import { CallGraphVisitor, mkCallGraphContext } from '../static/callgraph' -import { walkModule } from '../IRVisitor' +import { walkModule } from '../ir/IRVisitor' import { toposort } from '../static/toposort' import { ErrorCode } from '../quintError' diff --git a/quint/src/quintAnalyzer.ts b/quint/src/quintAnalyzer.ts index a60ae572d..ab4770a7f 100644 --- a/quint/src/quintAnalyzer.ts +++ b/quint/src/quintAnalyzer.ts @@ -13,7 +13,7 @@ */ import { LookupTable } from './names/base' -import { OpQualifier, QuintDef, QuintModule } from './quintIr' +import { OpQualifier, QuintDef, QuintModule } from './ir/quintIr' import { TypeScheme } from './types/base' import { TypeInferrer } from './types/inferrer' import { EffectScheme } from './effects/base' diff --git a/quint/src/repl.ts b/quint/src/repl.ts index abebe457e..32551f790 100644 --- a/quint/src/repl.ts +++ b/quint/src/repl.ts @@ -17,7 +17,7 @@ import { Either, left, right } from '@sweet-monads/either' import chalk from 'chalk' import { format } from './prettierimp' -import { FlatDef, QuintEx, isFlat } from './quintIr' +import { FlatDef, QuintEx, isFlat } from './ir/quintIr' import { CompilationContext, CompilationState, @@ -39,7 +39,7 @@ import { version } from './version' import { fileSourceResolver } from './parsing/sourceResolver' import { cwd } from 'process' import { newIdGenerator } from './idGenerator' -import { moduleToString } from './IRprinting' +import { moduleToString } from './ir/IRprinting' import { EvaluationState, newEvaluationState } from './runtime/impl/compilerImpl' // tunable settings diff --git a/quint/src/runtime/compile.ts b/quint/src/runtime/compile.ts index 02816cfb8..7f5881fc1 100644 --- a/quint/src/runtime/compile.ts +++ b/quint/src/runtime/compile.ts @@ -18,9 +18,9 @@ import { } from '../parsing/quintParserFrontend' import { Computable, ComputableKind, kindName } from './runtime' import { ExecutionListener } from './trace' -import { FlatDef, FlatModule, IrErrorMessage, QuintDef, QuintEx, QuintModule } from '../quintIr' +import { FlatDef, FlatModule, IrErrorMessage, QuintDef, QuintEx, QuintModule } from '../ir/quintIr' import { CompilerVisitor, EvaluationState, newEvaluationState } from './impl/compilerImpl' -import { walkDefinition } from '../IRVisitor' +import { walkDefinition } from '../ir/IRVisitor' import { LookupTable } from '../names/base' import { AnalysisOutput, analyzeInc, analyzeModules } from '../quintAnalyzer' import { mkErrorMessage } from '../cliCommands' diff --git a/quint/src/runtime/impl/compilerImpl.ts b/quint/src/runtime/impl/compilerImpl.ts index a9a0cdaa2..320e0c825 100644 --- a/quint/src/runtime/impl/compilerImpl.ts +++ b/quint/src/runtime/impl/compilerImpl.ts @@ -14,7 +14,7 @@ import { Maybe, just, merge, none } from '@sweet-monads/maybe' import { List, OrderedMap, Set } from 'immutable' import { LookupTable } from '../../names/base' -import { IRVisitor } from '../../IRVisitor' +import { IRVisitor } from '../../ir/IRVisitor' import { TypeScheme } from '../../types/base' import { Callable, @@ -30,12 +30,13 @@ import { import { ExecutionListener } from '../trace' -import * as ir from '../../quintIr' +import * as ir from '../../ir/quintIr' 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/runtime/impl/runtimeValue.ts b/quint/src/runtime/impl/runtimeValue.ts index 5f47b45a1..4ee4eaf65 100644 --- a/quint/src/runtime/impl/runtimeValue.ts +++ b/quint/src/runtime/impl/runtimeValue.ts @@ -65,10 +65,10 @@ import { Maybe, just, merge, none } from '@sweet-monads/maybe' import { strict as assert } from 'assert' import { IdGenerator } from '../../idGenerator' -import { expressionToString } from '../../IRprinting' +import { expressionToString } from '../../ir/IRprinting' import { Callable, EvalResult } from '../runtime' -import { QuintEx } from '../../quintIr' +import { QuintEx } from '../../ir/quintIr' /** The default entry point of this module */ export default rv diff --git a/quint/src/runtime/runtime.ts b/quint/src/runtime/runtime.ts index 7343a99b3..d748225f3 100644 --- a/quint/src/runtime/runtime.ts +++ b/quint/src/runtime/runtime.ts @@ -16,7 +16,7 @@ import { Maybe, just, none } from '@sweet-monads/maybe' import { ValueObject } from 'immutable' -import { QuintEx } from '../quintIr' +import { QuintEx } from '../ir/quintIr' import { IdGenerator } from '../idGenerator' diff --git a/quint/src/runtime/testing.ts b/quint/src/runtime/testing.ts index c1108a29a..87cd695cd 100644 --- a/quint/src/runtime/testing.ts +++ b/quint/src/runtime/testing.ts @@ -12,7 +12,7 @@ import { Either, left, merge, right } from '@sweet-monads/either' import { just } from '@sweet-monads/maybe' import { ErrorMessage, fromIrErrorMessage } from '../parsing/quintParserFrontend' -import { QuintEx, QuintOpDef } from '../quintIr' +import { QuintEx, QuintOpDef } from '../ir/quintIr' import { CompilationContext, CompilationState, compile, lastTraceName } from './compile' import { zerog } from './../idGenerator' diff --git a/quint/src/runtime/trace.ts b/quint/src/runtime/trace.ts index f5bb0f86c..d8c8d871a 100644 --- a/quint/src/runtime/trace.ts +++ b/quint/src/runtime/trace.ts @@ -11,7 +11,7 @@ import { Maybe, just, none } from '@sweet-monads/maybe' import { strict as assert } from 'assert' -import { QuintApp } from '../quintIr' +import { QuintApp } from '../ir/quintIr' import { EvalResult } from './runtime' import { verbosity } from './../verbosity' import { Rng } from './../rng' diff --git a/quint/src/simulation.ts b/quint/src/simulation.ts index 595856f6f..4e7c0ac9b 100644 --- a/quint/src/simulation.ts +++ b/quint/src/simulation.ts @@ -12,7 +12,7 @@ import { Either } from '@sweet-monads/either' import { compileFromCode, contextNameLookup, lastTraceName } from './runtime/compile' import { ErrorMessage } from './parsing/quintParserFrontend' -import { QuintEx } from './quintIr' +import { QuintEx } from './ir/quintIr' import { Computable } from './runtime/runtime' import { ExecutionFrame, newTraceRecorder } from './runtime/trace' import { IdGenerator } from './idGenerator' diff --git a/quint/src/static/callgraph.ts b/quint/src/static/callgraph.ts index dec115a4e..7dd071dc0 100644 --- a/quint/src/static/callgraph.ts +++ b/quint/src/static/callgraph.ts @@ -12,10 +12,10 @@ import { Map, Record, Set } from 'immutable' import type { RecordOf } from 'immutable' -import { IRVisitor } from '../IRVisitor' +import { IRVisitor } from '../ir/IRVisitor' import { LookupTable } from '../names/base' -import { QuintApp, QuintDef, QuintExport, QuintImport, QuintInstance, QuintModule, QuintName } from '../quintIr' -import { QuintConstType } from '../quintTypes' +import { QuintApp, QuintDef, QuintExport, QuintImport, QuintInstance, QuintModule, QuintName } from '../ir/quintIr' +import { QuintConstType } from '../ir/quintTypes' /** * The call graph is simply a mapping from the caller's id diff --git a/quint/src/static/toposort.ts b/quint/src/static/toposort.ts index 924fb3b7a..10b8214b4 100644 --- a/quint/src/static/toposort.ts +++ b/quint/src/static/toposort.ts @@ -19,7 +19,7 @@ import { Either, left, right } from '@sweet-monads/either' import { Map } from 'immutable' import { Set } from 'immutable' -import { WithId } from '../quintIr' +import { WithId } from '../ir/quintIr' // the type of edges type Edges = Map> diff --git a/quint/src/types/aliasInliner.ts b/quint/src/types/aliasInliner.ts index f6bcadafc..7e635090e 100644 --- a/quint/src/types/aliasInliner.ts +++ b/quint/src/types/aliasInliner.ts @@ -13,11 +13,11 @@ * @module */ -import { IRTransformer, transformDefinition, transformModule, transformType } from '../IRTransformer' +import { IRTransformer, transformDefinition, transformModule, transformType } from '../ir/IRTransformer' import { LookupTable } from '../names/base' import { AnalysisOutput } from '../quintAnalyzer' -import { QuintDef, QuintModule } from '../quintIr' -import { QuintType } from '../quintTypes' +import { QuintDef, QuintModule } from '../ir/quintIr' +import { QuintType } from '../ir/quintTypes' /** * Inlines all type aliases in a set of QuintModules, LookupTable and AnalysisOutput. diff --git a/quint/src/types/base.ts b/quint/src/types/base.ts index 25192671c..0c6ebdba4 100644 --- a/quint/src/types/base.ts +++ b/quint/src/types/base.ts @@ -1,4 +1,4 @@ -import { QuintType } from '../quintTypes' +import { QuintType } from '../ir/quintTypes' /* * A type constraint can be either an equality of two types, a conjunction of diff --git a/quint/src/types/builtinSignatures.ts b/quint/src/types/builtinSignatures.ts index b771e83ca..69e83c3f7 100644 --- a/quint/src/types/builtinSignatures.ts +++ b/quint/src/types/builtinSignatures.ts @@ -13,9 +13,10 @@ */ import { parseTypeOrThrow } from './parser' -import { typeNames } from '../quintTypes' +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/constraintGenerator.ts b/quint/src/types/constraintGenerator.ts index d2786e6db..dde5ca78c 100644 --- a/quint/src/types/constraintGenerator.ts +++ b/quint/src/types/constraintGenerator.ts @@ -12,7 +12,7 @@ * @module */ -import { IRVisitor } from '../IRVisitor' +import { IRVisitor } from '../ir/IRVisitor' import { QuintApp, QuintAssume, @@ -29,9 +29,9 @@ import { QuintStr, QuintVar, isAnnotatedDef, -} from '../quintIr' -import { QuintType, typeNames } from '../quintTypes' -import { expressionToString, rowToString, typeToString } from '../IRprinting' +} from '../ir/quintIr' +import { QuintType, typeNames } from '../ir/quintTypes' +import { expressionToString, rowToString, typeToString } from '../ir/IRprinting' import { Either, left, mergeInMany, right } from '@sweet-monads/either' import { Error, ErrorTree, buildErrorLeaf, buildErrorTree, errorTreeToString } from '../errorTree' import { getSignatures } from './builtinSignatures' diff --git a/quint/src/types/constraintSolver.ts b/quint/src/types/constraintSolver.ts index 8a87df7a8..1fc340d04 100644 --- a/quint/src/types/constraintSolver.ts +++ b/quint/src/types/constraintSolver.ts @@ -14,8 +14,8 @@ import { Either, left, right } from '@sweet-monads/either' import { Error, ErrorTree, buildErrorLeaf, buildErrorTree } from '../errorTree' -import { rowToString, typeToString } from '../IRprinting' -import { QuintConstType, QuintType, Row, rowNames, typeNames } from '../quintTypes' +import { rowToString, typeToString } from '../ir/IRprinting' +import { QuintConstType, QuintType, Row, rowNames, typeNames } from '../ir/quintTypes' import { Constraint } from './base' import { Substitutions, applySubstitution, applySubstitutionToConstraint, compose } from './substitutions' import { unzip } from 'lodash' diff --git a/quint/src/types/inferrer.ts b/quint/src/types/inferrer.ts index 3e7ecd242..07f74acfb 100644 --- a/quint/src/types/inferrer.ts +++ b/quint/src/types/inferrer.ts @@ -14,9 +14,9 @@ */ import { ErrorTree } from '../errorTree' -import { walkDefinition } from '../IRVisitor' +import { walkDefinition } from '../ir/IRVisitor' import { LookupTable } from '../names/base' -import { QuintDef } from '../quintIr' +import { QuintDef } from '../ir/quintIr' import { TypeScheme } from './base' import { ConstraintGeneratorVisitor } from './constraintGenerator' import { solveConstraint } from './constraintSolver' diff --git a/quint/src/types/parser.ts b/quint/src/types/parser.ts index 694b619c6..3aa36eacc 100644 --- a/quint/src/types/parser.ts +++ b/quint/src/types/parser.ts @@ -18,7 +18,7 @@ import { QuintListener } from '../generated/QuintListener' import { ToIrListener } from '../parsing/ToIrListener' import { ParseTreeWalker } from 'antlr4ts/tree/ParseTreeWalker' import { CharStreams, CommonTokenStream } from 'antlr4ts' -import { QuintType, Row } from '../quintTypes' +import { QuintType, Row } from '../ir/quintTypes' import { newIdGenerator } from '../idGenerator' import { Either, left, right } from '@sweet-monads/either' diff --git a/quint/src/types/printing.ts b/quint/src/types/printing.ts index 6c2a800d0..2e0e430f2 100644 --- a/quint/src/types/printing.ts +++ b/quint/src/types/printing.ts @@ -1,5 +1,5 @@ -import { rowToString, typeToString } from '../IRprinting' -import { QuintType } from '../quintTypes' +import { rowToString, typeToString } from '../ir/IRprinting' +import { QuintType } from '../ir/quintTypes' import { Constraint, TypeScheme } from './base' import { Substitutions, applySubstitution, compose } from './substitutions' diff --git a/quint/src/types/specialConstraints.ts b/quint/src/types/specialConstraints.ts index 9699dc7b2..20598eb09 100644 --- a/quint/src/types/specialConstraints.ts +++ b/quint/src/types/specialConstraints.ts @@ -15,9 +15,9 @@ import { Either, left, mergeInMany, right } from '@sweet-monads/either' import { Error, buildErrorLeaf } from '../errorTree' -import { expressionToString } from '../IRprinting' -import { QuintEx } from '../quintIr' -import { QuintType, QuintVarType } from '../quintTypes' +import { expressionToString } from '../ir/IRprinting' +import { QuintEx } from '../ir/quintIr' +import { QuintType, QuintVarType } from '../ir/quintTypes' import { Constraint } from './base' import { chunk, times } from 'lodash' diff --git a/quint/src/types/substitutions.ts b/quint/src/types/substitutions.ts index 674c1efb8..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 '../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/quint/test/builders/ir.ts b/quint/test/builders/ir.ts index cd12325fb..90ff4bbf5 100644 --- a/quint/test/builders/ir.ts +++ b/quint/test/builders/ir.ts @@ -1,8 +1,8 @@ import { parsePhase1fromText } from '../../src/parsing/quintParserFrontend' import { IdGenerator, newIdGenerator } from '../../src/idGenerator' -import { QuintDef, QuintEx, QuintModule } from '../../src/quintIr' +import { QuintDef, QuintEx, QuintModule } from '../../src/ir/quintIr' import JSONbig from 'json-bigint' -import { QuintType } from '../../src/quintTypes' +import { QuintType } from '../../src/ir/quintTypes' export function buildModuleWithExpressions(expressions: string[]): QuintModule { return buildModule([], expressions) diff --git a/quint/test/effects/modeChecker.test.ts b/quint/test/effects/modeChecker.test.ts index 5273e532b..854ff44b8 100644 --- a/quint/test/effects/modeChecker.test.ts +++ b/quint/test/effects/modeChecker.test.ts @@ -1,6 +1,6 @@ import { describe, it } from 'mocha' import { assert } from 'chai' -import { OpQualifier } from '../../src/quintIr' +import { OpQualifier } from '../../src/ir/quintIr' import { EffectInferrer } from '../../src/effects/inferrer' import { ModeChecker } from '../../src/effects/modeChecker' import { QuintError, quintErrorToString } from '../../src/quintError' diff --git a/quint/test/flatenning.test.ts b/quint/test/flatenning.test.ts index b08a32c6e..7433e65fc 100644 --- a/quint/test/flatenning.test.ts +++ b/quint/test/flatenning.test.ts @@ -2,8 +2,7 @@ import { assert } from 'chai' import { describe, it } from 'mocha' import { addDefToFlatModule, flattenModules } from '../src/flattening' import { newIdGenerator } from '../src/idGenerator' -import { definitionToString } from '../src/IRprinting' -import { collectIds } from './util' +import { definitionToString } from '../src/ir/IRprinting' import { parse } from '../src/parsing/quintParserFrontend' import { FlatModule, analyzeModules } from '../src' import { SourceLookupPath } from '../src/parsing/sourceResolver' @@ -20,7 +19,6 @@ describe('flattenModules', () => { assert.fail('Failed to parse mocked up module') } const { modules, table, sourceMap } = parseResult.unwrap() - const [moduleA, _module] = modules const [analysisErrors, analysisOutput] = analyzeModules(table, modules) assert.isEmpty(analysisErrors) @@ -41,26 +39,6 @@ describe('flattenModules', () => { ) }) - it('does not repeat ids', () => { - const ids = collectIds(flattenedModule) - assert.notDeepInclude(collectIds(moduleA), ids) - assert.sameDeepMembers(ids, [...new Set(ids)]) - }) - - it('adds new entries to the source map', () => { - assert.includeDeepMembers( - [...sourceMap.keys()], - flattenedModule.defs.map(def => def.id) - ) - }) - - it('adds new entries to the types map', () => { - assert.includeDeepMembers( - [...flattenedAnalysis.types.keys()], - flattenedModule.defs.filter(def => def.kind !== 'typedef').map(def => def.id) - ) - }) - it('has no aliases in the types map', () => { assert.notIncludeMembers( [...flattenedAnalysis.types.values()].map(t => t.type.kind), @@ -205,7 +183,7 @@ describe('addDefToFlatModule', () => { assert.fail('Failed to parse mocked up module') } const { modules, table, sourceMap } = parseResult.unwrap() - const [moduleA, module] = modules + const [_moduleA, module] = modules const [analysisErrors, analysisOutput] = analyzeModules(table, modules) assert.isEmpty(analysisErrors) @@ -229,26 +207,6 @@ describe('addDefToFlatModule', () => { ) }) - it('does not repeat ids', () => { - const ids = collectIds(flattenedModule) - assert.notDeepInclude(collectIds(moduleA), ids) - assert.sameDeepMembers(ids, [...new Set(ids)]) - }) - - it('adds new entries to the source map', () => { - assert.includeDeepMembers( - [...sourceMap.keys()], - flattenedModule.defs.map(def => def.id) - ) - }) - - it('adds new entries to the types map', () => { - assert.includeDeepMembers( - [...flattenedAnalysis.types.keys()], - flattenedModule.defs.filter(def => def.kind !== 'typedef').map(def => def.id) - ) - }) - it('has no aliases in the types map', () => { assert.notIncludeMembers( [...flattenedAnalysis.types.values()].map(t => t.type.kind), diff --git a/quint/test/IRFinder.test.ts b/quint/test/ir/IRFinder.test.ts similarity index 96% rename from quint/test/IRFinder.test.ts rename to quint/test/ir/IRFinder.test.ts index 3c5f6ec15..0d6ed76af 100644 --- a/quint/test/IRFinder.test.ts +++ b/quint/test/ir/IRFinder.test.ts @@ -1,7 +1,7 @@ import { assert } from 'chai' import { describe, it } from 'mocha' -import { findDefinitionWithId, findExpressionWithId, findTypeWithId } from '../src/IRFinder' -import { buildModuleWithDefs, buildModuleWithExpressions } from './builders/ir' +import { findDefinitionWithId, findExpressionWithId, findTypeWithId } from '../../src/ir/IRFinder' +import { buildModuleWithDefs, buildModuleWithExpressions } from '../builders/ir' describe('findExpressionWithId', () => { const modules = [buildModuleWithExpressions(['Nat'])] diff --git a/quint/test/IRTransformer.test.ts b/quint/test/ir/IRTransformer.test.ts similarity index 90% rename from quint/test/IRTransformer.test.ts rename to quint/test/ir/IRTransformer.test.ts index 5d7a49dff..0fec005c1 100644 --- a/quint/test/IRTransformer.test.ts +++ b/quint/test/ir/IRTransformer.test.ts @@ -1,10 +1,10 @@ import { describe, it } from 'mocha' import { assert } from 'chai' -import { buildModuleWithDefs } from './builders/ir' -import { QuintDef, QuintEx, isFlat } from '../src/quintIr' -import { moduleToString } from '../src/IRprinting' -import { IRTransformer, transformModule } from '../src/IRTransformer' -import { ConcreteRow, QuintType } from '../src/quintTypes' +import { buildModuleWithDefs } from '../builders/ir' +import { QuintDef, QuintEx, isFlat } from '../../src/ir/quintIr' +import { moduleToString } from '../../src/ir/IRprinting' +import { IRTransformer, transformModule } from '../../src/ir/IRTransformer' +import { ConcreteRow, QuintType } from '../../src/ir/quintTypes' const quintModule = buildModuleWithDefs([ 'var a: int', diff --git a/quint/test/IRVisitor.test.ts b/quint/test/ir/IRVisitor.test.ts similarity index 98% rename from quint/test/IRVisitor.test.ts rename to quint/test/ir/IRVisitor.test.ts index 6ef9be8e4..b943cbd7b 100644 --- a/quint/test/IRVisitor.test.ts +++ b/quint/test/ir/IRVisitor.test.ts @@ -1,10 +1,10 @@ import { describe, it } from 'mocha' import { assert } from 'chai' -import { buildModuleWithDefs } from './builders/ir' -import { IRVisitor, walkModule } from '../src/IRVisitor' -import { QuintDef, QuintEx, QuintModule } from '../src/quintIr' -import { definitionToString, expressionToString, moduleToString, typeToString } from '../src/IRprinting' -import { QuintType } from '../src/quintTypes' +import { buildModuleWithDefs } from '../builders/ir' +import { IRVisitor, walkModule } from '../../src/ir/IRVisitor' +import { QuintDef, QuintEx, QuintModule } from '../../src/ir/quintIr' +import { definitionToString, expressionToString, moduleToString, typeToString } from '../../src/ir/IRprinting' +import { QuintType } from '../../src/ir/quintTypes' describe('walkModule', () => { const quintModule = buildModuleWithDefs([ diff --git a/quint/test/IRprinting.test.ts b/quint/test/ir/IRprinting.test.ts similarity index 97% rename from quint/test/IRprinting.test.ts rename to quint/test/ir/IRprinting.test.ts index 4013ad7e9..37ef529cd 100644 --- a/quint/test/IRprinting.test.ts +++ b/quint/test/ir/IRprinting.test.ts @@ -1,9 +1,9 @@ import { describe, it } from 'mocha' import { assert } from 'chai' -import { buildDef, buildExpression, buildModuleWithDefs, buildType } from './builders/ir' -import { definitionToString, expressionToString, moduleToString, typeToString } from '../src/IRprinting' -import { toScheme } from '../src/types/base' -import { QuintSumType, unitValue } from '../src' +import { buildDef, buildExpression, buildModuleWithDefs, buildType } from '../builders/ir' +import { definitionToString, expressionToString, moduleToString, typeToString } from '../../src/ir/IRprinting' +import { toScheme } from '../../src/types/base' +import { QuintSumType, unitValue } from '../../src' describe('moduleToString', () => { const quintModule = buildModuleWithDefs(['var S: Set[int]', 'val f = S.filter(x => x + 1)']) diff --git a/quint/test/ir/idRefresher.test.ts b/quint/test/ir/idRefresher.test.ts new file mode 100644 index 000000000..23cc09c18 --- /dev/null +++ b/quint/test/ir/idRefresher.test.ts @@ -0,0 +1,68 @@ +import { describe, it } from 'mocha' +import { assert } from 'chai' +import { newIdGenerator } from '../../src/idGenerator' +import { generateFreshIds } from '../../src/ir/idRefresher' +import { SourceLookupPath } from '../../src/parsing/sourceResolver' +import { parse } from '../../src/parsing/quintParserFrontend' +import { analyzeModules } from '../../src/quintAnalyzer' +import { collectIds } from '../util' + +describe('generateFreshIds', () => { + // Generate ids starting from 100, so that we can easily distinguish them from + // the ids generated in the parser + const mockGenerator = newIdGenerator(100n) + + const defs = [ + 'var a: int', + 'const N: int', + 'type MY_TYPE = int', + 'assume _ = N > 1', + 'val f = Set(1, 2).filter(x => x > 1)', + 'def l = val x = false { x }', + ] + + const idGenerator = newIdGenerator() + const fake_path: SourceLookupPath = { normalizedPath: 'fake_path', toSourceName: () => 'fake_path' } + + const quintModules: string = `module A { ${defs.join('\n')} }` + + const parseResult = parse(idGenerator, 'fake_location', fake_path, quintModules) + if (parseResult.isLeft()) { + it('should parse the mocked up module', () => { + assert.fail(`Failed to parse mocked up module. Errors: ${parseResult.value.map(e => e.explanation).join('\n')}`) + }) + } + const { modules, table, sourceMap } = parseResult.unwrap() + const [module] = modules + + const [analysisErrors, analysisOutput] = analyzeModules(table, modules) + it('should analyze the mocked up module', () => { + assert.isEmpty(analysisErrors) + }) + + const result = module.defs.map(def => generateFreshIds(def, mockGenerator, sourceMap, analysisOutput)) + const newModule = { ...module, defs: result, id: 200n } + + it('does not repeat ids', () => { + const ids = collectIds(newModule) + assert.isTrue( + ids.every(id => id >= 100n), + 'ids should be greater than 100 if they were generated by the mock generator' + ) + assert.sameDeepMembers(ids, [...new Set(ids)]) + }) + + it('adds new entries to the source map', () => { + assert.includeDeepMembers( + [...sourceMap.keys()], + newModule.defs.map(def => def.id) + ) + }) + + it('adds new entries to the types map', () => { + assert.includeDeepMembers( + [...analysisOutput.types.keys()], + newModule.defs.filter(def => def.kind !== 'typedef').map(def => def.id) + ) + }) +}) diff --git a/quint/test/ir/namespacer.test.ts b/quint/test/ir/namespacer.test.ts new file mode 100644 index 000000000..e0736ca7d --- /dev/null +++ b/quint/test/ir/namespacer.test.ts @@ -0,0 +1,48 @@ +import { describe, it } from 'mocha' +import { assert } from 'chai' +import { buildDef } from '../builders/ir' +import { definitionToString } from '../../src/ir/IRprinting' +import { addNamespaceToDefinition } from '../../src/ir/namespacer' +import { builtinNames } from '../../src/names/base' + +describe('addNamespaceToDefinition', () => { + it('adds namespace to variables', () => { + const def = buildDef('var x: int') + + const result = addNamespaceToDefinition(def, 'M', new Set()) + + assert.deepEqual(definitionToString(result), 'var M::x: int') + }) + + it('adds namespace to constants and type aliases', () => { + const def = buildDef('const N: MY_TYPE') + + const result = addNamespaceToDefinition(def, 'M', new Set()) + + assert.deepEqual(definitionToString(result), 'const M::N: M::MY_TYPE') + }) + + it('adds namespace to type defs', () => { + const def = buildDef('type MY_TYPE = int') + + const result = addNamespaceToDefinition(def, 'M', new Set()) + + assert.deepEqual(definitionToString(result), 'type M::MY_TYPE = int') + }) + + it('adds namespace to operators, ignoring builtins', () => { + const def = buildDef('val a = pure val b = Set(1, 2) { b.map(x => x) }') + + const result = addNamespaceToDefinition(def, 'M', new Set(builtinNames)) + + assert.deepEqual(definitionToString(result), 'val M::a = pure val M::b = Set(1, 2) { map(M::b, ((M::x) => M::x)) }') + }) + + it('keeps imports as is', () => { + const def = buildDef('import A.*') + + const result = addNamespaceToDefinition(def, 'M', new Set()) + + assert.deepEqual(definitionToString(result), 'import A.*') + }) +}) diff --git a/quint/test/quintTypes.test.ts b/quint/test/ir/quintTypes.test.ts similarity index 88% rename from quint/test/quintTypes.test.ts rename to quint/test/ir/quintTypes.test.ts index 29f876f63..1df799947 100644 --- a/quint/test/quintTypes.test.ts +++ b/quint/test/ir/quintTypes.test.ts @@ -1,7 +1,7 @@ import { describe, it } from 'mocha' import { assert } from 'chai' -import { typeNames } from '../src/quintTypes' -import { parseType, parseTypeOrThrow } from '../src/types/parser' +import { typeNames } from '../../src/ir/quintTypes' +import { parseType, parseTypeOrThrow } from '../../src/types/parser' describe('typeNames', () => { it('find names in types', () => { diff --git a/quint/test/names/collector.test.ts b/quint/test/names/collector.test.ts index 15ed88029..9bae37496 100644 --- a/quint/test/names/collector.test.ts +++ b/quint/test/names/collector.test.ts @@ -3,7 +3,7 @@ import { assert } from 'chai' import { buildModuleWithDefs } from '../builders/ir' import { QuintError, QuintModule } from '../../src' import { NameCollector } from '../../src/names/collector' -import { walkModule } from '../../src/IRVisitor' +import { walkModule } from '../../src/ir/IRVisitor' import { DefinitionsByName } from '../../src/names/base' import { zerog } from '../../src/idGenerator' diff --git a/quint/test/runtime/compile.test.ts b/quint/test/runtime/compile.test.ts index 98f67b12d..8c0f52046 100644 --- a/quint/test/runtime/compile.test.ts +++ b/quint/test/runtime/compile.test.ts @@ -2,7 +2,7 @@ import { describe, it } from 'mocha' import { assert } from 'chai' import { Either, left, right } from '@sweet-monads/either' import { just } from '@sweet-monads/maybe' -import { expressionToString } from '../../src/IRprinting' +import { expressionToString } from '../../src/ir/IRprinting' import { Computable, ComputableKind, fail, kindName } from '../../src/runtime/runtime' import { noExecutionListener } from '../../src/runtime/trace' import { diff --git a/quint/test/runtime/trace.test.ts b/quint/test/runtime/trace.test.ts index 85ae1f373..7c9f34c66 100644 --- a/quint/test/runtime/trace.test.ts +++ b/quint/test/runtime/trace.test.ts @@ -3,7 +3,7 @@ import { assert } from 'chai' import { none } from '@sweet-monads/maybe' import { newTraceRecorder } from '../../src/runtime/trace' -import { QuintApp } from '../../src/quintIr' +import { QuintApp } from '../../src/ir/quintIr' import { verbosity } from '../../src/verbosity' import { newRng } from '../../src/rng' diff --git a/quint/test/static/callgraph.test.ts b/quint/test/static/callgraph.test.ts index 882a548ab..63a497d02 100644 --- a/quint/test/static/callgraph.test.ts +++ b/quint/test/static/callgraph.test.ts @@ -11,7 +11,7 @@ import { import { SourceLookupPath, fileSourceResolver } from '../../src/parsing/sourceResolver' import { LookupTable, QuintDef, QuintExport, QuintImport, QuintInstance, QuintModule } from '../../src' import { CallGraphVisitor, mkCallGraphContext } from '../../src/static/callgraph' -import { walkModule } from '../../src/IRVisitor' +import { walkModule } from '../../src/ir/IRVisitor' describe('compute call graph', () => { // Parse Quint code without, stopping after name resolution diff --git a/quint/test/types/aliasInliner.test.ts b/quint/test/types/aliasInliner.test.ts index 9713b6f14..988ff6cfd 100644 --- a/quint/test/types/aliasInliner.test.ts +++ b/quint/test/types/aliasInliner.test.ts @@ -4,9 +4,9 @@ import { SourceLookupPath } from '../../src/parsing/sourceResolver' import { parse } from '../../src/parsing/quintParserFrontend' import { dedent } from '../textUtils' import { inlineTypeAliases } from '../../src/types/aliasInliner' -import { QuintModule } from '../../src/quintIr' +import { QuintModule } from '../../src/ir/quintIr' import { LookupTable } from '../../src/names/base' -import { moduleToString } from '../../src/IRprinting' +import { moduleToString } from '../../src/ir/IRprinting' import { AnalysisOutput, analyzeModules } from '../../src/quintAnalyzer' function inlineModule(text: string): { modules: QuintModule[]; table: LookupTable; analysisOutput: AnalysisOutput } { diff --git a/quint/test/types/constraintGenerator.test.ts b/quint/test/types/constraintGenerator.test.ts index 62be3c0ce..80b6db3fc 100644 --- a/quint/test/types/constraintGenerator.test.ts +++ b/quint/test/types/constraintGenerator.test.ts @@ -3,7 +3,7 @@ import { assert } from 'chai' import { Constraint } from '../../src/types/base' import { ConstraintGeneratorVisitor, SolvingFunctionType } from '../../src/types/constraintGenerator' import { left, right } from '@sweet-monads/either' -import { walkModule } from '../../src/IRVisitor' +import { walkModule } from '../../src/ir/IRVisitor' import { constraintToString } from '../../src/types/printing' import { ErrorTree } from '../../src/errorTree' import { LookupTable } from '../../src/names/base' diff --git a/quint/test/types/constraintSolver.test.ts b/quint/test/types/constraintSolver.test.ts index 9b16aaaa7..125f5918a 100644 --- a/quint/test/types/constraintSolver.test.ts +++ b/quint/test/types/constraintSolver.test.ts @@ -5,7 +5,7 @@ import { parseRowOrThrow, parseTypeOrThrow } from '../../src/types/parser' import { Constraint } from '../../src/types/base' import { substitutionsToString } from '../../src/types/printing' import { Substitutions } from '../../src/types/substitutions' -import { Row } from '../../src/quintTypes' +import { Row } from '../../src/ir/quintTypes' import { errorTreeToString } from '../../src/errorTree' import { LookupTable } from '../../src/names/base' diff --git a/quint/test/util.ts b/quint/test/util.ts index f136563b5..959df0df6 100644 --- a/quint/test/util.ts +++ b/quint/test/util.ts @@ -1,5 +1,5 @@ import { assert } from 'chai' -import { IRVisitor, walkModule } from '../src/IRVisitor' +import { IRVisitor, walkModule } from '../src/ir/IRVisitor' import { QuintBool, QuintDef, @@ -10,8 +10,8 @@ import { QuintModule, QuintStr, QuintTypeDef, -} from '../src/quintIr' -import { QuintType } from '../src/quintTypes' +} from '../src/ir/quintIr' +import { QuintType } from '../src/ir/quintTypes' import lodash from 'lodash' import { ParserPhase3, parse } from '../src/parsing/quintParserFrontend' import { SourceLookupPath } from '../src/parsing/sourceResolver' 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"