Lean4
/-- Check if two expressions are different at reducible transparency.
Attempt to log an info message for the first subexpressions which are different
(but agree at default transparency).
Also returns an array of messages for the `verbose` report.
-/
def logDiffs (tk : Syntax) (e₁ e₂ : Expr) : StateT (Array (Unit → MessageData)) MetaM Bool := do
withOptions (fun opts => opts.setBool `pp.analyze true)
(do
if ← withReducible (isDefEq e₁ e₂) then
verbose
m! "{checkEmoji} at reducible transparency,\
{(indentD e₁)}\nand{indentD e₂}\nare defeq."
return false
else
verbose
m! "{crossEmoji} at reducible transparency,\
{(indentD e₁)}\nand{indentD e₂}\nare not defeq."
if ← isDefEq e₁ e₂ then
match e₁, e₂ with
| Expr.app f₁ a₁, Expr.app f₂ a₂ =>
if ← logDiffs tk a₁ a₂ then
return true
else
if ← logDiffs tk f₁ f₂ then
return true
else
logInfoAt tk
m! "{crossEmoji} at reducible transparency,\
{(indentD
e₁)}\nand{indentD e₂}\nare not defeq, but they are at default transparency."
return true
| Expr.const _ _, Expr.const _ _ =>
logInfoAt tk
m! "{crossEmoji} at reducible transparency,\
{(indentD e₁)}\nand{indentD e₂}\nare not defeq, but they are at default transparency."
return true
| _, _ =>
verbose m! "{crossEmoji}{(indentD e₁)}\nand{indentD e₂}\nare not both applications or constants."
return false
else
verbose m! "{crossEmoji}{(indentD e₁)}\nand{indentD e₂}\nare not defeq at default transparency."
return false)
