chore: update stage0

stage0/src/Init/Prelude.lean

@@ -170,7 +170,9 @@ structure Subtype {α : Sort u} (p : α → Prop) where
 /-- Auxiliary Declaration used to implement the notation (a : α) -/
 @[reducible] def typedExpr (α : Sort u) (a : α) : α := a
 
-/-- Auxiliary Declaration used to implement the named patterns `x@p` -/
+/-- Auxiliary Declaration used to implement the named patterns `x@p`
+    -- TODO: add proof for `x = a`
+-/
 @[reducible] def namedPattern {α : Sort u} (x a : α) : α := a
 
 /- Auxiliary axiom used to implement `sorry`. -/

stage0/src/Init/SizeOf.lean

@@ -25,9 +25,13 @@ protected def default.sizeOf (α : Sort u) : α → Nat
 instance (priority := low) (α : Sort u) : SizeOf α where
   sizeOf := default.sizeOf α
 
+@[simp] theorem sizeOf_default (n : α) : sizeOf n = 0 := rfl
+
 instance : SizeOf Nat where
   sizeOf n := n
 
+@[simp] theorem sizeOf_nat (n : Nat) : sizeOf n = n := rfl
+
 deriving instance SizeOf for Prod
 deriving instance SizeOf for PUnit
 deriving instance SizeOf for Bool

stage0/src/Init/WFTactics.lean

@@ -8,7 +8,7 @@ import Init.SizeOf
 import Init.WF
 
 macro "decreasing_tactic" : tactic =>
- `((simp [invImage, InvImage, Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel, sizeOf, WellFoundedRelation.rel];
+ `((simp [invImage, InvImage, Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel, WellFoundedRelation.rel]
     repeat (first | apply Prod.Lex.right | apply Prod.Lex.left)
     repeat (first | apply PSigma.Lex.right | apply PSigma.Lex.left)
     first

stage0/src/Lean/Elab/Match.lean

@@ -493,7 +493,8 @@ partial def main (e : Expr) : M Pattern := do
     | some (α, lits) =>
       return Pattern.arrayLit α (← lits.mapM main)
     | none =>
-      if e.isAppOfArity `namedPattern 3 then
+      -- TODO: namedPattern will have 4 arguments
+      if e.isAppOfArity ``_root_.namedPattern 3 then
         let p ← main <| e.getArg! 2
         match e.getArg! 1 with
         | Expr.fvar fvarId _ => return Pattern.as fvarId p

stage0/src/Lean/Elab/PatternVar.lean

@@ -201,10 +201,14 @@ partial def collect (stx : Syntax) : M Syntax := withRef stx <| withFreshMacroSc
     processCtor stx[0]
   else if k == ``Lean.Parser.Term.namedPattern then
     /- Recall that
-      def namedPattern := check... >> trailing_parser "@" >> termParser -/
+      ```
+      def namedPattern := check... >> trailing_parser "@" >> optional (atomic (ident >> ":")) >> termParser
+      ```
+      TODO: pattern variable for equality proof
+     -/
     let id := stx[0]
     discard <| processVar id
-    let pat := stx[2]
+    let pat := stx[3]
     let pat ← collect pat
     `(_root_.namedPattern $id $pat)
   else if k == ``Lean.Parser.Term.binop then

stage0/src/Lean/Meta/Match/Basic.lean

@@ -15,6 +15,7 @@ inductive Pattern : Type where
   | ctor         (ctorName : Name) (us : List Level) (params : List Expr) (fields : List Pattern) : Pattern
   | val          (e : Expr) : Pattern
   | arrayLit     (type : Expr) (xs : List Pattern) : Pattern
+  -- TODO: add case for equality
   | as           (varId : FVarId) (p : Pattern) : Pattern
   deriving Inhabited
 
@@ -42,6 +43,7 @@ where
     | var fvarId                     => pure $ mkFVar fvarId
     | val e                          => pure e
     | as fvarId p                    =>
+      -- TODO
       if annotate then
         mkAppM `namedPattern #[mkFVar fvarId, (← visit p)]
       else
@@ -275,7 +277,8 @@ partial def toPattern (e : Expr) : MetaM Pattern := do
     | some (α, lits) =>
       return Pattern.arrayLit α (← lits.mapM toPattern)
     | none =>
-      if e.isAppOfArity `namedPattern 3 then
+      -- TODO: `namedPattern` will have 4 arguments
+      if e.isAppOfArity ``namedPattern 3 then
         let p ← toPattern <| e.getArg! 2
         match e.getArg! 1 with
         | Expr.fvar fvarId _ => return Pattern.as fvarId p

stage0/src/Lean/Meta/SizeOf.lean

@@ -393,6 +393,7 @@ end SizeOfSpecNested
 private def mkSizeOfSpecTheorem (indInfo : InductiveVal) (sizeOfFns : Array Name) (recMap : NameMap Name) (ctorName : Name) : MetaM Unit := do
   let ctorInfo ← getConstInfoCtor ctorName
   let us := ctorInfo.levelParams.map mkLevelParam
+  let simpAttr ← ofExcept <| getAttributeImpl (← getEnv) `simp
   forallTelescopeReducing ctorInfo.type fun xs _ => do
     let params := xs[:ctorInfo.numParams]
     let fields := xs[ctorInfo.numParams:]
@@ -415,12 +416,14 @@ private def mkSizeOfSpecTheorem (indInfo : InductiveVal) (sizeOfFns : Array Name
         else
           mkEqRefl rhs
       let thmValue ← mkLambdaFVars thmParams thmValue
+      trace[Meta.sizeOf] "sizeOf spec theorem: {thmName}"
       addDecl <| Declaration.thmDecl {
         name        := thmName
         levelParams := ctorInfo.levelParams
         type        := thmType
         value       := thmValue
       }
+      simpAttr.add thmName default AttributeKind.global
 
 private def mkSizeOfSpecTheorems (indTypeNames : Array Name) (sizeOfFns : Array Name) (recMap : NameMap Name) : MetaM Unit := do
   for indTypeName in indTypeNames do

stage0/src/Lean/Parser/Term.lean

@@ -265,7 +265,7 @@ def isIdent (stx : Syntax) : Bool :=
   stx.isAntiquot || stx.isIdent
 
 @[builtinTermParser] def explicitUniv : TrailingParser := trailing_parser checkStackTop isIdent "expected preceding identifier" >> checkNoWsBefore "no space before '.{'" >> ".{" >> sepBy1 levelParser ", " >> "}"
-@[builtinTermParser] def namedPattern : TrailingParser := trailing_parser checkStackTop isIdent "expected preceding identifier" >> checkNoWsBefore "no space before '@'" >> "@" >> termParser maxPrec
+@[builtinTermParser] def namedPattern : TrailingParser := trailing_parser checkStackTop isIdent "expected preceding identifier" >> checkNoWsBefore "no space before '@'" >> "@" >> optional (atomic (ident >> ":")) >> termParser maxPrec
 
 @[builtinTermParser] def pipeProj   := trailing_parser:minPrec " |>." >> checkNoWsBefore >> (fieldIdx <|> ident) >> many argument
 @[builtinTermParser] def pipeCompletion := trailing_parser:minPrec " |>."

stage0/src/library/compiler/ir_interpreter.cpp

@@ -1047,8 +1047,9 @@ optional<name> get_sorry_dep(environment const & env, name const & n) {
 }
 
 object * run_boxed(environment const & env, options const & opts, name const & fn, unsigned n, object **args) {
-    if (get_sorry_dep(env, fn)) {
-        throw exception("cannot evaluate code because it uses 'sorry' and/or contains errors");
+    if (optional<name> decl_with_sorry = get_sorry_dep(env, fn)) {
+        throw exception(sstream() << "cannot evaluate code because '" << *decl_with_sorry
+            << "' uses 'sorry' and/or contains errors");
     }
     return interpreter::with_interpreter<object *>(env, opts, fn, [&](interpreter & interp) { return interp.call_boxed(fn, n, args); });
 }

stage0/stdlib/Lean/Elab/Match.c

@@ -24976,7 +24976,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; 
 x_1 = l___private_Lean_Elab_Match_0__Lean_Elab_Term_isMatchUnit_x3f___closed__4;
 x_2 = l___private_Lean_Elab_Match_0__Lean_Elab_Term_isMatchUnit_x3f___closed__5;
-x_3 = lean_unsigned_to_nat(757u);
+x_3 = lean_unsigned_to_nat(758u);
 x_4 = lean_unsigned_to_nat(2u);
 x_5 = l___private_Lean_Elab_Match_0__Lean_Elab_Term_isMatchUnit_x3f___closed__3;
 x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

stage0/stdlib/Lean/Elab/PatternVar.c

@@ -5885,7 +5885,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; 
 x_1 = l_Lean_Elab_Term_CollectPatternVars_collect_pushNewArg___closed__1;
 x_2 = l_Lean_Elab_Term_CollectPatternVars_collect_pushNewArg___closed__2;
-x_3 = lean_unsigned_to_nat(267u);
+x_3 = lean_unsigned_to_nat(271u);
 x_4 = lean_unsigned_to_nat(11u);
 x_5 = l_Lean_Elab_Term_CollectPatternVars_collect_pushNewArg___closed__3;
 x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@@ -6439,7 +6439,7 @@ lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16;
 x_13 = lean_ctor_get(x_12, 1);
 lean_inc(x_13);
 lean_dec(x_12);
-x_14 = lean_unsigned_to_nat(2u);
+x_14 = lean_unsigned_to_nat(3u);
 x_15 = l_Lean_Syntax_getArg(x_3, x_14);
 lean_inc(x_10);
 lean_inc(x_9);