Stream: metaprogramming / tactics

Topic: Introspecting a definition in a tactic

Yakov Pechersky (Feb 18 2021 at 08:11):

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 (Feb 18 2021 at 08:58):

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 (Feb 18 2021 at 09:02):

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 (Feb 18 2021 at 09:12):

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 (Feb 18 2021 at 09:21): 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 (Feb 18 2021 at 09:23):

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


Yakov Pechersky (Feb 18 2021 at 09:26):

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 (Feb 18 2021 at 09:35): 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 (Feb 18 2021 at 09:37): I'm not seeing the connection to the derive handler but I guess I'm just missing the context Rob Lewis (Feb 18 2021 at 09:38): What is the derive handler supposed to be looking for in the expr? Yakov Pechersky (Feb 18 2021 at 09:39): 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 (Feb 18 2021 at 09:41): That's not really true, see e.g. docs#tactic.delta_instance_handler Rob Lewis (Feb 18 2021 at 09:41): 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 (Feb 18 2021 at 09:41):

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 (Feb 18 2021 at 09:42):

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

Yakov Pechersky (Feb 18 2021 at 09:48):

In fact, it seems to work even with

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


Rob Lewis (Feb 18 2021 at 09:50):

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

Rob Lewis (Feb 18 2021 at 09:51):

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

Rob Lewis (Feb 18 2021 at 09:51):

Because it has higher priority

Yakov Pechersky (Feb 18 2021 at 09:53):

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

Yakov Pechersky (Feb 18 2021 at 09:53):

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

Yakov Pechersky (Feb 18 2021 at 09:53):

That is quite awesome.

Rob Lewis (Feb 18 2021 at 09:57):

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 (Feb 18 2021 at 09:59):

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

Last updated: May 09 2021 at 22:13 UTC