Add ProofMode.SynthInstance #108
Conversation
| -/ | ||
| import Iris.ProofMode.Goals | ||
|
|
||
| /- TODO: How to call these functions? ProofMode.synthInstance, ipmSynthInstance, synthIPMInstance, synthInstanceIPM? -/ |
There was a problem hiding this comment.
Are there any opinions how should this new synthInstance should be called? Some ideas are:
- ProofMode.synthInstance (current)
- ipmSynthInstance
- synthIPMInstance
- synthInstanceIPM
There was a problem hiding this comment.
I think this doesn't matter too much
Add a custom version of synthInstance for the proof mode that can create and instantiate mvars. It is implemented as a simple backtracking search, reusing the standard instance infrastructure. This version of synthInstance should be used for the IPM proof mode classes, marked with the attribute ipm_class. Also some other small refactorings: - Allow iexists to take multiple arguments - Fix handling of created goals in iexists - Use the Goals structure more consistently - Add some more error messages - Generalize AsEmpValid over the direction similar to the Rocq version
MackieLoeffel
force-pushed
the
msammler/ipm_synth_instance
branch
from
0a055eb to
0fc0868
Compare
This commit adds [InOut] that is used to dynamically determine whether a type class parameter is an input or an output. This is important for classes that are used with multiple modings, e.g., IntoWand. Instances can match on the InOut parameter to avoid accidentially instantiating outputs if matching on an input was intended.
Backtracking can be selectively enabled for specific instanes with ipm_backtrack
|
Cool! Looks really good. I tidied some of the proofmode names, and I added a top-level Would you also be able to (briefly) document the differences |
| -- TODO: change this to replace main goal that deduplicates goals | ||
| def Goals.getGoals {prop : Q(Type u)} {bi : Q(BI $prop)} (g : Goals bi) : MetaM (List MVarId) := do | ||
| let goals ← g.goals.get | ||
| -- put the goals that depend on other goals last |
There was a problem hiding this comment.
Not proposing we change this, but does this matter?
| foApprox := true, ctxApprox := true, constApprox := false, univApprox := false }) do | ||
| withInTypeClassResolution do | ||
| let type ← instantiateMVars type | ||
| -- TODO: Should we run whnf under the ∀ quantifiers of type? |
There was a problem hiding this comment.
Is it possible to create a test for this?
| let type ← instantiateMVars type | ||
| -- TODO: Should we run whnf under the ∀ quantifiers of type? | ||
| -- let type ← preprocess type | ||
| -- TODO: should we create mvars for outParams? |
There was a problem hiding this comment.
I believe that for normal outParams there should be no need, but there may be edge cases with instances that have checkSynthOrder disabled.
| for inst in instances.reverse do | ||
| let mctx0 ← getMCtx | ||
| let (res, match?) ← withTraceNode `Meta.synthInstance | ||
| (λ r => withMCtx mctx0 do return MessageData.withMCtx mctx0 m!"{exceptOptionEmoji (r.map (·.1))} apply {inst.val} to {← instantiateMVars (← inferType mvar)}") do |
There was a problem hiding this comment.
It's not clear to me why mctx0 is used instead of mctx. In the case that backtracking is enabled and the previous iteration fails, mctx0 is the polluted context from the failed resolution.
3 participants
Based on #107
Add a custom version of synthInstance for the proof mode that can create and instantiate mvars. It is implemented as a simple backtracking search, reusing the standard instance infrastructure. This version of synthInstance should be used for the IPM proof mode classes, marked with the attribute ipm_class. This search only backtracks on instances marked with
ipm_backtrack.Also some other small refactorings: