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

remove tuples from the pool of potential auto triggers #1199

Open
wants to merge 1 commit into
base: main
Choose a base branch
from

Conversation

JoPolzin
Copy link

Ideally Closes #695 , which fixed itself in the meantime, but raised the problem that tuples are chosen as auto-triggers, as they are handled as functions internally.

Checking if a typeconstructor is a Tuple-constructor and discarding it from the set of possible triggers resolves this.

@JoPolzin
Copy link
Author

This is the new output for the issue #695 :)

error: Could not automatically infer triggers for this quantifer.  Use #[trigger] annotations to manually mark trigger terms instead.
 --> tuple.rs:6:12
  |
6 |   requires forall |x| f.requires((x,))
  |            ^^^^^^^^^^^^^^^^^^^^^^^^^^^

error: aborting due to 1 previous error

@JoPolzin
Copy link
Author

@utaal @Chris-Hawblitzel can you take a look at the failing tests? It looks like requires and ensures clauses for closures depend on triggering on tuples. Does that change anything?

@Chris-Hawblitzel Chris-Hawblitzel self-requested a review July 3, 2024 21:28
@utaal
Copy link
Collaborator

utaal commented Jul 4, 2024

It does change things. I don't yet know in what way exactly. Perhaps we can allow them just for closures.

@Chris-Hawblitzel are you already looking into it? (I saw you self-assigned as reviewer)

@Chris-Hawblitzel
Copy link
Collaborator

@Chris-Hawblitzel are you already looking into it? (I saw you self-assigned as reviewer)

I haven't actually started. I'm happy to work on it, but feel free to take it if you want.

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.

Imprecise trigger report for requires clause
3 participants