Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: finding terms of a certain type in a `expr`


view this post on Zulip Eric Wieser (Feb 28 2021 at 17:59):

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.

view this post on Zulip Alex J. Best (Feb 28 2021 at 18:06):

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

view this post on Zulip Eric Wieser (Feb 28 2021 at 18:07):

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

view this post on Zulip Yakov Pechersky (Feb 28 2021 at 18:07):

Would infer_type help here?

view this post on Zulip Eric Wieser (Feb 28 2021 at 18:16):

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

view this post on Zulip Yakov Pechersky (Feb 28 2021 at 18:48):

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

view this post on Zulip Eric Wieser (Feb 28 2021 at 18:54):

Does docs#expr.get_free_var_range reveal anything?

view this post on Zulip Yakov Pechersky (Feb 28 2021 at 18:57):

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

view this post on Zulip Floris van Doorn (Mar 02 2021 at 17:17):

Are you just looking for docs#expr.contains_constant?

view this post on Zulip Floris van Doorn (Mar 02 2021 at 17:18):

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

view this post on Zulip Eric Wieser (Mar 02 2021 at 17:22):

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

view this post on Zulip Floris van Doorn (Mar 03 2021 at 18:56):

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.

view this post on Zulip Floris van Doorn (Mar 03 2021 at 18:57):

Except maybe some macros...


Last updated: May 09 2021 at 23:10 UTC