add hoist_ifs_in_goal
#1315
add hoist_ifs_in_goal
#1315
Conversation
There was a problem hiding this comment.
I'm not a fan of the InternalTacticEvidence construct. The idea behind Evidence is that they represent the trusted proof steps we are willing to accept, and thus should have some pretty strong scrutiny applied when adding new ones. We can't evaluate InternalTacticEvidence because callers could put whatever transformation they want there.
I'd much rather see a dedicated HoistIfsEvidence.
nano-o
force-pushed
the
hoist_ifs
branch
2 times, most recently
from
7c6333e to
5ecaf75
Compare
| case asEqTrue body of | ||
| Just t -> pure t | ||
| Nothing -> fail "hoistIfsInGoal: expected EqTrue" | ||
| ecs <- traverse (\(nm, ty) -> scFreshEC sc nm ty) args |
There was a problem hiding this comment.
We should really check to make sure that there aren't dependencies among these types, otherwise we will have dangling variables. Either that, or we should handle it properly by substituting into the types of later variables as well.
There was a problem hiding this comment.
Looks like we use this same pattern elsewhere. Let's not hold up this PR for this, but it's definitely something that should get fixed.
There was a problem hiding this comment.
Looks like doing this properly is over my head for now. I presume this is not critical at the moment since you approved the changes. Is that right?
There was a problem hiding this comment.
Yeah, I don't think we need to fix this right now. CF #1316
| @@ -343,6 +359,8 @@ data Evidence | |||
| -- evidence is use to check the modified goal. | |||
| | EvalEvidence (Set VarIndex) Evidence | |||
|
|
|||
There was a problem hiding this comment.
This could use a comment.
nano-o
added
PR: ready to merge
We may put a custom one in place later
nano-o
added
the
PR: ready to merge
No description provided.