From 8b2710c8b3e63380938ed3933099e9ff5b29aa07 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 2 Mar 2024 08:58:26 -0800 Subject: [PATCH] chore: use `let_expr` to cleanup code --- src/Lean/Elab/StructInst.lean | 6 +- src/Lean/Expr.lean | 52 ++++++++------- src/Lean/Meta/Injective.lean | 6 +- src/Lean/Meta/LitValues.lean | 22 +++---- .../Tactic/Simp/BuiltinSimprocs/BitVec.lean | 64 +++++++++---------- .../Tactic/Simp/BuiltinSimprocs/Char.lean | 10 +-- .../Tactic/Simp/BuiltinSimprocs/Core.lean | 24 +++---- .../Meta/Tactic/Simp/BuiltinSimprocs/Int.lean | 8 +-- .../Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean | 2 +- 9 files changed, 91 insertions(+), 103 deletions(-) diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean index ceb379a8c1..674428ca15 100644 --- a/src/Lean/Elab/StructInst.lean +++ b/src/Lean/Elab/StructInst.lean @@ -802,10 +802,8 @@ partial def mkDefaultValueAux? (struct : Struct) : Expr → TermElabM (Option Ex let arg ← mkFreshExprMVar d mkDefaultValueAux? struct (b.instantiate1 arg) | e => - if e.isAppOfArity ``id 2 then - return some e.appArg! - else - return some e + let_expr id _ a := e | return some e + return some a def mkDefaultValue? (struct : Struct) (cinfo : ConstantInfo) : TermElabM (Option Expr) := withRef struct.ref do diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean index d0a41ac834..ba853af364 100644 --- a/src/Lean/Expr.lean +++ b/src/Lean/Expr.lean @@ -1075,33 +1075,6 @@ def isAppOfArity' : Expr → Name → Nat → Bool | app f _, n, a+1 => isAppOfArity' f n a | _, _, _ => false -/-- -Checks if an expression is a "natural number numeral in normal form", -i.e. of type `Nat`, and explicitly of the form `OfNat.ofNat n` -where `n` matches `.lit (.natVal n)` for some literal natural number `n`. -and if so returns `n`. --/ --- Note that `Expr.lit (.natVal n)` is not considered in normal form! -def nat? (e : Expr) : Option Nat := do - guard <| e.isAppOfArity ``OfNat.ofNat 3 - let lit (.natVal n) := e.appFn!.appArg! | none - n - -/-- -Checks if an expression is an "integer numeral in normal form", -i.e. of type `Nat` or `Int`, and either a natural number numeral in normal form (as specified by `nat?`), -or the negation of a positive natural number numberal in normal form, -and if so returns the integer. --/ -def int? (e : Expr) : Option Int := - if e.isAppOfArity ``Neg.neg 3 then - match e.appArg!.nat? with - | none => none - | some 0 => none - | some n => some (-n) - else - e.nat? - private def getAppNumArgsAux : Expr → Nat → Nat | app f _, n => getAppNumArgsAux f (n+1) | _, n => n @@ -1638,6 +1611,31 @@ def isFalse (e : Expr) : Bool := def isTrue (e : Expr) : Bool := e.cleanupAnnotations.isConstOf ``True +/-- +Checks if an expression is a "natural number numeral in normal form", +i.e. of type `Nat`, and explicitly of the form `OfNat.ofNat n` +where `n` matches `.lit (.natVal n)` for some literal natural number `n`. +and if so returns `n`. +-/ +-- Note that `Expr.lit (.natVal n)` is not considered in normal form! +def nat? (e : Expr) : Option Nat := do + let_expr OfNat.ofNat _ n _ := e | failure + let lit (.natVal n) := n | failure + n + +/-- +Checks if an expression is an "integer numeral in normal form", +i.e. of type `Nat` or `Int`, and either a natural number numeral in normal form (as specified by `nat?`), +or the negation of a positive natural number numberal in normal form, +and if so returns the integer. +-/ +def int? (e : Expr) : Option Int := + let_expr Neg.neg _ _ a := e | e.nat? + match a.nat? with + | none => none + | some 0 => none + | some n => some (-n) + /-- Return true iff `e` contains a free variable which satisfies `p`. -/ @[inline] def hasAnyFVar (e : Expr) (p : FVarId → Bool) : Bool := let rec @[specialize] visit (e : Expr) := if !e.hasFVar then false else diff --git a/src/Lean/Meta/Injective.lean b/src/Lean/Meta/Injective.lean index a1a3ea6a6a..c1d1aaa82f 100644 --- a/src/Lean/Meta/Injective.lean +++ b/src/Lean/Meta/Injective.lean @@ -26,10 +26,8 @@ private def mkAnd? (args : Array Expr) : Option Expr := Id.run do def elimOptParam (type : Expr) : CoreM Expr := do Core.transform type fun e => - if e.isAppOfArity ``optParam 2 then - return TransformStep.visit (e.getArg! 0) - else - return .continue + let_expr optParam _ a := e | return .continue + return TransformStep.visit a private partial def mkInjectiveTheoremTypeCore? (ctorVal : ConstructorVal) (useEq : Bool) : MetaM (Option Expr) := do let us := ctorVal.levelParams.map mkLevelParam diff --git a/src/Lean/Meta/LitValues.lean b/src/Lean/Meta/LitValues.lean index 319814c896..c316c1ac2c 100644 --- a/src/Lean/Meta/LitValues.lean +++ b/src/Lean/Meta/LitValues.lean @@ -27,11 +27,10 @@ def getRawNatValue? (e : Expr) : Option Nat := /-- Return `some (n, type)` if `e` is an `OfNat.ofNat`-application encoding `n` for a type with name `typeDeclName`. -/ def getOfNatValue? (e : Expr) (typeDeclName : Name) : MetaM (Option (Nat × Expr)) := OptionT.run do - let e := e.consumeMData - guard <| e.isAppOfArity' ``OfNat.ofNat 3 - let type ← whnfD (e.getArg!' 0) + let_expr OfNat.ofNat type n _ ← e | failure + let type ← whnfD type guard <| type.getAppFn.isConstOf typeDeclName - let .lit (.natVal n) := (e.getArg!' 1).consumeMData | failure + let .lit (.natVal n) := n.consumeMData | failure return (n, type) /-- Return `some n` if `e` is a raw natural number or an `OfNat.ofNat`-application encoding `n`. -/ @@ -46,16 +45,15 @@ def getNatValue? (e : Expr) : MetaM (Option Nat) := do def getIntValue? (e : Expr) : MetaM (Option Int) := do if let some (n, _) ← getOfNatValue? e ``Int then return some n - if e.isAppOfArity' ``Neg.neg 3 then - let some (n, _) ← getOfNatValue? (e.getArg!' 2) ``Int | return none - return some (-n) - return none + let_expr Neg.neg _ _ a ← e | return none + let some (n, _) ← getOfNatValue? a ``Int | return none + return some (-↑n) /-- Return `some c` if `e` is a `Char.ofNat`-application encoding character `c`. -/ -def getCharValue? (e : Expr) : MetaM (Option Char) := OptionT.run do - guard <| e.isAppOfArity' ``Char.ofNat 1 - let n ← getNatValue? (e.getArg!' 0) - return Char.ofNat n +def getCharValue? (e : Expr) : MetaM (Option Char) := do + let_expr Char.ofNat n ← e | return none + let some n ← getNatValue? n | return none + return some (Char.ofNat n) /-- Return `some s` if `e` is of the form `.lit (.strVal s)`. -/ def getStringValue? (e : Expr) : (Option String) := diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean index 94749b34d2..0ac8c1ced9 100644 --- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean +++ b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean @@ -162,42 +162,42 @@ builtin_simproc [simp, seval] reduceRotateRight (BitVec.rotateRight _ _) := /-- Simplification procedure for append on `BitVec`. -/ 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_expr HAppend.hAppend _ _ _ _ a b ← e | return .continue + let some v₁ ← fromExpr? a | return .continue + let some v₂ ← fromExpr? b | return .continue 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_expr cast _ m _ v ← e | return .continue + let some v ← fromExpr? v | return .continue + let some m ← Nat.fromExpr? m | return .continue 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 - unless e.isAppOfArity ``BitVec.toNat 2 do return .continue - let some v ← fromExpr? e.appArg! | return .continue + let_expr BitVec.toNat _ v ← e | return .continue + let some v ← fromExpr? v | return .continue return .done { expr := mkNatLit v.value.toNat } /-- Simplification procedure for `BitVec.toInt`. -/ 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 + let_expr BitVec.toInt _ v ← e | return .continue + let some v ← fromExpr? v | return .continue 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_expr BitVec.ofInt n i ← e | return .continue + let some n ← Nat.fromExpr? n | return .continue + let some i ← Int.fromExpr? i | return .continue 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 - unless e.isAppOfArity ``BitVec.ofNat 2 do return .continue - let some n ← Nat.fromExpr? e.appFn!.appArg! | return .continue - let some v ← Nat.fromExpr? e.appArg! | return .continue + let_expr BitVec.ofNat n v ← e | return .continue + let some n ← Nat.fromExpr? n | return .continue + let some v ← Nat.fromExpr? v | return .continue let bv := BitVec.ofNat n v if bv.toNat == v then return .continue -- already normalized return .done { expr := toExpr (BitVec.ofNat n v) } @@ -226,9 +226,9 @@ builtin_simproc [simp, seval] reduceSLE (BitVec.sle _ _) := /-- Simplification procedure for `zeroExtend'` on `BitVec`s. -/ builtin_simproc [simp, seval] reduceZeroExtend' (zeroExtend' _ _) := fun e => do - unless e.isAppOfArity ``zeroExtend' 4 do return .continue - let some v ← fromExpr? e.appArg! | return .continue - let some w ← Nat.fromExpr? e.appFn!.appFn!.appArg! | return .continue + let_expr zeroExtend' _ w _ v ← e | return .continue + let some v ← fromExpr? v | return .continue + let some w ← Nat.fromExpr? w | return .continue if h : v.n ≤ w then return .done { expr := toExpr (v.value.zeroExtend' h) } else @@ -236,25 +236,25 @@ builtin_simproc [simp, seval] reduceZeroExtend' (zeroExtend' _ _) := fun e => do /-- Simplification procedure for `shiftLeftZeroExtend` on `BitVec`s. -/ builtin_simproc [simp, seval] reduceShiftLeftZeroExtend (shiftLeftZeroExtend _ _) := fun e => do - 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_expr shiftLeftZeroExtend _ v m ← e | return .continue + let some v ← fromExpr? v | return .continue + let some m ← Nat.fromExpr? m | return .continue return .done { expr := toExpr (v.value.shiftLeftZeroExtend m) } /-- Simplification procedure for `extractLsb'` on `BitVec`s. -/ builtin_simproc [simp, seval] reduceExtracLsb' (extractLsb' _ _ _) := fun e => do - unless e.isAppOfArity ``extractLsb' 4 do return .continue - 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_expr extractLsb' _ start len v ← e | return .continue + let some v ← fromExpr? v | return .continue + let some start ← Nat.fromExpr? start | return .continue + let some len ← Nat.fromExpr? len | return .continue 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 - return .done { expr := toExpr (v.value.replicate w) } + let_expr replicate _ i v ← e | return .continue + let some v ← fromExpr? v | return .continue + let some i ← Nat.fromExpr? i | return .continue + return .done { expr := toExpr (v.value.replicate i) } /-- Simplification procedure for `zeroExtend` on `BitVec`s. -/ builtin_simproc [simp, seval] reduceZeroExtend (zeroExtend _ _) := reduceExtend ``zeroExtend zeroExtend @@ -264,8 +264,8 @@ builtin_simproc [simp, seval] reduceSignExtend (signExtend _ _) := reduceExtend /-- Simplification procedure for `allOnes` -/ 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_expr allOnes n ← e | return .continue + let some n ← Nat.fromExpr? n | return .continue 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 40d2aa6920..5647fdadb8 100644 --- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Char.lean +++ b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Char.lean @@ -42,8 +42,8 @@ builtin_simproc [simp, seval] reduceIsDigit (Char.isDigit _) := reduceUnary ``Ch builtin_simproc [simp, seval] reduceIsAlphaNum (Char.isAlphanum _) := reduceUnary ``Char.isAlphanum Char.isAlphanum builtin_simproc [simp, seval] reduceToString (toString (_ : Char)) := reduceUnary ``toString toString 3 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 + let_expr Char.val arg ← e | return .continue + let some c ← fromExpr? arg | return .continue return .done { expr := toExpr c.val } builtin_simproc [simp, seval] reduceEq (( _ : Char) = _) := reduceBinPred ``Eq 3 (. = .) builtin_simproc [simp, seval] reduceNe (( _ : Char) ≠ _) := reduceBinPred ``Ne 3 (. ≠ .) @@ -60,12 +60,12 @@ builtin_simproc ↓ [simp, seval] isValue (Char.ofNat _ ) := fun e => do return .done { expr := e } builtin_simproc [simp, seval] reduceOfNatAux (Char.ofNatAux _ _) := fun e => do - unless e.isAppOfArity ``Char.ofNatAux 2 do return .continue - let some n ← Nat.fromExpr? e.appFn!.appArg! | return .continue + let_expr Char.ofNatAux n _ ← e | return .continue + let some n ← Nat.fromExpr? n | return .continue return .done { expr := toExpr (Char.ofNat n) } builtin_simproc [simp, seval] reduceDefault ((default : Char)) := fun e => do - unless e.isAppOfArity ``default 2 do return .continue + let_expr default _ _ ← e | return .continue return .done { expr := toExpr (default : Char) } end Char diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Core.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Core.lean index 948e3241ff..eda1dc348c 100644 --- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Core.lean +++ b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Core.lean @@ -10,33 +10,29 @@ import Lean.Meta.Tactic.Simp.Simproc open Lean Meta Simp builtin_simproc ↓ [simp, seval] reduceIte (ite _ _ _) := fun e => do - unless e.isAppOfArity ``ite 5 do return .continue - let c := e.getArg! 1 + let_expr f@ite α c i tb eb ← e | return .continue let r ← simp c if r.expr.isTrue then - let eNew := e.getArg! 3 - let pr := mkApp (mkAppN (mkConst ``ite_cond_eq_true e.getAppFn.constLevels!) e.getAppArgs) (← r.getProof) - return .visit { expr := eNew, proof? := pr } + let pr := mkApp (mkApp5 (mkConst ``ite_cond_eq_true f.constLevels!) α c i tb eb) (← r.getProof) + return .visit { expr := tb, proof? := pr } if r.expr.isFalse then - let eNew := e.getArg! 4 - let pr := mkApp (mkAppN (mkConst ``ite_cond_eq_false e.getAppFn.constLevels!) e.getAppArgs) (← r.getProof) - return .visit { expr := eNew, proof? := pr } + let pr := mkApp (mkApp5 (mkConst ``ite_cond_eq_false f.constLevels!) α c i tb eb) (← r.getProof) + return .visit { expr := eb, proof? := pr } return .continue builtin_simproc ↓ [simp, seval] reduceDite (dite _ _ _) := fun e => do - unless e.isAppOfArity ``dite 5 do return .continue - let c := e.getArg! 1 + let_expr f@dite α c i tb eb ← e | return .continue let r ← simp c if r.expr.isTrue then let pr ← r.getProof let h := mkApp2 (mkConst ``of_eq_true) c pr - let eNew := mkApp (e.getArg! 3) h |>.headBeta - let prNew := mkApp (mkAppN (mkConst ``dite_cond_eq_true e.getAppFn.constLevels!) e.getAppArgs) pr + let eNew := mkApp tb h |>.headBeta + let prNew := mkApp (mkApp5 (mkConst ``dite_cond_eq_true f.constLevels!) α c i tb eb) pr return .visit { expr := eNew, proof? := prNew } if r.expr.isFalse then let pr ← r.getProof let h := mkApp2 (mkConst ``of_eq_false) c pr - let eNew := mkApp (e.getArg! 4) h |>.headBeta - let prNew := mkApp (mkAppN (mkConst ``dite_cond_eq_false e.getAppFn.constLevels!) e.getAppArgs) pr + let eNew := mkApp eb h |>.headBeta + let prNew := mkApp (mkApp5 (mkConst ``dite_cond_eq_false f.constLevels!) α c i tb eb) pr return .visit { expr := eNew, proof? := prNew } return .continue diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean index 67f64c229d..c031524bcc 100644 --- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean +++ b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean @@ -57,7 +57,7 @@ builtin_simproc [simp, seval] reduceNeg ((- _ : Int)) := fun e => do /-- Return `.done` for positive Int values. We don't want to unfold in the symbolic evaluator. -/ builtin_simproc [seval] isPosValue ((OfNat.ofNat _ : Int)) := fun e => do - unless e.isAppOfArity ``OfNat.ofNat 3 do return .continue + let_expr OfNat.ofNat _ _ _ ← e | return .continue return .done { expr := e } builtin_simproc [simp, seval] reduceAdd ((_ + _ : Int)) := reduceBin ``HAdd.hAdd 6 (· + ·) @@ -67,9 +67,9 @@ builtin_simproc [simp, seval] reduceDiv ((_ / _ : Int)) := reduceBin ``HDiv.hDiv builtin_simproc [simp, seval] reduceMod ((_ % _ : Int)) := reduceBin ``HMod.hMod 6 (· % ·) builtin_simproc [simp, seval] reducePow ((_ : Int) ^ (_ : Nat)) := fun e => do - unless e.isAppOfArity ``HPow.hPow 6 do return .continue - let some v₁ ← fromExpr? e.appFn!.appArg! | return .continue - let some v₂ ← Nat.fromExpr? e.appArg! | return .continue + let_expr HPow.hPow _ _ _ _ a b ← e | return .continue + let some v₁ ← fromExpr? a | return .continue + let some v₂ ← Nat.fromExpr? b | return .continue return .done { expr := toExpr (v₁ ^ v₂) } builtin_simproc [simp, seval] reduceLT (( _ : Int) < _) := reduceBinPred ``LT.lt 4 (. < .) diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean index 3fe3fd7659..367df2346d 100644 --- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean +++ b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean @@ -65,7 +65,7 @@ builtin_simproc [simp, seval] reduceBNe (( _ : Nat) != _) := reduceBoolPred `` /-- Return `.done` for Nat values. We don't want to unfold in the symbolic evaluator. -/ builtin_simproc [seval] isValue ((OfNat.ofNat _ : Nat)) := fun e => do - unless e.isAppOfArity ``OfNat.ofNat 3 do return .continue + let_expr OfNat.ofNat _ _ _ ← e | return .continue return .done { expr := e } end Nat