elaborate pexpr into expr

Stream: metaprogramming / tactics

[Johan Commelin]

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]

pexpr numerals are stored completely differently

[Rob Lewis]

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

[Mario Carneiro]

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

[Johan Commelin]

Hmm, ok

[Johan Commelin]

I'll think more about this after dinner

[Mario Carneiro]

We really need to make macro_def transparent in lean

[Rob Lewis]

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]

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

[Rob Lewis]

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

[Rob Lewis]

Not what numeral it is.

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

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]

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]

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