Introspecting a definition in a tactic

Stream: metaprogramming / tactics

[Yakov Pechersky]

How does introspection of a defn work? Let's say I wanted to write a meta def that told me whether I used (+) in a definition's body. How would that work?

import data.nat.basic

def f (n : ℕ) : ℕ := n + n

open tactic

meta def uses_addition (f : ℕ → ℕ) : bool := sorry

[Mario Carneiro]

The easiest way is to use environment.get_decl or the shorthand tactic.get_decl to obtain the declaration from the environment, and then use declaration.value to get the expression corresponding to the def

[Mario Carneiro]

import data.nat.basic

def f (n : ℕ) : ℕ := n + n
def g (n : ℕ) : ℕ := 2 * n

open tactic

meta def uses_addition (n : name) : tactic bool :=
do d ← get_decl n,
  pure $ expr.fold d.value ff $ λ e _ b, b || e.is_constant_of ``has_add.add

#eval uses_addition `f >>= trace -- tt
#eval uses_addition `g >>= trace -- ff

[Rob Lewis]

Slightly golfed, since that second line is common enough to be a library function.

meta def uses_addition (n : name) : tactic bool :=
do d ← get_decl n, pure $ d.value.contains_constant (= ``has_add.add)

[Yakov Pechersky]

What I'm really trying to do is write something like a derive handler, but for parser properties. Right now, the only property is parser.mono, and I've defined a parser.numeral. So instead of me introspecting the definition I wrote manually:

variables (α : Type) [has_zero α] [has_one α] [has_add α]

def numeral : parser α :=
nat.bin_cast <$> nat

instance : mono (numeral α) := mono.map

I want to make a tactic that will do that introspection for me.

[Yakov Pechersky]

Right now, I'm trying to figure out how to generate ex nihilo the mvars for (α : Type) [has_zero α] [has_one α] [has_add α] after starting with something like:

example : true := by do
  let n : name := ``numeral,
  f ← resolve_name n >>= to_expr,
  tgt ← mk_app ``parser.mono [f], -- this breaks because it is `numeral` and not `numeral α`
  triv

[Rob Lewis]

What are your imports/open namespaces?

[Yakov Pechersky]

import data.fintype.card
import data.buffer.parser.basic

open parser parse_result

namespace parser

variables (α : Type) [has_zero α] [has_one α] [has_add α]

/--
Parse a string of digits as a numeral while casting it to target type `α`.
-/
def numeral : parser α :=
nat.bin_cast <$> nat

instance : mono (numeral α) := mono.map

namespace tactic

open tactic

set_option trace.app_builder true

example : true := by do
  let n : name := ``numeral,
  f ← resolve_name n >>= to_expr,
  trace f.is_constant,
  triv

end tactic

end parser

[Rob Lewis]

I'm still not completely sure what you're trying to do. To get the parameters to the type of numeral (as local consts) you can do something like this

example : true := by do
  let n : name := ``numeral,
  f ← resolve_name n >>= to_expr,
  (args, body) ← infer_type f >>= open_pis,
  trace args, trace body,
  trace f.is_constant,
  triv

[Rob Lewis]

I'm not seeing the connection to the derive handler but I guess I'm just missing the context

[Rob Lewis]

What is the derive handler supposed to be looking for in the expr?

[Yakov Pechersky]

The derive handler is only able to make instances for inductive types. In my case, numeral : parser α, so writing a derive handler won't work.

[Rob Lewis]

That's not really true, see e.g. docs#tactic.delta_instance_handler

[Rob Lewis]

import data.fintype.card
import data.buffer.parser.basic

open parser parse_result


@[derive_handler]
meta def mono_derive : derive_handler :=
instance_derive_handler `parser.mono `[apply mono.map]

namespace parser

variables (α : Type) [has_zero α] [has_one α] [has_add α]

/--
Parse a string of digits as a numeral while casting it to target type `α`.
-/
@[derive mono] def numeral : parser α :=
nat.bin_cast <$> nat

#check numeral.mono

[Yakov Pechersky]

The pseudo code would be:

create a goal of `mono (numeral α)`
get the definition body for the parser, likely written in functor/seq/bind notation or do notation,
map notation symbol to corresponding `mono.{map,seq,bind}` instance that already exists
try to prove the goal using something like `convert mono.bind`.
deal with the new goals that might appear

[Yakov Pechersky]

How does that pass guard (env.is_inductive n) in the body of meta def instance_derive_handler??

[Yakov Pechersky]

In fact, it seems to work even with

@[derive_handler]
meta def mono_derive : derive_handler :=
instance_derive_handler `parser.mono `[trivial]

[Rob Lewis]

Heh, you're right, that derive handler isn't doing anything :upside_down:

[Rob Lewis]

docs#tactic.delta_instance_handler is succeeding before it tries the new one

[Rob Lewis]

Because it has higher priority

[Yakov Pechersky]

I have to say, I'm quite impressed with how easily that worked, it seems

[Yakov Pechersky]

Ah, so that delta_instance_handler is just the very generalized version of what I was trying to do

[Yakov Pechersky]

That is quite awesome.

[Rob Lewis]

More or less. If def d := t ..., delta_instance creates an instance of C d if it can infer an instance C (t ...) (taking into account arguments to d). So if that's enough for you, great

[Yakov Pechersky]

That makes my life much easier, and lets me easily bring #5463 into very neat order