printing expr

Stream: metaprogramming / tactics

[Patrick Massot]

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.

[Edward Ayers]

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

[Edward Ayers]

Pushed to #5440

[Edward Ayers]

There is a new method called pretty_print_with_collapsed_quantifiers that you can use