From 6ffe310c48e120a261d5f67a5f6ca8a7ea1915da Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 24 Mar 2020 15:35:58 +0100
Subject: [PATCH] feat: delab coercions

---
 src/Init/Lean/Delaborator.lean           | 26 ++++++++++++++++++++++++
 tests/lean/Delaborator.lean              |  2 ++
 tests/lean/Delaborator.lean.expected.out | 20 ++++++++----------
 3 files changed, 37 insertions(+), 11 deletions(-)

diff --git a/src/Init/Lean/Delaborator.lean b/src/Init/Lean/Delaborator.lean
index 4b3f19dd78..5f8a01919e 100644
--- a/src/Init/Lean/Delaborator.lean
+++ b/src/Init/Lean/Delaborator.lean
@@ -53,6 +53,7 @@ instance HasQuote : HasQuote Level := ⟨Level.quote⟩
 end Level
 
 def getPPBinderTypes (o : Options) : Bool := o.get `pp.binder_types true
+def getPPCoercions (o : Options) : Bool := o.get `pp.coercions true
 def getPPExplicit (o : Options) : Bool := o.get `pp.explicit false
 def getPPStructureProjections (o : Options) : Bool := o.get `pp.structure_projections true
 def getPPUniverses (o : Options) : Bool := o.get `pp.universes false
@@ -372,6 +373,12 @@ match l with
 | Literal.natVal n => pure $ quote n
 | Literal.strVal s => pure $ quote s
 
+-- `ofNat 0` ~> `0`
+@[builtinDelab app.HasOfNat.ofNat]
+def delabOfNat : Delab := whenPPOption getPPCoercions $ do
+e@(Expr.app _ (Expr.lit (Literal.natVal n) _) _) ← getExpr | failure;
+pure $ quote n
+
 /--
 Delaborate a projection primitive. These do not usually occur in
 user code, but are pretty-printed when e.g. `#print`ing a projection
@@ -405,6 +412,25 @@ assert $ !expl || info.nparams == 0;
 appStx ← withAppArg delab;
 `($(appStx).$(mkIdent f):ident)
 
+-- abbrev coe {α : Sort u} {β : Sort v} (a : α) [CoeT α a β] : β
+@[builtinDelab app.coe]
+def delabCoe : Delab := whenPPOption getPPCoercions $ do
+e ← getExpr;
+assert $ e.getAppNumArgs >= 4;
+-- delab as application, then discard function
+stx ← delabAppImplicit;
+match_syntax stx with
+| `($fn $args*) =>
+  if args.size == 1 then
+    pure $ args.get! 0
+  else
+    `($(args.get! 0) $(args.eraseIdx 0)*)
+| _             => failure
+
+-- abbrev coeFun {α : Sort u} {γ : α → Sort v} (a : α) [CoeFun α γ] : γ a
+@[builtinDelab app.coeFun]
+def delabCoeFun : Delab := delabCoe
+
 end Delaborator
 
 /-- "Delaborate" the given term into surface-level syntax using the given general and subterm-specific options. -/
diff --git a/tests/lean/Delaborator.lean b/tests/lean/Delaborator.lean
index 54ba6ee25b..878e5b2b6e 100644
--- a/tests/lean/Delaborator.lean
+++ b/tests/lean/Delaborator.lean
@@ -51,3 +51,5 @@ end
 #eval check `("hi")
 
 #eval check `((1,2).fst)
+
+#eval check `(1 < 2 || true)
diff --git a/tests/lean/Delaborator.lean.expected.out b/tests/lean/Delaborator.lean.expected.out
index 6f099cebfd..3418ac096b 100644
--- a/tests/lean/Delaborator.lean.expected.out
+++ b/tests/lean/Delaborator.lean.expected.out
@@ -86,15 +86,13 @@
     (Term.id `Bool.true (null)))
    (null))
   ")"))
-(Term.app (Term.id `HasOfNat.ofNat (null)) (null (Term.id `Nat (null)) (Term.num (numLit "0"))))
-(Term.app (Term.id `HasOfNat.ofNat (null)) (null (Term.id `Nat (null)) (Term.num (numLit "1"))))
-(Term.app (Term.id `HasOfNat.ofNat (null)) (null (Term.id `Nat (null)) (Term.num (numLit "42"))))
+(Term.num (numLit "0"))
+(Term.num (numLit "1"))
+(Term.num (numLit "42"))
 (Term.str (strLit "\"hi\""))
-(Term.proj
- (Term.app
-  (Term.id `Prod.mk (null))
-  (null
-   (Term.app (Term.id `HasOfNat.ofNat (null)) (null (Term.id `Nat (null)) (Term.num (numLit "1"))))
-   (Term.app (Term.id `HasOfNat.ofNat (null)) (null (Term.id `Nat (null)) (Term.num (numLit "2"))))))
- "."
- `fst)
+(Term.proj (Term.app (Term.id `Prod.mk (null)) (null (Term.num (numLit "1")) (Term.num (numLit "2")))) "." `fst)
+(Term.app
+ (Term.id `or (null))
+ (null
+  (Term.app (Term.id `HasLess.Less (null)) (null (Term.num (numLit "1")) (Term.num (numLit "2"))))
+  (Term.id `Bool.true (null))))