Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: printing expr


view this post on Zulip Patrick Massot (Jan 24 2021 at 16:45):

I'm still desperately trying to get fully usable #5440 before my course starts but @Edward Ayers doesn't have time for this (he started his real world job). The code in the PR works great for display but the "copy to clipboard" button still has the default rendering of expr. In the PR, the quantifier collapsing code is deeply intertwined with the complicated annotated expressions needed for widgets. I'd like to reproduce the collapsing effect in a function from expr to tactic string. But I don't know how to print expression that actually feature de Bruijn indices. I made a small start with

import tactic

namespace tactic
setup_tactic_parser
open tactic

meta def collapsed_pp : expr  tactic string
| (expr.pi x xbi xy (expr.pi p pbi py b)) := do
    pp_py  tactic.pp py,
    body  collapsed_pp b,
    pure ("∀ " ++ to_string pp_py ++ ", " ++ body)
| e := do pp_e  pp e, pure pp_e.to_string

@[interactive]
meta def test (n : parse ident) : tactic unit :=
do e  get_local n >>= infer_type,
   s  collapsed_pp e,
   trace s,
   skip

end tactic

example (h :  n > 0, true) : true :=
begin
  test h,
  sorry
end

but the output is ∀ #0 > 0, true, which makes sense. How can I get my ∀ n > 0, true back by re-injecting the name x? Or should I do something else entirely? The global goal here is to go from e : expr to string which is a version of pp e where quantifiers are nicely collapsed as you can do on input.

view this post on Zulip Edward Ayers (Jan 24 2021 at 21:58):

Hi Patrick I'm having a look now dw :)

view this post on Zulip Edward Ayers (Jan 24 2021 at 22:16):

Pushed to #5440

view this post on Zulip Edward Ayers (Jan 24 2021 at 22:17):

There is a new method called pretty_print_with_collapsed_quantifiers that you can use


Last updated: May 09 2021 at 21:10 UTC