Ids for lambda parameters #689
Conversation
| @@ -147,7 +147,7 @@ module erc20 { | |||
| balanceOf' = balanceOf, | |||
| val failed = or { | |||
| tx.value < 0, | |||
| tx.sender > tx.spender, | |||
| tx.sender == tx.spender, | |||
There was a problem hiding this comment.
This is a fix for a type error that was not flagged by the type checker before, but is now. The reason why this PR change impacted this is not quite clear to me yet. However, @konnov reported a similar bug this morning which is not solved by this, so I'll further investigate this behavior when looking at that.
| @@ -91,24 +91,6 @@ export class EffectInferrer implements IRVisitor { | |||
| } | |||
|
|
|||
| switch (def.kind) { | |||
| case 'param': { | |||
There was a problem hiding this comment.
No need for this special treatment/workaround anymore now that lambdas have their own IDs.
| // an identifier or a hole '_' | ||
| identOrHole : '_' | IDENTIFIER | ||
| ; | ||
|
|
||
| parameter: identOrHole; |
There was a problem hiding this comment.
This is not completely necessary, but makes the code in ToIRListener more consistent, and I think it makes some sense to differentiate parameters from simple identifiers at the grammar level: parameters will later become a QuintLambdaParameter, while identOrHole is just used as a string.
There was a problem hiding this comment.
Good call I think this makes great sense!
| @@ -23,7 +23,16 @@ describe('inferEffects', () => { | |||
|
|
|||
| const inferrer = new EffectInferrer(definitionsTable) | |||
| return inferrer.inferEffects(quintModule) | |||
| } | |||
|
|
|||
| function effectForDef(quintModule: QuintModule, effects: Map<bigint, EffectScheme>, defName: string ) { | |||
There was a problem hiding this comment.
Dealing with IDs was getting to hard, so I wrote this helper function instead.
| .map(_ => assert.fail('Expected errors')) | ||
| }) | ||
|
|
||
| it('find unresolved names inside lambdas', () => { |
There was a problem hiding this comment.
This test was duplicated somehow, so I removed one copy of it.
|
@shonfeder This breaks compatibility with the Apalache translation, as we anticipated 😞. How can we handle the broken tests? Since we don't have backwards compatibility in neither side, it might be tricky to release a new Apalache version with this change that will break every other PR tests except for this. Perhaps this should be a non-required CI check? |
|
I'll start working on a fix and maybe we can discuss our testing and compatibility strategies in the meeting today? |
| export interface QuintLambdaParameter extends WithId { | ||
| /** The name of the formal parameter */ | ||
| name: string, | ||
| } | ||
|
|
||
| export interface QuintLambda extends WithId { | ||
| /** Expressions kind ('lambda' -- operator abstraction) */ | ||
| kind: 'lambda', | ||
| /** Identifiers for the formal parameters */ | ||
| params: string[], | ||
| /** The formal parameters */ | ||
| params: QuintLambdaParameter[], |
There was a problem hiding this comment.
Why not use QuintName for the params?
There was a problem hiding this comment.
To be clear, i expect there is a good reason, but i'm curious what it is :)
There was a problem hiding this comment.
Why not use
QuintNamefor theparams?
That's an option indeed. Normally we are using QuintName to refer to something that has been defined before. QuintLambdaParameter defines a name.
There was a problem hiding this comment.
Yep, so it would be tricky since, in many times we analyze a NameEx, we look for something already defined, which isn't the case here (i.e. the type inferrer, when visiting a NameEx, will use the lookup table to obtain the original definition and get the type for that)
The apalache side fix corresponding to informalsystems/quint#689
* Update QuintIR for new parameter representation The apalache side fix corresponding to informalsystems/quint#689 * update changelog
| // an identifier or a hole '_' | ||
| identOrHole : '_' | IDENTIFIER | ||
| ; | ||
|
|
||
| parameter: identOrHole; |
There was a problem hiding this comment.
Good call I think this makes great sense!
Hello
Big diff because of tests and generated (antlr) code.
This PR introduces ids for lambda parameters, which unblocks several issues and allows us to report errors and provide information more precisely.
Closes #624
npm run format(or had formatting run automatically on all files edited)CHANGELOG.mdfor any new functionalityREADME.mdupdated for any listed functionality