refactor: use LitValue.lean to implement simprocs

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import Lean.Meta.LitValues
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int
 import Init.Data.BitVec.Basic
@@ -18,39 +19,13 @@ structure Literal where
   /-- Actual value. -/
   value : BitVec n
 
-/--
-Try to convert an `OfNat.ofNat`-application into a bitvector literal.
--/
-private def fromOfNatExpr? (e : Expr) : SimpM (Option Literal) := OptionT.run do
-  guard (e.isAppOfArity ``OfNat.ofNat 3)
-  let type ← whnf e.appFn!.appFn!.appArg!
-  guard (type.isAppOfArity ``BitVec 1)
-  let n ← Nat.fromExpr? type.appArg!
-  let v ← Nat.fromExpr? e.appFn!.appArg!
-  return { n, value := BitVec.ofNat n v }
-
-/--
-Try to convert an `BitVec.ofNat`-application into a bitvector literal.
--/
-private def fromBitVecExpr? (e : Expr) : SimpM (Option Literal) := OptionT.run do
-  guard (e.isAppOfArity ``BitVec.ofNat 2)
-  let n ← Nat.fromExpr? e.appFn!.appArg!
-  let v ← Nat.fromExpr? e.appArg!
-  return { n, value := BitVec.ofNat n v }
-
 /--
 Try to convert `OfNat.ofNat`/`BitVec.OfNat` application into a
 bitvector literal.
 -/
-def fromExpr? (e : Expr) : SimpM (Option Literal) := OptionT.run do
-  fromBitVecExpr? e <|> fromOfNatExpr? e
-
-/--
-Convert a bitvector literal into an expression.
--/
--- Using `BitVec.ofNat` because it is being used in `simp` theorems
-def Literal.toExpr (lit : Literal) : Expr :=
-  mkApp2 (mkConst ``BitVec.ofNat) (mkNatLit lit.n) (mkNatLit lit.value.toNat)
+def fromExpr? (e : Expr) : SimpM (Option Literal) := do
+  let some ⟨n, value⟩ ← getBitVecValue? e | return none
+  return some { n, value }
 
 /--
 Helper function for reducing homogenous unary bitvector operators.
@@ -59,8 +34,7 @@ Helper function for reducing homogenous unary bitvector operators.
     (op : {n : Nat} → BitVec n → BitVec n) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue
   let some v ← fromExpr? e.appArg! | return .continue
-  let v := { v with value := op v.value }
-  return .done { expr := v.toExpr }
+  return .done { expr := toExpr (op v.value) }
 
 /--
 Helper function for reducing homogenous binary bitvector operators.
@@ -72,8 +46,7 @@ Helper function for reducing homogenous binary bitvector operators.
   let some v₂ ← fromExpr? e.appArg! | return .continue
   if h : v₁.n = v₂.n then
     trace[Meta.debug] "reduce [{declName}] {v₁.value}, {v₂.value}"
-    let v := { v₁ with value := op v₁.value (h ▸ v₂.value) }
-    return .done { expr := v.toExpr }
+    return .done { expr := toExpr (op v₁.value (h ▸ v₂.value)) }
   else
     return .continue
 
@@ -83,8 +56,7 @@ Helper function for reducing homogenous binary bitvector operators.
   unless e.isAppOfArity declName 3 do return .continue
   let some v ← fromExpr? e.appArg! | return .continue
   let some n ← Nat.fromExpr? e.appFn!.appArg! | return .continue
-  let lit : Literal := { n, value := op n v.value }
-  return .done { expr := lit.toExpr }
+  return .done { expr := toExpr (op n v.value) }
 
 /--
 Helper function for reducing bitvector functions such as `getLsb` and `getMsb`.
@@ -105,8 +77,7 @@ Helper function for reducing bitvector functions such as `shiftLeft` and `rotate
   unless e.isAppOfArity declName arity do return .continue
   let some v ← fromExpr? e.appFn!.appArg! | return .continue
   let some i ← Nat.fromExpr? e.appArg! | return .continue
-  let v := { v with value := op v.value i }
-  return .done { expr := v.toExpr }
+  return .done { expr := toExpr (op v.value i) }
 
 /--
 Helper function for reducing bitvector predicates.
@@ -194,16 +165,14 @@ builtin_simproc [simp, seval] reduceAppend ((_ ++ _ : BitVec _)) := fun e => do
   unless e.isAppOfArity ``HAppend.hAppend 6 do return .continue
   let some v₁ ← fromExpr? e.appFn!.appArg! | return .continue
   let some v₂ ← fromExpr? e.appArg! | return .continue
-  let v : Literal := { n := v₁.n + v₂.n, value := v₁.value ++ v₂.value }
-  return .done { expr := v.toExpr }
+  return .done { expr := toExpr (v₁.value ++ v₂.value) }
 
 /-- Simplification procedure for casting `BitVec`s along an equality of the size. -/
 builtin_simproc [simp, seval] reduceCast (cast _ _) := fun e => do
   unless e.isAppOfArity ``cast 4 do return .continue
   let some v ← fromExpr? e.appArg! | return .continue
   let some m ← Nat.fromExpr? e.appFn!.appFn!.appArg! | return .continue
-  let v : Literal := { n := m, value := BitVec.ofNat m v.value.toNat }
-  return .done { expr := v.toExpr }
+  return .done { expr := toExpr (BitVec.ofNat m v.value.toNat) }
 
 /-- Simplification procedure for `BitVec.toNat`. -/
 builtin_simproc [simp, seval] reduceToNat (BitVec.toNat _) := fun e => do
@@ -215,15 +184,14 @@ builtin_simproc [simp, seval] reduceToNat (BitVec.toNat _) := fun e => do
 builtin_simproc [simp, seval] reduceToInt (BitVec.toInt _) := fun e => do
   unless e.isAppOfArity ``BitVec.toInt 2 do return .continue
   let some v ← fromExpr? e.appArg! | return .continue
-  return .done { expr := Int.toExpr v.value.toInt }
+  return .done { expr := toExpr v.value.toInt }
 
 /-- Simplification procedure for `BitVec.ofInt`. -/
 builtin_simproc [simp, seval] reduceOfInt (BitVec.ofInt _ _) := fun e => do
   unless e.isAppOfArity ``BitVec.ofInt 2 do return .continue
   let some n ← Nat.fromExpr? e.appFn!.appArg! | return .continue
   let some i ← Int.fromExpr? e.appArg! | return .continue
-  let lit : Literal := { n, value := BitVec.ofInt n i }
-  return .done { expr := lit.toExpr }
+  return .done { expr := toExpr (BitVec.ofInt n i) }
 
 /-- Simplification procedure for ensuring `BitVec.ofNat` literals are normalized. -/
 builtin_simproc [simp, seval] reduceOfNat (BitVec.ofNat _ _) := fun e => do
@@ -232,7 +200,7 @@ builtin_simproc [simp, seval] reduceOfNat (BitVec.ofNat _ _) := fun e => do
   let some v ← Nat.fromExpr? e.appArg! | return .continue
   let bv := BitVec.ofNat n v
   if bv.toNat == v then return .continue -- already normalized
-  return .done { expr := { n, value := BitVec.ofNat n v : Literal }.toExpr }
+  return .done { expr := toExpr (BitVec.ofNat n v) }
 
 /-- Simplification procedure for `<` on `BitVec`s. -/
 builtin_simproc [simp, seval] reduceLT (( _ : BitVec _) < _)  := reduceBinPred ``LT.lt 4 (· < ·)
@@ -262,8 +230,7 @@ builtin_simproc [simp, seval] reduceZeroExtend' (zeroExtend' _ _) := fun e => do
   let some v ← fromExpr? e.appArg! | return .continue
   let some w ← Nat.fromExpr? e.appFn!.appFn!.appArg! | return .continue
   if h : v.n ≤ w then
-    let lit : Literal := { n := w, value := v.value.zeroExtend' h }
-    return .done { expr := lit.toExpr }
+    return .done { expr := toExpr (v.value.zeroExtend' h) }
   else
     return .continue
 
@@ -272,8 +239,7 @@ builtin_simproc [simp, seval] reduceShiftLeftZeroExtend (shiftLeftZeroExtend _ _
   unless e.isAppOfArity ``shiftLeftZeroExtend 3 do return .continue
   let some v ← fromExpr? e.appFn!.appArg! | return .continue
   let some m ← Nat.fromExpr? e.appArg! | return .continue
-  let lit : Literal := { n := v.n + m, value := v.value.shiftLeftZeroExtend m }
-  return .done { expr := lit.toExpr }
+  return .done { expr := toExpr (v.value.shiftLeftZeroExtend m) }
 
 /-- Simplification procedure for `extractLsb'` on `BitVec`s. -/
 builtin_simproc [simp, seval] reduceExtracLsb' (extractLsb' _ _ _) := fun e => do
@@ -281,16 +247,14 @@ builtin_simproc [simp, seval] reduceExtracLsb' (extractLsb' _ _ _) := fun e => d
   let some v ← fromExpr? e.appArg! | return .continue
   let some start ← Nat.fromExpr? e.appFn!.appFn!.appArg! | return .continue
   let some len ← Nat.fromExpr? e.appFn!.appArg! | return .continue
-  let lit : Literal := { n := len, value := v.value.extractLsb' start len }
-  return .done { expr := lit.toExpr }
+  return .done { expr := toExpr (v.value.extractLsb' start len) }
 
 /-- Simplification procedure for `replicate` on `BitVec`s. -/
 builtin_simproc [simp, seval] reduceReplicate (replicate _ _) := fun e => do
   unless e.isAppOfArity ``replicate 3 do return .continue
   let some v ← fromExpr? e.appArg! | return .continue
   let some w ← Nat.fromExpr? e.appFn!.appArg! | return .continue
-  let lit : Literal := { n := v.n * w, value := v.value.replicate w }
-  return .done { expr := lit.toExpr }
+  return .done { expr := toExpr (v.value.replicate w) }
 
 /-- Simplification procedure for `zeroExtend` on `BitVec`s. -/
 builtin_simproc [simp, seval] reduceZeroExtend (zeroExtend _ _) := reduceExtend ``zeroExtend zeroExtend
@@ -302,7 +266,6 @@ builtin_simproc [simp, seval] reduceSignExtend (signExtend _ _) := reduceExtend
 builtin_simproc [simp, seval] reduceAllOnes (allOnes _) := fun e => do
   unless e.isAppOfArity ``allOnes 1 do return .continue
   let some n ← Nat.fromExpr? e.appArg! | return .continue
-  let lit : Literal := { n, value := allOnes n }
-  return .done { expr := lit.toExpr }
+  return .done { expr := toExpr (allOnes n) }
 
 end BitVec

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Char.lean

@@ -5,15 +5,14 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.ToExpr
+import Lean.Meta.LitValues
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
 
 namespace Char
 open Lean Meta Simp
 
-def fromExpr? (e : Expr) : SimpM (Option Char) := OptionT.run do
-  guard (e.isAppOfArity ``Char.ofNat 1)
-  let value ← Nat.fromExpr? e.appArg!
-  return Char.ofNat value
+def fromExpr? (e : Expr) : SimpM (Option Char) :=
+  getCharValue? e
 
 @[inline] def reduceUnary [ToExpr α] (declName : Name) (op : Char → α) (arity : Nat := 1) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue
@@ -45,7 +44,7 @@ builtin_simproc [simp, seval] reduceToString (toString (_ : Char)) := reduceUnar
 builtin_simproc [simp, seval] reduceVal (Char.val _) := fun e => do
   unless e.isAppOfArity ``Char.val 1 do return .continue
   let some c ← fromExpr? e.appArg! | return .continue
-  return .done { expr := UInt32.toExprCore c.val }
+  return .done { expr := toExpr c.val }
 builtin_simproc [simp, seval] reduceEq  (( _ : Char) = _)  := reduceBinPred ``Eq 3 (. = .)
 builtin_simproc [simp, seval] reduceNe  (( _ : Char) ≠ _)  := reduceBinPred ``Ne 3 (. ≠ .)
 builtin_simproc [simp, seval] reduceBEq  (( _ : Char) == _)  := reduceBoolPred ``BEq.beq 4 (. == .)

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.lean

@@ -5,37 +5,29 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.ToExpr
+import Lean.Meta.LitValues
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
 
 namespace Fin
 open Lean Meta Simp
 
 structure Value where
-  ofNatFn   : Expr
-  size      : Nat
-  value     : Nat
+  n     : Nat
+  value : Fin n
 
-def fromExpr? (e : Expr) : SimpM (Option Value) := OptionT.run do
-  guard (e.isAppOfArity ``OfNat.ofNat 3)
-  let type ← whnf e.appFn!.appFn!.appArg!
-  guard (type.isAppOfArity ``Fin 1)
-  let size ← Nat.fromExpr? type.appArg!
-  guard (size > 0)
-  let value ← Nat.fromExpr? e.appFn!.appArg!
-  let value := value % size
-  return { size, value, ofNatFn := e.appFn!.appFn! }
+def fromExpr? (e : Expr) : SimpM (Option Value) := do
+  let some ⟨n, value⟩ ← getFinValue? e | return none
+  return some { n, value }
 
-def Value.toExpr (v : Value) : Expr :=
-  let vExpr := mkRawNatLit v.value
-  mkApp2 v.ofNatFn vExpr (mkApp2 (mkConst ``Fin.instOfNat) (Lean.toExpr (v.size - 1)) vExpr)
-
-@[inline] def reduceBin (declName : Name) (arity : Nat) (op : Nat → Nat → Nat) (e : Expr) : SimpM Step := do
+@[inline] def reduceBin (declName : Name) (arity : Nat) (op : {n : Nat} → Fin n → Fin n → Fin n) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue
   let some v₁ ← fromExpr? e.appFn!.appArg! | return .continue
   let some v₂ ← fromExpr? e.appArg! | return .continue
-  unless v₁.size == v₂.size do return .continue
-  let v := { v₁ with value := op v₁.value v₂.value % v₁.size }
-  return .done { expr := v.toExpr }
+  if h : v₁.n = v₂.n then
+    let v := op v₁.value (h ▸ v₂.value)
+    return .done { expr := toExpr v }
+  else
+    return .continue
 
 @[inline] def reduceBinPred (declName : Name) (arity : Nat) (op : Nat → Nat → Bool) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue
@@ -71,12 +63,12 @@ builtin_simproc [simp, seval] reduceBNe  (( _ : Fin _) != _)  := reduceBoolPred
 
 /-- Simplification procedure for ensuring `Fin` literals are normalized. -/
 builtin_simproc [simp, seval] isValue ((OfNat.ofNat _ : Fin _)) := fun e => do
-  let some v ← fromExpr? e | return .continue
-  let v' ← Nat.fromExpr? e.appFn!.appArg!
-  if v.value == v' then
+  let some ⟨n, v⟩ ← getFinValue? e | return .continue
+  let some m ← getNatValue? e.appFn!.appArg! | return .continue
+  if n == m then
     -- Design decision: should we return `.continue` instead of `.done` when simplifying.
     -- In the symbolic evaluator, we must return `.done`, otherwise it will unfold the `OfNat.ofNat`
     return .done { expr := e }
-  return .done { expr := v.toExpr }
+  return .done { expr := toExpr v }
 
 end Fin

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean

@@ -5,33 +5,14 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.ToExpr
+import Lean.Meta.LitValues
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
 
 namespace Int
 open Lean Meta Simp
 
-def fromExpr? (e : Expr) : SimpM (Option Int) := OptionT.run do
-  let mut e := e
-  let mut isNeg := false
-  if e.isAppOfArity ``Neg.neg 3 then
-    e := e.appArg!
-    isNeg := true
-  guard (e.isAppOfArity ``OfNat.ofNat 3)
-  let type ← whnf e.appFn!.appFn!.appArg!
-  guard (type.isConstOf ``Int)
-  let value ← Nat.fromExpr? e.appFn!.appArg!
-  let mut value : Int := value
-  if isNeg then value := - value
-  return value
-
-def toExpr (v : Int) : Expr :=
-  let n := v.natAbs
-  let r := mkRawNatLit n
-  let e := mkApp3 (mkConst ``OfNat.ofNat [levelZero]) (mkConst ``Int) r (mkApp (mkConst ``instOfNat) r)
-  if v < 0 then
-    mkAppN (mkConst ``Neg.neg [levelZero]) #[mkConst ``Int, mkConst ``instNegInt, e]
-  else
-    e
+def fromExpr? (e : Expr) : SimpM (Option Int) :=
+  getIntValue? e
 
 @[inline] def reduceUnary (declName : Name) (arity : Nat) (op : Int → Int) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Simproc
+import Lean.Meta.LitValues
 import Lean.Meta.Offset
 import Lean.Meta.Tactic.Simp.Simproc
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Util
@@ -12,20 +13,19 @@ import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Util
 namespace Nat
 open Lean Meta Simp
 
-def fromExpr? (e : Expr) : SimpM (Option Nat) := do
-  let some n ← evalNat e |>.run | return none
-  return n
+def fromExpr? (e : Expr) : SimpM (Option Nat) :=
+  getNatValue? e
 
 @[inline] def reduceUnary (declName : Name) (arity : Nat) (op : Nat → Nat) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue
   let some n ← fromExpr? e.appArg! | return .continue
-  return .done { expr := mkNatLit (op n) }
+  return .done { expr := toExpr (op n) }
 
 @[inline] def reduceBin (declName : Name) (arity : Nat) (op : Nat → Nat → Nat) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue
   let some n ← fromExpr? e.appFn!.appArg! | return .continue
   let some m ← fromExpr? e.appArg! | return .continue
-  return .done { expr := mkNatLit (op n m) }
+  return .done { expr := toExpr (op n m) }
 
 @[inline] def reduceBinPred (declName : Name) (arity : Nat) (op : Nat → Nat → Bool) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/String.lean

@@ -10,9 +10,8 @@ import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Char
 namespace String
 open Lean Meta Simp
 
-def fromExpr? (e : Expr) : SimpM (Option String) := OptionT.run do
-  let .lit (.strVal s) := e | failure
-  return s
+def fromExpr? (e : Expr) : SimpM (Option String) := do
+  return getStringValue? e
 
 builtin_simproc [simp, seval] reduceAppend ((_ ++ _ : String)) := fun e => do
   unless e.isAppOfArity ``HAppend.hAppend 6 do return .continue

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/UInt.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import Lean.Meta.LitValues
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
 
 open Lean Meta Simp
@@ -13,49 +14,30 @@ let ofNat := typeName.getId ++ `ofNat
 let ofNatCore := mkIdent (typeName.getId ++ `ofNatCore)
 let toNat := mkIdent (typeName.getId ++ `toNat)
 let fromExpr := mkIdent `fromExpr
-let toExprCore := mkIdent `toExprCore
-let toExpr := mkIdent `toExpr
 `(
 namespace $typeName
 
-structure Value where
-  ofNatFn : Expr
-  value   : $typeName
-
-def $fromExpr (e : Expr) : OptionT SimpM Value := do
-  guard (e.isAppOfArity ``OfNat.ofNat 3)
-  let type ← whnf e.appFn!.appFn!.appArg!
-  guard (type.isConstOf $(quote typeName.getId))
-  let value ← Nat.fromExpr? e.appFn!.appArg!
-  let value := $(mkIdent ofNat) value
-  return { value, ofNatFn := e.appFn!.appFn! }
-
-def $toExprCore (v : $typeName) : Expr :=
-  let vExpr := mkRawNatLit v.val
-  mkApp3 (mkConst ``OfNat.ofNat [levelZero]) (mkConst $(quote typeName.getId)) vExpr (mkApp (mkConst $(quote (typeName.getId ++ `instOfNat))) vExpr)
-
-def $toExpr (v : Value) : Expr :=
-  let vExpr := mkRawNatLit v.value.val
-  mkApp2 v.ofNatFn vExpr (mkApp (mkConst $(quote (typeName.getId ++ `instOfNat))) vExpr)
+def $fromExpr (e : Expr) : SimpM (Option $typeName) := do
+  let some (n, _) ← getOfNatValue? e $(quote typeName.getId) | return none
+  return $(mkIdent ofNat) n
 
 @[inline] def reduceBin (declName : Name) (arity : Nat) (op : $typeName → $typeName → $typeName) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue
   let some n ← ($fromExpr e.appFn!.appArg!) | return .continue
   let some m ← ($fromExpr e.appArg!) | return .continue
-  let r := { n with value := op n.value m.value }
-  return .done { expr := $toExpr r }
+  return .done { expr := toExpr (op n m) }
 
 @[inline] def reduceBinPred (declName : Name) (arity : Nat) (op : $typeName → $typeName → Bool) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue
   let some n ← ($fromExpr e.appFn!.appArg!) | return .continue
   let some m ← ($fromExpr e.appArg!) | return .continue
-  evalPropStep e (op n.value m.value)
+  evalPropStep e (op n m)
 
 @[inline] def reduceBoolPred (declName : Name) (arity : Nat) (op : $typeName → $typeName → Bool) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue
   let some n ← ($fromExpr e.appFn!.appArg!) | return .continue
   let some m ← ($fromExpr e.appArg!) | return .continue
-  return .done { expr := Lean.toExpr (op n.value m.value) }
+  return .done { expr := toExpr (op n m) }
 
 builtin_simproc [simp, seval] $(mkIdent `reduceAdd):ident ((_ + _ : $typeName)) := reduceBin ``HAdd.hAdd 6 (· + ·)
 builtin_simproc [simp, seval] $(mkIdent `reduceMul):ident ((_ * _ : $typeName)) := reduceBin ``HMul.hMul 6 (· * ·)
@@ -76,14 +58,13 @@ builtin_simproc [simp, seval] $(mkIdent `reduceOfNatCore):ident ($ofNatCore _ _)
   unless e.isAppOfArity $(quote ofNatCore.getId) 2 do return .continue
   let some value ← Nat.fromExpr? e.appFn!.appArg! | return .continue
   let value := $(mkIdent ofNat) value
-  let eNew := $toExprCore value
-  return .done { expr := eNew }
+  return .done { expr := toExpr value }
 
 builtin_simproc [simp, seval] $(mkIdent `reduceToNat):ident ($toNat _) := fun e => do
   unless e.isAppOfArity $(quote toNat.getId) 1 do return .continue
   let some v ← ($fromExpr e.appArg!) | return .continue
-  let n := $toNat v.value
-  return .done { expr := mkNatLit n }
+  let n := $toNat v
+  return .done { expr := toExpr n }
 
 /-- Return `.done` for UInt values. We don't want to unfold in the symbolic evaluator. -/
 builtin_simproc [seval] isValue ((OfNat.ofNat _ : $typeName)) := fun e => do