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.

Sign up for GitHub

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

Jump to bottom

[auto-reverse] apply reversible selection #71

Draft
wants to merge 3 commits into
base: master
Choose a base branch
from
Draft

[auto-reverse] apply reversible selection #71

wants to merge 3 commits into from

Conversation

olaure01
Copy link
Collaborator

Fixes #64

@olaure01 olaure01 added the enhancement Enhancement to an existing feature label Apr 26, 2021
etiennecallies
etiennecallies requested changes Apr 28, 2021
View reviewed changes
Copy link
Collaborator

@etiennecallies etiennecallies left a comment

Choose a reason for hiding this comment

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

There is an infinite loop :( Because this is a recursive function.

Ex: ?A -> A,?A -> A,A,?A -> A,A,A,?A -> ... -> A,...,A,?A

It's very different spirit form previous auto-reverse rules :

  • the other rules only apply one rule
  • the other rules simplify the sequent, whether this one makes it longer.

Perhaps we should rethink it.

@olaure01
Copy link
Collaborator Author

Absolutely!
It is meaningless to apply twice the reversible selection rule in a given asynchronous phase.
I will correct it.

@etiennecallies
Copy link
Collaborator

etiennecallies commented Apr 29, 2021 •
edited
Loading

See video on #64 : we should prevent selection if it has been already applied.

@olaure01
Copy link
Collaborator Author

Selection is not applied anymore if sub-formula already present.
I see 3 possible directions:

  • do not use reversible selection at all
  • use it as done here: iterated action of the user on the auto-reverse button could repeat applying selection, but it is not so unnatural since it is on request of the user
  • [my favorite] add a sub-option to auto-reverse mode for incorporating selection or not (can rely on auto_reverse_selection Boolean in auto_reverse_sequent.ml)

@olaure01 olaure01 added the wontfix This will not be worked on label May 7, 2021
@olaure01 olaure01 marked this pull request as draft May 9, 2021 21:18
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@etiennecallies etiennecallies etiennecallies requested changes

Assignees
No one assigned
Labels
enhancement Enhancement to an existing feature wontfix This will not be worked on
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Auto-reverse selection rule in atomic context
2 participants
@olaure01 @etiennecallies