Skip to content

Commit

Permalink
improve message when missing lambda theorems for fun_trans
Browse files Browse the repository at this point in the history
  • Loading branch information
lecopivo committed Aug 7, 2024
1 parent 7283084 commit 2babb7f
Show file tree
Hide file tree
Showing 2 changed files with 35 additions and 22 deletions.
53 changes: 33 additions & 20 deletions SciLean/Tactic/FunTrans/Core.lean
Original file line number Diff line number Diff line change
Expand Up @@ -165,9 +165,11 @@ def tryTheorem? (e : Expr) (thmOrigin : FunProp.Origin) : SimpM (Option Simp.Res
def applyIdRule (funTransDecl : FunTransDecl) (e : Expr) : SimpM (Option Simp.Result) := do
trace[Meta.Tactic.fun_trans.step] "id case"

let .some thms ← getLambdaTheorems funTransDecl.funTransName .id e.getAppNumArgs
| trace[Meta.Tactic.fun_trans] "missing identity rule to transform `{← ppExpr e}`"
return none
let thms ← getLambdaTheorems funTransDecl.funTransName .id e.getAppNumArgs

if thms.size = 0 then
trace[Meta.Tactic.fun_trans] "missing identity rule to transform `{← ppExpr e}`"
return none

for thm in thms do
if let .some r ← tryTheorem? e (.decl thm.thmName) then
Expand All @@ -176,9 +178,11 @@ def applyIdRule (funTransDecl : FunTransDecl) (e : Expr) : SimpM (Option Simp.Re
return none

def applyConstRule (funTransDecl : FunTransDecl) (e : Expr) : SimpM (Option Simp.Result) := do
let .some thms ← getLambdaTheorems funTransDecl.funTransName .const e.getAppNumArgs
| trace[Meta.Tactic.fun_trans] "missing const rule to transform `{← ppExpr e}`"
return none
let thms ← getLambdaTheorems funTransDecl.funTransName .const e.getAppNumArgs

if thms.size = 0 then
trace[Meta.Tactic.fun_trans] "missing const rule to transform `{← ppExpr e}`"
return none

for thm in thms do
if let .some r ← tryTheorem? e (.decl thm.thmName) then
Expand All @@ -187,9 +191,11 @@ def applyConstRule (funTransDecl : FunTransDecl) (e : Expr) : SimpM (Option Simp
return none

def applyCompRule (funTransDecl : FunTransDecl) (e f g : Expr) : SimpM (Option Simp.Result) := do
let .some thms ← getLambdaTheorems funTransDecl.funTransName .comp e.getAppNumArgs
| trace[Meta.Tactic.fun_trans] "missing comp rule to transform `{← ppExpr e}`"
return none
let thms ← getLambdaTheorems funTransDecl.funTransName .comp e.getAppNumArgs

if thms.size = 0 then
trace[Meta.Tactic.fun_trans] "missing comp rule to transform `{← ppExpr e}`"
return none

for thm in thms do
let .comp id_f id_g := thm.thmArgs | continue
Expand All @@ -200,9 +206,11 @@ def applyCompRule (funTransDecl : FunTransDecl) (e f g : Expr) : SimpM (Option S
return none

def applyLetRule (funTransDecl : FunTransDecl) (e f g : Expr) : SimpM (Option Simp.Result) := do
let .some thms ← getLambdaTheorems funTransDecl.funTransName .letE e.getAppNumArgs
| trace[Meta.Tactic.fun_trans] "missing let rule to transform `{← ppExpr e}`"
return none
let thms ← getLambdaTheorems funTransDecl.funTransName .letE e.getAppNumArgs

if thms.size = 0 then
trace[Meta.Tactic.fun_trans] "missing let rule to transform `{← ppExpr e}`"
return none

for thm in thms do
let .letE id_f id_g := thm.thmArgs | continue
Expand All @@ -213,20 +221,25 @@ def applyLetRule (funTransDecl : FunTransDecl) (e f g : Expr) : SimpM (Option Si
return none

def applyApplyRule (funTransDecl : FunTransDecl) (e : Expr) : SimpM (Option Simp.Result) := do
let .some thms ← getLambdaTheorems funTransDecl.funTransName .apply e.getAppNumArgs
| trace[Meta.Tactic.fun_trans]
"missing projection rule to transform `{← ppExpr e}`"
return none
let thms ← getLambdaTheorems funTransDecl.funTransName .apply e.getAppNumArgs

if thms.size = 0 then
trace[Meta.Tactic.fun_trans]
"missing projection rule to transform `{← ppExpr e}`"
return none

for thm in thms do
if let .some r ← tryTheorem? e (.decl thm.thmName) then
return r

return none

def applyPiRule (funTransDecl : FunTransDecl) (e : Expr) : SimpM (Option Simp.Result) := do
let .some thms ← getLambdaTheorems funTransDecl.funTransName .pi e.getAppNumArgs
| trace[Meta.Tactic.fun_trans] "missing pi rule to transform `{← ppExpr e}`"
return none
let thms ← getLambdaTheorems funTransDecl.funTransName .pi e.getAppNumArgs

if thms.size = 0 then
trace[Meta.Tactic.fun_trans] "missing pi rule to transform `{← ppExpr e}`"
return none

for thm in thms do
if let .some r ← tryTheorem? e (.decl thm.thmName) then
Expand Down Expand Up @@ -364,7 +377,7 @@ def tryTheorems (funTransDecl : FunTransDecl) (e : Expr) (fData : FunProp.Functi
return r
| .some (.some (f,g)) =>
trace[Meta.Tactic.fun_trans.step]
s!"decomposing to later use {←ppOrigin' thm.thmOrigin}"
s!"decomposing to later use {←ppOrigin' thm.thmOrigin}, {← ppExpr (←fData.toExpr)} = {← ppExpr f}{← ppExpr g}"
if let .some r ← applyCompRule funTransDecl e f g then
return r
| _ => continue
Expand Down
4 changes: 2 additions & 2 deletions SciLean/Tactic/FunTrans/Theorems.lean
Original file line number Diff line number Diff line change
Expand Up @@ -153,9 +153,9 @@ deriv (fun x' => 1/(1-x')) x
we prefer the version `deriv (fun x' => f (g x')) x` over `deriv (fun x' => f (g x'))` as the former
uses `DifferntiableAt` insed of `Differentiable` as preconditions. -/
def getLambdaTheorems (funTransName : Name) (type : LambdaTheoremType) (nargs : Option Nat):
CoreM (Option (Array LambdaTheorem)) := do
CoreM (Array LambdaTheorem) := do
let .some thms := (lambdaTheoremsExt.getState (← getEnv)).theorems.find? (funTransName,type)
| return none
| return #[]

match nargs with
| none => return thms
Expand Down

0 comments on commit 2babb7f

Please sign in to comment.