max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: add simproc for BitVec.signExtend (#3409)

Browse source
This commit is contained in:
Leonardo de Moura 2024-02-19 15:15:37 -08:00 • committed by GitHub
parent 75d7bc0ef1
commit 489f2da711
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 17 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean
View file

@ -77,6 +77,15 @@ Helper function for reducing homogenous binary bitvector operators.
else
return .continue
/-- Simplification procedure for `zeroExtend` and `signExtend` on `BitVec`s. -/
@[inline] def reduceExtend (declName : Name)
(op : {n : Nat} → (m : Nat) → BitVec n → BitVec m) (e : Expr) : SimpM Step := do
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 }
/--
Helper function for reducing bitvector functions such as `getLsb` and `getMsb`.
-/
@ -275,12 +284,10 @@ builtin_simproc [simp, seval] reduceReplicate (replicate _ _) := fun e => do
return .done { expr := lit.toExpr }
/-- Simplification procedure for `zeroExtend` on `BitVec`s. -/
builtin_simproc [simp, seval] reduceZeroExtend (zeroExtend _ _) := fun e => do
unless e.isAppOfArity ``zeroExtend 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 := v.value.zeroExtend n }
return .done { expr := lit.toExpr }
builtin_simproc [simp, seval] reduceZeroExtend (zeroExtend _ _) := reduceExtend ``zeroExtend zeroExtend
/-- Simplification procedure for `signExtend` on `BitVec`s. -/
builtin_simproc [simp, seval] reduceSignExtend (signExtend _ _) := reduceExtend ``signExtend signExtend
/-- Simplification procedure for `allOnes` -/
builtin_simproc [simp, seval] reduceAllOnes (allOnes _) := fun e => do

4
tests/lean/run/bitvec_simproc.lean
View file

@ -109,3 +109,7 @@ example (h : x = (9: Std.BitVec 6)) : x = (1#3).replicate 2 := by
simp; guard_target =ₛ x = 9#6; assumption
example (h : x = (5 : Std.BitVec 7)) : x = (5#3).zeroExtend 7 := by
simp; guard_target =ₛ x = 5#7; assumption
example (h : -5#10 = x) : signExtend 10 (-5#8) = x := by
simp; guard_target =ₛ1019#10 = x; assumption
example (h : 5#10 = x) : -signExtend 10 (-5#8) = x := by
simp; guard_target =ₛ5#10 = x; assumption