refactor: rewrite TerminationHint elaborators #2958
Conversation
In order to familiarize myself with this code, and so that the next person has an easier time, I * added docstrings explaining what I found out these things to * rewrote the syntax expansion functions using syntax pattern matches, to the extend possible
| match terminationHint with | ||
| | `(terminationByCore|termination_by' $hint1:terminationHint1) | ||
| | `(decreasingBy|decreasing_by $hint1:terminationHint1) => | ||
| return TerminationHint.one { ref, value := hint1.raw[0] } | ||
| | `(terminationByCore|termination_by' $hints:terminationHintMany) | ||
| | `(decreasingBy|decreasing_by $hints:terminationHintMany) => do | ||
| let m ← hints.raw[0].getArgs.foldlM (init := {}) fun m arg => | ||
| let declName? := cliques.findSome? fun clique => clique.findSome? fun declName => | ||
| if arg[0].getId.isSuffixOf declName then some declName else none | ||
| match declName? with | ||
| | none => Macro.throwErrorAt arg[0] s!"function '{arg[0].getId}' not found in current declaration" | ||
| | some declName => return m.insert declName { ref := arg, value := arg[2] } | ||
| for clique in cliques do | ||
| let mut found? := Option.none | ||
| for declName in clique do | ||
| if let some { ref, .. } := m.find? declName then | ||
| if let some found := found? then | ||
| Macro.throwErrorAt ref s!"invalid termination hint element, '{declName}' and '{found}' are in the same clique" | ||
| found? := some declName | ||
| return TerminationHint.many m | ||
| | _ => Macro.throwUnsupported |
There was a problem hiding this comment.
Here I wasn’t able to use more syntax matches. Is that because terminationHint1 and terminationHintMany are parametric parsers, so the syntax match elaboration doesn’t work? Or was I just not trying the right things?
There was a problem hiding this comment.
Yes, parametric parsers cannot be used as quotation parsers but you can still match through them:
`(terminationByCore| termination_by' $e:term)
Now, for the Many case something like
`(terminationByCore| termination_by' $[$ids:ident => $es $[;]?]*)
should work but I believe the lookahead is preventing that as it's not happy to see the $ instead of an actual identifier :/
There was a problem hiding this comment.
I never figured out complex syntax like that, with nested parsers. Thanks for the example!
Wrapping patternIgnore around the lookahead won’t help, I assume.
There was a problem hiding this comment.
It won't, no. I suppose the lookahead can be called a workaround for tactics not currently being (contextual) keywords, which we want to fix. But also your "per-declaration termination_by" would fix it as well I assume as there would be no more need for Many?
There was a problem hiding this comment.
Yes, was about to say that; no need to dwell on this too much.
Happy with the rest of this PR?
nomeata
added
the
needs-update-stage0
github-actions
bot
added
the
toolchain-available
leanprover-community-mathlib4-bot
added
the
builds-mathlib
|
In order to familiarize myself with this code, and so that the next
person has an easier time, I
to the extend possible