## Stream: metaprogramming / tactics

### Topic: elaborate pexpr into expr

#### 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.

#### Mario Carneiro (Oct 27 2020 at 16:10):

pexpr numerals are stored completely differently

#### Rob Lewis (Oct 27 2020 at 16:10):

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

#### 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

Hmm, ok

#### Mario Carneiro (Oct 27 2020 at 16:13):

We really need to make macro_def transparent in lean

#### 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.

#### Rob Lewis (Oct 27 2020 at 16:13):

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


#### Rob Lewis (Oct 27 2020 at 16:14):

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

#### Rob Lewis (Oct 27 2020 at 16:14):

Not what numeral it is.

#### Mario Carneiro (Oct 27 2020 at 16:15):

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

#### 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

#### 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

#### 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...

#### 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

#### 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


#### 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