Lean.Meta.Tactic.Simp.SimpLemmas

source

structure Lean.Meta.SimpLemma :

Type

keys : Array Lean.Meta.DiscrTree.Key
levelParams : Array Lean.Name
proof : Lean.Expr
priority : Nat
post : Bool
perm : Bool
name? : Option Lean.Name

source

instance Lean.Meta.instInhabitedSimpLemma :

Inhabited Lean.Meta.SimpLemma

Equations

Lean.Meta.instInhabitedSimpLemma = { default := { keys := default, levelParams := default, proof := default, priority := default, post := default, perm := default, name? := default } }

source

def Lean.Meta.SimpLemma.getName (s : Lean.Meta.SimpLemma) :

Lean.Name

Equations

Lean.Meta.SimpLemma.getName s = match s.name? with | some n => n | none => Lean.Name.mkSimple ""

source

instance Lean.Meta.instToFormatSimpLemma :

Lean.ToFormat Lean.Meta.SimpLemma

Equations

Lean.Meta.instToFormatSimpLemma = { format := fun s => let perm := if s.perm = true then ":perm" else ""; let name := Lean.format (Lean.Meta.SimpLemma.getName s); let prio := Lean.format ":" ++ Lean.format s.priority ++ Lean.format ""; name ++ prio ++ Std.Format.text perm }

source

instance Lean.Meta.instToMessageDataSimpLemma :

Lean.ToMessageData Lean.Meta.SimpLemma

Equations

Lean.Meta.instToMessageDataSimpLemma = { toMessageData := fun s => Lean.MessageData.ofFormat (Lean.format s) }

source

instance Lean.Meta.instBEqSimpLemma :

BEq Lean.Meta.SimpLemma

Equations

Lean.Meta.instBEqSimpLemma = { beq := fun e₁ e₂ => e₁.proof == e₂.proof }

source

structure Lean.Meta.SimpLemmas :

Type

pre : Lean.Meta.DiscrTree Lean.Meta.SimpLemma
post : Lean.Meta.DiscrTree Lean.Meta.SimpLemma
lemmaNames : Std.PHashSet Lean.Name
toUnfold : Std.PHashSet Lean.Name
erased : Std.PHashSet Lean.Name
toUnfoldThms : Std.PHashMap Lean.Name (Array Lean.Name)

source

instance Lean.Meta.instInhabitedSimpLemmas :

Inhabited Lean.Meta.SimpLemmas

Equations

Lean.Meta.instInhabitedSimpLemmas = { default := { pre := default, post := default, lemmaNames := default, toUnfold := default, erased := default, toUnfoldThms := default } }

source

def Lean.Meta.addSimpLemmaEntry (d : Lean.Meta.SimpLemmas) (e : Lean.Meta.SimpLemma) :

Lean.Meta.SimpLemmas

Equations

Lean.Meta.addSimpLemmaEntry d e = (fun updateLemmaNames => if e.post = true then { pre := d.pre, post := Lean.Meta.DiscrTree.insertCore d.post e.keys e, lemmaNames := updateLemmaNames d.lemmaNames, toUnfold := d.toUnfold, erased := d.erased, toUnfoldThms := d.toUnfoldThms } else { pre := Lean.Meta.DiscrTree.insertCore d.pre e.keys e, post := d.post, lemmaNames := updateLemmaNames d.lemmaNames, toUnfold := d.toUnfold, erased := d.erased, toUnfoldThms := d.toUnfoldThms }) (Lean.Meta.addSimpLemmaEntry.updateLemmaNames e)

source

def Lean.Meta.addSimpLemmaEntry.updateLemmaNames (e : Lean.Meta.SimpLemma) (s : Std.PHashSet Lean.Name) :

Std.PHashSet Lean.Name

Equations

Lean.Meta.addSimpLemmaEntry.updateLemmaNames e s = match e.name? with | none => s | some name => Std.PersistentHashSet.insert s name

source

def Lean.Meta.SimpLemmas.addDeclToUnfoldCore (d : Lean.Meta.SimpLemmas) (declName : Lean.Name) :

Lean.Meta.SimpLemmas

Equations

Lean.Meta.SimpLemmas.addDeclToUnfoldCore d declName = { pre := d.pre, post := d.post, lemmaNames := d.lemmaNames, toUnfold := Std.PersistentHashSet.insert d.toUnfold declName, erased := d.erased, toUnfoldThms := d.toUnfoldThms }

source

def Lean.Meta.SimpLemmas.isDeclToUnfold (d : Lean.Meta.SimpLemmas) (declName : Lean.Name) :

Bool

Equations

Lean.Meta.SimpLemmas.isDeclToUnfold d declName = Std.PersistentHashSet.contains d.toUnfold declName

source

def Lean.Meta.SimpLemmas.isLemma (d : Lean.Meta.SimpLemmas) (declName : Lean.Name) :

Bool

Equations

Lean.Meta.SimpLemmas.isLemma d declName = Std.PersistentHashSet.contains d.lemmaNames declName

source

def Lean.Meta.SimpLemmas.registerDeclToUnfoldThms (d : Lean.Meta.SimpLemmas) (declName : Lean.Name) (eqThms : Array Lean.Name) :

Lean.Meta.SimpLemmas

Equations

Lean.Meta.SimpLemmas.registerDeclToUnfoldThms d declName eqThms = { pre := d.pre, post := d.post, lemmaNames := d.lemmaNames, toUnfold := d.toUnfold, erased := d.erased, toUnfoldThms := Std.PersistentHashMap.insert d.toUnfoldThms declName eqThms }

source

partial def Lean.Meta.SimpLemmas.eraseCore (d : Lean.Meta.SimpLemmas) (declName : Lean.Name) :

Lean.Meta.SimpLemmas

source

def Lean.Meta.SimpLemmas.erase {m : Type → Type} [inst : Monad m] [inst : Lean.MonadError m] (d : Lean.Meta.SimpLemmas) (declName : Lean.Name) :

m Lean.Meta.SimpLemmas

Equations

Lean.Meta.SimpLemmas.erase d declName = let _do_jp := fun y => pure (Lean.Meta.SimpLemmas.eraseCore d declName); if (Lean.Meta.SimpLemmas.isLemma d declName || Lean.Meta.SimpLemmas.isDeclToUnfold d declName || Std.PersistentHashMap.contains d.toUnfoldThms declName) = true then do let y ← pure PUnit.unit _do_jp y else do let y ← Lean.throwError (Lean.toMessageData "'" ++ Lean.toMessageData declName ++ Lean.toMessageData "' does not have [simp] attribute") _do_jp y

source

inductive Lean.Meta.SimpEntry :

Type

lemma: Lean.Meta.SimpLemma → Lean.Meta.SimpEntry
toUnfold: Lean.Name → Lean.Meta.SimpEntry
toUnfoldThms: Lean.Name → Array Lean.Name → Lean.Meta.SimpEntry

source

instance Lean.Meta.instInhabitedSimpEntry :

Inhabited Lean.Meta.SimpEntry

Equations

Lean.Meta.instInhabitedSimpEntry = { default := Lean.Meta.SimpEntry.lemma default }

source

@[inline]

abbrev Lean.Meta.SimpExtension :

Type

Equations

Lean.Meta.SimpExtension = Lean.SimpleScopedEnvExtension Lean.Meta.SimpEntry Lean.Meta.SimpLemmas

source

def Lean.Meta.SimpExtension.getLemmas (ext : Lean.Meta.SimpExtension) :

Lean.CoreM Lean.Meta.SimpLemmas

Equations

Lean.Meta.SimpExtension.getLemmas ext = do let a ← Lean.getEnv pure (Lean.ScopedEnvExtension.getState ext a)

source

def Lean.Meta.addSimpLemma (ext : Lean.Meta.SimpExtension) (declName : Lean.Name) (post : Bool) (inv : Bool) (attrKind : Lean.AttributeKind) (prio : Nat) :

Lean.MetaM Unit

Equations

Lean.Meta.addSimpLemma ext declName post inv attrKind prio = do let simpLemmas ← Lean.Meta.mkSimpLemmasFromConst declName post inv prio let r ← forIn simpLemmas PUnit.unit fun simpLemma r => do Lean.ScopedEnvExtension.add ext (Lean.Meta.SimpEntry.lemma simpLemma) attrKind pure (ForInStep.yield PUnit.unit) let x : PUnit := r pure PUnit.unit

source

def Lean.Meta.mkSimpAttr (attrName : Lean.Name) (attrDescr : String) (ext : Lean.Meta.SimpExtension) :

IO Unit

Equations

Lean.Meta.mkSimpAttr attrName attrDescr ext = Lean.registerBuiltinAttribute { toAttributeImplCore := { name := attrName, descr := attrDescr, applicationTime := Lean.AttributeApplicationTime.afterCompilation }, add := fun declName stx attrKind => let go := do let info ← Lean.getConstInfo declName let post : Bool := if Lean.Syntax.isNone (Lean.Syntax.getOp stx 1) = true then true else Lean.Syntax.getKind (Lean.Syntax.getOp (Lean.Syntax.getOp stx 1) 0) == `Lean.Parser.Tactic.simpPost let prio ← liftM (Lean.getAttrParamOptPrio (Lean.Syntax.getOp stx 2)) let a ← Lean.Meta.isProp (Lean.ConstantInfo.type info) if a = true then Lean.Meta.addSimpLemma ext declName post false attrKind prio else if Lean.ConstantInfo.hasValue info = true then do let a ← Lean.Meta.getEqnsFor? declName match a with | some eqns => do let r ← forIn eqns PUnit.unit fun eqn r => do Lean.Meta.addSimpLemma ext eqn post false attrKind prio pure (ForInStep.yield PUnit.unit) let x : PUnit := r Lean.ScopedEnvExtension.add ext (Lean.Meta.SimpEntry.toUnfoldThms declName eqns) attrKind let a ← Lean.getEnv if Lean.Meta.hasSmartUnfoldingDecl a declName = true then Lean.ScopedEnvExtension.add ext (Lean.Meta.SimpEntry.toUnfold declName) attrKind else pure PUnit.unit | x => Lean.ScopedEnvExtension.add ext (Lean.Meta.SimpEntry.toUnfold declName) attrKind else Lean.throwError (Lean.toMessageData "invalid 'simp', it is not a proposition nor a definition (to unfold)"); discard (Lean.Meta.MetaM.run go { config := { foApprox := false, ctxApprox := false, quasiPatternApprox := false, constApprox := false, isDefEqStuckEx := false, transparency := Lean.Meta.TransparencyMode.default, zetaNonDep := true, trackZeta := false, unificationHints := true, proofIrrelevance := true, assignSyntheticOpaque := false, ignoreLevelMVarDepth := true, offsetCnstrs := true, etaStruct := true }, lctx := { fvarIdToDecl := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, decls := { root := Std.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Std.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Std.PersistentArray.branching), size := 0, shift := Std.PersistentArray.initShift, tailOff := 0 } }, localInstances := #[], defEqCtx? := none, synthPendingDepth := 0, canUnfold? := none } { mctx := { depth := 0, mvarCounter := 0, lDepth := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, decls := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, userNames := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, lAssignment := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, eAssignment := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, dAssignment := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 } }, cache := { inferType := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, funInfo := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, synthInstance := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, whnfDefault := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, whnfAll := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, defEqDefault := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, defEqAll := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 } }, zetaFVarIds := ∅, postponed := { root := Std.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Std.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Std.PersistentArray.branching), size := 0, shift := Std.PersistentArray.initShift, tailOff := 0 } }), erase := fun declName => do let a ← Lean.getEnv let s ← pure (Lean.ScopedEnvExtension.getState ext a) let s ← Lean.Meta.SimpLemmas.erase s declName Lean.modifyEnv fun env => Lean.ScopedEnvExtension.modifyState ext env fun x => s }

source

def Lean.Meta.mkSimpExt (extName : Lean.Name) :

IO Lean.Meta.SimpExtension

Equations

Lean.Meta.mkSimpExt extName = Lean.registerSimpleScopedEnvExtension { name := extName, addEntry := fun d e => match e with | Lean.Meta.SimpEntry.lemma e => Lean.Meta.addSimpLemmaEntry d e | Lean.Meta.SimpEntry.toUnfold n => Lean.Meta.SimpLemmas.addDeclToUnfoldCore d n | Lean.Meta.SimpEntry.toUnfoldThms n thms => Lean.Meta.SimpLemmas.registerDeclToUnfoldThms d n thms, initial := { pre := Lean.Meta.DiscrTree.empty, post := Lean.Meta.DiscrTree.empty, lemmaNames := ∅, toUnfold := ∅, erased := ∅, toUnfoldThms := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 } }, finalizeImport := id }

source

def Lean.Meta.registerSimpAttr (attrName : Lean.Name) (attrDescr : String) (extName : optParam Lean.Name (Lean.Name.appendAfter attrName "Ext")) :

IO Lean.Meta.SimpExtension

Equations

Lean.Meta.registerSimpAttr attrName attrDescr extName = do let ext ← Lean.Meta.mkSimpExt extName Lean.Meta.mkSimpAttr attrName attrDescr ext pure ext

source

constant Lean.Meta.simpExtension :

Lean.Meta.SimpExtension

source

def Lean.Meta.getSimpLemmas :

Lean.CoreM Lean.Meta.SimpLemmas

Equations

Lean.Meta.getSimpLemmas = Lean.Meta.SimpExtension.getLemmas Lean.Meta.simpExtension

source

def Lean.Meta.SimpLemmas.addConst (s : Lean.Meta.SimpLemmas) (declName : Lean.Name) (post : optParam Bool true) (inv : optParam Bool false) (prio : optParam Nat 1000) :

Lean.MetaM Lean.Meta.SimpLemmas

Equations

Lean.Meta.SimpLemmas.addConst s declName post inv prio = let s := { pre := s.pre, post := s.post, lemmaNames := s.lemmaNames, toUnfold := s.toUnfold, erased := Std.PersistentHashSet.erase s.erased declName, toUnfoldThms := s.toUnfoldThms }; do let simpLemmas ← Lean.Meta.mkSimpLemmasFromConst declName post inv prio pure (Array.foldl Lean.Meta.addSimpLemmaEntry s simpLemmas 0 (Array.size simpLemmas))

source

def Lean.Meta.SimpLemma.getValue (simpLemma : Lean.Meta.SimpLemma) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.SimpLemma.getValue simpLemma = if (Lean.Expr.isConst simpLemma.proof && Array.isEmpty simpLemma.levelParams) = true then do let info ← Lean.getConstInfo (Lean.Expr.constName! simpLemma.proof) if List.isEmpty (Lean.ConstantInfo.levelParams info) = true then pure simpLemma.proof else do let a ← List.mapM (fun x => Lean.Meta.mkFreshLevelMVar) (Lean.ConstantInfo.levelParams info) pure (Lean.Expr.updateConst! simpLemma.proof a) else do let us ← Array.mapM (fun x => Lean.Meta.mkFreshLevelMVar) simpLemma.levelParams pure (Lean.Expr.instantiateLevelParamsArray simpLemma.proof simpLemma.levelParams us)

source

def Lean.Meta.mkSimpLemmas (levelParams : Array Lean.Name) (proof : Lean.Expr) (post : optParam Bool true) (inv : optParam Bool false) (prio : optParam Nat 1000) (name? : optParam (Option Lean.Name) none) :

Lean.MetaM (Array Lean.Meta.SimpLemma)

Equations

Lean.Meta.mkSimpLemmas levelParams proof post inv prio name? = Lean.Meta.withReducible do let a ← Lean.Meta.preprocessProof proof inv Array.mapM (fun val => Lean.Meta.mkSimpLemmaCore val levelParams val post prio name?) a

source

def Lean.Meta.SimpLemmas.add (s : Lean.Meta.SimpLemmas) (levelParams : Array Lean.Name) (proof : Lean.Expr) (inv : optParam Bool false) (post : optParam Bool true) (prio : optParam Nat 1000) (name? : optParam (Option Lean.Name) none) :

Lean.MetaM Lean.Meta.SimpLemmas

Equations

Lean.Meta.SimpLemmas.add s levelParams proof inv post prio name? = (fun getName? => if Lean.Expr.isConst proof = true then Lean.Meta.SimpLemmas.addConst s (Lean.Expr.constName! proof) post inv prio else do let a ← getName? proof let simpLemmas ← Lean.Meta.mkSimpLemmas levelParams proof post inv prio a pure (Array.foldl Lean.Meta.addSimpLemmaEntry s simpLemmas 0 (Array.size simpLemmas))) (Lean.Meta.SimpLemmas.add.getName? name?)

source

def Lean.Meta.SimpLemmas.add.getName? (name? : optParam (Option Lean.Name) none) (e : Lean.Expr) :

Lean.MetaM (Option Lean.Name)

Equations

Lean.Meta.SimpLemmas.add.getName? name? e = match name? with | some x => pure name? | none => let f := Lean.Expr.getAppFn e; if Lean.Expr.isConst f = true then pure (some (Lean.Expr.constName! f)) else if Lean.Expr.isFVar f = true then do let localDecl ← Lean.Meta.getFVarLocalDecl f pure (some (Lean.LocalDecl.userName localDecl)) else pure none

source

def Lean.Meta.SimpLemmas.addDeclToUnfold (d : Lean.Meta.SimpLemmas) (declName : Lean.Name) :

Lean.MetaM Lean.Meta.SimpLemmas

Equations

Lean.Meta.SimpLemmas.addDeclToUnfold d declName = Lean.Meta.withLCtx { fvarIdToDecl := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, decls := { root := Std.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Std.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Std.PersistentArray.branching), size := 0, shift := Std.PersistentArray.initShift, tailOff := 0 } } ∅ do let a ← Lean.Meta.getEqnsFor? declName match a with | some eqns => let d := d; do let r ← forIn eqns d fun eqn r => let d := r; do let r ← Lean.Meta.SimpLemmas.addConst d eqn true false 1000 let d : Lean.Meta.SimpLemmas := r pure PUnit.unit pure (ForInStep.yield d) let x : Lean.Meta.SimpLemmas := r let d : Lean.Meta.SimpLemmas := x let a ← Lean.getEnv let _do_jp : Lean.Meta.SimpLemmas → PUnit → Lean.MetaM Lean.Meta.SimpLemmas := fun d y => pure d if Lean.Meta.hasSmartUnfoldingDecl a declName = true then let d := Lean.Meta.SimpLemmas.addDeclToUnfoldCore d declName; do let y ← pure PUnit.unit _do_jp d y else do let y ← pure PUnit.unit _do_jp d y | x => pure (Lean.Meta.SimpLemmas.addDeclToUnfoldCore d declName)