From 6d569aa7b5c2fa394a1a69958c0dc3efe699c533 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 23 Feb 2024 21:13:43 -0800 Subject: [PATCH] refactor: use `LitValue.lean` to implement simprocs --- .../Tactic/Simp/BuiltinSimprocs/BitVec.lean | 73 +++++-------------- .../Tactic/Simp/BuiltinSimprocs/Char.lean | 9 +-- .../Meta/Tactic/Simp/BuiltinSimprocs/Fin.lean | 40 ++++------ .../Meta/Tactic/Simp/BuiltinSimprocs/Int.lean | 25 +------ .../Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean | 10 +-- .../Tactic/Simp/BuiltinSimprocs/String.lean | 5 +- .../Tactic/Simp/BuiltinSimprocs/UInt.lean | 39 +++------- 7 files changed, 58 insertions(+), 143 deletions(-) diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean index 1fdd1272d5..94749b34d2 100644 --- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean +++ b/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 diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Char.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Char.lean index b05242b891..40d2aa6920 100644 --- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Char.lean +++ b/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 (. == .) diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.lean index 80cd362891..55aa9a2d04 100644 --- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.lean +++ b/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 diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean index dd714ec4d2..67f64c229d 100644 --- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean +++ b/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 diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean index 357f745a46..3fe3fd7659 100644 --- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean +++ b/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 diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/String.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/String.lean index 72eba30ff1..f0872003b7 100644 --- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/String.lean +++ b/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 diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/UInt.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/UInt.lean index 937829c96f..5e9868bb61 100644 --- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/UInt.lean +++ b/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