fix: app unexpander for sorryAx (#5759)

Fixes a long-standing bug in the the `sorryAx` app unexpander that
prevented it from applying. Now `sorry` pretty prints as `sorry`.

src/Init/NotationExtra.lean

@@ -168,9 +168,9 @@ end Lean
   | _                => throw ()
 
 @[app_unexpander sorryAx] def unexpandSorryAx : Lean.PrettyPrinter.Unexpander
-  | `($(_) _)   => `(sorry)
-  | `($(_) _ _) => `(sorry)
-  | _           => throw ()
+  | `($(_) $_)    => `(sorry)
+  | `($(_) $_ $_) => `(sorry)
+  | _             => throw ()
 
 @[app_unexpander Eq.ndrec] def unexpandEqNDRec : Lean.PrettyPrinter.Unexpander
   | `($(_) $m $h) => `($h ▸ $m)

tests/lean/1074b.lean.expected.out

@@ -2,4 +2,4 @@
 1074b.lean:11:43-11:53: error: tactic 'assumption' failed
 a n z✝ : Term
 a✝ : Brx z✝
-⊢ Brx (sorryAx Term true)
+⊢ Brx sorry

tests/lean/1301.lean.expected.out

@@ -6,4 +6,4 @@ a' : True ∧ True
 1301.lean:9:25-9:29: error: elaboration function for 'termTerm' has not been implemented
   term
 def b : Nat → Nat :=
-sorryAx (Nat → Nat) true
+sorry

tests/lean/255.lean.expected.out

@@ -1,6 +1,6 @@
 A : α
 id x✝ : α
 255.lean:16:7-16:8: error: unknown constant 'x✝'
-id (sorryAx ?m true) : ?m
+id sorry : ?m
 255.lean:20:9-20:10: error: unknown constant 'x✝'
-id (sorryAx ?m true) : ?m
+id sorry : ?m

tests/lean/StxQuot.lean.expected.out

@@ -45,7 +45,7 @@ StxQuot.lean:83:7-83:19: error: unknown identifier 'sufficesDecl'
 "#[(num \"1\"), [(num \"2\") (num \"3\")], (num \"4\")]"
 "#[(num \"2\")]"
 StxQuot.lean:97:39-97:44: error: unexpected antiquotation splice
-fun x => sorryAx (?m x) true : (x : ?m) → ?m x
+fun x => sorry : (x : ?m) → ?m x
 "#[(some 1), (some 2)]"
 StxQuot.lean:104:13-104:14: error: unknown identifier 'x' at quotation precheck; you can use `set_option quotPrecheck false` to disable this check.
 "`id._@.UnhygienicMain._hyg.1"

tests/lean/binrelTypeMismatch.lean.expected.out

@@ -10,11 +10,11 @@ has type
   Prop : Type
 but is expected to have type
   Bool : Type
-Prop → sorryAx (Sort u_1) true : Sort (imax 1 u_1)
+Prop → sorry : Sort (imax 1 u_1)
 binrelTypeMismatch.lean:20:27-20:28: error: type mismatch
   p
 has type
   Prop : Type
 but is expected to have type
   Bool : Type
-Prop → sorryAx (Sort u_1) true : Sort (imax 1 u_1)
+Prop → sorry : Sort (imax 1 u_1)

tests/lean/defInst.lean.expected.out

@@ -2,7 +2,7 @@
 defInst.lean:8:26-8:32: error: failed to synthesize
   BEq Foo
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
-fun x y => sorryAx (?m x y) true : (x y : Foo) → ?m x y
+fun x y => sorry : (x y : Foo) → ?m x y
 [4, 5, 6]
 fun x y => x == y : Foo → Foo → Bool
 [("hello", "hello")]

tests/lean/macroSwizzle.lean.expected.out

@@ -9,4 +9,4 @@ has type
   String : Type
 but is expected to have type
   Nat : Type
-(sorryAx Nat true).succ : Nat
+sorry.succ : Nat

tests/lean/nameArgErrorIssue.lean.expected.out

@@ -7,7 +7,7 @@ has type
   String : Type
 but is expected to have type
   Nat : Type
-bla (sorryAx Nat true) 5 : Nat
+bla sorry 5 : Nat
 nameArgErrorIssue.lean:6:20-6:24: error: application type mismatch
   bla "hi"
 argument

tests/lean/namedHoles.lean.expected.out

@@ -6,13 +6,13 @@ has type
   Nat : Type
 but is expected to have type
   Bool : Type
-f ?x (sorryAx Bool true) : Nat
+f ?x sorry : Nat
 g ?x ?x : Nat
 20
 foo (fun x => ?hole) ?hole : Nat
 bla ?hole fun x => ?hole : Nat
 namedHoles.lean:35:38-35:43: error: synthetic hole has already been defined with an incompatible local context
-boo (fun x => ?hole) fun y => sorryAx Nat true : Nat
+boo (fun x => ?hole) fun y => sorry : Nat
 11
 12
 namedHoles.lean:58:26-58:31: error: synthetic hole has already been defined and assigned to value incompatible with the current context

tests/lean/noTabs.lean.expected.out

@@ -1,3 +1,3 @@
 noTabs.lean:3:0: error: tabs are not allowed; please configure your editor to expand them
 let a := 1;
-sorryAx ?m true : ?m
+sorry : ?m

tests/lean/run/1163.lean

@@ -1,7 +1,7 @@
 import Lean
 open Lean Elab Tactic
 
-macro "obviously1" : tactic => `(tactic| exact sorryAx _)
+macro "obviously1" : tactic => `(tactic| exact sorryAx _ false)
 
 theorem result1 : False := by obviously1
 

tests/lean/run/1910.lean

@@ -56,7 +56,7 @@ error: invalid field notation, function 'Nat.foo' has argument with the expected
   Nat
 but it cannot be used
 ---
-info: fun n => sorryAx (?_ n) true : (n : Nat) → ?_ n
+info: fun n => sorry : (n : Nat) → ?_ n
 -/
 #guard_msgs in #check fun (n : Nat) => n.foo
 
@@ -81,7 +81,7 @@ def Bar.bar : Bar true := {}
 /--
 error: invalid field notation, function 'Bar.bar' does not have argument with type (Bar ...) that can be used, it must be explicit or implicit with a unique name
 ---
-info: fun f => sorryAx (?_ f) true : (f : Bar false) → ?_ f
+info: fun f => sorry : (f : Bar false) → ?_ f
 -/
 #guard_msgs in #check fun (f : Bar false) => f.bar false
 
@@ -90,6 +90,6 @@ info: fun f => sorryAx (?_ f) true : (f : Bar false) → ?_ f
 /--
 error: invalid field notation, function 'Bar.bar' does not have argument with type (Bar ...) that can be used, it must be explicit or implicit with a unique name
 ---
-info: fun f => sorryAx (?_ f) true : (f : Bar false) → ?_ f
+info: fun f => sorry : (f : Bar false) → ?_ f
 -/
 #guard_msgs in #check fun (f : Bar false) => f.bar true false

tests/lean/run/2283.lean

@@ -33,11 +33,11 @@ instance hasLimitsOfSize : HasLimitsOfSize.{v} (Type max v u) := sorry
 set_option pp.mvars false
 /--
 error: type mismatch
-  limit.π (sorryAx (Functor' ?_ ?_)) (sorryAx ?_)
+  limit.π sorry sorry
 has type
-  sorryAx (Sort _) : Sort _
+  sorry : Sort _
 but is expected to have type
-  limit f → sorryAx (Sort _) : Sort (imax (max (u + 1) (v + 1)) _)
+  limit f → sorry : Sort (imax (max (u + 1) (v + 1)) _)
 -/
 #guard_msgs in
 theorem pi_lift_π_apply {C : Type v} [Category.{v} C] (f : Functor' C (Type max v u)) :

tests/lean/run/3554.lean

@@ -15,7 +15,7 @@ theorem bar : True := by
 
 /--
 info: theorem bar : True :=
-sorryAx True true
+sorry
 -/
 #guard_msgs in
 #print bar
@@ -31,7 +31,7 @@ theorem bar2 : True := by
 
 /--
 info: theorem bar2 : True :=
-sorryAx True true
+sorry
 -/
 #guard_msgs in
 #print bar2

tests/lean/run/3943.lean

@@ -8,9 +8,9 @@ example (f : Nat → Nat) : f x = 0 → f x + 1 = y := by
   guard_target =ₛ f x = 0 → 1 = y
   sorry
 
-example (f : Nat → Nat) : let _  : f x = 0 := sorry; f x + 1 = y := by
+example (f : Nat → Nat) : let _  : f x = 0 := sorryAx _ false; f x + 1 = y := by
   simp (config := { contextual := true, zeta := false })
-  guard_target =ₛ let _  : f x = 0 := sorry; 1 = y
+  guard_target =ₛ let _  : f x = 0 := sorryAx _ false; 1 = y
   sorry
 
 def overlap : Nat → Nat
@@ -45,7 +45,7 @@ example : (if p x then g x else g x + 1) + g x = y := by
   guard_target =ₛ (if p x then x else g x + 1) + g x = y
   sorry
 
-example : (let _  : p x := sorry; g x + 1 = y) ↔ g x = y := by
+example : (let _  : p x := sorryAx _ false; g x + 1 = y) ↔ g x = y := by
   simp (config := { zeta := false }) (discharger := assumption)
-  guard_target =ₛ (let _  : p x := sorry; x + 1 = y) ↔ g x = y
+  guard_target =ₛ (let _  : p x := sorryAx _ false; x + 1 = y) ↔ g x = y
   sorry

tests/lean/run/4365.lean

@@ -19,7 +19,7 @@ def f (α : Sort u) : α :=
 error: numerals are data in Lean, but the expected type is universe polymorphic and may be a proposition
   α : Sort u
 ---
-info: fun {α} => id (id (sorryAx α true)) : {α : Sort u} → α
+info: fun {α} => id (id sorry) : {α : Sort u} → α
 -/
 #guard_msgs in
 #check fun {α : Sort u} => id (α := α) (id 0)

tests/lean/run/4670.lean

@@ -20,7 +20,7 @@ has type
 but is expected to have type
   Foo : Type
 ---
-info: (sorryAx Foo true).out : Nat
+info: sorry.out : Nat
 -/
 #guard_msgs in #check Foo.out true
 
@@ -38,7 +38,7 @@ has type
 but is expected to have type
   Foo : Type
 ---
-info: (sorryAx Foo true).out' : Nat
+info: sorry.out' : Nat
 -/
 #guard_msgs in #check Foo.out' true
 

tests/lean/run/4920.lean

@@ -34,7 +34,7 @@ xm : List (Vect m A)
 h0 : xm.length = as.length
 ih : i < (List.zipWith cons as xm).length
 jh : j < m
-⊢ ?_ (sorryAx ?_ true) j
+⊢ ?_ sorry j
 -/
 #guard_msgs in
 theorem Vect.aux

tests/lean/run/CoeNew.lean

@@ -19,8 +19,8 @@ instance constantFunctionCoe {α β : Type} : CoeFun (ConstantFunction α β) (f
 
 set_option pp.explicit true
 
-#synth CoeT { x : Nat // x > 0 } ⟨1, sorryAx _⟩ Nat
-#synth CoeT { x : Nat // x > 0 } ⟨1, sorryAx _⟩ Bool
+#synth CoeT { x : Nat // x > 0 } ⟨1, sorryAx _ false⟩ Nat
+#synth CoeT { x : Nat // x > 0 } ⟨1, sorryAx _ false⟩ Bool
 #synth CoeT Nat 0 (Option Nat)
 #synth CoeT Bool true (Option Nat)
 #synth CoeT Prop (0 = 1) Bool

tests/lean/run/autoLift.lean

@@ -27,7 +27,7 @@ but is expected to have type
   M ?_ : Type
 ---
 info: id do
-  let a ← sorryAx (M Nat) true
+  let a ← sorry
   g a : M Unit
 -/
 #guard_msgs in

tests/lean/run/sorry.lean

@@ -0,0 +1,26 @@
+/-!
+# Tests of the `sorry` term elaborator
+-/
+
+/-!
+Basic usage.
+-/
+
+/-- warning: declaration uses 'sorry' -/
+#guard_msgs in example : False := sorry
+
+/-- warning: declaration uses 'sorry' -/
+#guard_msgs in example : False := by sorry
+
+/-!
+Pretty printing
+-/
+
+/-- info: sorry : Nat -/
+#guard_msgs in #check (sorry : Nat)
+
+/-- info: fun x => sorry : Nat → Nat -/
+#guard_msgs in #check fun x : Nat => (sorry : Nat)
+
+/-- info: fun x => sorry (x + 1) : Nat → Nat -/
+#guard_msgs in #check fun x : Nat => (sorry : Nat → Nat) (x + 1)