print `expr` in plaintext

Stream: general

[Zesen Qian]

How to print an expr in a plaintext way? That is, represented as all constructors app lam var, etc..

[Zesen Qian]

Maybe I should provide a context: I'm parsing a expr which (in pretty print) read like \forall (a b : bool), (b -> a). But somehow I encouter var 2 at b 's position, which is not possible because there should be only 0(refering to b) and 1(refering to a).

[Simon Hudon]

use e.to_raw_fmt

[Zesen Qian]

it's actually ∀ (a b : bool), ↥b → ↥a, to be precise.

[Simon Hudon]

Did you use expr.lambdas or expr.pis?

[Zesen Qian]

thank you, I got this:

(pi a default (const bool []) (pi b default (const bool []) (pi a default (app (app (app (const coe_sort [1,
         1]) (const bool [])) (const coe_sort_bool [])) (var 0)) (app (app (app (const coe_sort [1,
         1]) (const bool [])) (const coe_sort_bool [])) (var 2)))))

[Simon Hudon]

pis and lambdas have a known bug which behaves like you showed and there's a fix in mathlib, in meta.expr

[Simon Hudon]

Oh, no, that's not what I thought

[Zesen Qian]

I think I didn't use expr.lambdas/pis explicitly. I just wrote the formula in this form.

[Simon Hudon]

You don't have only two bound variables, you have three because implication is also a pi-type

[Zesen Qian]

Gee.. rookie mistake...

[Simon Hudon]

I recommend you don't manipulate var directly, there's a better interface for it. What do you need with them?

[Zesen Qian]

I need to parse a user-provided formula to generate a query to SMT solvers.

[Zesen Qian]

these formulas are mostly like the one I said above.

[Zesen Qian]

So first I need extract declarations, (a, b : bool), then the assertions (a -> b), or something more complex.

[Simon Hudon]

I see. So you're trying to use constants in your smt formulas rather than use quantifiers. What you can do is strip one quantifier at a time like this:

meta def unbind_vars : expr -> tactic (list expr × expr)
| e :=
do (expr.pi n bi d b) ← return e | return ([],e),
   v ← mk_local' n bi d,
   let b' := b.instantiate_var v,
   (vs,b'') ← unbind_vars b',
   return (v :: vs, b'')

[Simon Hudon]

The only thing you do with var in this code is use intantiate_var

[Zesen Qian]

this is so much better than mine. Right now I have to keep track of the variable stack myself.

[Simon Hudon]

The more you know ... :shooting_star:

[Zesen Qian]

..the more I have to worry about?

[Zesen Qian]

:grinning:

[Simon Hudon]

I'm hoping not in this case :laughing: