Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: elaborate pexpr into expr


view this post on Zulip Johan Commelin (Oct 27 2020 at 15:58):

I want to check that e : pexpr is a numeral. There exists expr.is_numeral. So how do I turn my e into an expr?
I'm a bit confused this doesn't work by default... because pexpr := expr ff.

view this post on Zulip Mario Carneiro (Oct 27 2020 at 16:10):

pexpr numerals are stored completely differently

view this post on Zulip Rob Lewis (Oct 27 2020 at 16:10):

There are a few complications, most importantly, that a pexpr numeral is typically a macro.

view this post on Zulip Mario Carneiro (Oct 27 2020 at 16:10):

You could just turn your pexpr into a expr by unchecked_cast, but the result would not work

view this post on Zulip Johan Commelin (Oct 27 2020 at 16:12):

Hmm, ok

view this post on Zulip Johan Commelin (Oct 27 2020 at 16:12):

I'll think more about this after dinner

view this post on Zulip Mario Carneiro (Oct 27 2020 at 16:13):

We really need to make macro_def transparent in lean

view this post on Zulip Rob Lewis (Oct 27 2020 at 16:13):

If you know the pexpr is going to be an "input numeral" parsed from the user (not created by some tactic or whatever) you can check if it's the right macro.

view this post on Zulip Rob Lewis (Oct 27 2020 at 16:13):

run_cmd match ``(0) with
| expr.macro md _ := trace $ expr.macro_def_name md
| _ := failed
end

view this post on Zulip Rob Lewis (Oct 27 2020 at 16:14):

It's "transparent enough" to test if something's a numeral.

view this post on Zulip Rob Lewis (Oct 27 2020 at 16:14):

Not what numeral it is.

view this post on Zulip Mario Carneiro (Oct 27 2020 at 16:15):

The fact that it mutually recurs with expr is a potential issue for making it transparent

view this post on Zulip Mario Carneiro (Oct 27 2020 at 16:17):

What if we had another type macro_def' which is the same as macro_def but is an inductive defined in expr? I'm afraid that actually using mutual meta def will break something

view this post on Zulip Mario Carneiro (Oct 27 2020 at 16:18):

BTW, I've already written down what macro_def should be as an inductive: https://github.com/digama0/olean-rs/blob/master/olean.lean#L16-L48

view this post on Zulip Rob Lewis (Oct 27 2020 at 16:20):

I have no clue what would break, but to be honest this seems complicated and not very high priority...

view this post on Zulip Mario Carneiro (Oct 27 2020 at 16:27):

Well the advantage of the macro_def' approach (with an explicit unfold : macro_def -> macro_def' function) is that it's a pure addition, so nothing will break

view this post on Zulip Mario Carneiro (Oct 27 2020 at 16:30):

In the meantime, here's an alternative way to get the value, although I don't think it can be done as a pure function (isn't there some unsafe_perform_tactic function?):

meta def nat_value (e : pexpr) : tactic  :=
match e with
| expr.macro md _ := do
  guard (expr.macro_def_name md = "prenum"),
  e  to_expr e, e.to_nat
| _ := failed
end

view this post on Zulip Mario Carneiro (Oct 27 2020 at 16:34):

Oh, it appears that this function has already been implemented as a pure function in core: src#expr.get_nat_value


Last updated: May 09 2021 at 21:10 UTC