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

perf: Expr.hasSorry and similar functions

Browse source 
Functions were ignoring sharing while traversing `Expr`.

Addresses performance problem exposed by #1287
This commit is contained in:
Leonardo de Moura 2022-07-10 07:39:38 -07:00
parent 2f1b80721e
commit 394d49da58
1 changed files with 27 additions and 45 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

72
src/Lean/Util/Sorry.lean
View file

@ -5,72 +5,54 @@ Authors: Leonardo de Moura
-/
import Lean.Message
import Lean.Exception
import Lean.Util.FindExpr
namespace Lean
def Expr.isSorry : Expr → Bool
| Expr.app (Expr.app (Expr.const ``sorryAx _ _) _ _) _ _ => true
| app (app (.const ``sorryAx ..) ..) .. => true
| _ => false
def Expr.isSyntheticSorry : Expr → Bool
| Expr.app (Expr.app (Expr.const ``sorryAx _ _) _ _) (Expr.const ``Bool.true _ _) _ => true
| app (app (const ``sorryAx ..) ..) (const ``Bool.true ..) _ => true
| _ => false
def Expr.isNonSyntheticSorry : Expr → Bool
| Expr.app (Expr.app (Expr.const ``sorryAx _ _) _ _) (Expr.const ``Bool.false _ _) _ => true
| app (app (const ``sorryAx ..) ..) (const ``Bool.false ..) _ => true
| _ => false
def Expr.hasSorry : Expr → Bool
| Expr.const c _ _ => c == `sorryAx
| Expr.app f a _ => f.hasSorry || a.hasSorry
| Expr.letE _ t v b _ => t.hasSorry || v.hasSorry || b.hasSorry
| Expr.forallE _ d b _ => d.hasSorry || b.hasSorry
| Expr.lam _ d b _ => d.hasSorry || b.hasSorry
| Expr.mdata _ e _ => e.hasSorry
| Expr.proj _ _ e _ => e.hasSorry
| _ => false
def Expr.hasSorry (e : Expr) : Bool :=
Option.isSome <| e.find? (·.isConstOf ``sorryAx)
def Expr.hasSyntheticSorry : Expr → Bool
| e@(Expr.app f a _) => e.isSyntheticSorry || f.hasSyntheticSorry || a.hasSyntheticSorry
| Expr.letE _ t v b _ => t.hasSyntheticSorry || v.hasSyntheticSorry || b.hasSyntheticSorry
| Expr.forallE _ d b _ => d.hasSyntheticSorry || b.hasSyntheticSorry
| Expr.lam _ d b _ => d.hasSyntheticSorry || b.hasSyntheticSorry
| Expr.mdata _ e _ => e.hasSyntheticSorry
| Expr.proj _ _ e _ => e.hasSyntheticSorry
| _ => false
def Expr.hasSyntheticSorry (e : Expr) : Bool :=
Option.isSome <| e.find? (·.isSyntheticSorry)
def Expr.hasNonSyntheticSorry : Expr → Bool
| e@(Expr.app f a _) => e.isNonSyntheticSorry || f.hasNonSyntheticSorry || a.hasNonSyntheticSorry
| Expr.letE _ t v b _ => t.hasNonSyntheticSorry || v.hasNonSyntheticSorry || b.hasNonSyntheticSorry
| Expr.forallE _ d b _ => d.hasNonSyntheticSorry || b.hasNonSyntheticSorry
| Expr.lam _ d b _ => d.hasNonSyntheticSorry || b.hasNonSyntheticSorry
| Expr.mdata _ e _ => e.hasNonSyntheticSorry
| Expr.proj _ _ e _ => e.hasNonSyntheticSorry
| _ => false
def Expr.hasNonSyntheticSorry (e : Expr) : Bool :=
Option.isSome <| e.find? (·.isNonSyntheticSorry)
partial def MessageData.hasSorry : MessageData → Bool
| MessageData.ofExpr e => e.hasSorry
| MessageData.withContext _ msg => msg.hasSorry
| MessageData.nest _ msg => msg.hasSorry
| MessageData.group msg => msg.hasSorry
| MessageData.compose msg₁ msg₂ => msg₁.hasSorry || msg₂.hasSorry
| MessageData.tagged _ msg => msg.hasSorry
| MessageData.node msgs => msgs.any hasSorry
| _ => false
| ofExpr e => e.hasSorry
| withContext _ msg => msg.hasSorry
| nest _ msg => msg.hasSorry
| group msg => msg.hasSorry
| compose msg₁ msg₂ => msg₁.hasSorry || msg₂.hasSorry
| tagged _ msg => msg.hasSorry
| node msgs => msgs.any hasSorry
| _ => false
partial def MessageData.hasSyntheticSorry (msg : MessageData) : Bool :=
visit msg.instantiateMVars
where
visit : MessageData → Bool
| MessageData.ofExpr e => e.hasSyntheticSorry
| MessageData.withContext _ msg => visit msg
| MessageData.withNamingContext _ msg => visit msg
| MessageData.nest _ msg => visit msg
| MessageData.group msg => visit msg
| MessageData.compose msg₁ msg₂ => visit msg₁ || visit msg₂
| MessageData.tagged _ msg => visit msg
| MessageData.node msgs => msgs.any hasSyntheticSorry
| _ => false
| ofExpr e => e.hasSyntheticSorry
| withContext _ msg => visit msg
| withNamingContext _ msg => visit msg
| nest _ msg => visit msg
| group msg => visit msg
| compose msg₁ msg₂ => visit msg₁ || visit msg₂
| tagged _ msg => visit msg
| node msgs => msgs.any hasSyntheticSorry
| _ => false
def Exception.hasSyntheticSorry : Exception → Bool
| Exception.error _ msg => msg.hasSyntheticSorry