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

chore: cleanup builtin simprocs using OptionT

Browse source
This commit is contained in:
Leonardo de Moura 2024-01-07 11:12:23 -08:00 • committed by Sebastian Ullrich
parent 0342d62109
commit 94d51b2321
5 changed files with 95 additions and 95 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Core.lean
View file

@ -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

38
src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.lean
View file

@ -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.

68
src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean
View file

@ -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 (. ≤ .)

32
src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean
View file

@ -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)

32
src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/UInt.lean
View file

@ -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 (· * ·)