Zulip Chat Archive

Stream: general

Topic: get the "visible" head of an expression


view this post on Zulip Scott Morrison (Mar 11 2021 at 23:19):

I would like a function that takes an expr, and returns to me the "head", including implicit arguments.

Thus @rfl X should stay as @rfl X, nat.factorial 7 should produce nat.factorial, and 3 + 7 should produce @has_add.add nat nat.has_add.

view this post on Zulip Scott Morrison (Mar 11 2021 at 23:19):

Does that make sense? Do we already have it?

view this post on Zulip Scott Morrison (Mar 11 2021 at 23:20):

There is expr.get_app_fn, which gets the very topmost head of the app. (But this turns @rfl X into just @rfl, etc.)

view this post on Zulip Scott Morrison (Mar 11 2021 at 23:25):

I guess if it existed it would be in src/meta/expr.lean, and there doesn't seem to be anything like this.

view this post on Zulip Scott Morrison (Mar 11 2021 at 23:30):

I had hoped that I could achieve this using pattern matching, e.g. something like

match e with
| `(%%f %%x) := return f
| _ := sorry
end

but this just gives me a function expected at error on the %%f.

view this post on Zulip Scott Morrison (Mar 12 2021 at 00:28):

meta def app_implicits : expr  list expr  tactic expr
| f [] := return f
| f (x :: xs) := do
  ty  infer_type f,
  match binding_info ty with
  | binder_info.default := return f
  | _ := app_implicits (f x) xs
  end

meta def get_app_fn_with_implicits (e : expr) : tactic expr :=
do
  let (f, args) := e.get_app_fn_args,
  app_implicits f args

seems to do it.

view this post on Zulip Mario Carneiro (Mar 12 2021 at 02:38):

Here's a version that avoids multiple calls to infer_type:

import tactic.core
open tactic expr

meta def app_implicits : expr  list expr  expr  expr
| f (x :: xs) (pi _ binder_info.default _ ty) := f
| f (x :: xs) (pi _ _ _ ty) := app_implicits (f x) xs ty
| f _ _ := f

meta def get_app_fn_with_implicits (e : expr) : tactic expr :=
let (f, args) := e.get_app_fn_args in
app_implicits f args <$> infer_type f

view this post on Zulip Scott Morrison (Mar 12 2021 at 10:47):

Thanks!


Last updated: May 13 2021 at 21:12 UTC