chore: update stage0

We need it because we have changed the `SimpLemma` representation and
they are stored in the .olean files.

stage0/src/Lean/Elab/Tactic/Simp.lean

@@ -38,14 +38,7 @@ def elabSimpConfig (optConfig : Syntax) (ctx : Bool) : TermElabM Meta.Simp.Confi
       else
         evalSimpConfig (← instantiateMVars c)
 
-private def elabSimpLemmaTerm (stx : Syntax) : TacticM Expr := do
-  withRef stx <| Term.withoutErrToSorry do
-    let e ← Term.elabTerm stx none
-    Term.synthesizeSyntheticMVarsUsingDefault
-    let e ← instantiateMVars e
-    return e.eta
-
-private def addLemma (lemmas : Meta.SimpLemmas) (e : Expr) (post : Bool): MetaM Meta.SimpLemmas := do
+private def addDeclToUnfoldOrLemma (lemmas : Meta.SimpLemmas) (e : Expr) (post : Bool) : MetaM Meta.SimpLemmas := do
   if e.isConst then
     let declName := e.constName!
     let info ← getConstInfo declName
@@ -54,7 +47,20 @@ private def addLemma (lemmas : Meta.SimpLemmas) (e : Expr) (post : Bool): MetaM
     else
       lemmas.addDeclToUnfold declName
   else
-    lemmas.add e post
+    lemmas.add #[] e post
+
+private def addSimpLemma (lemmas : Meta.SimpLemmas) (stx : Syntax) (post : Bool) : TermElabM Meta.SimpLemmas := do
+  let (levelParams, proof) ← Term.withoutModifyingElabMetaState <| withRef stx <| Term.withoutErrToSorry do
+    let e ← Term.elabTerm stx none
+    Term.synthesizeSyntheticMVarsUsingDefault
+    let e ← instantiateMVars e
+    let e := e.eta
+    if e.hasMVar then
+      let r ← abstractMVars e
+      return (r.paramNames, r.expr)
+    else
+      return (#[], e)
+  lemmas.add levelParams proof
 
 /--
   Elaborate extra simp lemmas provided to `simp`. `stx` is of the `simpLemma,*`
@@ -89,10 +95,8 @@ private def elabSimpLemmas (stx : Syntax) (ctx : Simp.Context) (eraseLocal : Boo
             else
               arg[0][0].getKind == ``Parser.Tactic.simpPost
           match (← resolveSimpIdLemma? arg[1]) with
-          | some e => lemmas ← addLemma lemmas e post
-          | _ =>
-            let e ← elabSimpLemmaTerm arg[1]
-            lemmas ← addLemma lemmas e post
+          | some e => lemmas ← addDeclToUnfoldOrLemma lemmas e post
+          | _      => lemmas ← addSimpLemma lemmas arg[1] post
       return { ctx with simpLemmas := lemmas }
 where
   resolveSimpIdLemma? (simpArgTerm : Syntax) : TacticM (Option Expr) := do
@@ -118,6 +122,7 @@ private def mkSimpContext (stx : Syntax) (eraseLocal : Bool) (ctx := false) : Ta
 -/
 @[builtinTactic Lean.Parser.Tactic.simp] def evalSimp : Tactic := fun stx => do
   let ctx  ← mkSimpContext stx (eraseLocal := false)
+  -- trace[Meta.debug] "Lemmas {← toMessageData ctx.simpLemmas.post}"
   let loc := expandOptLocation stx[4]
   match loc with
   | Location.targets hUserNames simpTarget =>

stage0/src/Lean/Meta/Tactic/Simp/Main.lean

@@ -254,7 +254,7 @@ where
       let mut updated := false
       for x in xs do
         if (← isProof x) then
-          s ← s.add x
+          s ← s.add #[] x
           updated := true
       if updated then
         withSimpLemmas s f
@@ -284,7 +284,7 @@ where
       trace[Debug.Meta.Tactic.simp] "ctx arrow {rp.expr} -> {q}"
       withLocalDeclD e.bindingName! rp.expr fun h => do
         let s ← getSimpLemmas
-        let s ← s.add h
+        let s ← s.add #[] h
         withSimpLemmas s do
           let rq ← simp q
           match rq.proof? with

stage0/src/Lean/Meta/Tactic/Simp/SimpAll.lean

@@ -36,7 +36,7 @@ private def initEntries : M Unit := do
       let fvarId := localDecl.fvarId
       let proof  := localDecl.toExpr
       let id     ← mkFreshUserName `h
-      let simpLemmas ← (← get).ctx.simpLemmas.add proof (name? := id)
+      let simpLemmas ← (← get).ctx.simpLemmas.add #[] proof (name? := id)
       let entry : Entry := { fvarId := fvarId, userName := localDecl.userName, id := id, type := (← instantiateMVars localDecl.type), proof := proof }
       modify fun s => { s with entries := s.entries.push entry, ctx.simpLemmas := simpLemmas }
 
@@ -57,7 +57,7 @@ private partial def loop : M Bool := do
     | some (proofNew, typeNew) =>
       unless typeNew == entry.type do
         let id ← mkFreshUserName `h
-        let simpLemmasNew ← (← getSimpLemmas).add proofNew (name? := id)
+        let simpLemmasNew ← (← getSimpLemmas).add #[] proofNew (name? := id)
         modify fun s => { s with
           modified       := true
           ctx.simpLemmas := simpLemmasNew

stage0/src/Lean/Meta/Tactic/Simp/SimpLemmas.lean

@@ -8,22 +8,26 @@ import Lean.Util.Recognizers
 import Lean.Meta.LevelDefEq
 import Lean.Meta.DiscrTree
 import Lean.Meta.AppBuilder
-import Lean.Meta.AbstractMVars
 import Lean.Meta.Tactic.AuxLemma
 namespace Lean.Meta
 
-inductive SimpLemma.Proof where
-  | expr (val : Expr)
-  | abst (val : AbstractMVarsResult)
-  deriving Inhabited, BEq
+/--
+  The fields `levelParams` and `proof` are used to encode the proof of the simp lemma.
+  If the `proof` is a global declaration `c`, we store `Expr.const c []` at `proof` without the universe levels, and `levelParams` is set to `#[]`
+  When using the lemma, we create fresh universe metavariables.
+  Motivation: most simp lemmas are global declarations, and this approach is faster and saves memory.
 
+  The field `levelParams` is not empty only when we elaborate an expression provided by the user, and it contains universe metavariables.
+  Then, we use `abstractMVars` to abstract the universe metavariables and create new fresh universe parameters that are stored at the field `levelParams`.
+-/
 structure SimpLemma where
-  keys     : Array DiscrTree.Key
-  val      : SimpLemma.Proof
-  priority : Nat
-  post     : Bool
-  perm     : Bool -- true is lhs and rhs are identical modulo permutation of variables
-  name?    : Option Name := none -- for debugging and tracing purposes
+  keys        : Array DiscrTree.Key
+  levelParams : Array Name -- non empty for local universe polymorhic proofs.
+  proof       : Expr
+  priority    : Nat
+  post        : Bool
+  perm        : Bool -- true is lhs and rhs are identical modulo permutation of variables
+  name?       : Option Name := none -- for debugging and tracing purposes
   deriving Inhabited
 
 def SimpLemma.getName (s : SimpLemma) : Name :=
@@ -42,7 +46,7 @@ instance : ToMessageData SimpLemma where
   toMessageData s := fmt s
 
 instance : BEq SimpLemma where
-  beq e₁ e₂ := e₁.val == e₂.val
+  beq e₁ e₂ := e₁.proof == e₂.proof
 
 structure SimpLemmas where
   pre         : DiscrTree SimpLemma := DiscrTree.empty
@@ -145,7 +149,7 @@ private def checkTypeIsProp (type : Expr) : MetaM Unit :=
   unless (← isProp type) do
     throwError "invalid 'simp', proposition expected{indentExpr type}"
 
-def mkSimpLemmaCore (e : Expr) (val : Expr) (post : Bool) (prio : Nat) (name? : Option Name) : MetaM SimpLemma := do
+private def mkSimpLemmaCore (e : Expr) (levelParams : Array Name) (proof : Expr) (post : Bool) (prio : Nat) (name? : Option Name) : MetaM SimpLemma := do
   let type ← instantiateMVars (← inferType e)
   withNewMCtxDepth do
     let (xs, _, type) ← withReducible <| forallMetaTelescopeReducing type
@@ -153,9 +157,9 @@ def mkSimpLemmaCore (e : Expr) (val : Expr) (post : Bool) (prio : Nat) (name? :
       match type.eq? with
       | some (_, lhs, rhs) => pure (← DiscrTree.mkPath lhs, ← isPerm lhs rhs)
       | none => throwError "unexpected kind of 'simp' lemma"
-    return { keys := keys, perm := perm, post := post, val := SimpLemma.Proof.expr val, name? := name?, priority := prio }
+    return { keys := keys, perm := perm, post := post, levelParams := levelParams, proof := proof, name? := name?, priority := prio }
 
-def mkSimpLemmasFromConst (declName : Name) (post : Bool) (prio : Nat) : MetaM (Array SimpLemma) := do
+private def mkSimpLemmasFromConst (declName : Name) (post : Bool) (prio : Nat) : MetaM (Array SimpLemma) := do
   let cinfo ← getConstInfo declName
   let val := mkConst declName (cinfo.levelParams.map mkLevelParam)
   withReducible do
@@ -165,10 +169,10 @@ def mkSimpLemmasFromConst (declName : Name) (post : Bool) (prio : Nat) : MetaM (
       let mut r := #[]
       for (val, type) in (← preprocess val type) do
         let auxName ← mkAuxLemma cinfo.levelParams type val
-        r := r.push <| (← mkSimpLemmaCore (mkConst auxName (cinfo.levelParams.map mkLevelParam)) (mkConst auxName) post prio declName)
+        r := r.push <| (← mkSimpLemmaCore (mkConst auxName (cinfo.levelParams.map mkLevelParam)) #[] (mkConst auxName) post prio declName)
       return r
     else
-      #[← mkSimpLemmaCore (mkConst declName (cinfo.levelParams.map mkLevelParam)) (mkConst declName) post prio declName]
+      #[← mkSimpLemmaCore (mkConst declName (cinfo.levelParams.map mkLevelParam)) #[] (mkConst declName) post prio declName]
 
 def addSimpLemma (declName : Name) (post : Bool) (attrKind : AttributeKind) (prio : Nat) : MetaM Unit := do
   let simpLemmas ← mkSimpLemmasFromConst declName post prio
@@ -206,28 +210,37 @@ def SimpLemmas.addConst (s : SimpLemmas) (declName : Name) (post : Bool := true)
   let simpLemmas ← mkSimpLemmasFromConst declName post prio
   return simpLemmas.foldl addSimpLemmaEntry s
 
-/- Auxiliary method for creating simp lemmas from a proof term `val`. -/
-def mkSimpLemmas (val : Expr) (post : Bool := true) (prio : Nat := eval_prio default) (name? : Option Name := none): MetaM (Array SimpLemma) :=
-  withReducible do
-    let type ← inferType val
-    checkTypeIsProp type
-    if (← shouldPreprocess type) then
-      let mut r := #[]
-      for (val, _) in (← preprocess val type) do
-        r := r.push <| (← mkSimpLemmaCore val val post prio name?)
-      return r
+def SimpLemma.getValue (simpLemma : SimpLemma) : MetaM Expr := do
+  if simpLemma.proof.isConst && simpLemma.levelParams.isEmpty then
+    let info ← getConstInfo simpLemma.proof.constName!
+    if info.levelParams.isEmpty then
+      return simpLemma.proof
     else
-      #[← mkSimpLemmaCore val val post prio name?]
+      return simpLemma.proof.updateConst! (← info.levelParams.mapM (fun _ => mkFreshLevelMVar))
+  else
+    let us ← simpLemma.levelParams.mapM fun _ => mkFreshLevelMVar
+    simpLemma.proof.instantiateLevelParamsArray simpLemma.levelParams us
+
+private def preprocessProof (val : Expr) : MetaM (Array Expr) := do
+  let type ← inferType val
+  checkTypeIsProp type
+  let ps ← preprocess val type
+  return ps.toArray.map fun (val, _) => val
+
+/- Auxiliary method for creating simp lemmas from a proof term `val`. -/
+def mkSimpLemmas (levelParams : Array Name) (proof : Expr) (post : Bool := true) (prio : Nat := eval_prio default) (name? : Option Name := none): MetaM (Array SimpLemma) :=
+  withReducible do
+    (← preprocessProof proof).mapM fun val => mkSimpLemmaCore val levelParams val post prio name?
 
 /- Auxiliary method for adding a local simp lemma to a `SimpLemmas` datastructure. -/
-def SimpLemmas.add (s : SimpLemmas) (e : Expr) (post : Bool := true) (prio : Nat := eval_prio default) (name? : Option Name := none): MetaM SimpLemmas := do
-  if e.isConst then
-    s.addConst e.constName! post prio
+def SimpLemmas.add (s : SimpLemmas) (levelParams : Array Name) (proof : Expr) (post : Bool := true) (prio : Nat := eval_prio default) (name? : Option Name := none): MetaM SimpLemmas := do
+  if proof.isConst then
+    s.addConst proof.constName! post prio
   else
-    let simpLemmas ← mkSimpLemmas e post prio (← getName?)
+    let simpLemmas ← mkSimpLemmas levelParams proof post prio (← getName? proof)
     return simpLemmas.foldl addSimpLemmaEntry s
 where
-  getName? : MetaM (Option Name) := do
+  getName? (e : Expr) : MetaM (Option Name) := do
     match name? with
     | some _ => return name?
     | none   =>
@@ -240,15 +253,4 @@ where
       else
         return none
 
-def SimpLemma.getValue (simpLemma : SimpLemma) : MetaM Expr := do
-  match simpLemma.val with
-  | Proof.expr e@(Expr.const declName [] _) =>
-    let info ← getConstInfo declName
-    if info.levelParams.isEmpty then
-      return e
-    else
-      return e.updateConst! (← info.levelParams.mapM (fun _ => mkFreshLevelMVar))
-  | Proof.expr e => return e
-  | _ => throwError "NIY"
-
 end Lean.Meta

stage0/stdlib/Lean/Meta/Tactic/Simp/Rewrite.c

@@ -3410,7 +3410,7 @@ uint8_t l_Lean_Meta_Simp_rewrite_inErasedSet(lean_object* x_1, lean_object* x_2)
 _start:
 {
 lean_object* x_3; 
-x_3 = lean_ctor_get(x_2, 3);
+x_3 = lean_ctor_get(x_2, 4);
 if (lean_obj_tag(x_3) == 0)
 {
 uint8_t x_4; 
@@ -3740,7 +3740,7 @@ lean_object* l_Lean_Meta_Simp_rewrite_tryLemma_x3f___lambda__4(lean_object* x_1,
 _start:
 {
 uint8_t x_14; 
-x_14 = lean_ctor_get_uint8(x_3, sizeof(void*)*4 + 1);
+x_14 = lean_ctor_get_uint8(x_3, sizeof(void*)*5 + 1);
 if (x_14 == 0)
 {
 lean_object* x_15; lean_object* x_16; 
@@ -4642,10 +4642,6 @@ _start:
 {
 lean_object* x_9; 
 x_9 = l_Lean_Meta_Simp_rewrite_tryLemma_x3f___lambda__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
-lean_dec(x_7);
-lean_dec(x_6);
-lean_dec(x_5);
-lean_dec(x_4);
 lean_dec(x_3);
 lean_dec(x_2);
 return x_9;
@@ -4734,10 +4730,10 @@ x_6 = lean_unsigned_to_nat(1u);
 x_7 = lean_nat_sub(x_2, x_6);
 x_8 = lean_array_fget(x_1, x_2);
 x_9 = lean_array_fget(x_1, x_7);
-x_10 = lean_ctor_get(x_8, 2);
+x_10 = lean_ctor_get(x_8, 3);
 lean_inc(x_10);
 lean_dec(x_8);
-x_11 = lean_ctor_get(x_9, 2);
+x_11 = lean_ctor_get(x_9, 3);
 lean_inc(x_11);
 lean_dec(x_9);
 x_12 = lean_nat_dec_lt(x_10, x_11);