pretty-printer things

forked-from-1kasper · Nov 8, 2023 · a141fd1 · a141fd1
1 parent ef976e7
commit a141fd1
Show file tree

Hide file tree

Showing 3 changed files with 35 additions and 7 deletions.
diff --git a/GroundZero/Meta/Notation.lean b/GroundZero/Meta/Notation.lean
@@ -4,6 +4,11 @@ open Lean.PrettyPrinter.Delaborator
 
 namespace GroundZero.Meta.Notation
 
+@[app_unexpander Nat.succ]
+def natSuccUnexpander : Lean.PrettyPrinter.Unexpander
+| `($_ $n) => `($n + 1)
+| _        => throw ()
+
 syntax "Π " many1(ppSpace (binderIdent <|> bracketedBinder)) ", " term : term
 macro_rules | `(Π $xs*, $y) => `(∀ $xs*, $y)
 
@@ -16,7 +21,7 @@ def delabPi : Delab := whenPPOption Lean.getPPNotation do {
   | stx                                           => pure stx
 }
 
-macro "λ " xs:many1(funBinder) ", " f:term : term => `(fun $xs* => $f)
+macro "λ " xs:(ppSpace funBinder)+ ", " f:term : term => `(fun $xs* => $f)
 
 @[delab lam]
 def delabLambda : Delab := whenPPOption Lean.getPPNotation do {
@@ -33,8 +38,8 @@ section
   def delabSig : Delab := whenPPOption Lean.getPPNotation do {
     match (← delabSigma) with
     | `($group:bracketedExplicitBinders × Σ $groups*, $body) => `(Σ $group:bracketedExplicitBinders $groups*, $body)
-    | `($group:bracketedExplicitBinders × $body) => `(Σ $group:bracketedExplicitBinders, $body)
-    | stx => pure stx
+    | `($group:bracketedExplicitBinders × $body)             => `(Σ $group:bracketedExplicitBinders, $body)
+    | stx                                                    => pure stx
   }
 end
 

diff --git a/GroundZero/Types/Equiv.lean b/GroundZero/Types/Equiv.lean
@@ -619,12 +619,17 @@ namespace Equiv
   | Nat.zero,   x => B x
   | Nat.succ n, α => @LoopOver (a = a) (λ p, b =[p] b) (idp a) (idp b) n α
 
-  macro:max "Ω" n:superscript "(" τ:term "," ε:term "," η:term ")" : term => do
+  macro:max "Ω" n:superscript "(" τ:term ", " ε:term ", " η:term ")" : term => do
     `(@LoopOver _ $τ _ $ε $(← Meta.Notation.parseSuperscript n) $η)
 
-  macro:max "Ω" "[" n:term "]" "(" τ:term "," ε:term "," η:term ")" : term => do
+  macro:max "Ω" "[" n:term "]" "(" τ:term ", " ε:term ", " η:term ")" : term => do
     `(@LoopOver _ $τ _ $ε $n $η)
 
+  @[app_unexpander LoopOver]
+  def loopOverUnexpander : Lean.PrettyPrinter.Unexpander
+  | `($_ $B $b $n $α) => `(Ω[$n]($B, $b, $α))
+  | _                 => throw ()
+
   hott def apdΩ {A : Type u} {B : A → Type v} (f : Π x, B x)
     {a : A} : Π {n : ℕ} (α : Ωⁿ(A, a)), Ωⁿ(B, f a, α)
   | Nat.zero   => f

diff --git a/GroundZero/Types/Id.lean b/GroundZero/Types/Id.lean
@@ -169,15 +169,33 @@ namespace Id
   macro:max "Ω" n:superscript "(" τ:term ")" : term => do
     `(Loop (pointOf $τ) $(← Meta.Notation.parseSuperscript n))
 
-  macro:max "Ω" n:superscript "(" τ:term "," ε:term ")" : term => do
+  macro:max "Ω" n:superscript "(" τ:term ", " ε:term ")" : term => do
     `(@Loop $τ $ε $(← Meta.Notation.parseSuperscript n))
 
   macro:max "Ω" "[" n:term "]" "(" τ:term ")" : term => do
     `(Loop (pointOf $τ) $n)
 
-  macro:max "Ω" "[" n:term "]" "(" τ:term "," ε:term ")" : term => do
+  macro:max "Ω" "[" n:term "]" "(" τ:term ", " ε:term ")" : term => do
     `(@Loop $τ $ε $n)
 
+  section
+    open Lean Lean.PrettyPrinter.Delaborator
+
+    def isPointOf (e : Expr) := e.isAppOfArity' `GroundZero.Types.Id.pointOf 2
+
+    @[delab app.GroundZero.Types.Id.Loop]
+    def delabLoop : Delab := whenPPOption Lean.getPPNotation do {
+      let ε ← SubExpr.getExpr;
+      guard (ε.isAppOfArity' `GroundZero.Types.Id.Loop 3);
+
+      let B ← SubExpr.withNaryArg 0 delab;
+      let b ← SubExpr.withNaryArg 1 delab;
+      let n ← SubExpr.withNaryArg 2 delab;
+
+      if isPointOf (ε.getArg! 1) then `(Ω[$n]($B)) else `(Ω[$n]($B, $b))
+    }
+  end
+
   hott def idΩ {B : Type u} (b : B) : Π n, Ωⁿ(B, b)
   | Nat.zero   => b
   | Nat.succ n => idΩ (idp b) n