From 05ab0d995eb5150b63e9155e7bea121dfed292ec 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 | 32 ++++++++++++++++++++++++++++---- src/Lean/Environment.lean | 30 +++--------------------------- src/library/elab_environment.cpp | 10 ++++------ 3 files changed, 35 insertions(+), 37 deletions(-) diff --git a/src/Lean/AddDecl.lean b/src/Lean/AddDecl.lean index 57dcbdac2514..f2a9e47139b0 100644 --- a/src/Lean/AddDecl.lean +++ b/src/Lean/AddDecl.lean @@ -8,19 +8,43 @@ import Lean.CoreM namespace Lean +@[deprecated "use `Lean.addAndCompile` instead"] 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? 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).addDecl (← 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/Environment.lean b/src/Lean/Environment.lean index df078fd93a1a..c9b6b5584859 100644 --- a/src/Lean/Environment.lean +++ b/src/Lean/Environment.lean @@ -320,6 +320,7 @@ opaque addDeclCore (env : Environment) (maxHeartbeats : USize) (decl : @& Declar @[inherit_doc Kernel.Environment.addDeclWithoutChecking, extern "lean_elab_add_decl_without_checking"] opaque addDeclWithoutChecking (env : Environment) (decl : @& Declaration) : Except Kernel.Exception Environment +@[deprecated "use `Lean.addDecl` instead"] def addDecl (env : Environment) (opts : Options) (decl : Declaration) (cancelTk? : Option IO.CancelToken := none) : Except Kernel.Exception Environment := if debug.skipKernelTC.get opts then @@ -1103,34 +1104,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/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,