New instances syntax #739
New instances syntax #739
Conversation
| @@ -283,23 +283,23 @@ quint run --init=Init --step=Next --seed=abcde --max-steps=4 \ | |||
| An example execution: | |||
| --------------------------------------------- | |||
| action step0 = all { | |||
| counters::n' = 1, | |||
| n' = 1, | |||
There was a problem hiding this comment.
This works because we only need to evaluate the main module now that it is self-contained by flattening. WDYT @konnov ? Is there something I'm missing here or is this great? 😅
There was a problem hiding this comment.
Perhaps this ended up being a solution to #731 ?
There was a problem hiding this comment.
Yes, these traces look much better now! I was also annoyed by counters::.
| @@ -8,7 +8,7 @@ false | |||
| true | |||
| -40 | |||
| 104 | |||
| runtime error: error: Variable kettle::temperature is not set | |||
| runtime error: error: Variable temperature is not set | |||
There was a problem hiding this comment.
I changed this and the markdown by hand because setting up a go env to build lmt didn't fit my schedule for this week 😝. I hope it doesn't break automatic generation.
| const lastId = modules.map(m => m.id).sort((a, b) => Number(a - b))[modules.length - 1] | ||
| const idGenerator = newIdGenerator(lastId) |
There was a problem hiding this comment.
I am worried about this computation. This looks fragile to me. If other code is using a global id generator (which we kind of have in CLI commands), this local id generator will go ahead and produce conflicting ids. This will be very hard to debug in the future. Can we pass an id generator as a parameter?
There was a problem hiding this comment.
Hm, I think that if other code is using a "global" id generator, than other code is wrong 😅. Atm, we only use id generators on parsePhase1 and here. If we use it somewhere else, I think we should do some check similar to this one, to make sure that it is initialized in a valid state. Otherwise, we might as well have an actual global state as you suggested the first time, which has all the problems we already mentioned.
There was a problem hiding this comment.
The simulator converts runtime values back to QuintEx. That's where it can introduces new identifiers, which would clash with the identifiers here.
There was a problem hiding this comment.
But the ids generated in toQuintEx are not used for anything, right? If we did use them, we should find a way to get the original ids back somehow (by storing them in the runtime value, for example). The current ids used there won't have a source map entry nor a lookup table entry for them, so anything would most likely break if we tried to use them.
If there's no real problem in the clashing right now, I'd like to merge this and take a look at this generator problem again. I don't think simulating a global state is a good solution here.
| switchModule(moduleId: bigint, moduleName: string) { | ||
| this.currentModule = { id: moduleId, name: moduleName } | ||
| } | ||
|
|
There was a problem hiding this comment.
This is so good that we don't have to worry about multiple modules now!
| const tableA = collectDefinitions(moduleA) | ||
| const lookupTableA = resolveNames(moduleA, tableA, treeFromModule(moduleA)).unwrap() | ||
|
|
||
| const module = buildModuleWithDefs(defs, undefined, idGenerator) | ||
| const module = result.value.modules[1] |
There was a problem hiding this comment.
not sure, why there is moduleA and module? Can we rename module to moduleB?
There was a problem hiding this comment.
module is like a main module here, and moduleA is the module called A imported by module. I'll add some comments.
Hello
This introduces our new syntax for instances, introduced in ADR 6, which closes #724. In order to use that syntax in a nice way, I needed to combine it with imports (see the Tendermint example), so I also implemented flattening for modules, which closes #11.
With flattened modules, the main module is now self contained and we only need to evaluate that single module in the REPL. So I have removed some support for multiple modules in the compiler, which makes variable names easier to read. But that broke error reporting since source maps for flattened modules were still not consistent. So, I also fixed the source map problem, which closes #730.
npm run format(or had formatting run automatically on all files edited)CHANGELOG.mdfor any new functionalityREADME.mdupdated for any listed functionality