namespace Lean

def addMeta (env : Environment) (declName : Name) : Environment :=

builtin_initialize defeqAttr : TagAttribute ←

registerTagAttribute `defeq "mark theorem as a definitional equality, to be used by `dsimp`"

(validate := validateDefEqAttr) (applicationTime := .afterTypeChecking)

private partial def isRflProofCore (type : Expr) (proof : Expr) : CoreM Bool := do

match type with

def getState {α σ : Type} [Inhabited σ] (ext : SimplePersistentEnvExtension α σ) (env : Environment)

def setState {α σ : Type} (ext : SimplePersistentEnvExtension α σ) (env : Environment) (s : σ) : Environment :=

def modifyState {α σ : Type} (ext : SimplePersistentEnvExtension α σ) (env : Environment) (f : σ → σ) : Environment :=

PersistentEnvExtension.modifyState ext env (fun ⟨entries, s⟩ => (entries, f s))

end SimplePersistentEnvExtension

def isTagged (ext : TagDeclarationExtension) (env : Environment) (declName : Name) : Bool :=

match env.getModuleIdxFor? declName with

| some modIdx => (ext.getModuleEntries env modIdx).binSearchContains declName Name.quickLt

end TagDeclarationExtension

addImportedFn := fun _ => pure {}

addEntryFn := fun s (n, v) => s.insert n v

exportEntriesFnEx env s level := exportEntriesFn env s level

replay? := some fun _ newState newConsts s =>

newConsts.foldl (init := s) fun s c =>

if let some a := newState.find? c then

match (ext.getModuleEntries (level := level) env modIdx).binSearch (declName, default) (fun a b => Name.quickLt a.1 b.1) with

| some e => some e.2

| none => none

def contains [Inhabited α] (ext : MapDeclarationExtension α) (env : Environment) (declName : Name) : Bool :=

match env.getModuleIdxFor? declName with

| some modIdx => (ext.getModuleEntries env modIdx).binSearchContains (declName, default) (fun a b => Name.quickLt a.1 b.1)

end MapDeclarationExtension

let some aconsts := aconsts.get? AsyncConsts | .pure none

AsyncConsts.findRecTask aconsts declName

private inductive Visibility where

/-- Information private to the module. -/

end ConstantInfo

deriving Inhabited

abbrev ReplayFn (σ : Type) :=

private unsafe def getStateUnsafe {σ : Type} [Inhabited σ] (ext : EnvExtension σ)

-- safety: `ext`'s constructor is private, so we can assume the entry at `ext.idx` is of type `σ`

match asyncMode with

| _ => ext.getStateImpl env.base.private.extensions

end EnvExtension

def getState {α β σ : Type} [Inhabited σ] (ext : PersistentEnvExtension α β σ) (env : Environment)

def setState {α β σ : Type} (ext : PersistentEnvExtension α β σ) (env : Environment) (s : σ) : Environment :=

(asyncMode := ext.toEnvExtension.asyncMode) : Environment :=

ext.toEnvExtension.modifyState (asyncMode := asyncMode) env fun ps => { ps with state := f (ps.state) }

end PersistentEnvExtension

builtin_initialize persistentEnvExtensionsRef : IO.Ref (Array (PersistentEnvExtension EnvExtensionEntry EnvExtensionEntry EnvExtensionState)) ← IO.mkRef #[]

let entries := pExts.map fun pExt => Id.run do

-- get state from `checked` at the end if `async`; it would otherwise panic

let mut asyncMode := pExt.toEnvExtension.asyncMode

asyncMode := .sync

let state := pExt.getState (asyncMode := asyncMode) env

(pExt.name, pExt.exportEntriesFn env state level)

IO.println ("extension '" ++ toString extDescr.name ++ "'")

-- get state from `checked` at the end if `async`; it would otherwise panic

let mut asyncMode := extDescr.toEnvExtension.asyncMode

asyncMode := .sync

let s := extDescr.toEnvExtension.getState (asyncMode := asyncMode) env

let fmt := extDescr.statsFn s.state

builtin_initialize recExt : TagDeclarationExtension ←

-- `realizeConst` as well as for looking up the resultant environment extension state via

-- `findStateAsync`.

realizeConst matchDeclName splitterName (go baseName splitterName)

where go baseName splitterName := withConfig (fun c => { c with etaStruct := .none }) do

let constInfo ← getConstInfo matchDeclName

let us := constInfo.levelParams.map mkLevelParam

let baseName := mkPrivateName (← getEnv) matchDeclName

let firstEqnName := .str baseName congrEqn1ThmSuffix

realizeConst matchDeclName firstEqnName (go baseName)

where go baseName := withConfig (fun c => { c with etaStruct := .none }) do

withConfig (fun c => { c with etaStruct := .none }) do

let constInfo ← getConstInfo matchDeclName

let .str _ s := declName.eraseMacroScopes | return false

if !isEqnLikeSuffix s then

return false

end Lean.Meta.Match

registerSimplePersistentEnvExtension {

addEntryFn := State.addEntry

addImportedFn := fun es => (mkStateFromImportedEntries State.addEntry {} es).switch

}

def addMatcherInfo (env : Environment) (matcherName : Name) (info : MatcherInfo) : Environment :=

-- avoid blocking on async decls whose names look nothing like matchers

let .str _ s := declName.eraseMacroScopes | none

guard <| s.startsWith "match_"

end Extension