chore: update stage0

stage0/src/Lean/Elab/Extra.lean

@@ -136,7 +136,7 @@ there is no coercion `Matrix Real 5 4` from `Matrix Real 4 8` and vice-versa, bu
 
 private inductive Tree where
   | term  (ref : Syntax) (val : Expr)
-  | op    (ref : Syntax) (f : Expr) (lhs rhs : Tree)
+  | op    (ref : Syntax) (lazy : Bool) (f : Expr) (lhs rhs : Tree)
 
 private partial def toTree (s : Syntax) : TermElabM Tree := do
   let result ← go (← liftMacroM <| expandMacros s)
@@ -145,13 +145,16 @@ private partial def toTree (s : Syntax) : TermElabM Tree := do
 where
   go (s : Syntax) := do
     match s with
-    | `(binop% $f $lhs $rhs) =>
-       let some f ← resolveId? f | throwUnknownConstant f.getId
-       return Tree.op s f (← go lhs) (← go rhs)
+    | `(binop% $f $lhs $rhs) => processOp (lazy := false) f lhs rhs
+    | `(binop_lazy% $f $lhs $rhs) => processOp (lazy := true) f lhs rhs
     | `(($e)) => (← go e)
     | _ =>
        return Tree.term s (← elabTerm s none)
 
+  processOp (f lhs rhs : Syntax) (lazy : Bool) := do
+    let some f ← resolveId? f | throwUnknownConstant f.getId
+    return Tree.op s (lazy := lazy) f (← go lhs) (← go rhs)
+
 -- Auxiliary function used at `analyze`
 private def hasCoe (fromType toType : Expr) : TermElabM Bool := do
   if (← getEnv).contains ``CoeHTCT then
@@ -188,7 +191,7 @@ where
    go (t : Tree) : StateRefT AnalyzeResult TermElabM Unit := do
      unless (← get).hasUncomparable do
        match t with
-       | Tree.op _ _ lhs rhs => go lhs; go rhs
+       | Tree.op _ _ _ lhs rhs => go lhs; go rhs
        | Tree.term _ val =>
          let type ← instantiateMVars (← inferType val)
          unless isUnknow type do
@@ -209,15 +212,16 @@ private def mkOp (f : Expr) (lhs rhs : Expr) : TermElabM Expr :=
 
 private def toExpr (t : Tree) : TermElabM Expr := do
   match t with
-  | Tree.term _ e         => return e
-  | Tree.op ref f lhs rhs => withRef ref <| mkOp f (← toExpr lhs) (← toExpr rhs)
+  | Tree.term _ e               => return e
+  | Tree.op ref true f lhs rhs  => withRef ref <| mkOp f (← toExpr lhs) (← mkFunUnit (← toExpr rhs))
+  | Tree.op ref false f lhs rhs => withRef ref <| mkOp f (← toExpr lhs) (← toExpr rhs)
 
 private def applyCoe (t : Tree) (maxType : Expr) : TermElabM Tree := do
   go t
 where
   go (t : Tree) : TermElabM Tree := do
     match t with
-    | Tree.op ref f lhs rhs => return Tree.op ref f (← go lhs) (← go rhs)
+    | Tree.op ref lazy f lhs rhs => return Tree.op ref lazy f (← go lhs) (← go rhs)
     | Tree.term ref e       =>
       let type ← inferType e
       trace[Elab.binop] "visiting {e} : {type} =?= {maxType}"
@@ -240,6 +244,9 @@ def elabBinOp : TermElab :=  fun stx expectedType? => do
     trace[Elab.binop] "result: {result}"
     ensureHasType expectedType? result
 
+@[builtinTermElab binop_lazy]
+def elabBinOpLazy : TermElab := elabBinOp
+
 /--
   Decompose `e` into `(r, a, b)`.
 

stage0/src/Lean/Meta/Basic.lean

@@ -481,6 +481,10 @@ def mkLetFVars (xs : Array Expr) (e : Expr) (usedLetOnly := true) : MetaM Expr :
 def mkArrow (d b : Expr) : MetaM Expr :=
   return Lean.mkForall (← mkFreshUserName `x) BinderInfo.default d b
 
+/-- `fun _ : Unit => a` -/
+def mkFunUnit (a : Expr) : MetaM Expr :=
+  return Lean.mkLambda (← mkFreshUserName `x) BinderInfo.default (mkConst ``Unit) a
+
 def elimMVarDeps (xs : Array Expr) (e : Expr) (preserveOrder : Bool := false) : MetaM Expr :=
   if xs.isEmpty then pure e else liftMkBindingM <| MetavarContext.elimMVarDeps xs e preserveOrder
 

stage0/stdlib/Lean/Meta/Basic.c

@@ -74,6 +74,7 @@ lean_object* lean_array_uget(lean_object*, size_t);
 lean_object* lean_io_error_to_string(lean_object*);
 lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_forallMetaTelescopeReducingAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_isReadOnlyExprMVar___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Meta_mkFunUnit(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint64_t lean_uint64_of_nat(lean_object*);
 lean_object* l_Lean_ConstantInfo_numLevelParams(lean_object*);
 static lean_object* l_Lean_getConstInfo___at_Lean_Meta_mkConstWithFreshMVarLevels___spec__1___closed__3;
@@ -89,6 +90,7 @@ lean_object* l_Lean_Meta_savingCache(lean_object*);
 lean_object* l_Lean_Meta_mkConstWithFreshMVarLevels(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_mkFreshExprMVarAt___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_isClassExpensive_x3f_match__1(lean_object*);
+static lean_object* l_Lean_Meta_mkFunUnit___closed__1;
 lean_object* l_Lean_Meta_withMCtx___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_local_ctx_mk_let_decl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t);
 lean_object* l_Lean_Meta_forallMetaTelescope___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -98,6 +100,7 @@ uint8_t l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_beqTransparencyMode_
 lean_object* l_Lean_Meta_ParamInfo_isInstImplicit___boxed(lean_object*);
 lean_object* l_Lean_Meta_mapError(lean_object*, lean_object*);
 extern lean_object* l_Lean_maxRecDepthErrorMessage;
+lean_object* l_Lean_Meta_mkFunUnit___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Meta_instMonadMetaM___closed__1;
 lean_object* lean_array_uset(lean_object*, size_t, lean_object*);
 lean_object* l_Lean_Meta_mkLetFVars(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -151,6 +154,7 @@ lean_object* l_Lean_Meta_mkFreshExprMVarWithId___boxed(lean_object*, lean_object
 static lean_object* l_Lean_Meta_instAlternativeMetaM___lambda__1___closed__2;
 lean_object* l_Lean_Meta_fullApproxDefEq(lean_object*);
 lean_object* l_Lean_Meta_instAlternativeMetaM___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+static lean_object* l_Lean_Meta_mkFunUnit___closed__2;
 lean_object* l_Lean_throwError___at___private_Lean_Meta_Basic_0__Lean_Meta_getConstTemp_x3f___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_withLocalDecls_loop_match__1___rarg(lean_object*, lean_object*);
 lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Meta_Basic_0__Lean_Meta_withNewBinderInfosImp___spec__1(lean_object*, size_t, size_t, lean_object*);
@@ -410,6 +414,7 @@ lean_object* l_Lean_Core_getMaxHeartbeats(lean_object*);
 lean_object* l_Lean_Meta_saveAndResetSynthInstanceCache___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_liftMkBindingM___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_instInhabitedSavedState;
+static lean_object* l_Lean_Meta_mkFunUnit___closed__3;
 lean_object* l_Lean_Meta_instantiateLambda___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_resettingSynthInstanceCacheWhen___rarg(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*);
 extern lean_object* l_Lean_Expr_instHashableExpr;
@@ -471,6 +476,7 @@ lean_object* l_Lean_LocalDecl_toExpr(lean_object*);
 extern lean_object* l_Lean_firstFrontendMacroScope;
 lean_object* l_Lean_Meta_getLocalInstances(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Meta_instInhabitedSavedState___closed__1;
+lean_object* l_Lean_mkLambda(lean_object*, uint8_t, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_ParamInfo_backDeps___default;
 uint8_t l_Lean_Meta_Config_quasiPatternApprox___default;
 lean_object* l_Lean_Meta_instAlternativeMetaM;
@@ -14713,6 +14719,81 @@ lean_dec(x_3);
 return x_8;
 }
 }
+static lean_object* _init_l_Lean_Meta_mkFunUnit___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_mk_string("Unit");
+return x_1;
+}
+}
+static lean_object* _init_l_Lean_Meta_mkFunUnit___closed__2() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = lean_box(0);
+x_2 = l_Lean_Meta_mkFunUnit___closed__1;
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
+}
+}
+static lean_object* _init_l_Lean_Meta_mkFunUnit___closed__3() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = lean_box(0);
+x_2 = l_Lean_Meta_mkFunUnit___closed__2;
+x_3 = l_Lean_mkConst(x_2, x_1);
+return x_3;
+}
+}
+lean_object* l_Lean_Meta_mkFunUnit(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
+_start:
+{
+lean_object* x_7; lean_object* x_8; uint8_t x_9; 
+x_7 = l_Lean_Meta_mkArrow___closed__2;
+x_8 = l___private_Lean_CoreM_0__Lean_Core_mkFreshNameImp(x_7, x_4, x_5, x_6);
+x_9 = !lean_is_exclusive(x_8);
+if (x_9 == 0)
+{
+lean_object* x_10; uint8_t x_11; lean_object* x_12; lean_object* x_13; 
+x_10 = lean_ctor_get(x_8, 0);
+x_11 = 0;
+x_12 = l_Lean_Meta_mkFunUnit___closed__3;
+x_13 = l_Lean_mkLambda(x_10, x_11, x_12, x_1);
+lean_ctor_set(x_8, 0, x_13);
+return x_8;
+}
+else
+{
+lean_object* x_14; lean_object* x_15; uint8_t x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; 
+x_14 = lean_ctor_get(x_8, 0);
+x_15 = lean_ctor_get(x_8, 1);
+lean_inc(x_15);
+lean_inc(x_14);
+lean_dec(x_8);
+x_16 = 0;
+x_17 = l_Lean_Meta_mkFunUnit___closed__3;
+x_18 = l_Lean_mkLambda(x_14, x_16, x_17, x_1);
+x_19 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_19, 0, x_18);
+lean_ctor_set(x_19, 1, x_15);
+return x_19;
+}
+}
+}
+lean_object* l_Lean_Meta_mkFunUnit___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
+_start:
+{
+lean_object* x_7; 
+x_7 = l_Lean_Meta_mkFunUnit(x_1, x_2, x_3, x_4, x_5, x_6);
+lean_dec(x_5);
+lean_dec(x_4);
+lean_dec(x_3);
+lean_dec(x_2);
+return x_7;
+}
+}
 lean_object* l_Lean_Meta_elimMVarDeps(lean_object* x_1, lean_object* x_2, uint8_t x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
 _start:
 {
@@ -29526,6 +29607,12 @@ l_Lean_Meta_mkArrow___closed__1 = _init_l_Lean_Meta_mkArrow___closed__1();
 lean_mark_persistent(l_Lean_Meta_mkArrow___closed__1);
 l_Lean_Meta_mkArrow___closed__2 = _init_l_Lean_Meta_mkArrow___closed__2();
 lean_mark_persistent(l_Lean_Meta_mkArrow___closed__2);
+l_Lean_Meta_mkFunUnit___closed__1 = _init_l_Lean_Meta_mkFunUnit___closed__1();
+lean_mark_persistent(l_Lean_Meta_mkFunUnit___closed__1);
+l_Lean_Meta_mkFunUnit___closed__2 = _init_l_Lean_Meta_mkFunUnit___closed__2();
+lean_mark_persistent(l_Lean_Meta_mkFunUnit___closed__2);
+l_Lean_Meta_mkFunUnit___closed__3 = _init_l_Lean_Meta_mkFunUnit___closed__3();
+lean_mark_persistent(l_Lean_Meta_mkFunUnit___closed__3);
 l___private_Lean_Meta_Basic_0__Lean_Meta_isClassExpensive_x3f___closed__1 = _init_l___private_Lean_Meta_Basic_0__Lean_Meta_isClassExpensive_x3f___closed__1();
 lean_mark_persistent(l___private_Lean_Meta_Basic_0__Lean_Meta_isClassExpensive_x3f___closed__1);
 l_Lean_Meta_getParamNames___lambda__1___boxed__const__1 = _init_l_Lean_Meta_getParamNames___lambda__1___boxed__const__1();