Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

updated files to support new tuple representation #1519

Open
wants to merge 16 commits into
base: main
Choose a base branch
from

Conversation

MahtabNorouzi
Copy link
Collaborator

Updated the tuple structure across the codebase from { kind: 'app', opcode: 'Tup', args: [...] } to { kind: 'tuple', elements: [...] }. This refactor improves clarity and consistency in tuple handling and removes support for the previous Tup syntax. All affected files and references have been modified accordingly.

Comment on lines +66 to +86
exitTuple(tup: QuintTup): QuintTup {
// Process each element of the tuple
const namespacedElements = tup.elements.map(element => {
// If the element is a name, apply the namespace
if (element.kind === 'name' && typeof element.name === 'string') {
return {
...element,
name: namespacedName(this.namespace, element.name), // Apply the namespace
}
}
// Otherwise, return the element as-is
return element
})

// Return a new tuple with namespaced elements
return {
...tup,
elements: namespacedElements,
}
}

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We actually don't need this! The IR transformer itself should already guarantee that we visited/transformed all of the elements before reaching the tuple. This works as it is right now because namespacedName is idempotent (it can be applied more than once and the result will be the same as if it was applied once, that is, f(x) = f(f(x))), but it will also work as if we remove this, and we should 😄

Suggested change
exitTuple(tup: QuintTup): QuintTup {
// Process each element of the tuple
const namespacedElements = tup.elements.map(element => {
// If the element is a name, apply the namespace
if (element.kind === 'name' && typeof element.name === 'string') {
return {
...element,
name: namespacedName(this.namespace, element.name), // Apply the namespace
}
}
// Otherwise, return the element as-is
return element
})
// Return a new tuple with namespaced elements
return {
...tup,
elements: namespacedElements,
}
}

quint/src/ir/quintIr.ts Outdated Show resolved Hide resolved
quint/src/runtime/impl/runtimeValue.ts Outdated Show resolved Hide resolved
@@ -166,6 +167,33 @@ export class ConstraintGeneratorVisitor implements IRVisitor {
this.addToResults(e.id, right(toScheme({ kind: e.kind })))
}

exitTuple(e: QuintTup) {
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

As we did with the effects inferrer, I think we can also generalize something here so we don't have to repeat this code between exitTuple and exitApp. This will also repeat with the other structures (lists, maps, records, etc), so we can try to generalize when adding the next one.

quint/testFixture/SuperSpec.qnt Outdated Show resolved Hide resolved
quint/testFixture/SuperSpec.qnt Outdated Show resolved Hide resolved
quint/src/ir/IRTransformer.ts Outdated Show resolved Hide resolved
quint/src/effects/builtinSignatures.ts Outdated Show resolved Hide resolved
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants