From c23d6e9018c96034bbd492146d4de254d48cd238 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 20 Nov 2024 13:21:14 +0100 Subject: [PATCH] refactor: move registration of namespaces on kernel add into elaborator --- src/Lean/AddDecl.lean | 41 ++++++++++++++++++++++++++----- src/Lean/Compiler/InitAttr.lean | 11 +++++---- src/Lean/Elab/BuiltinCommand.lean | 4 +-- src/Lean/Environment.lean | 29 ++-------------------- src/Lean/ParserCompiler.lean | 7 ++---- src/Lean/Replay.lean | 2 +- src/library/elab_environment.cpp | 10 +++----- 7 files changed, 51 insertions(+), 53 deletions(-) diff --git a/src/Lean/AddDecl.lean b/src/Lean/AddDecl.lean index e17cfdb029eb..6bfd77d78b9d 100644 --- a/src/Lean/AddDecl.lean +++ b/src/Lean/AddDecl.lean @@ -22,26 +22,55 @@ def Kernel.Environment.addDecl (env : Environment) (opts : Options) (decl : Decl else addDeclCore env (Core.getMaxHeartbeats opts).toUSize decl cancelTk? -def Environment.addDecl (env : Environment) (opts : Options) (decl : Declaration) +private def Environment.addDeclAux (env : Environment) (opts : Options) (decl : Declaration) (cancelTk? : Option IO.CancelToken := none) : Except Kernel.Exception Environment := if debug.skipKernelTC.get opts then addDeclWithoutChecking env decl else addDeclCore env (Core.getMaxHeartbeats opts).toUSize decl cancelTk? +@[deprecated "use `Lean.addDecl` instead to ensure new namespaces are registered" (since := "2024-12-03")] +def Environment.addDecl (env : Environment) (opts : Options) (decl : Declaration) + (cancelTk? : Option IO.CancelToken := none) : Except Kernel.Exception Environment := + Environment.addDeclAux env opts decl cancelTk? + +@[deprecated "use `Lean.addAndCompile` instead to ensure new namespaces are registered" (since := "2024-12-03")] def Environment.addAndCompile (env : Environment) (opts : Options) (decl : Declaration) (cancelTk? : Option IO.CancelToken := none) : Except Kernel.Exception Environment := do - let env ← addDecl env opts decl cancelTk? + let env ← addDeclAux env opts decl cancelTk? compileDecl env opts decl +private def isNamespaceName : Name → Bool + | .str .anonymous _ => true + | .str p _ => isNamespaceName p + | _ => false + +private def registerNamePrefixes (env : Environment) (name : Name) : Environment := + match name with + | .str _ s => + if s.get 0 == '_' then + -- Do not register namespaces that only contain internal declarations. + env + else + go env name + | _ => env +where go env + | .str p _ => if isNamespaceName p then go (env.registerNamespace p) p else env + | _ => env + def addDecl (decl : Declaration) : CoreM Unit := do profileitM Exception "type checking" (← getOptions) do - withTraceNode `Kernel (fun _ => return m!"typechecking declaration") do + let mut env ← withTraceNode `Kernel (fun _ => return m!"typechecking declaration") do if !(← MonadLog.hasErrors) && decl.hasSorry then logWarning "declaration uses 'sorry'" - match (← getEnv).addDecl (← getOptions) decl (← read).cancelTk? with - | .ok env => setEnv env - | .error ex => throwKernelException ex + (← getEnv).addDeclAux (← getOptions) decl (← read).cancelTk? |> ofExceptKernelException + + -- register namespaces for newly added constants; this used to be done by the kernel itself + -- but that is incompatible with moving it to a separate task + env := decl.getNames.foldl registerNamePrefixes env + if let .inductDecl _ _ types _ := decl then + env := types.foldl (registerNamePrefixes · <| ·.name ++ `rec) env + setEnv env def addAndCompile (decl : Declaration) : CoreM Unit := do addDecl decl diff --git a/src/Lean/Compiler/InitAttr.lean b/src/Lean/Compiler/InitAttr.lean index 212e3c6de316..518ce6f13953 100644 --- a/src/Lean/Compiler/InitAttr.lean +++ b/src/Lean/Compiler/InitAttr.lean @@ -144,11 +144,12 @@ def declareBuiltin (forDecl : Name) (value : Expr) : CoreM Unit := do let type := mkApp (mkConst `IO) (mkConst `Unit) let decl := Declaration.defnDecl { name, levelParams := [], type, value, hints := ReducibilityHints.opaque, safety := DefinitionSafety.safe } - match (← getEnv).addAndCompile {} decl with - -- TODO: pretty print error - | Except.error e => do - let msg ← (e.toMessageData {}).toString + try + addAndCompile decl + catch e => do + -- TODO: pretty print error + let msg ← e.toMessageData.toString throwError "failed to emit registration code for builtin '{forDecl}': {msg}" - | Except.ok env => IO.ofExcept (setBuiltinInitAttr env name) >>= setEnv + IO.ofExcept (setBuiltinInitAttr (← getEnv) name) >>= setEnv end Lean diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean index 1175b39ce651..3d337e015ca7 100644 --- a/src/Lean/Elab/BuiltinCommand.lean +++ b/src/Lean/Elab/BuiltinCommand.lean @@ -124,9 +124,7 @@ private partial def elabChoiceAux (cmds : Array Syntax) (i : Nat) : CommandElabM n[1].forArgsM addUnivLevel @[builtin_command_elab «init_quot»] def elabInitQuot : CommandElab := fun _ => do - match (← getEnv).addDecl (← getOptions) Declaration.quotDecl with - | Except.ok env => setEnv env - | Except.error ex => throwError (ex.toMessageData (← getOptions)) + liftCoreM <| addDecl Declaration.quotDecl @[builtin_command_elab «export»] def elabExport : CommandElab := fun stx => do let `(export $ns ($ids*)) := stx | throwUnsupportedSyntax diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean index 60fa4e767a09..f43e4e504c55 100644 --- a/src/Lean/Environment.lean +++ b/src/Lean/Environment.lean @@ -1077,34 +1077,9 @@ def isNamespace (env : Environment) (n : Name) : Bool := def getNamespaceSet (env : Environment) : NameSSet := namespacesExt.getState env -private def isNamespaceName : Name → Bool - | .str .anonymous _ => true - | .str p _ => isNamespaceName p - | _ => false - -private def registerNamePrefixes (env : Environment) (name : Name) : Environment := - match name with - | .str _ s => - if s.get 0 == '_' then - -- Do not register namespaces that only contain internal declarations. - env - else - go env name - | _ => env -where go env - | .str p _ => if isNamespaceName p then go (registerNamespace env p) p else env - | _ => env - @[export lean_elab_environment_update_base_after_kernel_add] -private def updateBaseAfterKernelAdd (env : Environment) (added : Declaration) (base : Kernel.Environment) : Environment := Id.run do - let mut env := { env with base } - env := added.getNames.foldl registerNamePrefixes env - if let .inductDecl _ _ types _ := added then - -- also register inductive type names as namespaces; this used to be done by the kernel itself - -- when adding e.g. the recursor but now that the environment extension API exists only for - -- `Lean.Environment`, we have to do it here - env := types.foldl (registerNamePrefixes · <| ·.name ++ `rec) env - env +private def updateBaseAfterKernelAdd (env : Environment) (base : Kernel.Environment) : Environment := + { env with base } @[export lean_display_stats] def displayStats (env : Environment) : IO Unit := do diff --git a/src/Lean/ParserCompiler.lean b/src/Lean/ParserCompiler.lean index 3d15ea6436dc..6cdc9ce46a70 100644 --- a/src/Lean/ParserCompiler.lean +++ b/src/Lean/ParserCompiler.lean @@ -103,11 +103,8 @@ partial def compileParserExpr (e : Expr) : MetaM Expr := do name := c', levelParams := [] type := ty, value := value, hints := ReducibilityHints.opaque, safety := DefinitionSafety.safe } - let env ← getEnv - let env ← match env.addAndCompile {} decl with - | Except.ok env => pure env - | Except.error kex => do throwError (← (kex.toMessageData {}).toString) - setEnv <| ctx.combinatorAttr.setDeclFor env c c' + addAndCompile decl + modifyEnv (ctx.combinatorAttr.setDeclFor · c c') if cinfo.type.isConst then if let some kind ← parserNodeKind? cinfo.value! then -- If the parser is parameter-less and produces a node of kind `kind`, diff --git a/src/Lean/Replay.lean b/src/Lean/Replay.lean index 93977b5c660a..930ae4f0be9c 100644 --- a/src/Lean/Replay.lean +++ b/src/Lean/Replay.lean @@ -55,7 +55,7 @@ def throwKernelException (ex : Kernel.Exception) : M Unit := do /-- Add a declaration, possibly throwing a `Kernel.Exception`. -/ def addDecl (d : Declaration) : M Unit := do - match (← get).env.addDecl {} d with + match (← get).env.addDeclCore 0 d (cancelTk? := none) with | .ok env => modify fun s => { s with env := env } | .error ex => throwKernelException ex diff --git a/src/library/elab_environment.cpp b/src/library/elab_environment.cpp index 537169f4ec51..3c43d127293f 100644 --- a/src/library/elab_environment.cpp +++ b/src/library/elab_environment.cpp @@ -11,19 +11,17 @@ Authors: Leonardo de Moura, Sebastian Ullrich #include "library/compiler/ir_interpreter.h" namespace lean { -/* updateBaseAfterKernelAdd (env : Environment) (added : Declaration) (base : Kernel.Environment) : - Environment +/* updateBaseAfterKernelAdd (env : Environment) (base : Kernel.Environment) : Environment - Updates an elab environment with a given kernel environment after the declaration `d` has been - added to it. `d` is used to adjust further elab env data such as registering new namespaces. + Updates an elab environment with a given kernel environment. NOTE: Ideally this language switching would not be necessary and we could do all this in Lean only but the old code generator and `mk_projections` still need a C++ `elab_environment::add`. */ -extern "C" obj_res lean_elab_environment_update_base_after_kernel_add(obj_arg env, obj_arg d, obj_arg kenv); +extern "C" obj_res lean_elab_environment_update_base_after_kernel_add(obj_arg env, obj_arg kenv); elab_environment elab_environment::add(declaration const & d, bool check) const { environment kenv = to_kernel_env().add(d, check); - return elab_environment(lean_elab_environment_update_base_after_kernel_add(this->to_obj_arg(), d.to_obj_arg(), kenv.to_obj_arg())); + return elab_environment(lean_elab_environment_update_base_after_kernel_add(this->to_obj_arg(), kenv.to_obj_arg())); } extern "C" LEAN_EXPORT object * lean_elab_add_decl(object * env, size_t max_heartbeat, object * decl,