match expression with unification

Stream: metaprogramming / tactics

[Miroslav Olšák]

Is there a way to pattern match on an expression with definition unfolding (like tactic.unify does)? For example, how to make the following function get_first_summand working also in the other cases?

meta def get_first_summand (e : expr) : tactic expr
:=
do
  -- tactic.unify `(nat.add 2 5) e, -- tactic.unify would work but there is no space for variables
  `(nat.add %%a %%_) ← return e,
  return a

-- succeeds with 2
run_cmd tactic.trace (get_first_summand `(nat.add 2 5))

def new_func (n : ℕ) : ℕ := (nat.add n 5)

-- fails
run_cmd tactic.trace (get_first_summand `(new_func 2))
run_cmd tactic.trace (get_first_summand `(2 + 5))

I don't want to just add more cases for new_func or has_add.add because function new_func could be defined after the tactic.

[Jannis Limperg]

You'll have to use whnf or dsimp to reduce the expression to head-normal form, then match on it. There is unfortunately no way to directly match 'up to conversion'. You'll also have to decide what transparency to use; this controls which constants get unfolded during the whnf reduction.

[Jannis Limperg]

(Actually, you could unify with a term containing metavariables, then read those. But that's probably more expensive.)

[Miroslav Olšák]

I do not need too much efficiency in this case, how do I construct an expression with metavariables?

[Jannis Limperg]

I guess there's no quotation for mvars, so you'll have to build it manually. Something like this (untested):

summand1 <- mk_mvar nat,
summand2 <- mk_mvar nat,
let pattern := `(nat.add %summand1 %summand2),
unify e pattern,
summand1 <- instantiate_mvars summand1,
pure summand1

I should stress this is highly unidiomatic; I just had this idea. YMMV.

[Miroslav Olšák]

thanks, I will play with it, maybe whnf will suffice (but I don't want to expand what could be expanded in the match, so I will have to play with reducibility a bit)

[Miroslav Olšák]

For completeness, this is a working code with metavariables.

meta def get_first_summand (e : expr) : tactic expr
:=
do
  summand1 <- tactic.mk_mvar,
  summand2 <- tactic.mk_mvar,
  let pattern := `(nat.add %%summand1 %%summand2),
  tactic.unify e pattern,
  summand1 <- tactic.instantiate_mvars summand1,
  return summand1