Easiest way to get `Repr` from `Unexpander`s

Stream: metaprogramming / tactics

[Will Bradley]

I have an inductive type for which I have written custom macro notation and, via @app_unexpander, delaborators. This is working well for #checking terms, but there is not an obvious way to print at runtime.

Am I better off just writing the Repr instance by hand?

[Henrik Böving]

You can either use deriving Repr or write one by hand yes. You can also work with ToString if nested formatting and such isn't too important

[Kyle Miller]

Will Bradley said:

not an obvious way to print at runtime.

What kind of programs are you running? If you're in the right monads, you can embed expressions in MessageData with for example logInfo m!"the value of e is {e}" and it uses the pretty printer. Terms are hoverable too.

[Will Bradley]

Kyle Miller said:

Will Bradley said:

not an obvious way to print at runtime.

What kind of programs are you running? If you're in the right monads, you can embed expressions in MessageData with for example logInfo m!"the value of e is {e}" and it uses the pretty printer. Terms are hoverable too.

I mean I really just want the Repr to be exactly what I see when I run #check. Btw, how do I get hover information to work well? My project is about a propositional logic, and all the notation I want to use is already hardcoded to be for the (meta-logical) Props, so I wrote a DSL (I tried overriding the notation but it just wasn't working)

inductive Prop' (A: Type u)
| atom: A → Prop' A
| true | false
| not: Prop' A → Prop' A
| or : Prop' A → Prop' A → Prop' A
| and: Prop' A → Prop' A → Prop' A

@[reducible]
def implies (p q: Prop' A) :=
  or (not p) q

@[reducible]
def iff (p q: Prop' A) :=
  and (implies p q) (implies q p)

declare_syntax_cat prop'

/-- Bring an external Prop' name into the syntax as a proposition -/
syntax ident : prop'
/-- Bring an external variable into the syntax as an atom. -/
syntax:max "@" term:max : prop'
/-- Bring any external term into the syntax as a proposition -/
syntax:max "{" term "}" : prop'
syntax "⊤" : prop'
syntax "⊥" : prop'
syntax:max "¬" prop':40 : prop'
syntax:30 prop':31 " ∨ " prop':30 : prop' -- right-associative
syntax:35 prop':36 " ∧ " prop':35 : prop' -- right-associative
syntax "(" prop' ")" : prop'
syntax:max "P![" prop' "]" : term

macro_rules
| `(P![$x:ident]) => `($x)
| `(P![@$a:term]) => `(atom $a)
| `(P![{$p:term}]) => `($p)
| `(P![⊤]) => `(true)
| `(P![⊥]) => `(false)
| `(P![¬$q:prop']) => `(not P![$q])
| `(P![$q:prop' ∨ $r:prop']) => `(or P![$q] P![$r])
| `(P![$q:prop' ∧ $r:prop']) => `(and P![$q] P![$r])
| `(P![($q)]) => `(P![$q])

syntax:20 prop':21 " → " prop':20 : prop' -- right-associative
syntax:20 prop':21 " ↔ " prop':20 : prop' -- right-associative (unlike in `Prop`)

macro_rules
| `(P![$q:prop' → $r:prop']) => `(implies P![$q] P![$r])
| `(P![$q:prop' ↔ $r:prop']) => `(iff P![$q] P![$r])

open Lean (TSyntax)
open Lean.PrettyPrinter (Unexpander UnexpandM)

inductive Parenthesize
| or | and | implies | iff
deriving BEq, Hashable

/-- This `Unexpander`-like function turns `P![$a ∧ $b]` into `($a ∧ $b)`
(a `TSyntax prop'`), and similarly for `P![$a ∨ $b]`.
The `targets` argument controls exactly which binary operations will be parenthesized. -/
def parenthesize (targets: Std.HashSet (Parenthesize))
    : Lean.TSyntax [`term, `ident] → UnexpandM (TSyntax `prop')
| `(term| P![$p]) => do
  let target?: Option Parenthesize := match p with
  | `(prop'| $_ ∨ $_) => some .or
  | `(prop'| $_ ∧ $_) => some .and
  | `(prop'| $_ → $_) => some .implies
  | `(prop'| $_ ↔ $_) => some .iff
  | _ => none
  match target? with
  | some target =>
    if target ∈ targets then `(prop'| ($p)) else pure p
  | none => pure p
-- We don't delaborate singleton `atom`s or booleans
-- since it looks better
| `(atom $a) => `(prop'| @$a) -- TODO: are these ok?
| `(true) => `(prop'| ⊤)
| `(false) => `(prop'| ⊥)
| `($p) =>
    if p.raw.isIdent then -- this might be jank too idk
      pure ⟨p⟩
    else
      `(prop'| {$p})

@[app_unexpander Prop'.not] def unexpNot : Unexpander
| `($_ $p) => do
  let p' ← parenthesize {.or, .and, .implies, .iff} p
  `(P![¬$p'])
| _ => throw ()

@[app_unexpander Prop'.and] def unexpAnd : Unexpander
| `($_ $p $q) => do
  let p' ← parenthesize {.or, .and, .implies, .iff} p  -- arity ≤ current
  let q' ← parenthesize {.or,       .implies, .iff} q -- right-associative
  `(P![$p' ∧ $q'])
| _ => throw ()

@[app_unexpander Prop'.or] def unexpOr : Unexpander
| `($_ $p $q) => do
  let p' ← parenthesize {.or, .implies, .iff} p
  let q' ← parenthesize {     .implies, .iff} q
  `(P![$p' ∨ $q'])
| _ => throw ()

@[app_unexpander Prop'.implies] def unexpImplies : Unexpander
| `($_ $p $q) => do
  let p' ← parenthesize {.implies, .iff} p -- < 21
  /- exception to the usual < 20 rule, since it's unclear
  that e.g. `P![p → q ↔ r] ≝ P![p → (q ↔ r)]` unless you know the
  order of operations already.
  -/
  let q' ← parenthesize {.iff} q
  `(P![$p' → $q'])
| _ => throw ()

@[app_unexpander Prop'.iff] def unexpIff : Unexpander
| `($_ $p $q) => do
  let p' ← parenthesize {} p
  let q' ← parenthesize {.implies, .iff} q
  `(P![$p' ↔ $q'])
| _ => throw ()

/-- info: P![@(0 + 3) ∧ @(-1) ∧ @7 ∧ ⊤] : Prop' ℤ -/
#guard_msgs in #check P![@(0 + 3) ∧ @(-1) ∧ @7 ∧ true]

def p: Prop' α := true
def q: Prop' α := true
def r: Prop' α := true
def a: α := sorry

/-- info: P![p ∧ q ↔ r] : Prop' α -/
#guard_msgs in #check P![(p ∧ q) ↔ r]
/-- info: P![p ∧ q ↔ (@a → r)] : Prop' α -/
#guard_msgs in #check P![(p ∧ q) ↔ @a → r]
/-- info: P![{if 2 < 3 then p else q} ∧ r] : Prop' α -/
#guard_msgs in #check P![{if 2 < 3 then p else q} ∧ r]

-- TODO: remove unnecessary parentheses around delaborated `P![...]`. For example,
/-- info: id (P![@0 ∧ @1]) : Prop' ℕ -/
#guard_msgs in #check id P![@0 ∧ @1]

-- TODO: get hover working inside `P![·]` syntax

This might be an XY question!

[Kyle Miller]

Can you XY a bit? In what context are you printing out expressions where you only have Repr and can't run the pretty printer?

[Will Bradley]

Kyle Miller said:

Can you XY a bit? In what context are you printing out expressions where you only have Repr and can't run the pretty printer?

Sorry, I'm very new to metaprogramming. How do I invoke the pretty printer?

[Kyle Miller]

Could you share code where you're printing anything? It looks like what you've shared is your syntax and unexpanders.

[Will Bradley]

Kyle Miller said:

Could you share code where you're printing anything? It looks like what you've shared is your syntax and unexpanders.

I just figured I should have it (e.g. for #eval) and was wondering if there was an easy automation to do it, that's all.

[Robin Arnez]

If you care about #eval only then deriving Lean.ToExpr (at the inductive definition) should do the trick and let your unexapanders do its thing

[Kyle Miller]

Exactly, you shouldn't need a Repr instance if all you're doing is using #eval and using things like logInfo (the message log doesn't need Lean.ToExpr instances btw, but #eval makes use of them to reflect the runtime values back into something that's pretty printable using the main pretty printer).

(If you have any code where you're getting stuck with printing things nicely, please post a #mwe here!)