Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: Introspecting a definition in a tactic


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Rob Lewis (Feb 18 2021 at 09:24):

What are your imports/open namespaces?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Rob Lewis (Feb 18 2021 at 09:38):

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

view this post on Zulip 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.

view this post on Zulip Rob Lewis (Feb 18 2021 at 09:41):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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??

view this post on Zulip 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]

view this post on Zulip Rob Lewis (Feb 18 2021 at 09:50):

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

view this post on Zulip Rob Lewis (Feb 18 2021 at 09:51):

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

view this post on Zulip Rob Lewis (Feb 18 2021 at 09:51):

Because it has higher priority

view this post on Zulip Yakov Pechersky (Feb 18 2021 at 09:53):

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

view this post on Zulip 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

view this post on Zulip Yakov Pechersky (Feb 18 2021 at 09:53):

That is quite awesome.

view this post on Zulip 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

view this post on Zulip 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