filtering an expr list for matches

Stream: metaprogramming / tactics

[Robert Maxton]

So, just getting my toes wet with meta here...

Let's say I have a list of expressions, and I would like to partition them into a sublist that matches a given pattern and a sublist that does not. What's the easiest way to do this? There's docs#tactic.match_expr but a) that's a tactic and b) there's a weird argument I don't understand (what exactly does it mean a function takes an argument that's already defined, anyway?); there's also docs#expr.match_app (for example) but it also takes a fixed argument, in this case elab.

[Robert Maxton]

which I don't know how to provide

[Kevin Buzzard]

The := in the function input is a default value:

def add (n : ℕ) (m : ℕ := 2) : ℕ := n + m

#eval add 5 -- 7
#eval add 5 3 -- 8

[Alex J. Best]

Can you give a bit more detail about what sort of thing you want to match, or even some code with blanks to be filled in?

[Damiano Testa]

This may not be the most efficient code, but, given what I imagine that you want to do with the smul application, it might be useful.

import tactic.core

namespace tactic

/-- Sort a list of `expr`s into two lists: one consisting of expressions that begin with an `expr.app` and one consisting of the rest. -/
meta def select_apps : list expr → list expr × list expr
| [] := ([], [])
| (e@(expr.app _ _) :: as) := let (l, r) := select_apps as in  -- the `e@` assigns the name `e` to the matched expression, so you can use it later.
  (e :: l, r)
| (e :: as) := let (l, r) := select_apps as in
  (l, e :: r)

example : 5 + 4 = 0 ∧ (let k : ℕ := 1 in 3 * k = 3) ∧ ite (4 = 5) 7 8 = 0 ∧ (∀ n : ℕ, n = 0) :=
by do  -- <--- put the cursor here to see the result of the `trace`s
  `(%%e1 ∧ %%e2 ∧ %%e3 ∧ %%e4) ← target,
  let (apps, napps) := select_apps [e1, e2, e3, e4],
  trace "* applications:",
  trace apps,
  trace "\n* non applications:",
  trace napps

end tactic

I think that this code contains most of the tricks that I constantly use when meta-programming.

[Robert Maxton]

Alex J. Best said:

Can you give a bit more detail about what sort of thing you want to match, or even some code with blanks to be filled in?

Well, I'd like to be able to match any pattern, really; but specifically I want to find things of the form ( _ • r) for a constant r

[Robert Maxton]

Damiano Testa said:

This may not be the most efficient code, but, given what I imagine that you want to do with the smul application, it might be useful.
(snip)
I think that this code contains most of the tricks that I constantly use when meta-programming.

Yeah, I was wondering if I would have to just write my own inductive destructor. Thanks!

[Robert Maxton]

Chasing both approaches at once, can anyone guess what's going wrong here?

meta def tactic.interactive.multiset_smul_collect : conv unit :=
  do {
    (_, lhs, rhs) ← tactic.target_lhs_rhs,
    match expr.to_list (λ e, some e) lhs with
    | some (hd :: tl) :=
          do {
            `(%%a • %%r) ← return hd,
            tactic.trace (list.filter_map (``(_ • %%r)).match_app tl )
          }
    | _ := tactic.trace "oops"
    end
    },
    return

It's not intended to really do anything yet (other than trace), but there's an error under list.filter_map complaining about a type mismatch:

type mismatch at application
  list.filter_map (``(λ (_x_1 : _), has_scalar.smul _ _x_1).subst (to_pexpr r)).match_app
term
  (``(λ (_x_1 : _), has_scalar.smul _ _x_1).subst (to_pexpr r)).match_app
has type
  option (expr ff × expr ff) : Type
but is expected to have type
  ?m_1 → option ?m_2 : Type (max ? ?)

[Robert Maxton]

which I don't know what to make of

[Robert Maxton]

Oh, wait, dammit I got my wires crossed and thought I was working with the generic match-a-pattern functionality from tactics. Nevermind lol

[Damiano Testa]

If I understood correctly, this might be useful:

import tactic.core
import algebra.group.defs

namespace expr

--  this function appears in `move_add`
meta def list_summands : expr → list expr
| `(%%a + %%b) := a.list_summands ++ b.list_summands
| a            := [a]

--  similar to function `candidates` in `move_add`
meta def list_smuls : expr → list (expr × expr)
| `(%%a • %%r)   := prod.mk <$> a.list_summands <*> r.list_summands
| (lam _ _ e f)  := e.list_smuls ++ f.list_smuls
| (pi  _ _ e f)  := e.list_smuls ++ f.list_smuls
| (mvar  _ _ e)  := e.list_smuls
| (app e f)      := e.list_smuls ++ f.list_smuls
| (elet _ e f g) := e.list_smuls ++ f.list_smuls ++ g.list_smuls
| e              := []

end expr

variables {R M : Type*} [has_add R] [has_mul R] [has_add M] [has_scalar R M]
  (a b c d e f : R) (p q r s t : M)

example : ∀ x : ℕ,  let k := d • t in -- `∀` adds useless noise, the `let` contributes below
  (a + b * c) • p + (c + (d + e) * f) • (q + r) = (a + (b + c) + d + (e + f)) • s + t :=
by do  --  note that the isolated `t` on the rhs does not appear in the list :(
  t ← tactic.target,
  tactic.trace t.list_smuls

[Robert Maxton]

Damiano Testa said:

If I understood correctly, this might be useful:
snip

hmm, this does look useful
thanks, I was actually just about to ask about a related issue
let's see if this pattern works