From e6dd41255b128feaab2a85a295c062a736f262de Mon Sep 17 00:00:00 2001
From: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date: Fri, 26 Sep 2025 14:02:55 +1000
Subject: [PATCH] feat: upstream ReduceEval instances from quote4 (#10563)

This PR moves some `ReduceEval` instances about basic types up from the
`quote4` library.
---
 src/Lean/Meta/ReduceEval.lean | 84 +++++++++++++++++++++++++++++++++++
 1 file changed, 84 insertions(+)

diff --git a/src/Lean/Meta/ReduceEval.lean b/src/Lean/Meta/ReduceEval.lean
index bc74d73d46..a4d6ccb662 100644
--- a/src/Lean/Meta/ReduceEval.lean
+++ b/src/Lean/Meta/ReduceEval.lean
@@ -63,4 +63,88 @@ private partial def evalName (e : Expr) : MetaM Name := do
 instance : ReduceEval Name where
   reduceEval := private evalName
 
+private partial def evalList [ReduceEval α] (e : Expr) : MetaM (List α) := do
+  let e ← whnf e
+  let .const c _ := e.getAppFn | throwFailedToEval e
+  let nargs := e.getAppNumArgs
+  match c, nargs with
+    | ``List.nil, 1 => pure []
+    | ``List.cons, 3 => return (← reduceEval (e.getArg! 1)) :: (← evalList (e.getArg! 2))
+    | _, _ => throwFailedToEval e
+
+instance [ReduceEval α] : ReduceEval (List α) where
+  reduceEval := private evalList
+
+instance [NeZero n] : ReduceEval (Fin n) where
+  reduceEval := private fun e => do
+    let e ← whnf e
+    if e.isAppOfArity ``Fin.mk 3 then
+      return Fin.ofNat _ (← reduceEval (e.getArg! 1))
+    else
+      throwFailedToEval e
+
+instance {n : Nat} : ReduceEval (BitVec n) where
+  reduceEval := private fun e => do
+    let e ← whnf e
+    if e.isAppOfArity ``BitVec.ofFin 2 then
+      have : 2^n - 1 + 1 = 2^n := Nat.sub_one_add_one_eq_of_pos (Nat.two_pow_pos n)
+      let _ : ReduceEval (Fin (2^n)) := this ▸ (inferInstanceAs <| ReduceEval (Fin (2^n - 1 + 1)))
+      pure ⟨(← reduceEval (e.getArg! 1))⟩
+    else
+      throwFailedToEval e
+
+instance : ReduceEval Bool where
+  reduceEval := private fun e => do
+    let e ← whnf e
+    if e.isAppOf ``true then
+      pure true
+    else if e.isAppOf ``false then
+      pure false
+    else
+      throwFailedToEval e
+
+instance : ReduceEval BinderInfo where
+  reduceEval := private fun e => do
+    match (← whnf e).constName? with
+    | some ``BinderInfo.default => pure .default
+    | some ``BinderInfo.implicit => pure .implicit
+    | some ``BinderInfo.strictImplicit => pure .strictImplicit
+    | some ``BinderInfo.instImplicit => pure .instImplicit
+    | _ => throwFailedToEval e
+
+instance : ReduceEval Literal where
+  reduceEval := private fun e => do
+    let e ← whnf e
+    if e.isAppOfArity ``Literal.natVal 1 then
+      return .natVal (← reduceEval (e.getArg! 0))
+    else if e.isAppOfArity ``Literal.strVal 1 then
+      return .strVal (← reduceEval (e.getArg! 0))
+    else
+      throwFailedToEval e
+
+instance : ReduceEval MVarId where
+  reduceEval e := private do
+    let e ← whnf e
+    if e.isAppOfArity ``MVarId.mk 1 then
+      return ⟨← reduceEval (e.getArg! 0)⟩
+    else
+      throwFailedToEval e
+
+instance : ReduceEval LevelMVarId where
+  reduceEval e := private do
+    let e ← whnf e
+    if e.isAppOfArity ``LevelMVarId.mk 1 then
+      return ⟨← reduceEval (e.getArg! 0)⟩
+    else
+      throwFailedToEval e
+
+instance : ReduceEval FVarId where
+  reduceEval e := private do
+    let e ← whnf e
+    if e.isAppOfArity ``FVarId.mk 1 then
+      return ⟨← reduceEval (e.getArg! 0)⟩
+    else
+      throwFailedToEval e
+
+
 end Lean.Meta