Making custom pretty-printers work in tactic mode

Stream: general

[Wojciech Nawrocki]

How can I force Lean to use my pretty-printer when printing types/expressions in the tactic state? I defined all instances I could think of but it still insists on using the full constructor form. (I don't want to use infix/notation in this case).

inductive Expr
| Mul: Expr → Expr → Expr
| Const (n: ℕ): Expr
open Expr

def Expr.to_string: Expr → string
| (Mul e1 e2) := "(" ++ e1.to_string ++ "*" ++ e2.to_string ++ ")"
| (Const n) := has_to_string.to_string n

instance : has_to_string Expr := ⟨Expr.to_string⟩
instance : has_repr Expr := ⟨Expr.to_string⟩ /- NB this instance is invalid, eval (repr e) = e doesn't hold -/
meta instance : has_to_format Expr := ⟨λe, ↑e.to_string⟩

#eval (Mul (Const 0) (Const 1)) -- (0*1) :)

example : true :=
begin
  let x := (Mul (Const 0) (Const 1)),
/- Tactic State:
x : Expr := Mul (Const 0) (Const 1) -- :(
⊢ true -/
end

[Marc Huisinga]

i'm not sure if you can do that, what if a parameter to Expr isn't fully evaluated in the tactic state? what should to_string do then?

the usual way to do this is to use the notation command - notations will show up in the tactic state.
according to @Sebastian Ullrich, one can also write some kind of parser, but i've never done that in lean and i'm not sure if that shows up in the tactic state.

edit: i just realized that i don't really understand to_format, so disregard what i said for to_format ...

[Wojciech Nawrocki]

Ah okay, I see what you mean. There could be something like maybe_uneval_to_string: maybe_uneval mytype -> string which would also have to handle cases where the value is a metavariable/let-binding/etc but with the current system, to_string expects the whole value to be well-defined. to_format is basically the same in this respect - it differs only in allowing finer control over the formatting.

[Sebastian Ullrich]

You most certainly do not want to evaluate things in the tactic state in order to print them; the most interesting parts in there usually are not constructors

[Sebastian Ullrich]

Apart from notations, the only customization Lean 3 gives you for tactic state reporting is overriding the has_to_format tactic_state instance - but then you'll have to format the whole goal yourself

[Wojciech Nawrocki]

I agree that evaluation is not the way to go, but I think there would still be a lot of value in pretty printers that can handle metavariables, local constants and so on. Thanks to notation commands we can get nice output like |- x*(y*z) = x*y*z, but notation is limited - for example, if I wanted to print a tree structure in some form within the goal:

|-
+- root
 +- left
  +- leaf1
  +- leaf2
 +- right
=
some_other_tree

[Marc Huisinga]

Apart from notations, the only customization Lean 3 gives you for tactic state reporting is overriding the has_to_format tactic_state instance - but then you'll have to format the whole goal yourself

aha! i was getting really confused when i tried to implement has_to_format similar to other inductive types like list in format.lean and it wouldn't work.

[Sebastian Ullrich]

I agree that evaluation is not the way to go

Right, so what you'd want instead is a reflected analog to has_to_format - for a given type (identified by its constant name), take a term (expr) of that type and return its format. That is how notations pretty-printing in Lean 3 works, it's just missing such a user hook.

[Simon Hudon]

@Sebastian Ullrich I just got this PR in #1222 which among other things lets you use tactic to pretty print stuff (e.g. trace!"expr: {e}; type: {infer_type e}"). Are you saying that's definitely a bad idea?

[Sebastian Ullrich]

No, has_to_tactic_format is fine. This was about using evaluation for printing terms.