Prettyprinting the result of an #eval

Stream: lean4

[Philip Wadler]

Lean makes it wonderfully easy to define appropriate syntax.

When giving an error message, it uses whatever syntax I have defined to print constructs concisely. However, if I use #eval to compute a term, then the result is not pretty-printed, and unreadably verbose. For example, if I write

def plus : Γ ⊢ ℕ ⇒ ℕ ⇒ ℕ :=
  μ ƛ ƛ (switch (# Z) (# S Z) ((# S S S Z ⬝ # S S Z ⬝ # Z) +1))
def two_plus_two : ∅ ⊢ ℕ :=
  plus ⬝ 2 ⬝ 2
#eval two_plus_two

Then the result is

Typesig.term.application
  (Typesig.term.application
    (Typesig.term.mu
      (Typesig.term.lambda
        (Typesig.term.lambda
          (Typesig.term.case
            (Typesig.term.var (Typesig.lookup.stop))
            (Typesig.term.var (Typesig.lookup.pop (Typesig.lookup.stop)))
            (Typesig.term.succ
              (Typesig.term.application
                (Typesig.term.application
                  (Typesig.term.var
                    (Typesig.lookup.pop (Typesig.lookup.pop (Typesig.lookup.pop (Typesig.lookup.stop)))))
                  (Typesig.term.var (Typesig.lookup.pop (Typesig.lookup.pop (Typesig.lookup.stop)))))
                (Typesig.term.var (Typesig.lookup.stop))))))))
    (Typesig.term.succ (Typesig.term.succ (Typesig.term.zero))))
  (Typesig.term.succ (Typesig.term.succ (Typesig.term.zero)))

What I would like to get instead is

(μ ƛ ƛ (switch (# Z) (# S Z) ((# S S S Z ⬝ # S S Z ⬝ # Z) +1)))  ⬝ 2 ⬝ 2

Is there any way to get the latter rather than the former?

[Eric Wieser]

Can you make this a #mwe? We can't really help without seeing the definition of your notations

[Eric Wieser]

Does it behave as you expect with #check?

[Shreyas Srinivas]

Do you have a repository for this? My suspicion is that there are no unexpanders getting activated for your syntax

[Philip Wadler]

The complete code is available here: https://github.com/plfa/plfl/blob/main/src/Typesig.lean. Apologies for forgetting to mention that earlier!

[Shreyas Srinivas]

You are using notation here. Lean 4 typically requires you to write something called a delaborator in many cases. One quick work around is to try using notation3 which is the lean3 version of this. It is somewhat more limited but the generation of delaboration code works automatically.

[Philip Wadler]

Thanks, Shreyas. How would I rewrite my code to use notation3? Could you point me to an example?

[Shreyas Srinivas]

All the notation3 examples I know are in mathlib. You can see some examples in this github search : https://github.com/search?q=repo%3Aleanprover-community%2Fmathlib4+notation3&type=code

[Shreyas Srinivas]

Fwiw, for PL purposes it might be worth mixing some notation3 stuff for expressing $$\Gamma \turnstile e : A$$ stuff while writing the language and its denotations with the syntax feature. I have an example from something I wrote a few weeks ago.

[Shreyas Srinivas]

under declare_syntax_cat, I define the syntactic structure of the language, translate them to the values of an inductive type using macro_rules and then teach lean how to get back the notation from the values back into the syntactic form in the unexpander functions

[Kyle Miller]

Shreyas Srinivas said:

Do you have a repository for this? My suspicion is that there are no unexpanders getting activated for your syntax

FYI, unexpanders and delaborators don't apply to Repr, which is what #eval uses. Delaborators are for Lean.Expr -> Lean.Syntax, not going from runtime terms.

That said, if you have a ToExpr instance you could probably make use of delaboration, though the fact that Repr doesn't use a monad might make that impossible.

[Kyle Miller]

@Philip Wadler The reason you get pretty printed error messages during typechecking is that your terms are still represented as Lean.Exprs. However, when you do #eval, it's compiling your expression into a program, evaluating that with a virtual machine, and then using the Repr class to reflect the run-time value back into something (hopefully) human/machine readable.

If you use #reduce, it never leaves the world of Lean.Exprs:

#reduce two_plus_two
-- (μƛƛswitch (#Z) (#S Z) ((#S S S Z⬝#S S Z⬝#Z)+1))⬝o+1+1⬝o+1+1

This uses expression reduction. (For pretty printing, make sure to write " ⬝ " instead of "⬝" if you want whitespace.)

If you want #evaled expressions to pretty print, I believe you'll need to write custom Reprs rather than deriving them.

[Kyle Miller]

(@Sebastian Ullrich If a type has a ToExpr instance, is there any trick or giant hack to create a Repr instance by using ppExpr?)

[Philip Wadler]

@Shreyas Srinivas and @Kyle Miller Many thanks! Using #reduce instead of #eval gives a much more readable result.

[Shreyas Srinivas]

Kyle Miller said:

FYI, unexpanders and delaborators don't apply to Repr, which is what #eval uses. Delaborators are for Lean.Expr -> Lean.Syntax, not going from runtime terms.

Yeah I should have considered and mentioned #reduce. I use it extensively in the code from which my example was extracted.

[Kyle Miller]

Also, it's worth knowing that notation does generate unexpanders in Philip's code, so there's no need for notation3 here. The notation command is happy when the RHS is a constant or a simple application, with each variable used exactly once. (You mentioned notation3 is more limited, but I believe it's a strict superset of notation -- do you have any examples where it's not?)

[Shreyas Srinivas]

Some mathlib4 discussions earlier in the year gave me that idea. Something about declaring precedence.

[Mario Carneiro]

@Philip Wadler Unrelated aside, but you can make use of the notation inside the definition of the inductive if you declare it beforehand with set_option hygiene false in a section:

section
set_option hygiene false
local infix:40  " ∋ " => lookup
local infix:40  " ⊢ " => term

inductive lookup : TpEnv → Tp → Type where
  | stop :
       ---------
       Γ ▷ A ∋ A
  | pop :
       Γ ∋ B
       ---------
     → Γ ▷ A ∋ B
  deriving Repr

inductive term : TpEnv → Tp → Type where
  | var :
        Γ ∋ A
        -----
      → Γ ⊢ A
  | lambda :
        Γ ▷ A ⊢ B
        ---------
      → Γ ⊢ A ⇒ B
  | application :
        Γ ⊢ A ⇒ B
      → Γ ⊢ A
        -----
      → Γ ⊢ B
  | zero :
        -----
        Γ ⊢ ℕ
  | succ :
        Γ ⊢ ℕ
        -----
      → Γ ⊢ ℕ
  | case :
        Γ ⊢ ℕ
      → Γ ⊢ A
      → (Γ ▷ ℕ) ⊢ A
        -----------
      → Γ ⊢ A
  | mu :
        (Γ ▷ A) ⊢ A
        -----------
      → Γ ⊢ A
  deriving Repr
end

infix:40  " ∋ " => lookup
infix:40  " ⊢ " => term

[Mario Carneiro]

@Kyle Miller Regarding ToExpr, there isn't a derive handler for it so it's not really simpler than writing a Repr instance by hand, but here's a basic example of using toExpr in #eval using a MetaEval instance:

import Lean
inductive Tp : Type where
| natural : Tp
| function : Tp → Tp → Tp

notation:max "ℕ" => Tp.natural
infixr:70 " ⇒ " => Tp.function

open Lean
instance : ToExpr Tp where
  toTypeExpr := .const ``Tp []
  toExpr := go
where
  go
  | ℕ => .const ``Tp.natural []
  | A ⇒ B => mkApp2 (.const ``Tp.function []) (go A) (go B)

instance {α} [ToExpr α] : MetaEval α where
  eval env opts a hideUnit :=
    MetaEval.eval env opts (Meta.ppExpr (toExpr a)) hideUnit

#eval ℕ ⇒ ℕ
-- ℕ ⇒ ℕ

[Shreyas Srinivas]

@Kyle Miller : Took me a while to find, but there was also this: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Pretty-printing.20of.20sums/near/355293664

[Kyle Miller]

@Mario Carneiro I'm sure there's a derive handler since I wrote it :smile: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Tactic/DeriveToExpr.html

[Kyle Miller]

@Shreyas Srinivas That's very old now. notation3 in the meantime got the ability to delaborate its notations.

[Mario Carneiro]

Oh nice, and I can confirm it works in the full example

[Kyle Miller]

I wonder if we should either have that instance as a low-priority instance in mathlib, or at least put it in the documentation somewhere. (Maybe a non-instance def, so you can quickly make a MetaEval instance for your type?)

[Mario Carneiro]

it should be in core

[Mario Carneiro]

If there is no other MetaEval instance I don't see any reason not to use this one, and it's a design decision whether to prefer this over Repr

[Philip Wadler]

@Mario Carneiro Thank you for that hint. I was wondering if there was a way to do that.