pretty printing underscores

Stream: general

[Scott Morrison]

Is there a good way to pretty print expressions, so metavariables get replaced by _ characters?

[Scott Morrison]

I see there is pp.use_holes which prints metavariables as {! !}.

[Scott Morrison]

or perhaps more simply --- does anyone know how I do substring replacement? (e.g. {! !} to _)

[Rob Lewis]

It might be easier to replace the metavars with pexpr.mk_placeholder before printing.

[Scott Morrison]

I see. Any suggestions on how to do the replacement? I tried just folding, but I need to turn exprs back into pexprs.

[Scott Morrison]

of, pexpr.of_expr

[Rob Lewis]

No promises that this works beyond the two little examples I just tried, but give it a shot.

meta def replace_mvars (e : expr) : expr :=
e.replace (λ e' _, if e'.is_meta_var then some (unchecked_cast pexpr.mk_placeholder) else none)

[Scott Morrison]

Looking good!!

[Scott Morrison]

I still need to learn how to do string munging in Lean, I'm flailing about trying to decide is a string contains a given character... :-(

[Scott Morrison]

'_' ∈ s.to_list?

[Scott Morrison]

Seems to work, but presumably there's something more natural.

[Keeley Hoek]

Just on the strings scott
Resist the temptation to use string.iterators
I thought they were the future (they are VM implemented), and changed the expr deserialiser to use them
About a 5% slowdown