chore: update stage0

stage0/src/Init/Control/Except.lean

@@ -8,6 +8,7 @@ The Except monad transformer.
 prelude
 import Init.Control.Basic
 import Init.Control.Id
+import Init.Coe
 
 universes u v w u'
 
@@ -119,7 +120,7 @@ variable {ε : Type u} {m : Type v → Type w}
 /-- Alternative orelse operator that allows to select which exception should be used.
     The default is to use the first exception since the standard `orelse` uses the second. -/
 @[inline] def orelse' [MonadExcept ε m] {α : Type v} (t₁ t₂ : m α) (useFirstEx := true) : m α :=
-  tryCatch t₁ fun e₁ => tryCatch t₂ fun e₂ => throw (if useFirstEx = true then e₁ else e₂)
+  tryCatch t₁ fun e₁ => tryCatch t₂ fun e₂ => throw (if useFirstEx then e₁ else e₂)
 
 end MonadExcept
 

stage0/src/Init/Data/Repr.lean

@@ -195,7 +195,7 @@ protected def Char.repr (c : Char) : String :=
   c.quote
 
 def String.quote (s : String) : String :=
-  if s.isEmpty = true then "\"\""
+  if s.isEmpty then "\"\""
   else s.foldl (fun s c => s ++ c.quoteCore) "\"" ++ "\""
 
 instance : Repr String where

stage0/src/Lean/Meta/WHNF.lean

@@ -307,6 +307,31 @@ def reduceProj? (e : Expr) : MetaM (Option Expr) := do
   | Expr.proj _ i c _ => project? c i
   | _                 => return none
 
+/-
+  Auxiliary method for reducing terms of the form `?m t_1 ... t_n` where `?m` is delayed assigned.
+  Recall that we can only expand a delayed assignment when all holes/metavariables in the assigned value have been "filled".
+-/
+private def whnfDelayedAssigned? (f' : Expr) (e : Expr) : MetaM (Option Expr) := do
+  if f'.isMVar then
+    match (← getDelayedAssignment? f'.mvarId!) with
+    | none => return none
+    | some { fvars := fvars, val := val, .. } =>
+      let args := e.getAppArgs
+      if fvars.size > args.size then
+        -- Insufficient number of argument to expand delayed assignment
+        return none
+      else
+        let newVal ← instantiateMVars val
+        if newVal.hasExprMVar then
+           -- Delayed assignment still contains metavariables
+           return none
+        else
+           let newVal := newVal.abstract fvars
+           let result := newVal.instantiateRevRange 0 fvars.size args
+           return mkAppRange result fvars.size args.size args
+  else
+    return none
+
 /--
   Apply beta-reduction, zeta-reduction (i.e., unfold let local-decls), iota-reduction,
   expand let-expressions, expand assigned meta-variables. -/
@@ -322,23 +347,25 @@ partial def whnfCore (e : Expr) : MetaM Expr :=
       if f'.isLambda then
         let revArgs := e.getAppRevArgs
         whnfCore <| f'.betaRev revArgs
-      else match (← reduceMatcher? e) with
+      else if let some eNew ← whnfDelayedAssigned? f' e then
+        whnfCore eNew
+      else
+        let e := if f == f' then e else e.updateFn f'
+        match (← reduceMatcher? e) with
         | ReduceMatcherResult.reduced eNew => whnfCore eNew
         | ReduceMatcherResult.partialApp   => pure e
         | ReduceMatcherResult.stuck _      => pure e
         | ReduceMatcherResult.notMatcher   =>
-          let done : Unit → MetaM Expr := fun _ =>
-            if f == f' then pure e else pure $ e.updateFn f'
-          matchConstAux f' done fun cinfo lvls =>
+          matchConstAux f' (fun _ => return e) fun cinfo lvls =>
             match cinfo with
-            | ConstantInfo.recInfo rec    => reduceRec rec lvls e.getAppArgs done whnfCore
-            | ConstantInfo.quotInfo rec   => reduceQuotRec rec lvls e.getAppArgs done whnfCore
+            | ConstantInfo.recInfo rec    => reduceRec rec lvls e.getAppArgs (fun _ => return e) whnfCore
+            | ConstantInfo.quotInfo rec   => reduceQuotRec rec lvls e.getAppArgs (fun _ => return e) whnfCore
             | c@(ConstantInfo.defnInfo _) => do
               if (← isAuxDef c.name) then
-                deltaBetaDefinition c lvls e.getAppRevArgs done whnfCore
+                deltaBetaDefinition c lvls e.getAppRevArgs (fun _ => return e) whnfCore
               else
-                done ()
-            | _ => done ()
+                return e
+            | _ => return e
     | Expr.proj .. => match (← reduceProj? e) with
       | some e => whnfCore e
       | none => return e

stage0/src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -108,7 +108,7 @@ def delabAppExplicit : Delab := do
       let fn ← getExpr
       let stx ← if fn.isConst then delabConst else delab
       let paramKinds ← liftM <| getParamKinds fn <|> pure #[]
-      let stx ← if paramKinds.any (fun | ParamKind.explicit => false | _ => true) = true then `(@$stx) else pure stx
+      let stx ← if paramKinds.any (fun | ParamKind.explicit => false | _ => true) then `(@$stx) else pure stx
       pure (stx, #[]))
     (fun ⟨fnStx, argStxs⟩ => do
       let argStx ← delab

stage0/src/Lean/Server/FileWorker.lean

@@ -71,7 +71,7 @@ section Utils
 
     def check [MonadExceptOf ElabTaskError m] [MonadLiftT (ST RealWorld) m] [Monad m] (tk : CancelToken) : m Unit := do
       let c ← tk.ref.get
-      if c = true then
+      if c then
         throw ElabTaskError.aborted
 
     def set (tk : CancelToken) : IO Unit :=

stage0/stdlib/Init/Control/Except.c

@@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: Init.Control.Except
-// Imports: Init.Control.Basic Init.Control.Id
+// Imports: Init.Control.Basic Init.Control.Id Init.Coe
 #include <lean/lean.h>
 #if defined(__clang__)
 #pragma clang diagnostic ignored "-Wunused-parameter"
@@ -2914,6 +2914,7 @@ return x_3;
 }
 lean_object* initialize_Init_Control_Basic(lean_object*);
 lean_object* initialize_Init_Control_Id(lean_object*);
+lean_object* initialize_Init_Coe(lean_object*);
 static bool _G_initialized = false;
 lean_object* initialize_Init_Control_Except(lean_object* w) {
 lean_object * res;
@@ -2925,6 +2926,9 @@ lean_dec_ref(res);
 res = initialize_Init_Control_Id(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
+res = initialize_Init_Coe(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
 l_Except_instMonadExcept___closed__1 = _init_l_Except_instMonadExcept___closed__1();
 lean_mark_persistent(l_Except_instMonadExcept___closed__1);
 l_Except_instMonadExcept___closed__2 = _init_l_Except_instMonadExcept___closed__2();