Lean4
/-- Matcher for expressions produced by `foldl`. -/
partial def matchFoldl (lit x y : Name) (smatcher : Matcher) (sinit : Matcher) : Matcher := fun s => do
s.withVar lit do
let expr ← getExpr
let s := { s with vars := s.vars |>.erase x |>.erase y }
let some s ←
try
some <$> smatcher s
catch _ =>
pure none |
-- We put this here rather than using a big try block to prevent backtracking.
-- We have `smatcher` match greedily, and then require that `sinit` *must* succeed
sinit s
let s :=
s.pushFold lit
(← s.delabVar y expr)
-- x gives the next lit
let some newLit := s.vars[x]? |
failure
if newLit.1.expr == expr then
failure
let s := { s with vars := s.vars.insert lit newLit }
matchFoldl lit x y smatcher sinit s
