Examples on delaborating for whitespace/indentation

Stream: metaprogramming / tactics

[nrs]

Am trying to make a delaborator that will print a top-level function as

someFunc
  • arg1
  • arg2

Does anyone have examples of delaborators or unexpanders that control whitespace and indentation?

[Kyle Miller]

Delaborators don't control whitespace or indentation.

Instead, you need to somehow encode whitespace handling in the syntax definition itself.

[nrs]

Hm I see. Any chance you could give me a vague idea of what it would mean to encode whitespace in Syntax? Do you mean e.g. using tab/space/whitespace characters in the String for e.g. Syntax.atom?

[Damiano Testa]

Wasn't there an example of exactly this in the early days of lean 4?

[Damiano Testa]

Maybe "early days" was not really correct, but this discussion is what I had in mind.

[Kyle Miller]

How about you give your syntax definition as a #mwe?

[Damiano Testa]

Oh, you want the arguments to be displayed in that format, not entered like that!

[nrs]

@Kyle Miller concretely I'm trying to make this for an arbitrary recursor. as a special case I'm working with the Expr from List.permutationsAux.rec (just so happened to be the example that made me start on ideas for making verbose Exprs easier to read)

def permutationsAux.rec {C : List α → List α → Sort v} (H0 : ∀ is, C [] is)
    (H1 : ∀ t ts is, C ts (t :: is) → C is [] → C (t :: ts) is) : ∀ l₁ l₂, C l₁ l₂
  | [], is => H0 is
  | t :: ts, is =>
      H1 t ts is (permutationsAux.rec H0 H1 ts (t :: is)) (permutationsAux.rec H0 H1 is [])
  termination_by ts is => (length ts + length is, length ts)
  decreasing_by all_goals (simp_wf; omega)

@Damiano Testa yeah, only pretty printing!

[Kyle Miller]

Maybe you could look at how match syntax is defined and look in Delaborators/Builtins for the builtin match delaborator.

[nrs]

will get started on that, thank you!

[Kyle Miller]

Note that since match syntax is builtin, it's using a lower-level parser description than syntax. For user-defined syntax, syntax is nicer.

[nrs]

open Std Format

def myFormat : Format :=
  .append (.text "theFunc")
  (.append (.nest 2 line)
  (.append (.text "arg, the First")
  (.append (.nest 2 line)
  (.text "seconarg"))))

#eval IO.println myFormat

[nrs]

more examples in the Wadler article mentioned at docs#Std.Format