finding terms of a certain type in a `expr`

Stream: metaprogramming / tactics

[Eric Wieser]

How can I write a function that detects if a (fully-elaborated) expr contains a certain type? For example, I want contains_nat `(1 + 1 > 0) to give tt, but contains_nat `(tt) to give ff.

[Alex J. Best]

I think we have docs#expr.contains for this. If you wanted to write it you would fold over the expr, oops I'm on mobile and that link doesn't work sorry

[Eric Wieser]

Even without folding, I can't find the API to ask for the elaborated type of an expression

[Yakov Pechersky]

Would infer_type help here?

[Eric Wieser]

That's certainly what I was looking for, although it seems not to be enough:

private meta def decidable_exact (d : declaration) : tactic (option string) :=
do (binders, body) ← open_pis d.type,
  body.mfold none $ λ e depth so_far, do
    t ← infer_type e,
    if t.is_app_of `decidable_eq
     ∨ t.is_app_of `decidable_pred ∨ t.is_app_of `decidable_rel
     ∨ t.is_app_of `decidable then do
      trace t
    else skip,
    pure (some ("ok"))

lemma bad {α : Type*} [inhabited α] [decidable_eq α] (x : α × α) :
  0 = if x = default _ then 0 else 0 :=
sorry

run_cmd do
  d ← get_decl `bad,
  x ← decidable_exact d,
  trace x

gives

tactic 'infer_type' failed, given expression should not contain de-Bruijn variables, they should be replaced with local constants before using this tactic

[Yakov Pechersky]

How about this?

private meta def decidable_exact (d : declaration) : tactic (option string) :=
do (binders, body) ← open_pis d.type,
  body.mfold none $ λ e depth so_far, do
    if (e.get_free_var_range = 0) then (do
      t ← infer_type e,
      if t.is_app_of `decidable_eq
          ∨ t.is_app_of `decidable_pred ∨ t.is_app_of `decidable_rel
          ∨ t.is_app_of `decidable then do
        trace t
      else skip)
    else skip,
    pure (some ("ok"))

lemma bad {α : Type*} [inhabited α] [decidable_eq α] (x : α × α) :
  0 = if x = default _ then 0 else 0 :=
sorry

run_cmd do
  d ← get_decl `bad,
  x ← decidable_exact d,
  trace x

[Eric Wieser]

Does docs#expr.get_free_var_range reveal anything?

[Yakov Pechersky]

I'm just using is to filter out the expressions where the de Brujin var is behind a lambda

[Floris van Doorn]

Are you just looking for docs#expr.contains_constant?

[Floris van Doorn]

You cannot use infer_type in an expr.mfold, since the subexpressions are not well-typed (they could contain free de Bruijn variables).

[Eric Wieser]

contains_constant wouldn't return true for contains_constant `(f x y) {`nat} right? even if x has type nat?

[Floris van Doorn]

If f has type nat -> ... then no. However, for something like `(1 + 1 > 0) you would get true, since has_lt is applied to nat.

One solution is to mfold over the expression:

• If you see nat it contains nat
• If you reach a local constant, use infer_type on it (which is safe, since it's a local constant) to see whether its type contains nat
• If you reach a constant, use docs#environment.get and docs#declaration.type to see whether its type contains nat.

This should cover all cases.

[Floris van Doorn]

Except maybe some macros...