chore: Turn Std.Do.Triple elaborator into a macro (#9251)

This PR demotes the builtin elaborators for `Std.Do.PostCond.total` and
`Std.Do.Triple` into macros, following the DefEq improvements of #9015.

Co-authored-by: Sebastian Graf <sg@lean-fro.org>

src/Lean/Elab/Tactic/Do/Syntax.lean

@@ -14,7 +14,8 @@ namespace Std.Do
 open Lean Parser Meta Elab Term PrettyPrinter Delaborator
 
 open Std.Do in
-@[builtin_delab app.Std.Do.PostCond.total]
+-- TODO: Remove after stage0 update
+-- @[builtin_delab app.Std.Do.PostCond.total]
 private meta def unexpandPostCondTotal : Delab := do
   match ← SubExpr.withAppArg <| delab with
   | `(fun $xs:term* => $e) =>
@@ -22,7 +23,8 @@ private meta def unexpandPostCondTotal : Delab := do
     return ⟨t.raw⟩
   | t => `($(mkIdent ``PostCond.total):term $t)
 
-@[inherit_doc Triple, builtin_doc, builtin_term_elab triple]
+-- TODO: Remove after stage0 update
+-- @[inherit_doc Triple, builtin_doc, builtin_term_elab triple]
 private meta def elabTriple : TermElab
   | `(⦃$P⦄ $x ⦃$Q⦄), _ => do
     -- In a simple world, this would just be a macro expanding to

src/Std/Do/PostCond.lean

@@ -190,7 +190,6 @@ abbrev PostCond (α : Type u) (ps : PostShape.{u}) : Type u :=
 scoped macro:max "post⟨" handlers:term,+,? "⟩" : term =>
   `(by exact ⟨$handlers,*, ()⟩)
   -- NB: Postponement through by exact is the entire point of this macro
-  -- until https://github.com/leanprover/lean4/pull/8074 lands
 
 /-- A postcondition expressing total correctness. -/
 abbrev PostCond.total (p : α → Assertion ps) : PostCond α ps :=
@@ -200,6 +199,12 @@ abbrev PostCond.total (p : α → Assertion ps) : PostCond α ps :=
 scoped macro:max ppAllowUngrouped "⇓" xs:term:max+ " => " e:term : term =>
   `(PostCond.total (by exact fun $xs* => spred($e)))
 
+@[app_unexpander PostCond.total]
+private meta def unexpandPostCondTotal : Lean.PrettyPrinter.Unexpander
+  | `($_ fun $xs:term* => $e) => do
+    `(⇓ $xs* => $(← SPred.Notation.unpack e))
+  | _ => throw ()
+
 /-- A postcondition expressing partial correctness. -/
 abbrev PostCond.partial (p : α → Assertion ps) : PostCond α ps :=
   (p, FailConds.true)

src/Std/Do/Triple/Basic.lean

@@ -33,7 +33,8 @@ def Triple [WP m ps] {α : Type u} (x : m α) (P : Assertion ps) (Q : PostCond
   P ⊢ₛ wp⟦x⟧ Q
 
 @[inherit_doc Std.Do.Triple]
-scoped syntax:lead (name := triple) "⦃" term "⦄ " term:lead " ⦃" term "⦄" : term
+scoped macro:lead (name := triple) "⦃" P:term "⦄ " x:term:lead " ⦃" Q:term "⦄" : term =>
+  `(Triple $x spred($P) $Q)
 
 @[app_unexpander Triple]
 private meta def unexpandTriple : Lean.PrettyPrinter.Unexpander