Zulip Chat Archive

Stream: general

Topic: pretty printing underscores


Scott Morrison (Nov 26 2018 at 23:20):

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

Scott Morrison (Nov 26 2018 at 23:20):

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

Scott Morrison (Nov 26 2018 at 23:25):

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

Rob Lewis (Nov 26 2018 at 23:27):

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

Scott Morrison (Nov 26 2018 at 23:30):

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 (Nov 26 2018 at 23:31):

of, pexpr.of_expr

Rob Lewis (Nov 26 2018 at 23:31):

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 (Nov 26 2018 at 23:32):

Looking good!!

Scott Morrison (Nov 26 2018 at 23:35):

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 (Nov 26 2018 at 23:36):

'_' ∈ s.to_list?

Scott Morrison (Nov 26 2018 at 23:36):

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

Keeley Hoek (Nov 27 2018 at 00:07):

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


Last updated: Dec 20 2023 at 11:08 UTC