feat: add cbv_eval attribute#12296
Conversation
github-actions
bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
|
Reference manual CI status:
|
wkrozowski
changed the title
cbv_eval attributecbv_eval attribute
This PR adds a default `Inhabited` instance to `Theorem` type. The need to do so came up in #12296 , as `Theorem` is one of the entries of the structure which is the key entry of `SimpleScopedEnvExtension`.
| structure CbvEvalEntry where | ||
| target : Name | ||
| thm : Theorem | ||
| deriving BEq, Inhabited |
There was a problem hiding this comment.
I know this PR is a draft, so I am not sure much attention to polish I should give, but here are some comments necessary. In particular what is target? Is it always the head symbol of the LHS of the theorem? If so, is it worth keeping it as a separate field?
(Generally reviewing is easier if there are already comments)
There was a problem hiding this comment.
Yes, target is the extracted head symbol from LHS of the theorem.
There was a problem hiding this comment.
I see your point. We could move the logic and do this when adding a Theorem object to the state of the extension, by inferring the type of an expression and extracting the name of the appFn on the LHS.
There was a problem hiding this comment.
Actually no, we want the name of appFn of the LHS of the theorem to be the key of the NameMap stored in the expression, so the name of it should be known at the moment of calling add on the extension (which is pure, and hence we cannot compute it inside of add)
| throwError "Invalid `cbv` theorem" | ||
| let fnName ← forallTelescope type fun _ body => do | ||
| let some (_, lhs, _) := body.eq? | throwError "Equality expected" | ||
| unless lhs.isApp do throwError "Application expected" |
There was a problem hiding this comment.
Do you really want to forbid cbv_eval on constants (nullary applications)? Maybe you can just drop this line; .getAppFn can still be used.
There was a problem hiding this comment.
Thanks, will do! I will also need to handle this case in Cbv.Main (so if I hit a constant that has an associated equation, we try to use it)
| initial := {} | ||
| addEntry := CbvEvalState.addEntry | ||
| exportEntry? := fun level entry => do | ||
| guard (level == .private || !isPrivateName entry.target) |
There was a problem hiding this comment.
I know the tests on the module system are still pending. Things to watch out: What if the target is public, but one of the arguments is private? What if the target is public but the theorem is private? (Maybe only look at whether the theorem itself is private)?
There was a problem hiding this comment.
Are there similar tests for simp annotations that could be an inspiration for me?
| let hasTheorems := (← getCbvEvalLemmas fnName).isSome | ||
| if hasTheorems then | ||
| let res ← (simpAppArgs >> tryCbvTheorems) e | ||
| match res with | ||
| | .rfl false => return .rfl (done := true) | ||
| | _ => return res | ||
| else | ||
| return .rfl (← isCbvOpaque fnName) |
There was a problem hiding this comment.
Do you even want to support theorem when `isOpaque = false?
There was a problem hiding this comment.
Yes! Imagine that we have a function that we have an optimisation for one set of inputs, but for the other ones, we would like to follow the standard path that involves using the associated equations/unfold equation.
3 participants
This (WIP) PR adds
cbv_evalattribute that allows to evaluate functions incbvtactic using pre-registered theorems.