search

epfl-lara / lisa

Proof assistant based on first-order logic and set theory
Apache License 2.0
33 stars 18 forks source link

Safe tactic calls for `Restate` #118

Closed sankalpgambhir closed 1 year ago

sankalpgambhir commented 1 year ago

Added unwrapTactic calls to Restate, as before this it had raw calls to kernel tactics, which subsequently raised kernel errors whenever it failed.

Also added RewriteTrue as a BasicStepTactic, since it didn't exist before, and was required for this.

sankalpgambhir commented 1 year ago

I did run scalaFix T_T

sankalpgambhir commented 1 year ago

Anyhow, making this a draft while I add some tests for the modified tactics as well.

sankalpgambhir commented 1 year ago

That took less time than I expected

SimonGuilloud commented 1 year ago

Ah! I think the confusion comes from having both a Restate and a Rewrite tactic, when they do the same thing. Restate take into account both Rewrite and RewriteTrue, depending on the number of parameters, but does not catch error. Can you maybe merge the three tactic (Restate, Rewrite, RewriteTrue) into a single one with the two adequate apply functions?

sankalpgambhir commented 1 year ago

Ah! I think the confusion comes from having both a Restate and a Rewrite tactic, when they do the same thing. Restate take into account both Rewrite and RewriteTrue, depending on the number of parameters, but does not catch error. Can you maybe merge the three tactic (Restate, Rewrite, RewriteTrue) into a single one with the two adequate apply functions?

The new Restate does exactly that. Would you like to remove the basic tactics Rewrite and RewriteTrue? There is some merit in keeping them separately, but not too much, I guess.

Some of the other tactics call Rewrite internally, that will change, that's all.

sankalpgambhir commented 1 year ago

Funny how and when issues manifest themselves #119

SimonGuilloud commented 1 year ago

Yeah, I think keeping all three is confusing and a waste of space since they do the exact same thing. Moreover Rewrite should be renamed Restate anyway

sankalpgambhir commented 1 year ago

Provided the build passes soon, we should merge this for now. Since Restate does not work in certain scenarios, we cannot remove the base versions for now. This PR makes using Restate safer in the meanwhile, and adds more tests.

SimonGuilloud commented 1 year ago

Ok let's merge that for now and I'll deal with the issue soon.