diff --git a/src/Lean/Attributes.lean b/src/Lean/Attributes.lean index 0b60c23553..405953f282 100644 --- a/src/Lean/Attributes.lean +++ b/src/Lean/Attributes.lean @@ -138,7 +138,7 @@ structure TagAttribute where def registerTagAttribute (name : Name) (descr : String) (validate : Name → AttrM Unit := fun _ => pure ()) (ref : Name := by exact decl_name%) : IO TagAttribute := do let ext : PersistentEnvExtension Name Name NameSet ← registerPersistentEnvExtension { - name := name + name := ref mkInitial := pure {} addImportedFn := fun _ _ => pure {} addEntryFn := fun (s : NameSet) n => s.insert n @@ -191,7 +191,7 @@ structure ParametricAttributeImpl (α : Type) extends AttributeImplCore where def registerParametricAttribute [Inhabited α] (impl : ParametricAttributeImpl α) : IO (ParametricAttribute α) := do let ext : PersistentEnvExtension (Name × α) (Name × α) (NameMap α) ← registerPersistentEnvExtension { - name := impl.name + name := impl.ref mkInitial := pure {} addImportedFn := fun s => impl.afterImport s *> pure {} addEntryFn := fun (s : NameMap α) (p : Name × α) => s.insert p.1 p.2 @@ -245,12 +245,12 @@ structure EnumAttributes (α : Type) where ext : PersistentEnvExtension (Name × α) (Name × α) (NameMap α) deriving Inhabited -def registerEnumAttributes [Inhabited α] (extName : Name) (attrDescrs : List (Name × String × α)) +def registerEnumAttributes [Inhabited α] (attrDescrs : List (Name × String × α)) (validate : Name → α → AttrM Unit := fun _ _ => pure ()) (applicationTime := AttributeApplicationTime.afterTypeChecking) (ref : Name := by exact decl_name%) : IO (EnumAttributes α) := do let ext : PersistentEnvExtension (Name × α) (Name × α) (NameMap α) ← registerPersistentEnvExtension { - name := extName + name := ref mkInitial := pure {} addImportedFn := fun _ _ => pure {} addEntryFn := fun (s : NameMap α) (p : Name × α) => s.insert p.1 p.2 @@ -366,7 +366,6 @@ private def addAttrEntry (s : AttributeExtensionState) (e : AttributeExtensionOL builtin_initialize attributeExtension : AttributeExtension ← registerPersistentEnvExtension { - name := `attrExt mkInitial := AttributeExtension.mkInitial addImportedFn := AttributeExtension.addImported addEntryFn := addAttrEntry diff --git a/src/Lean/AuxRecursor.lean b/src/Lean/AuxRecursor.lean index 3381a656c8..8e7dbd4ff1 100644 --- a/src/Lean/AuxRecursor.lean +++ b/src/Lean/AuxRecursor.lean @@ -19,7 +19,7 @@ def mkBRecOnName (indDeclName : Name) : Name := Name.mkStr indDeclName brecOnSu def mkBInductionOnName (indDeclName : Name) : Name := Name.mkStr indDeclName binductionOnSuffix def mkBelowName (indDeclName : Name) : Name := Name.mkStr indDeclName belowSuffix -builtin_initialize auxRecExt : TagDeclarationExtension ← mkTagDeclarationExtension `auxRec +builtin_initialize auxRecExt : TagDeclarationExtension ← mkTagDeclarationExtension @[export lean_mark_aux_recursor] def markAuxRecursor (env : Environment) (declName : Name) : Environment := @@ -47,7 +47,7 @@ def isRecOnRecursor (env : Environment) (declName : Name) : Bool := def isBRecOnRecursor (env : Environment) (declName : Name) : Bool := isAuxRecursorWithSuffix env declName brecOnSuffix -builtin_initialize noConfusionExt : TagDeclarationExtension ← mkTagDeclarationExtension `noConf +builtin_initialize noConfusionExt : TagDeclarationExtension ← mkTagDeclarationExtension @[export lean_mark_no_confusion] def markNoConfusion (env : Environment) (n : Name) : Environment := diff --git a/src/Lean/Class.lean b/src/Lean/Class.lean index c8e052d701..f996ff1b5d 100644 --- a/src/Lean/Class.lean +++ b/src/Lean/Class.lean @@ -54,7 +54,6 @@ Type class environment extension -- TODO: add support for scoped instances builtin_initialize classExtension : SimplePersistentEnvExtension ClassEntry ClassState ← registerSimplePersistentEnvExtension { - name := `classExt addEntryFn := ClassState.addEntry addImportedFn := fun es => (mkStateFromImportedEntries ClassState.addEntry {} es).switch } diff --git a/src/Lean/Compiler/CSimpAttr.lean b/src/Lean/Compiler/CSimpAttr.lean index 9af13161c8..1f15f55129 100644 --- a/src/Lean/Compiler/CSimpAttr.lean +++ b/src/Lean/Compiler/CSimpAttr.lean @@ -26,7 +26,6 @@ def State.switch : State → State builtin_initialize ext : SimpleScopedEnvExtension Entry State ← registerSimpleScopedEnvExtension { - name := `csimp initial := {} addEntry := fun { map, thmNames } { fromDeclName, toDeclName, thmName } => { map := map.insert fromDeclName toDeclName, thmNames := thmNames.insert thmName } finalizeImport := fun s => s.switch diff --git a/src/Lean/Compiler/IR/CompilerM.lean b/src/Lean/Compiler/IR/CompilerM.lean index 95964faf6d..159ce7ff10 100644 --- a/src/Lean/Compiler/IR/CompilerM.lean +++ b/src/Lean/Compiler/IR/CompilerM.lean @@ -81,7 +81,6 @@ private def mkEntryArray (decls : List Decl) : Array Decl := builtin_initialize declMapExt : SimplePersistentEnvExtension Decl DeclMap ← registerSimplePersistentEnvExtension { - name := `IRDecls, addImportedFn := fun as => let m : DeclMap := mkStateFromImportedEntries (fun s (d : Decl) => s.insert d.name d) {} as m.switch, diff --git a/src/Lean/Compiler/IR/ElimDeadBranches.lean b/src/Lean/Compiler/IR/ElimDeadBranches.lean index 0848c0547c..d2a1c36d4d 100644 --- a/src/Lean/Compiler/IR/ElimDeadBranches.lean +++ b/src/Lean/Compiler/IR/ElimDeadBranches.lean @@ -126,7 +126,6 @@ abbrev FunctionSummaries := SMap FunId Value builtin_initialize functionSummariesExt : SimplePersistentEnvExtension (FunId × Value) FunctionSummaries ← registerSimplePersistentEnvExtension { - name := `unreachBranchesFunSummary, addImportedFn := fun as => let cache : FunctionSummaries := mkStateFromImportedEntries (fun s (p : FunId × Value) => s.insert p.1 p.2) {} as cache.switch, diff --git a/src/Lean/Compiler/InlineAttrs.lean b/src/Lean/Compiler/InlineAttrs.lean index 71f808f107..e3607828b3 100644 --- a/src/Lean/Compiler/InlineAttrs.lean +++ b/src/Lean/Compiler/InlineAttrs.lean @@ -32,7 +32,7 @@ private def isValidMacroInline (declName : Name) : CoreM Bool := do return true builtin_initialize inlineAttrs : EnumAttributes InlineAttributeKind ← - registerEnumAttributes `inlineAttrs + registerEnumAttributes [(`inline, "mark definition to always be inlined", InlineAttributeKind.inline), (`inlineIfReduce, "mark definition to be inlined when resultant term after reduction is not a `cases_on` application", InlineAttributeKind.inlineIfReduce), (`noinline, "mark definition to never be inlined", InlineAttributeKind.noinline), diff --git a/src/Lean/Compiler/LCNF/Passes.lean b/src/Lean/Compiler/LCNF/Passes.lean index d8062de059..7347dfa3c4 100644 --- a/src/Lean/Compiler/LCNF/Passes.lean +++ b/src/Lean/Compiler/LCNF/Passes.lean @@ -69,7 +69,6 @@ def runImportedDecls (importedDeclNames : Array (Array Name)) : CoreM PassManage builtin_initialize passManagerExt : PersistentEnvExtension Name (Name × PassManager) (List Name × PassManager) ← registerPersistentEnvExtension { - name := `cpass mkInitial := return ([], builtinPassManager) addImportedFn := fun ns => return ([], ← ImportM.runCoreM <| runImportedDecls ns) addEntryFn := fun (installerDeclNames, _) (installerDeclName, managerNew) => (installerDeclName :: installerDeclNames, managerNew) diff --git a/src/Lean/Compiler/LCNF/PhaseExt.lean b/src/Lean/Compiler/LCNF/PhaseExt.lean index cc2f009993..8497046ac0 100644 --- a/src/Lean/Compiler/LCNF/PhaseExt.lean +++ b/src/Lean/Compiler/LCNF/PhaseExt.lean @@ -22,7 +22,7 @@ private abbrev findAtSorted? (decls : Array Decl) (declName : Name) : Option Dec abbrev DeclExt := PersistentEnvExtension Decl Decl DeclExtState -def mkDeclExt (name : Name) : IO DeclExt := do +def mkDeclExt (name : Name := by exact decl_name%) : IO DeclExt := do registerPersistentEnvExtension { name := name mkInitial := return {} @@ -33,8 +33,8 @@ def mkDeclExt (name : Name) : IO DeclExt := do sortDecls decls } -builtin_initialize baseExt : PersistentEnvExtension Decl Decl DeclExtState ← mkDeclExt `compBaseDecls -builtin_initialize monoExt : PersistentEnvExtension Decl Decl DeclExtState ← mkDeclExt `compMonoDecls +builtin_initialize baseExt : PersistentEnvExtension Decl Decl DeclExtState ← mkDeclExt +builtin_initialize monoExt : PersistentEnvExtension Decl Decl DeclExtState ← mkDeclExt def getDeclCore? (env : Environment) (ext : DeclExt) (declName : Name) : Option Decl := match env.getModuleIdxFor? declName with diff --git a/src/Lean/Compiler/LCNF/Simp/ConstantFold.lean b/src/Lean/Compiler/LCNF/Simp/ConstantFold.lean index a0a2d4f8e2..04262c1614 100644 --- a/src/Lean/Compiler/LCNF/Simp/ConstantFold.lean +++ b/src/Lean/Compiler/LCNF/Simp/ConstantFold.lean @@ -384,7 +384,6 @@ structure FolderEntry extends FolderOleanEntry where builtin_initialize folderExt : PersistentEnvExtension FolderOleanEntry FolderEntry (List FolderOleanEntry × SMap Name Folder) ← registerPersistentEnvExtension { - name := `cfolder mkInitial := return ([], builtinFolders) addImportedFn := fun entriesArray => do let ctx ← read diff --git a/src/Lean/Compiler/LCNF/SpecInfo.lean b/src/Lean/Compiler/LCNF/SpecInfo.lean index 41409a3d58..669904fb2d 100644 --- a/src/Lean/Compiler/LCNF/SpecInfo.lean +++ b/src/Lean/Compiler/LCNF/SpecInfo.lean @@ -74,7 +74,6 @@ Remark: we only store information for declarations that will be specialized. -/ builtin_initialize specExtension : SimplePersistentEnvExtension SpecEntry SpecState ← registerSimplePersistentEnvExtension { - name := `specInfoExt addEntryFn := SpecState.addEntry addImportedFn := fun es => mkStateFromImportedEntries SpecState.addEntry {} es |>.switch } diff --git a/src/Lean/Compiler/NoncomputableAttr.lean b/src/Lean/Compiler/NoncomputableAttr.lean index e5ebc2fe33..ad03125f4d 100644 --- a/src/Lean/Compiler/NoncomputableAttr.lean +++ b/src/Lean/Compiler/NoncomputableAttr.lean @@ -7,7 +7,7 @@ import Lean.Environment namespace Lean -builtin_initialize noncomputableExt : TagDeclarationExtension ← mkTagDeclarationExtension `noncomputable +builtin_initialize noncomputableExt : TagDeclarationExtension ← mkTagDeclarationExtension /-- Mark in the environment extension that the given declaration has been declared by the user as `noncomputable`. -/ def addNoncomputable (env : Environment) (declName : Name) : Environment := diff --git a/src/Lean/Compiler/Specialize.lean b/src/Lean/Compiler/Specialize.lean index ecdfd6f33b..1313be9dfb 100644 --- a/src/Lean/Compiler/Specialize.lean +++ b/src/Lean/Compiler/Specialize.lean @@ -106,7 +106,6 @@ end SpecState builtin_initialize specExtension : SimplePersistentEnvExtension SpecEntry SpecState ← registerSimplePersistentEnvExtension { - name := `specExt, addEntryFn := SpecState.addEntry, addImportedFn := fun es => (mkStateFromImportedEntries SpecState.addEntry {} es).switch } diff --git a/src/Lean/DeclarationRange.lean b/src/Lean/DeclarationRange.lean index 1a8e7e369c..7e0c2a099a 100644 --- a/src/Lean/DeclarationRange.lean +++ b/src/Lean/DeclarationRange.lean @@ -36,7 +36,7 @@ instance : ToExpr DeclarationRanges where toTypeExpr := mkConst ``DeclarationRanges builtin_initialize builtinDeclRanges : IO.Ref (NameMap DeclarationRanges) ← IO.mkRef {} -builtin_initialize declRangeExt : MapDeclarationExtension DeclarationRanges ← mkMapDeclarationExtension `declranges +builtin_initialize declRangeExt : MapDeclarationExtension DeclarationRanges ← mkMapDeclarationExtension def addBuiltinDeclarationRanges (declName : Name) (declRanges : DeclarationRanges) : IO Unit := builtinDeclRanges.modify (·.insert declName declRanges) diff --git a/src/Lean/DocString.lean b/src/Lean/DocString.lean index 48cbf7fbf4..e77e76b27e 100644 --- a/src/Lean/DocString.lean +++ b/src/Lean/DocString.lean @@ -9,7 +9,7 @@ import Lean.MonadEnv namespace Lean private builtin_initialize builtinDocStrings : IO.Ref (NameMap String) ← IO.mkRef {} -private builtin_initialize docStringExt : MapDeclarationExtension String ← mkMapDeclarationExtension `docstring +private builtin_initialize docStringExt : MapDeclarationExtension String ← mkMapDeclarationExtension private def findLeadingSpacesSize (s : String) : Nat := let it := s.iter @@ -72,7 +72,6 @@ structure ModuleDoc where declarationRange : DeclarationRange private builtin_initialize moduleDocExt : SimplePersistentEnvExtension ModuleDoc (PersistentArray ModuleDoc) ← registerSimplePersistentEnvExtension { - name := `moduleDocExt addImportedFn := fun _ => {} addEntryFn := fun s e => s.push e toArrayFn := fun es => es.toArray diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean index b55f3c48cd..d412f3acb7 100644 --- a/src/Lean/Elab/Command.lean +++ b/src/Lean/Elab/Command.lean @@ -213,13 +213,13 @@ instance : MonadQuotation CommandElabM where getMainModule := Command.getMainModule withFreshMacroScope := Command.withFreshMacroScope -unsafe def mkCommandElabAttributeUnsafe : IO (KeyedDeclsAttribute CommandElab) := - mkElabAttribute CommandElab `Lean.Elab.Command.commandElabAttribute `builtinCommandElab `commandElab `Lean.Parser.Command `Lean.Elab.Command.CommandElab "command" +unsafe def mkCommandElabAttributeUnsafe (ref : Name) : IO (KeyedDeclsAttribute CommandElab) := + mkElabAttribute CommandElab `builtinCommandElab `commandElab `Lean.Parser.Command `Lean.Elab.Command.CommandElab "command" ref @[implementedBy mkCommandElabAttributeUnsafe] -opaque mkCommandElabAttribute : IO (KeyedDeclsAttribute CommandElab) +opaque mkCommandElabAttribute (ref : Name) : IO (KeyedDeclsAttribute CommandElab) -builtin_initialize commandElabAttribute : KeyedDeclsAttribute CommandElab ← mkCommandElabAttribute +builtin_initialize commandElabAttribute : KeyedDeclsAttribute CommandElab ← mkCommandElabAttribute decl_name% private def mkInfoTree (elaborator : Name) (stx : Syntax) (trees : PersistentArray InfoTree) : CommandElabM InfoTree := do let ctx ← read diff --git a/src/Lean/Elab/PreDefinition/Structural/Eqns.lean b/src/Lean/Elab/PreDefinition/Structural/Eqns.lean index 6eb2de8a50..21c990b4c6 100644 --- a/src/Lean/Elab/PreDefinition/Structural/Eqns.lean +++ b/src/Lean/Elab/PreDefinition/Structural/Eqns.lean @@ -77,7 +77,7 @@ def mkEqns (info : EqnInfo) : MetaM (Array Name) := } return thmNames -builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ← mkMapDeclarationExtension `structEqInfo +builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ← mkMapDeclarationExtension def registerEqnsInfo (preDef : PreDefinition) (recArgPos : Nat) : CoreM Unit := do modifyEnv fun env => eqnInfoExt.insert env preDef.declName { preDef with recArgPos } diff --git a/src/Lean/Elab/PreDefinition/WF/Eqns.lean b/src/Lean/Elab/PreDefinition/WF/Eqns.lean index df87a094b3..22605f3b8e 100644 --- a/src/Lean/Elab/PreDefinition/WF/Eqns.lean +++ b/src/Lean/Elab/PreDefinition/WF/Eqns.lean @@ -206,7 +206,7 @@ def mkEqns (declName : Name) (info : EqnInfo) : MetaM (Array Name) := } return thmNames -builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ← mkMapDeclarationExtension `wfEqInfo +builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ← mkMapDeclarationExtension def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name) (fixedPrefixSize : Nat) : CoreM Unit := do let declNames := preDefs.map (·.declName) diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean index 369a902b94..21b2ae0327 100644 --- a/src/Lean/Elab/Tactic/Basic.lean +++ b/src/Lean/Elab/Tactic/Basic.lean @@ -97,7 +97,7 @@ protected def getCurrMacroScope : TacticM MacroScope := do pure (← readThe Cor protected def getMainModule : TacticM Name := do pure (← getEnv).mainModule unsafe def mkTacticAttribute : IO (KeyedDeclsAttribute Tactic) := - mkElabAttribute Tactic `Lean.Elab.Tactic.tacticElabAttribute `builtinTactic `tactic `Lean.Parser.Tactic `Lean.Elab.Tactic.Tactic "tactic" + mkElabAttribute Tactic `builtinTactic `tactic `Lean.Parser.Tactic `Lean.Elab.Tactic.Tactic "tactic" `Lean.Elab.Tactic.tacticElabAttribute @[builtinInit mkTacticAttribute] opaque tacticElabAttribute : KeyedDeclsAttribute Tactic diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index 8d44b773bd..6585e3c459 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -350,13 +350,13 @@ private def withoutModifyingStateWithInfoAndMessagesImpl (x : TermElabM α) : Te def withoutSavingRecAppSyntax (x : TermElabM α) : TermElabM α := withReader (fun ctx => { ctx with saveRecAppSyntax := false }) x -unsafe def mkTermElabAttributeUnsafe : IO (KeyedDeclsAttribute TermElab) := - mkElabAttribute TermElab `Lean.Elab.Term.termElabAttribute `builtinTermElab `termElab `Lean.Parser.Term `Lean.Elab.Term.TermElab "term" +unsafe def mkTermElabAttributeUnsafe (ref : Name) : IO (KeyedDeclsAttribute TermElab) := + mkElabAttribute TermElab `builtinTermElab `termElab `Lean.Parser.Term `Lean.Elab.Term.TermElab "term" ref @[implementedBy mkTermElabAttributeUnsafe] -opaque mkTermElabAttribute : IO (KeyedDeclsAttribute TermElab) +opaque mkTermElabAttribute (ref : Name) : IO (KeyedDeclsAttribute TermElab) -builtin_initialize termElabAttribute : KeyedDeclsAttribute TermElab ← mkTermElabAttribute +builtin_initialize termElabAttribute : KeyedDeclsAttribute TermElab ← mkTermElabAttribute decl_name% /-- Auxiliary datatatype for presenting a Lean lvalue modifier. diff --git a/src/Lean/Elab/Util.lean b/src/Lean/Elab/Util.lean index 6414a8e12d..c4478cdaa5 100644 --- a/src/Lean/Elab/Util.lean +++ b/src/Lean/Elab/Util.lean @@ -91,8 +91,8 @@ private unsafe def evalSyntaxConstantUnsafe (env : Environment) (opts : Options) @[implementedBy evalSyntaxConstantUnsafe] opaque evalSyntaxConstant (env : Environment) (opts : Options) (constName : Name) : ExceptT String Id Syntax := throw "" -unsafe def mkElabAttribute (γ) (attrDeclName attrBuiltinName attrName : Name) (parserNamespace : Name) (typeName : Name) (kind : String) - : IO (KeyedDeclsAttribute γ) := +unsafe def mkElabAttribute (γ) (attrBuiltinName attrName : Name) (parserNamespace : Name) (typeName : Name) (kind : String) + (attrDeclName : Name := by exact decl_name%) : IO (KeyedDeclsAttribute γ) := KeyedDeclsAttribute.init { builtinName := attrBuiltinName name := attrName @@ -118,13 +118,13 @@ unsafe def mkElabAttribute (γ) (attrDeclName attrBuiltinName attrName : Name) ( declareBuiltin (declName ++ `declRange) (mkAppN (mkConst ``addBuiltinDeclarationRanges) #[toExpr declName, toExpr declRanges]) } attrDeclName -unsafe def mkMacroAttributeUnsafe : IO (KeyedDeclsAttribute Macro) := - mkElabAttribute Macro `Lean.Elab.macroAttribute `builtinMacro `macro Name.anonymous `Lean.Macro "macro" +unsafe def mkMacroAttributeUnsafe (ref : Name) : IO (KeyedDeclsAttribute Macro) := + mkElabAttribute Macro `builtinMacro `macro Name.anonymous `Lean.Macro "macro" ref @[implementedBy mkMacroAttributeUnsafe] -opaque mkMacroAttribute : IO (KeyedDeclsAttribute Macro) +opaque mkMacroAttribute (ref : Name) : IO (KeyedDeclsAttribute Macro) -builtin_initialize macroAttribute : KeyedDeclsAttribute Macro ← mkMacroAttribute +builtin_initialize macroAttribute : KeyedDeclsAttribute Macro ← mkMacroAttribute decl_name% /-- Try to expand macro at syntax tree root and return macro declaration name and new syntax if successful. diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean index 7767c4b740..8ea1b315ff 100644 --- a/src/Lean/Environment.lean +++ b/src/Lean/Environment.lean @@ -440,7 +440,7 @@ end PersistentEnvExtension builtin_initialize persistentEnvExtensionsRef : IO.Ref (Array (PersistentEnvExtension EnvExtensionEntry EnvExtensionEntry EnvExtensionState)) ← IO.mkRef #[] structure PersistentEnvExtensionDescr (α β σ : Type) where - name : Name + name : Name := by exact decl_name% mkInitial : IO σ addImportedFn : Array (Array α) → ImportM σ addEntryFn : σ → β → σ @@ -478,7 +478,7 @@ def SimplePersistentEnvExtension (α σ : Type) := PersistentEnvExtension α α as.foldl (fun r es => es.foldl (fun r e => addEntryFn r e) r) initState structure SimplePersistentEnvExtensionDescr (α σ : Type) where - name : Name + name : Name := by exact decl_name% addEntryFn : σ → α → σ addImportedFn : Array (Array α) → σ toArrayFn : List α → Array α := fun es => es.toArray @@ -522,7 +522,7 @@ end SimplePersistentEnvExtension Declarations must only be tagged in the module where they were declared. -/ def TagDeclarationExtension := SimplePersistentEnvExtension Name NameSet -def mkTagDeclarationExtension (name : Name) : IO TagDeclarationExtension := +def mkTagDeclarationExtension (name : Name := by exact decl_name%) : IO TagDeclarationExtension := registerSimplePersistentEnvExtension { name := name, addImportedFn := fun _ => {}, @@ -551,7 +551,7 @@ end TagDeclarationExtension def MapDeclarationExtension (α : Type) := SimplePersistentEnvExtension (Name × α) (NameMap α) -def mkMapDeclarationExtension [Inhabited α] (name : Name) : IO (MapDeclarationExtension α) := +def mkMapDeclarationExtension [Inhabited α] (name : Name := by exact decl_name%) : IO (MapDeclarationExtension α) := registerSimplePersistentEnvExtension { name := name, addImportedFn := fun _ => {}, @@ -612,13 +612,9 @@ unsafe def Environment.freeRegions (env : Environment) : IO Unit := def mkModuleData (env : Environment) : IO ModuleData := do let pExts ← persistentEnvExtensionsRef.get - let entries : Array (Name × Array EnvExtensionEntry) := pExts.size.fold - (fun i result => - let state := (pExts.get! i).getState env - let exportEntriesFn := (pExts.get! i).exportEntriesFn - let extName := (pExts.get! i).name - result.push (extName, exportEntriesFn state)) - #[] + let entries := pExts.map fun pExt => + let state := pExt.getState env + (pExt.name, pExt.exportEntriesFn state) pure { imports := env.header.imports constants := env.constants.foldStage2 (fun cs _ c => cs.push c) #[] @@ -764,7 +760,6 @@ Environment extension for tracking all `namespace` declared by users. -/ builtin_initialize namespacesExt : SimplePersistentEnvExtension Name NameSSet ← registerSimplePersistentEnvExtension { - name := `namespaces addImportedFn := fun as => mkStateFromImportedEntries NameSSet.insert NameSSet.empty as |>.switch addEntryFn := fun s n => s.insert n } diff --git a/src/Lean/KeyedDeclsAttribute.lean b/src/Lean/KeyedDeclsAttribute.lean index be7634ffbb..d6dccb9dc9 100644 --- a/src/Lean/KeyedDeclsAttribute.lean +++ b/src/Lean/KeyedDeclsAttribute.lean @@ -100,10 +100,10 @@ def ExtensionState.erase (s : ExtensionState γ) (attrName : Name) (declName : N throwError "'{declName}' does not have [{attrName}] attribute" return { s with erased := s.erased.insert declName, declNames := s.declNames.erase declName } -protected unsafe def init {γ} (df : Def γ) (attrDeclName : Name) : IO (KeyedDeclsAttribute γ) := do +protected unsafe def init {γ} (df : Def γ) (attrDeclName : Name := by exact decl_name%) : IO (KeyedDeclsAttribute γ) := do let tableRef ← IO.mkRef ({} : Table γ) let ext : Extension γ ← registerScopedEnvExtension { - name := df.name + name := attrDeclName mkInitial := return mkStateOfTable (← tableRef.get) ofOLeanEntry := fun _ entry => do let ctx ← read diff --git a/src/Lean/Linter/MissingDocs.lean b/src/Lean/Linter/MissingDocs.lean index 19e237ad3a..ed129e66bd 100644 --- a/src/Lean/Linter/MissingDocs.lean +++ b/src/Lean/Linter/MissingDocs.lean @@ -49,7 +49,6 @@ builtin_initialize builtinHandlersRef : IO.Ref (NameMap Handler) ← IO.mkRef {} builtin_initialize missingDocsExt : PersistentEnvExtension (Name × Name) (Name × Name × Handler) (List (Name × Name) × NameMap Handler) ← registerPersistentEnvExtension { - name := "missing docs extension" mkInitial := return ([], ← builtinHandlersRef.get) addImportedFn := fun as => do ([], ·) <$> as.foldlM (init := ← builtinHandlersRef.get) fun s as => diff --git a/src/Lean/Linter/UnusedVariables.lean b/src/Lean/Linter/UnusedVariables.lean index 89e468c94a..399c1c37b6 100644 --- a/src/Lean/Linter/UnusedVariables.lean +++ b/src/Lean/Linter/UnusedVariables.lean @@ -104,7 +104,6 @@ builtin_initialize addBuiltinUnusedVariablesIgnoreFn (fun _ stack opts => builtin_initialize unusedVariablesIgnoreFnsExt : SimplePersistentEnvExtension Name Unit ← registerSimplePersistentEnvExtension { - name := `unusedVariablesIgnoreFns addEntryFn := fun _ _ => () addImportedFn := fun _ => () } diff --git a/src/Lean/Meta/GlobalInstances.lean b/src/Lean/Meta/GlobalInstances.lean index 6178e99269..db9b7e5c3e 100644 --- a/src/Lean/Meta/GlobalInstances.lean +++ b/src/Lean/Meta/GlobalInstances.lean @@ -10,7 +10,6 @@ namespace Lean.Meta builtin_initialize globalInstanceExtension : SimpleScopedEnvExtension Name (PersistentHashMap Name Unit) ← registerSimpleScopedEnvExtension { - name := `ginstanceExt initial := {} addEntry := fun s n => s.insert n () } diff --git a/src/Lean/Meta/Instances.lean b/src/Lean/Meta/Instances.lean index 7fb8445a6e..f3bb6a2d15 100644 --- a/src/Lean/Meta/Instances.lean +++ b/src/Lean/Meta/Instances.lean @@ -45,7 +45,6 @@ def Instances.erase [Monad m] [MonadError m] (d : Instances) (declName : Name) : builtin_initialize instanceExtension : SimpleScopedEnvExtension InstanceEntry Instances ← registerSimpleScopedEnvExtension { - name := `instanceExt initial := {} addEntry := addInstanceEntry } @@ -106,7 +105,6 @@ def addDefaultInstanceEntry (d : DefaultInstances) (e : DefaultInstanceEntry) : builtin_initialize defaultInstanceExtension : SimplePersistentEnvExtension DefaultInstanceEntry DefaultInstances ← registerSimplePersistentEnvExtension { - name := `defaultInstanceExt addEntryFn := addDefaultInstanceEntry addImportedFn := fun es => (mkStateFromImportedEntries addDefaultInstanceEntry {} es) } diff --git a/src/Lean/Meta/Match/MatcherInfo.lean b/src/Lean/Meta/Match/MatcherInfo.lean index 87f78e6092..2aff1764fe 100644 --- a/src/Lean/Meta/Match/MatcherInfo.lean +++ b/src/Lean/Meta/Match/MatcherInfo.lean @@ -79,7 +79,6 @@ def State.switch (s : State) : State := { s with map := s.map.switch } builtin_initialize extension : SimplePersistentEnvExtension Entry State ← registerSimplePersistentEnvExtension { - name := `matcher addEntryFn := State.addEntry addImportedFn := fun es => (mkStateFromImportedEntries State.addEntry {} es).switch } diff --git a/src/Lean/Meta/Tactic/ElimInfo.lean b/src/Lean/Meta/Tactic/ElimInfo.lean index 921485bdea..58fb1fa4ff 100644 --- a/src/Lean/Meta/Tactic/ElimInfo.lean +++ b/src/Lean/Meta/Tactic/ElimInfo.lean @@ -107,7 +107,6 @@ def addCustomEliminatorEntry (es : CustomEliminators) (e : CustomEliminator) : C builtin_initialize customEliminatorExt : SimpleScopedEnvExtension CustomEliminator CustomEliminators ← registerSimpleScopedEnvExtension { - name := `elimExt initial := {} addEntry := addCustomEliminatorEntry finalizeImport := fun { map := map } => { map := map.switch } diff --git a/src/Lean/Meta/Tactic/Simp/SimpCongrTheorems.lean b/src/Lean/Meta/Tactic/Simp/SimpCongrTheorems.lean index 3ecee3b311..fecade5fef 100644 --- a/src/Lean/Meta/Tactic/Simp/SimpCongrTheorems.lean +++ b/src/Lean/Meta/Tactic/Simp/SimpCongrTheorems.lean @@ -44,7 +44,6 @@ where builtin_initialize congrExtension : SimpleScopedEnvExtension SimpCongrTheorem SimpCongrTheorems ← registerSimpleScopedEnvExtension { - name := `congrExt initial := {} addEntry := addSimpCongrTheoremEntry finalizeImport := fun s => { s with lemmas := s.lemmas.switch } diff --git a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean index dcc99c5cdf..c45c0afe17 100644 --- a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean +++ b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean @@ -356,9 +356,9 @@ def mkSimpAttr (attrName : Name) (attrDescr : String) (ext : SimpExtension) modifyEnv fun env => ext.modifyState env fun _ => s } -def mkSimpExt (extName : Name) : IO SimpExtension := +def mkSimpExt (name : Name := by exact decl_name%) : IO SimpExtension := registerSimpleScopedEnvExtension { - name := extName + name := name initial := {} addEntry := fun d e => match e with @@ -372,9 +372,8 @@ abbrev SimpExtensionMap := HashMap Name SimpExtension builtin_initialize simpExtensionMapRef : IO.Ref SimpExtensionMap ← IO.mkRef {} def registerSimpAttr (attrName : Name) (attrDescr : String) - (ref : Name := by exact decl_name%) - (extName : Name := attrName.appendAfter "Ext") : IO SimpExtension := do - let ext ← mkSimpExt extName + (ref : Name := by exact decl_name%) : IO SimpExtension := do + let ext ← mkSimpExt ref mkSimpAttr attrName attrDescr ext ref -- Remark: it will fail if it is not performed during initialization simpExtensionMapRef.modify fun map => map.insert attrName ext return ext diff --git a/src/Lean/Meta/UnificationHint.lean b/src/Lean/Meta/UnificationHint.lean index 9c3957537f..6fb958b229 100644 --- a/src/Lean/Meta/UnificationHint.lean +++ b/src/Lean/Meta/UnificationHint.lean @@ -27,7 +27,6 @@ def UnificationHints.add (hints : UnificationHints) (e : UnificationHintEntry) : builtin_initialize unificationHintExtension : SimpleScopedEnvExtension UnificationHintEntry UnificationHints ← registerSimpleScopedEnvExtension { - name := `unifHints addEntry := UnificationHints.add initial := {} } diff --git a/src/Lean/Modifiers.lean b/src/Lean/Modifiers.lean index 710cc3d65e..741c69af09 100644 --- a/src/Lean/Modifiers.lean +++ b/src/Lean/Modifiers.lean @@ -7,7 +7,7 @@ import Lean.Environment namespace Lean -builtin_initialize protectedExt : TagDeclarationExtension ← mkTagDeclarationExtension `protected +builtin_initialize protectedExt : TagDeclarationExtension ← mkTagDeclarationExtension @[export lean_add_protected] def addProtected (env : Environment) (n : Name) : Environment := diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean index d983ee15f9..39a4f19e19 100644 --- a/src/Lean/Parser/Extension.lean +++ b/src/Lean/Parser/Extension.lean @@ -339,7 +339,6 @@ private def ParserExtension.OLeanEntry.toEntry (s : State) : OLeanEntry → Impo builtin_initialize parserExtension : ParserExtension ← registerScopedEnvExtension { - name := `parserExt mkInitial := ParserExtension.mkInitial addEntry := ParserExtension.addEntryImpl toOLeanEntry := ParserExtension.Entry.toOLeanEntry diff --git a/src/Lean/ParserCompiler/Attribute.lean b/src/Lean/ParserCompiler/Attribute.lean index 150fe0af8a..f4d3cf76c9 100644 --- a/src/Lean/ParserCompiler/Attribute.lean +++ b/src/Lean/ParserCompiler/Attribute.lean @@ -17,14 +17,15 @@ structure CombinatorAttribute where deriving Inhabited -- TODO(Sebastian): We'll probably want priority support here at some point -def registerCombinatorAttribute (name : Name) (descr : String) +def registerCombinatorAttribute (name : Name) (descr : String) (ref : Name := by exact decl_name%) : IO CombinatorAttribute := do let ext : SimplePersistentEnvExtension (Name × Name) (NameMap Name) ← registerSimplePersistentEnvExtension { - name := name, + name := ref, addImportedFn := mkStateFromImportedEntries (fun s p => s.insert p.1 p.2) {}, addEntryFn := fun (s : NameMap Name) (p : Name × Name) => s.insert p.1 p.2, } let attrImpl : AttributeImpl := { + ref := ref, name := name, descr := descr, add := fun decl stx _ => do diff --git a/src/Lean/ProjFns.lean b/src/Lean/ProjFns.lean index fa5f827a3d..e48f028e0c 100644 --- a/src/Lean/ProjFns.lean +++ b/src/Lean/ProjFns.lean @@ -29,7 +29,7 @@ def mkProjectionInfoEx (ctorName : Name) (numParams : Nat) (i : Nat) (fromClass def ProjectionFunctionInfo.fromClassEx (info : ProjectionFunctionInfo) : Bool := info.fromClass -builtin_initialize projectionFnInfoExt : MapDeclarationExtension ProjectionFunctionInfo ← mkMapDeclarationExtension `projinfo +builtin_initialize projectionFnInfoExt : MapDeclarationExtension ProjectionFunctionInfo ← mkMapDeclarationExtension @[export lean_add_projection_info] def addProjectionFnInfo (env : Environment) (projName : Name) (ctorName : Name) (numParams : Nat) (i : Nat) (fromClass : Bool) : Environment := diff --git a/src/Lean/ReducibilityAttrs.lean b/src/Lean/ReducibilityAttrs.lean index 5040d76a6d..9d3e66ec61 100644 --- a/src/Lean/ReducibilityAttrs.lean +++ b/src/Lean/ReducibilityAttrs.lean @@ -18,7 +18,7 @@ inductive ReducibilityStatus where Environment extension for storing the reducibility attribute for definitions. -/ builtin_initialize reducibilityAttrs : EnumAttributes ReducibilityStatus ← - registerEnumAttributes `reducibility + registerEnumAttributes [(`reducible, "reducible", ReducibilityStatus.reducible), (`semireducible, "semireducible", ReducibilityStatus.semireducible), (`irreducible, "irreducible", ReducibilityStatus.irreducible)] diff --git a/src/Lean/ResolveName.lean b/src/Lean/ResolveName.lean index 44645f5a55..6238ec3ad8 100644 --- a/src/Lean/ResolveName.lean +++ b/src/Lean/ResolveName.lean @@ -24,7 +24,6 @@ def addAliasEntry (s : AliasState) (e : AliasEntry) : AliasState := builtin_initialize aliasExtension : SimplePersistentEnvExtension AliasEntry AliasState ← registerSimplePersistentEnvExtension { - name := `aliasesExt, addEntryFn := addAliasEntry, addImportedFn := fun es => mkStateFromImportedEntries addAliasEntry {} es |>.switch } diff --git a/src/Lean/ScopedEnvExtension.lean b/src/Lean/ScopedEnvExtension.lean index 475da37e77..9feaaeafeb 100644 --- a/src/Lean/ScopedEnvExtension.lean +++ b/src/Lean/ScopedEnvExtension.lean @@ -30,7 +30,7 @@ structure StateStack (α : Type) (β : Type) (σ : Type) where deriving Inhabited structure Descr (α : Type) (β : Type) (σ : Type) where - name : Name + name : Name := by exact decl_name% mkInitial : IO σ ofOLeanEntry : σ → α → ImportM β toOLeanEntry : β → α @@ -197,7 +197,7 @@ def activateScoped [Monad m] [MonadEnv m] [MonadLiftT (ST IO.RealWorld) m] (name abbrev SimpleScopedEnvExtension (α : Type) (σ : Type) := ScopedEnvExtension α α σ structure SimpleScopedEnvExtension.Descr (α : Type) (σ : Type) where - name : Name + name : Name := by exact decl_name% addEntry : σ → α → σ initial : σ finalizeImport : σ → σ := id diff --git a/src/Lean/Server/Completion.lean b/src/Lean/Server/Completion.lean index 717c1e0c80..723b69c7f7 100644 --- a/src/Lean/Server/Completion.lean +++ b/src/Lean/Server/Completion.lean @@ -20,7 +20,7 @@ open Elab open Meta open FuzzyMatching -builtin_initialize completionBlackListExt : TagDeclarationExtension ← mkTagDeclarationExtension `blackListCompletion +builtin_initialize completionBlackListExt : TagDeclarationExtension ← mkTagDeclarationExtension @[export lean_completion_add_to_black_list] def addToBlackList (env : Environment) (declName : Name) : Environment := diff --git a/src/Lean/Server/Rpc/RequestHandling.lean b/src/Lean/Server/Rpc/RequestHandling.lean index 04bf080b1a..6aaad08984 100644 --- a/src/Lean/Server/Rpc/RequestHandling.lean +++ b/src/Lean/Server/Rpc/RequestHandling.lean @@ -21,7 +21,7 @@ they *can* easily create custom handlers and use them in the same file. -/ builtin_initialize builtinRpcProcedures : IO.Ref (PHashMap Name RpcProcedure) ← IO.mkRef {} builtin_initialize userRpcProcedures : MapDeclarationExtension Name ← - mkMapDeclarationExtension `userRpcProcedures + mkMapDeclarationExtension private unsafe def evalRpcProcedureUnsafe (env : Environment) (opts : Options) (procName : Name) : Except String RpcProcedure := diff --git a/src/Lean/Structure.lean b/src/Lean/Structure.lean index bf06c5fb54..19b5493dbe 100644 --- a/src/Lean/Structure.lean +++ b/src/Lean/Structure.lean @@ -44,7 +44,6 @@ private structure StructureState where deriving Inhabited builtin_initialize structureExt : SimplePersistentEnvExtension StructureInfo StructureState ← registerSimplePersistentEnvExtension { - name := `structExt addImportedFn := fun _ => {} addEntryFn := fun s e => { s with map := s.map.insert e.structName e } toArrayFn := fun es => es.toArray.qsort StructureInfo.lt diff --git a/src/Lean/Widget/UserWidget.lean b/src/Lean/Widget/UserWidget.lean index d2d07fbf80..d338dfcf99 100644 --- a/src/Lean/Widget/UserWidget.lean +++ b/src/Lean/Widget/UserWidget.lean @@ -54,10 +54,9 @@ private abbrev WidgetSourceRegistry := SimplePersistentEnvExtension (RBMap UInt64 Name compare) -- Mapping widgetSourceId to hash of sourcetext -builtin_initialize userWidgetRegistry : MapDeclarationExtension UserWidget ← mkMapDeclarationExtension `widgetRegistry +builtin_initialize userWidgetRegistry : MapDeclarationExtension UserWidget ← mkMapDeclarationExtension builtin_initialize widgetSourceRegistry : WidgetSourceRegistry ← registerSimplePersistentEnvExtension { - name := `widgetSourceRegistry addImportedFn := fun xss => xss.foldl (Array.foldl (fun s n => s.insert n.1 n.2)) ∅ addEntryFn := fun s n => s.insert n.1 n.2 toArrayFn := fun es => es.toArray diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h index aae6413ccc..82742d5e98 100644 --- a/stage0/src/stdlib_flags.h +++ b/stage0/src/stdlib_flags.h @@ -6,7 +6,7 @@ options get_default_options() { // see https://leanprover.github.io/lean4/doc/dev/bootstrap.html#further-bootstrapping-complications #if LEAN_IS_STAGE0 == 1 // switch to `true` for ABI-breaking changes affecting meta code - opts = opts.update({"interpreter", "prefer_native"}, false); + opts = opts.update({"interpreter", "prefer_native"}, true); // switch to `true` for changing built-in parsers used in quotations opts = opts.update({"internal", "parseQuotWithCurrentStage"}, false); opts = opts.update({"pp", "rawOnError"}, true); diff --git a/tests/pkg/user_ext/UserExt/BlaExt.lean b/tests/pkg/user_ext/UserExt/BlaExt.lean index 5284117fe9..2645b01cec 100644 --- a/tests/pkg/user_ext/UserExt/BlaExt.lean +++ b/tests/pkg/user_ext/UserExt/BlaExt.lean @@ -4,7 +4,6 @@ open Lean initialize blaExtension : SimplePersistentEnvExtension Name NameSet ← registerSimplePersistentEnvExtension { - name := `blaExt addEntryFn := NameSet.insert addImportedFn := fun es => mkStateFromImportedEntries NameSet.insert {} es } diff --git a/tests/pkg/user_ext/UserExt/FooExt.lean b/tests/pkg/user_ext/UserExt/FooExt.lean index 686ec53f82..252a3958f4 100644 --- a/tests/pkg/user_ext/UserExt/FooExt.lean +++ b/tests/pkg/user_ext/UserExt/FooExt.lean @@ -4,7 +4,6 @@ open Lean initialize fooExtension : SimplePersistentEnvExtension Name NameSet ← registerSimplePersistentEnvExtension { - name := `fooExt addEntryFn := NameSet.insert addImportedFn := fun es => mkStateFromImportedEntries NameSet.insert {} es }