Lean4
/-- `unifyMovements` takes as input
* an array of `Expr × Bool × Syntax`, as in the output of `parseArrows`,
* the `Name` `op` of a binary operation,
* an `Expr`ession `tgt`.
It unifies each `Expr`ession appearing as a first factor of the array with the atoms
for the operation `op` in the expression `tgt`, returning
* the lists of pairs of a matched subexpression with the corresponding `Bool`ean;
* a pair of a list of error messages and the corresponding list of Syntax terms where the error
should be thrown;
* an array of debugging messages.
-/
def unifyMovements (data : Array (Expr × Bool × Syntax)) (tgt : Expr) :
MetaM (List (Expr × Bool) × (List MessageData × List Syntax) × Array MessageData) := do
let ops ← getOps op tgt
let atoms :=
(ops.map Prod.fst).flatten.toList.filter
(!isBVar ·)
-- `instr` are the unified user-provided terms, `neverMatched` are non-unified ones
let (instr, neverMatched) ← pairUp data.toList atoms
let dbgMsg :=
#[m!"Matching of input variables:\n\
* pre-match: {(data.map (Prod.snd ∘ Prod.snd))}\n\
* post-match: {instr}",
m! "\nMaximum number of iterations: {ops.size}"]
-- if there are `neverMatched` terms, return the parsed terms and the syntax
let errMsg := neverMatched.map fun (t, a, stx) => (if a then m! "← {t}" else m! "{t}", stx)
return (instr, errMsg.unzip, dbgMsg)
