Infoview notation

Stream: lean4

[Martin Dvořák]

Inforview currently uses this notation:

List.get x { val := n, isLt := hn }

I would like it to use this notation in my project:

x.get ⟨n, hn⟩

Is there a way to do it? Is there set_option pp.something true I could write to switch the notation to the latter?

[Max Nowak 🐉]

I have been trying to find an option for this as well, I think ⟨...⟩ is much easier to read. Or even just T.mk ....

[Joachim Breitner]

set_option pp.structureInstances false

helps (make it use mk).
Live-ready-example:

def foo : Fin 2 := ⟨1, by sorry ⟩
set_option pp.structureInstances false
#print foo

This code is doing this:
https://github.com/leanprover/lean4/blob/819b5eaceaa433ea9105d7af3582a45d8f5a00e9/src/Lean/PrettyPrinter/Delaborator/Builtins.lean#L183-L205
I wonder if it could make a smart guess, or an attribute-guided guess, which structures it should pretty-print using ⟨…⟩ instead.

[Joachim Breitner]

Ah, you could declare an unexpander like this:

def foo : Fin 2 := ⟨1, Nat.succ_lt_succ (Nat.succ_pos n) ⟩
@[app_unexpander Fin.mk] def unexpandFinMk : Lean.PrettyPrinter.Unexpander
  | `($(_) $i $hi) => `(⟨$i, $hi⟩)
  | _ => throw ()
#print foo

So if you think that that’s a better way to print Fin value (and I agree), just PR these three lines to the repo of your choice (e.g. src/Init/NotationExtra.lean in lean4).

I am not sure if dropping the field names would cause type inference problems if you try to use the pretty-printed output in your code. But I guess not – the field names don't identify the type anyways.

[Martin Dvořák]

Thank you! And is there a setting for the dot notation? I want to see x.get instead of List.get x in the infoview.

[Arthur Adjedj]

This works for any structure:

import Lean

open Lean PrettyPrinter Delaborator SubExpr Parser

def unexpandStructs : Syntax → Delab
  | `({ $[ $_ := $fields],* $_? }) => `(⟨$[$fields],*⟩ )
  | `($s) => `($s)

@[delab app]
def delabApp : Delab := do unexpandStructs $ ← delabAppImplicit

def foo : Fin 2 := ⟨1, sorry⟩
#print foo

This is only a proof of concept, but it seems to work well enough

[Kyle Miller]

Martin Dvořák said:

Thank you! And is there a setting for the dot notation? I want to see x.get instead of List.get x in the infoview.

You can use the mathlib pp_dot attribute if you know the first explicit argument is the one that gets the dot notation's object.

import Mathlib.Tactic.ProjectionNotation

variable (l : List Nat) (i : Fin l.length)

#check l.get i
-- List.get l i

attribute [pp_dot] List.get

#check l.get i
-- l.get i

This module also turns on an elaborator that collapses sequences of projections from fields in parent structures.

[Patrick Massot]

I still don't understand why this is not the default.

[Martin Dvořák]

So I have these guys:

set_option pp.structureInstances false
attribute [pp_dot] List.get List.take List.drop List.takeWhile List.dropWhile

Is it possible to set them for the whole project, so that I don't have to repeat them in every file?

[Martin Dvořák]

Can I set those pp_dot attributes for my whole project?

[Scott Morrison]

Don't they propagate to imports automatically?

[Scott Morrison]

The set_option you can put in your lakefile.

[Martin Dvořák]

One thing I still don't understand:

import Mathlib.Tactic.ProjectionNotation

attribute [pp_dot] List.map

example (l : List Char) (f : Char → Char) : l.map f = [] := by
  sorry

The goal is l.map f = []. Infoview shows f.map l = []. Why?

[Kyle Miller]

pp_dot doesn't work unless the first explicit argument in the thing that's supposed to come before the dot. This limitation is in the docstring for the attribute.

[Kyle Miller]

The attribute writes an app_unexpander for you. You can write these yourself too. Here's a relevant example: https://leanprover.zulipchat.com/#narrow/stream/412902-Polynomial-Freiman-Ruzsa-conjecture/topic/Outstanding.20tasks.2C.20version.203.2E0/near/404282694

[Martin Dvořák]

Why is List.map.{u, v} {α : Type u} {β : Type v} (f : α → β) (a✝ : List α) : List β defined with arguments in this order?
Since using the dot notation, I've been thinking in my head that List.map takes the list as the first argument.

[Kyle Miller]

This way List.map is a functor. List.map f is a function that transforms lists.

[Kyle Miller]

(Though if it had the opposite argument order, you could always write (List.map · f) for this.)

[Kyle Miller]

The way dot notation works is that it looks for the first argument (either explicit or implicit) having a type whose head (List in this case) is the expected head.

[Martin Dvořák]

Whereäs pp_dot just replaces the first token (to the left of the dot) in the name by the first explicit argument without checking it is a well-typed term?

[Martin Dvořák]

This works!

@[app_unexpander List.map]
def Measure.map.unexpander : Lean.PrettyPrinter.Unexpander
  | `($_ $f $μ) => `($(μ).$(Lean.mkIdent `map) $f)
  | _ => throw ()

example (l : List Char) (f : Char → Char) : l.map f = [] := by
  sorry

Unfortunately, it seems that round tripping is not enforced by the type checker, as I could as well do:

@[app_unexpander List.map]
def Measure.map.unexpander : Lean.PrettyPrinter.Unexpander
  | `($_ $f $μ) => `($(μ).$(Lean.mkIdent `WWWWWWWWWWWWWWW) $f)
  | _ => throw ()

example (l : List Char) (f : Char → Char) : l.map f = [] := by
  sorry

[Kyle Miller]

app_unexpanders don't check types at all. It's purely a syntax to syntax transformation, and you have to be sure it's correct.

[Martin Dvořák]

Shouldn't we add these unexpanders for the most useful functions like List.map to Mathlib or Std?

[Kyle Miller]

Martin Dvořák said:

Whereäs pp_dot just replaces the first token (to the left of the dot) in the name by the first explicit argument without checking it is a well-typed term?

Yes, it's replacing List.map f xs by xs.map f. The Lean.mkIdent is to keep the name from printing with a hygiene tombstone.

[Kyle Miller]

Martin Dvořák said:

Shouldn't we add these unexpanders for the most useful functions like List.map to Mathlib or Std?

I find these unexpanders to be rather brittle, and I'd like to see some support for dot notation from the delaborator itself, where we can be sure it's being handled properly.

[Martin Dvořák]

It seems I will copypaste the following code into every project of mine, and it doesn't feel right.

@[app_unexpander List.map]
def List.map.unexpander : Lean.PrettyPrinter.Unexpander
  | `($_ $f $μ) => `($(μ).$(Lean.mkIdent `map) $f)
  | _ => throw ()

@[app_unexpander List.take]
def List.take.unexpander : Lean.PrettyPrinter.Unexpander
  | `($_ $f $μ) => `($(μ).$(Lean.mkIdent `take) $f)
  | _ => throw ()

@[app_unexpander List.drop]
def List.drop.unexpander : Lean.PrettyPrinter.Unexpander
  | `($_ $f $μ) => `($(μ).$(Lean.mkIdent `drop) $f)
  | _ => throw ()

@[app_unexpander List.takeWhile]
def List.takeWhile.unexpander : Lean.PrettyPrinter.Unexpander
  | `($_ $f $μ) => `($(μ).$(Lean.mkIdent `takeWhile) $f)
  | _ => throw ()

@[app_unexpander List.dropWhile]
def List.dropWhile.unexpander : Lean.PrettyPrinter.Unexpander
  | `($_ $f $μ) => `($(μ).$(Lean.mkIdent `dropWhile) $f)
  | _ => throw ()

[Martin Dvořák]

Are there any concrete plans on improving the delaborator?

If not, these unexpanders (plus other similar ones) should go somewhere, as a temporary solution.

[Martin Dvořák]

Or maybe not, if other Lean users don't even use attribute [pp_dot] as their default.

[Kyle Miller]

As far as I know there's no Lean 4 issue tracking this feature request.