derive has_repr for in inductive type

Stream: general

[Thorsten Altenkirch]

Is there a convenient way to automatically derive a representation for an inductive type? (so that I can print it). E.g.

inductive Instr : Type
| pushC : ℕ → Instr
| pushV : string → Instr
| add : Instr
| mult : Instr

[Mario Carneiro]

a quick and dirty solution is to use has_reflect as a proxy for has_repr, although the results aren't great:

@[derive has_reflect]
inductive Instr : Type
| pushC : ℕ → Instr
| pushV : string → Instr
| add : Instr
| mult : Instr

meta instance : has_repr Instr := ⟨λ x, to_string (reflect x : expr)⟩

#eval Instr.pushC 0
-- Instr.pushC (has_zero.zero.{0} nat nat.has_zero)

[Thorsten Altenkirch]

That is good but is there a way to get rid of the weird representation of nat?

[Mario Carneiro]

implement has_repr manually...

[Mario Carneiro]

I suppose you could also do a hybrid implementation like this:

meta instance : has_repr Instr := ⟨λ x, match x with
  | Instr.pushC x := sformat!"Instr.pushC {x}"
  | x := to_string (reflect x : expr)
  end⟩

#eval Instr.pushC 2
-- Instr.pushC 2
#eval Instr.pushV "A"
-- Instr.pushV "A"

[Eric Wieser]

I think it would be fairly easy to write a metaprogram to do this