get the "visible" head of an expression

Stream: general

[Scott Morrison]

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.

[Scott Morrison]

Does that make sense? Do we already have it?

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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.

[Scott Morrison]

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.

[Mario Carneiro]

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

[Scott Morrison]

Thanks!