From 94d51b232178c25dd7e772dea11fb36b2bcb1fe3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 7 Jan 2024 11:12:23 -0800 Subject: [PATCH] chore: cleanup builtin `simproc`s using `OptionT` --- .../Tactic/Simp/BuiltinSimprocs/Core.lean | 20 +++--- .../Meta/Tactic/Simp/BuiltinSimprocs/Fin.lean | 38 +++++------ .../Meta/Tactic/Simp/BuiltinSimprocs/Int.lean | 68 +++++++++---------- .../Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean | 32 ++++----- .../Tactic/Simp/BuiltinSimprocs/UInt.lean | 32 ++++----- 5 files changed, 95 insertions(+), 95 deletions(-) diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Core.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Core.lean index 461935f6ee..f1effb539f 100644 --- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Core.lean +++ b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Core.lean @@ -7,22 +7,22 @@ import Lean.Meta.Tactic.Simp.Simproc open Lean Meta Simp -builtin_simproc ↓ reduceIte (ite _ _ _) := fun e => do - unless e.isAppOfArity' ``ite 5 do return none +builtin_simproc ↓ reduceIte (ite _ _ _) := fun e => OptionT.run do + guard (e.isAppOfArity' ``ite 5) let c := e.getArg! 1 let r ← simp c if r.expr.isConstOf ``True then let eNew := e.getArg! 3 let pr := mkApp (mkAppN (mkConst ``ite_cond_eq_true e.getAppFn.constLevels!) e.getAppArgs) (← r.getProof) - return some (.visit { expr := eNew, proof? := pr }) + return .visit { expr := eNew, proof? := pr } if r.expr.isConstOf ``False then let eNew := e.getArg! 4 let pr := mkApp (mkAppN (mkConst ``ite_cond_eq_false e.getAppFn.constLevels!) e.getAppArgs) (← r.getProof) - return some (.visit { expr := eNew, proof? := pr }) - return none + return .visit { expr := eNew, proof? := pr } + failure -builtin_simproc ↓ reduceDite (dite _ _ _) := fun e => do - unless e.isAppOfArity' ``dite 5 do return none +builtin_simproc ↓ reduceDite (dite _ _ _) := fun e => OptionT.run do + guard (e.isAppOfArity' ``dite 5) let c := e.getArg! 1 let r ← simp c if r.expr.isConstOf ``True then @@ -30,11 +30,11 @@ builtin_simproc ↓ reduceDite (dite _ _ _) := fun e => do 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 - return some (.visit { expr := eNew, proof? := prNew }) + return .visit { expr := eNew, proof? := prNew } if r.expr.isConstOf ``False 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 - return some (.visit { expr := eNew, proof? := prNew }) - return none + return .visit { expr := eNew, proof? := prNew } + failure diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.lean index 8fadff9754..55fbb4825d 100644 --- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.lean +++ b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.lean @@ -14,37 +14,37 @@ structure Value where size : Nat value : Nat -def fromExpr? (e : Expr) : SimpM (Option Value) := do - unless e.isAppOfArity ``OfNat.ofNat 3 do return none +def fromExpr? (e : Expr) : OptionT SimpM Value := do + guard (e.isAppOfArity ``OfNat.ofNat 3) let type ← whnf e.appFn!.appFn!.appArg! - unless type.isAppOfArity ``Fin 1 do return none - let some size ← evalNat type.appArg! |>.run | return none - unless size > 0 do return none - let some value ← Nat.fromExpr? e.appFn!.appArg! | return none + 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 some { size, value, ofNatFn := e.appFn!.appFn! } + return { size, value, ofNatFn := e.appFn!.appFn! } 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 (Option Step) := do - unless e.isAppOfArity declName arity do return none - let some v₁ ← fromExpr? e.appFn!.appArg! | return none - let some v₂ ← fromExpr? e.appArg! | return none - unless v₁.size == v₂.size do return none +@[inline] def reduceBin (declName : Name) (arity : Nat) (op : Nat → Nat → Nat) (e : Expr) : OptionT SimpM Step := do + guard (e.isAppOfArity declName arity) + let v₁ ← fromExpr? e.appFn!.appArg! + let v₂ ← fromExpr? e.appArg! + guard (v₁.size == v₂.size) let v := { v₁ with value := op v₁.value v₂.value % v₁.size } - return some (.done { expr := v.toExpr }) + return .done { expr := v.toExpr } -@[inline] def reduceBinPred (declName : Name) (arity : Nat) (op : Nat → Nat → Bool) (e : Expr) : SimpM (Option Step) := do - unless e.isAppOfArity declName arity do return none - let some v₁ ← fromExpr? e.appFn!.appArg! | return none - let some v₂ ← fromExpr? e.appArg! | return none +@[inline] def reduceBinPred (declName : Name) (arity : Nat) (op : Nat → Nat → Bool) (e : Expr) : OptionT SimpM Step := do + guard (e.isAppOfArity declName arity) + let v₁ ← fromExpr? e.appFn!.appArg! + let v₂ ← fromExpr? e.appArg! let d ← mkDecide e if op v₁.value v₂.value then - return some (.done { expr := mkConst ``True, proof? := mkAppN (mkConst ``eq_true_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``true))] }) + return .done { expr := mkConst ``True, proof? := mkAppN (mkConst ``eq_true_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``true))] } else - return some (.done { expr := mkConst ``False, proof? := mkAppN (mkConst ``eq_false_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``false))] }) + return .done { expr := mkConst ``False, proof? := mkAppN (mkConst ``eq_false_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``false))] } /- The following code assumes users did not override the `Fin n` instances for the arithmetic operators. diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean index e368c72632..44e87aae12 100644 --- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean +++ b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean @@ -9,19 +9,19 @@ import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat namespace Int open Lean Meta Simp -def fromExpr? (e : Expr) : SimpM (Option Int) := do +def fromExpr? (e : Expr) : OptionT SimpM Int := do let mut e := e let mut isNeg := false if e.isAppOfArity ``Neg.neg 3 then e := e.appArg! isNeg := true - unless e.isAppOfArity ``OfNat.ofNat 3 do return none + guard (e.isAppOfArity ``OfNat.ofNat 3) let type ← whnf e.appFn!.appFn!.appArg! - unless type.isConstOf ``Int do return none - let some value ← Nat.fromExpr? e.appFn!.appArg! | return none + guard (type.isConstOf ``Int) + let value ← Nat.fromExpr? e.appFn!.appArg! let mut value : Int := value if isNeg then value := - value - return some value + return value def toExpr (v : Int) : Expr := let n := v.natAbs @@ -32,37 +32,37 @@ def toExpr (v : Int) : Expr := else e -@[inline] def reduceUnary (declName : Name) (arity : Nat) (op : Int → Int) (e : Expr) : SimpM (Option Step) := do - unless e.isAppOfArity declName arity do return none - let some n ← fromExpr? e.appArg! | return none - return some (.done { expr := toExpr (op n) }) +@[inline] def reduceUnary (declName : Name) (arity : Nat) (op : Int → Int) (e : Expr) : OptionT SimpM Step := do + guard (e.isAppOfArity declName arity) + let n ← fromExpr? e.appArg! + return .done { expr := toExpr (op n) } -@[inline] def reduceBin (declName : Name) (arity : Nat) (op : Int → Int → Int) (e : Expr) : SimpM (Option Step) := do - unless e.isAppOfArity declName arity do return none - let some v₁ ← fromExpr? e.appFn!.appArg! | return none - let some v₂ ← fromExpr? e.appArg! | return none - return some (.done { expr := toExpr (op v₁ v₂) }) +@[inline] def reduceBin (declName : Name) (arity : Nat) (op : Int → Int → Int) (e : Expr) : OptionT SimpM Step := do + guard (e.isAppOfArity declName arity) + let v₁ ← fromExpr? e.appFn!.appArg! + let v₂ ← fromExpr? e.appArg! + return .done { expr := toExpr (op v₁ v₂) } -@[inline] def reduceBinPred (declName : Name) (arity : Nat) (op : Int → Int → Bool) (e : Expr) : SimpM (Option Step) := do - unless e.isAppOfArity declName arity do return none - let some v₁ ← fromExpr? e.appFn!.appArg! | return none - let some v₂ ← fromExpr? e.appArg! | return none +@[inline] def reduceBinPred (declName : Name) (arity : Nat) (op : Int → Int → Bool) (e : Expr) : OptionT SimpM Step := OptionT.run do + guard (e.isAppOfArity declName arity) + let v₁ ← fromExpr? e.appFn!.appArg! + let v₂ ← fromExpr? e.appArg! let d ← mkDecide e if op v₁ v₂ then - return some (.done { expr := mkConst ``True, proof? := mkAppN (mkConst ``eq_true_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``true))] }) + return .done { expr := mkConst ``True, proof? := mkAppN (mkConst ``eq_true_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``true))] } else - return some (.done { expr := mkConst ``False, proof? := mkAppN (mkConst ``eq_false_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``false))] }) + return .done { expr := mkConst ``False, proof? := mkAppN (mkConst ``eq_false_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``false))] } /- The following code assumes users did not override the `Int` instances for the arithmetic operators. If they do, they must disable the following `simprocs`. -/ -builtin_simproc reduceNeg ((- _ : Int)) := fun e => do - unless e.isAppOfArity ``Neg.neg 3 do return none - let some v ← fromExpr? e.appArg! | return none - unless v < 0 do return none - return some (.done { expr := toExpr (- v) }) +builtin_simproc reduceNeg ((- _ : Int)) := fun e => OptionT.run do + guard (e.isAppOfArity ``Neg.neg 3) + let v ← fromExpr? e.appArg! + guard (v < 0) + return .done { expr := toExpr (- v) } builtin_simproc reduceAdd ((_ + _ : Int)) := reduceBin ``HAdd.hAdd 6 (· + ·) builtin_simproc reduceMul ((_ * _ : Int)) := reduceBin ``HMul.hMul 6 (· * ·) @@ -70,16 +70,16 @@ builtin_simproc reduceSub ((_ - _ : Int)) := reduceBin ``HSub.hSub 6 (· - ·) builtin_simproc reduceDiv ((_ / _ : Int)) := reduceBin ``HDiv.hDiv 6 (· / ·) builtin_simproc reduceMod ((_ % _ : Int)) := reduceBin ``HMod.hMod 6 (· % ·) -builtin_simproc reducePow ((_ : Int) ^ (_ : Nat)) := fun e => do - unless e.isAppOfArity ``HPow.hPow 6 do return none - let some v₁ ← fromExpr? e.appFn!.appArg! | return none - let some v₂ ← Nat.fromExpr? e.appArg! | return none - return some (.done { expr := toExpr (v₁ ^ v₂) }) +builtin_simproc reducePow ((_ : Int) ^ (_ : Nat)) := fun e => OptionT.run do + guard (e.isAppOfArity ``HPow.hPow 6) + let v₁ ← fromExpr? e.appFn!.appArg! + let v₂ ← Nat.fromExpr? e.appArg! + return .done { expr := toExpr (v₁ ^ v₂) } -builtin_simproc reduceAbs (natAbs _) := fun e => do - unless e.isAppOfArity ``natAbs 1 do return none - let some v ← fromExpr? e.appArg! | return none - return some (.done { expr := mkNatLit (natAbs v) }) +builtin_simproc reduceAbs (natAbs _) := fun e => OptionT.run do + guard (e.isAppOfArity ``natAbs 1) + let v ← fromExpr? e.appArg! + return .done { expr := mkNatLit (natAbs v) } builtin_simproc reduceLT (( _ : Int) < _) := reduceBinPred ``LT.lt 4 (. < .) builtin_simproc reduceLE (( _ : Int) ≤ _) := reduceBinPred ``LE.le 4 (. ≤ .) diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean index 1e6558fd6f..48005d5d6e 100644 --- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean +++ b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean @@ -11,28 +11,28 @@ open Lean Meta Simp def fromExpr? (e : Expr) : SimpM (Option Nat) := do let some n ← evalNat e |>.run | return none - return some n + return n -@[inline] def reduceUnary (declName : Name) (arity : Nat) (op : Nat → Nat) (e : Expr) : SimpM (Option Step) := do - unless e.isAppOfArity declName arity do return none - let some n ← fromExpr? e.appArg! | return none - return some (.done { expr := mkNatLit (op n) }) +@[inline] def reduceUnary (declName : Name) (arity : Nat) (op : Nat → Nat) (e : Expr) : OptionT SimpM Step := do + guard (e.isAppOfArity declName arity) + let n ← fromExpr? e.appArg! + return .done { expr := mkNatLit (op n) } -@[inline] def reduceBin (declName : Name) (arity : Nat) (op : Nat → Nat → Nat) (e : Expr) : SimpM (Option Step) := do - unless e.isAppOfArity declName arity do return none - let some n ← fromExpr? e.appFn!.appArg! | return none - let some m ← fromExpr? e.appArg! | return none - return some (.done { expr := mkNatLit (op n m) }) +@[inline] def reduceBin (declName : Name) (arity : Nat) (op : Nat → Nat → Nat) (e : Expr) : OptionT SimpM Step := do + guard (e.isAppOfArity declName arity) + let n ← fromExpr? e.appFn!.appArg! + let m ← fromExpr? e.appArg! + return .done { expr := mkNatLit (op n m) } -@[inline] def reduceBinPred (declName : Name) (arity : Nat) (op : Nat → Nat → Bool) (e : Expr) : SimpM (Option Step) := do - unless e.isAppOfArity declName arity do return none - let some n ← fromExpr? e.appFn!.appArg! | return none - let some m ← fromExpr? e.appArg! | return none +@[inline] def reduceBinPred (declName : Name) (arity : Nat) (op : Nat → Nat → Bool) (e : Expr) : OptionT SimpM Step := do + guard (e.isAppOfArity declName arity) + let n ← fromExpr? e.appFn!.appArg! + let m ← fromExpr? e.appArg! let d ← mkDecide e if op n m then - return some (.done { expr := mkConst ``True, proof? := mkAppN (mkConst ``eq_true_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``true))] }) + return .done { expr := mkConst ``True, proof? := mkAppN (mkConst ``eq_true_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``true))] } else - return some (.done { expr := mkConst ``False, proof? := mkAppN (mkConst ``eq_false_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``false))] }) + return .done { expr := mkConst ``False, proof? := mkAppN (mkConst ``eq_false_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``false))] } builtin_simproc reduceSucc (Nat.succ _) := reduceUnary ``Nat.succ 1 (· + 1) diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/UInt.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/UInt.lean index 10bd14c76d..9923f591ce 100644 --- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/UInt.lean +++ b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/UInt.lean @@ -18,34 +18,34 @@ structure Value where ofNatFn : Expr value : $typeName -def $fromExpr (e : Expr) : SimpM (Option Value) := do - unless e.isAppOfArity ``OfNat.ofNat 3 do return none +def $fromExpr (e : Expr) : OptionT SimpM Value := do + guard (e.isAppOfArity ``OfNat.ofNat 3) let type ← whnf e.appFn!.appFn!.appArg! - unless type.isConstOf $(quote typeName.getId) do return none - let some value ← Nat.fromExpr? e.appFn!.appArg! | return none + guard (type.isConstOf $(quote typeName.getId)) + let value ← Nat.fromExpr? e.appFn!.appArg! let value := $(mkIdent ofNat) value - return some { value, ofNatFn := e.appFn!.appFn! } + return { value, ofNatFn := e.appFn!.appFn! } def $toExpr (v : Value) : Expr := let vExpr := mkRawNatLit v.value.val mkApp2 v.ofNatFn vExpr (mkApp (mkConst $(quote (typeName.getId ++ `instOfNat))) vExpr) -@[inline] def reduceBin (declName : Name) (arity : Nat) (op : $typeName → $typeName → $typeName) (e : Expr) : SimpM (Option Step) := do - unless e.isAppOfArity declName arity do return none - let some n ← ($fromExpr e.appFn!.appArg!) | return none - let some m ← ($fromExpr e.appArg!) | return none +@[inline] def reduceBin (declName : Name) (arity : Nat) (op : $typeName → $typeName → $typeName) (e : Expr) : OptionT SimpM Step := do + guard (e.isAppOfArity declName arity) + let n ← ($fromExpr e.appFn!.appArg!) + let m ← ($fromExpr e.appArg!) let r := { n with value := op n.value m.value } - return some (.done { expr := $toExpr r }) + return .done { expr := $toExpr r } -@[inline] def reduceBinPred (declName : Name) (arity : Nat) (op : $typeName → $typeName → Bool) (e : Expr) : SimpM (Option Step) := do - unless e.isAppOfArity declName arity do return none - let some n ← ($fromExpr e.appFn!.appArg!) | return none - let some m ← ($fromExpr e.appArg!) | return none +@[inline] def reduceBinPred (declName : Name) (arity : Nat) (op : $typeName → $typeName → Bool) (e : Expr) : OptionT SimpM Step := do + guard (e.isAppOfArity declName arity) + let n ← ($fromExpr e.appFn!.appArg!) + let m ← ($fromExpr e.appArg!) let d ← mkDecide e if op n.value m.value then - return some (.done { expr := mkConst ``True, proof? := mkAppN (mkConst ``eq_true_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``true))] }) + return .done { expr := mkConst ``True, proof? := mkAppN (mkConst ``eq_true_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``true))] } else - return some (.done { expr := mkConst ``False, proof? := mkAppN (mkConst ``eq_false_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``false))] }) + return .done { expr := mkConst ``False, proof? := mkAppN (mkConst ``eq_false_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``false))] } builtin_simproc $(mkIdent `reduceAdd):ident ((_ + _ : $typeName)) := reduceBin ``HAdd.hAdd 6 (· + ·) builtin_simproc $(mkIdent `reduceMul):ident ((_ * _ : $typeName)) := reduceBin ``HMul.hMul 6 (· * ·)