From 3f09d74c25d05b8788b55a0eecd956a75b386c66 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 23 Aug 2024 17:39:05 +0200 Subject: [PATCH] feat: split `Lean.Kernel.Environment` from `Lean.Environment` --- src/CMakeLists.txt | 6 +- src/Lean/AddDecl.lean | 12 +- src/Lean/Compiler/Old.lean | 4 +- src/Lean/CoreM.lean | 4 +- src/Lean/Declaration.lean | 13 + src/Lean/Elab/Structure.lean | 2 +- src/Lean/Environment.lean | 401 +++++++++++------- src/Lean/Exception.lean | 4 +- src/Lean/Message.lean | 8 +- src/Lean/Meta/Constructions/CasesOn.lean | 4 +- src/Lean/Meta/Constructions/NoConfusion.lean | 4 +- src/Lean/Replay.lean | 10 +- src/kernel/environment.cpp | 35 +- src/kernel/environment.h | 17 +- src/kernel/kernel_exception.h | 4 +- src/kernel/trace.cpp | 16 +- src/kernel/trace.h | 14 +- src/kernel/type_checker.cpp | 24 +- src/kernel/type_checker.h | 2 + src/lake/Lake/Load/Lean/Elab.lean | 4 +- src/library/CMakeLists.txt | 3 +- src/library/aux_recursors.cpp | 4 +- src/library/aux_recursors.h | 6 +- src/library/class.cpp | 6 +- src/library/class.h | 7 +- src/library/compiler/closed_term_cache.cpp | 7 +- src/library/compiler/closed_term_cache.h | 6 +- src/library/compiler/compiler.cpp | 32 +- src/library/compiler/compiler.h | 6 +- src/library/compiler/cse.cpp | 17 +- src/library/compiler/cse.h | 12 +- src/library/compiler/csimp.cpp | 17 +- src/library/compiler/csimp.h | 8 +- src/library/compiler/eager_lambda_lifting.cpp | 16 +- src/library/compiler/eager_lambda_lifting.h | 4 +- src/library/compiler/erase_irrelevant.cpp | 9 +- src/library/compiler/erase_irrelevant.h | 6 +- src/library/compiler/export_attribute.cpp | 3 +- src/library/compiler/export_attribute.h | 6 +- src/library/compiler/extern_attribute.cpp | 12 +- src/library/compiler/extern_attribute.h | 14 +- src/library/compiler/extract_closed.cpp | 12 +- src/library/compiler/extract_closed.h | 4 +- src/library/compiler/find_jp.cpp | 6 +- src/library/compiler/find_jp.h | 4 +- .../compiler/implemented_by_attribute.cpp | 4 +- .../compiler/implemented_by_attribute.h | 6 +- src/library/compiler/init_attribute.cpp | 4 +- src/library/compiler/init_attribute.h | 6 +- src/library/compiler/ir.cpp | 29 +- src/library/compiler/ir.h | 10 +- src/library/compiler/ir_interpreter.cpp | 38 +- src/library/compiler/ir_interpreter.h | 6 +- src/library/compiler/lambda_lifting.cpp | 12 +- src/library/compiler/lambda_lifting.h | 4 +- src/library/compiler/lcnf.cpp | 9 +- src/library/compiler/lcnf.h | 6 +- src/library/compiler/ll_infer_type.cpp | 15 +- src/library/compiler/ll_infer_type.h | 8 +- src/library/compiler/llnf.cpp | 13 +- src/library/compiler/llnf.h | 8 +- src/library/compiler/reduce_arity.cpp | 4 +- src/library/compiler/reduce_arity.h | 2 +- src/library/compiler/simp_app_args.cpp | 7 +- src/library/compiler/simp_app_args.h | 4 +- src/library/compiler/specialize.cpp | 44 +- src/library/compiler/specialize.h | 4 +- src/library/compiler/struct_cases_on.cpp | 9 +- src/library/compiler/struct_cases_on.h | 4 +- src/library/compiler/util.cpp | 51 +-- src/library/compiler/util.h | 47 +- src/library/constructions/no_confusion.cpp | 10 +- src/library/constructions/no_confusion.h | 6 +- src/library/constructions/projection.cpp | 8 +- src/library/elab_environment.cpp | 74 ++++ src/library/elab_environment.h | 43 ++ src/library/module.cpp | 2 +- src/library/module.h | 4 +- src/library/projection.cpp | 6 +- src/library/projection.h | 12 +- src/library/reducible.cpp | 8 +- src/library/reducible.h | 9 +- src/util/shell.cpp | 13 +- stage0/src/stdlib_flags.h | 2 +- tests/lean/ctor_layout.lean.expected.out | 1 - tests/lean/prvCtor.lean | 2 +- tests/lean/prvCtor.lean.expected.out | 2 +- tests/lean/run/structure.lean | 4 +- 88 files changed, 779 insertions(+), 596 deletions(-) create mode 100644 src/library/elab_environment.cpp create mode 100644 src/library/elab_environment.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 95eece17470a2..2f03e98dc4dbf 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -698,17 +698,17 @@ else() endif() if(NOT ${CMAKE_SYSTEM_NAME} MATCHES "Emscripten") - add_custom_target(lake_lib ALL + add_custom_target(lake_lib WORKING_DIRECTORY ${LEAN_SOURCE_DIR} DEPENDS leanshared COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make Lake VERBATIM) - add_custom_target(lake_shared ALL + add_custom_target(lake_shared WORKING_DIRECTORY ${LEAN_SOURCE_DIR} DEPENDS lake_lib COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make libLake_shared VERBATIM) - add_custom_target(lake ALL + add_custom_target(lake #ALL WORKING_DIRECTORY ${LEAN_SOURCE_DIR} DEPENDS lake_shared COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make lake diff --git a/src/Lean/AddDecl.lean b/src/Lean/AddDecl.lean index 128fb20a00cfa..e17cfdb029eb4 100644 --- a/src/Lean/AddDecl.lean +++ b/src/Lean/AddDecl.lean @@ -14,15 +14,23 @@ register_builtin_option debug.skipKernelTC : Bool := { descr := "skip kernel type checker. WARNING: setting this option to true may compromise soundness because your proofs will not be checked by the Lean kernel" } +/-- Adds given declaration to the environment, respecting `debug.skipKernelTC`. -/ +def Kernel.Environment.addDecl (env : Environment) (opts : Options) (decl : Declaration) + (cancelTk? : Option IO.CancelToken := none) : Except Exception Environment := + if debug.skipKernelTC.get opts then + addDeclWithoutChecking env decl + else + addDeclCore env (Core.getMaxHeartbeats opts).toUSize decl cancelTk? + def Environment.addDecl (env : Environment) (opts : Options) (decl : Declaration) - (cancelTk? : Option IO.CancelToken := none) : Except KernelException Environment := + (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? def Environment.addAndCompile (env : Environment) (opts : Options) (decl : Declaration) - (cancelTk? : Option IO.CancelToken := none) : Except KernelException Environment := do + (cancelTk? : Option IO.CancelToken := none) : Except Kernel.Exception Environment := do let env ← addDecl env opts decl cancelTk? compileDecl env opts decl diff --git a/src/Lean/Compiler/Old.lean b/src/Lean/Compiler/Old.lean index 52908bc84eda8..a075766ccd751 100644 --- a/src/Lean/Compiler/Old.lean +++ b/src/Lean/Compiler/Old.lean @@ -61,10 +61,10 @@ Compile the given block of mutual declarations. Assumes the declarations have already been added to the environment using `addDecl`. -/ @[extern "lean_compile_decls"] -opaque compileDecls (env : Environment) (opt : @& Options) (decls : @& List Name) : Except KernelException Environment +opaque compileDecls (env : Environment) (opt : @& Options) (decls : @& List Name) : Except Kernel.Exception Environment /-- Compile the given declaration, it assumes the declaration has already been added to the environment using `addDecl`. -/ -def compileDecl (env : Environment) (opt : @& Options) (decl : @& Declaration) : Except KernelException Environment := +def compileDecl (env : Environment) (opt : @& Options) (decl : @& Declaration) : Except Kernel.Exception Environment := compileDecls env opt (Compiler.getDeclNamesForCodeGen decl) end Environment diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean index f6d34ca8042ad..214d52928f05b 100644 --- a/src/Lean/CoreM.lean +++ b/src/Lean/CoreM.lean @@ -523,7 +523,7 @@ def compileDecl (decl : Declaration) : CoreM Unit := do return (← getEnv).compileDecl opts decl match res with | Except.ok env => setEnv env - | Except.error (KernelException.other msg) => + | Except.error (.other msg) => checkUnsupported decl -- Generate nicer error message for unsupported recursors and axioms throwError msg | Except.error ex => @@ -535,7 +535,7 @@ def compileDecls (decls : List Name) : CoreM Unit := do compileDeclsNew decls match (← getEnv).compileDecls opts decls with | Except.ok env => setEnv env - | Except.error (KernelException.other msg) => + | Except.error (.other msg) => throwError msg | Except.error ex => throwKernelException ex diff --git a/src/Lean/Declaration.lean b/src/Lean/Declaration.lean index b764111ddaa99..3dbe9687e7217 100644 --- a/src/Lean/Declaration.lean +++ b/src/Lean/Declaration.lean @@ -193,6 +193,19 @@ def Declaration.definitionVal! : Declaration → DefinitionVal | .defnDecl val => val | _ => panic! "Expected a `Declaration.defnDecl`." +/-- +Returns all top-level names to be defined by adding this declaration to the environment. This does +not include auxiliary definitions such as projections. +-/ +def Declaration.getNames : Declaration → List Name + | .axiomDecl val => [val.name] + | .defnDecl val => [val.name] + | .thmDecl val => [val.name] + | .opaqueDecl val => [val.name] + | .quotDecl => [``Quot, ``Quot.mk, ``Quot.lift, ``Quot.ind] + | .mutualDefnDecl defns => defns.map (·.name) + | .inductDecl _ _ types _ => types.map (·.name) + @[specialize] def Declaration.foldExprM {α} {m : Type → Type} [Monad m] (d : Declaration) (f : α → Expr → m α) (a : α) : m α := match d with | Declaration.quotDecl => pure a diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean index 557a8b22991f9..925c0fd6c3aa2 100644 --- a/src/Lean/Elab/Structure.lean +++ b/src/Lean/Elab/Structure.lean @@ -681,7 +681,7 @@ private partial def checkResultingUniversesForFields (fieldInfos : Array StructF throwErrorAt info.ref msg @[extern "lean_mk_projections"] -private opaque mkProjections (env : Environment) (structName : Name) (projs : List Name) (isClass : Bool) : Except KernelException Environment +private opaque mkProjections (env : Environment) (structName : Name) (projs : List Name) (isClass : Bool) : Except Kernel.Exception Environment private def addProjections (r : ElabHeaderResult) (fieldInfos : Array StructFieldInfo) : TermElabM Unit := do if r.type.isProp then diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean index 7c28cedbf7c16..0070c97fe71c9 100644 --- a/src/Lean/Environment.lean +++ b/src/Lean/Environment.lean @@ -88,11 +88,6 @@ structure EnvironmentHeader where -/ trustLevel : UInt32 := 0 /-- - `quotInit = true` if the command `init_quot` has already been executed for the environment, and - `Quot` declarations have been added to the environment. - -/ - quotInit : Bool := false - /-- Name of the module being compiled. -/ mainModule : Name := default @@ -106,6 +101,15 @@ structure EnvironmentHeader where moduleData : Array ModuleData := #[] deriving Nonempty +namespace Kernel + +structure Diagnostics where + /-- Number of times each declaration has been unfolded by the kernel. -/ + unfoldCounter : PHashMap Name Nat := {} + /-- If `enabled = true`, kernel records declarations that have been unfolded. -/ + enabled : Bool := false + deriving Inhabited + /-- An environment stores declarations provided by the user. The kernel currently supports different kinds of declarations such as definitions, theorems, @@ -121,10 +125,33 @@ declared by users are stored in an environment extension. Users can declare new using meta-programming. -/ structure Environment where - /-- The constructor of `Environment` is private to protect against modification - that bypasses the kernel. -/ + /-- + The constructor of `Environment` is private to protect against modification that bypasses the + kernel. + -/ private mk :: /-- + Mapping from constant name to `ConstantInfo`. It contains all constants (definitions, theorems, + axioms, etc) that have been already type checked by the kernel. + -/ + constants : ConstMap + /-- + `quotInit = true` if the command `init_quot` has already been executed for the environment, and + `Quot` declarations have been added to the environment. When the flag is set, the type checker can + assume that the `Quot` declarations in the environment have indeed been added by the kernel and + not by the user. + -/ + quotInit : Bool := false + /-- + Diagnostic information collected during kernel execution. + + Remark: We store kernel diagnostic information in an environment field to simplify the interface + with the kernel implemented in C/C++. Thus, we can only track declarations in methods, such as + `addDecl`, which return a new environment. `Kernel.isDefEq` and `Kernel.whnf` do not update the + statistics. We claim this is ok since these methods are mainly used for debugging. + -/ + diagnostics : Diagnostics := {} + /-- Mapping from constant name to module (index) where constant has been declared. Recall that a Lean file has a header where previously compiled modules can be imported. Each imported module has a unique `ModuleIdx`. @@ -134,31 +161,155 @@ structure Environment where the field `constants`. These auxiliary constants are invisible to the Lean kernel and elaborator. Only the code generator uses them. -/ - const2ModIdx : Std.HashMap Name ModuleIdx - /-- - Mapping from constant name to `ConstantInfo`. It contains all constants (definitions, theorems, axioms, etc) - that have been already type checked by the kernel. - -/ - constants : ConstMap + const2ModIdx : Std.HashMap Name ModuleIdx /-- Environment extensions. It also includes user-defined extensions. -/ - extensions : Array EnvExtensionState + private extensions : Array EnvExtensionState /-- Constant names to be saved in the field `extraConstNames` at `ModuleData`. It contains auxiliary declaration names created by the code generator which are not in `constants`. When importing modules, we want to insert them at `const2ModIdx`. -/ - extraConstNames : NameSet - /-- The header contains additional information that is not updated often. -/ - header : EnvironmentHeader := {} - deriving Nonempty + private extraConstNames : NameSet + /-- The header contains additional information that is set at import time. -/ + header : EnvironmentHeader := {} +deriving Nonempty + +/-- Exceptions that can be raised by the kernel when type checking new declarations. -/ +inductive Exception where + | unknownConstant (env : Environment) (name : Name) + | alreadyDeclared (env : Environment) (name : Name) + | declTypeMismatch (env : Environment) (decl : Declaration) (givenType : Expr) + | declHasMVars (env : Environment) (name : Name) (expr : Expr) + | declHasFVars (env : Environment) (name : Name) (expr : Expr) + | funExpected (env : Environment) (lctx : LocalContext) (expr : Expr) + | typeExpected (env : Environment) (lctx : LocalContext) (expr : Expr) + | letTypeMismatch (env : Environment) (lctx : LocalContext) (name : Name) (givenType : Expr) (expectedType : Expr) + | exprTypeMismatch (env : Environment) (lctx : LocalContext) (expr : Expr) (expectedType : Expr) + | appTypeMismatch (env : Environment) (lctx : LocalContext) (app : Expr) (funType : Expr) (argType : Expr) + | invalidProj (env : Environment) (lctx : LocalContext) (proj : Expr) + | thmTypeIsNotProp (env : Environment) (name : Name) (type : Expr) + | other (msg : String) + | deterministicTimeout + | excessiveMemory + | deepRecursion + | interrupted namespace Environment -private def addAux (env : Environment) (cinfo : ConstantInfo) : Environment := +@[export lean_environment_find] +def find? (env : Environment) (n : Name) : Option ConstantInfo := + /- It is safe to use `find'` because we never overwrite imported declarations. -/ + env.constants.find?' n + +@[export lean_environment_mark_quot_init] +private def markQuotInit (env : Environment) : Environment := + { env with quotInit := true } + +@[export lean_environment_quot_init] +private def isQuotInit (env : Environment) : Bool := + env.quotInit + +/-- Type check given declaration and add it to the environment -/ +@[extern "lean_add_decl"] +opaque addDeclCore (env : Environment) (maxHeartbeats : USize) (decl : @& Declaration) + (cancelTk? : @& Option IO.CancelToken) : Except Exception Environment + +/-- +Add declaration to kernel without type checking it. + +**WARNING** This function is meant for temporarily working around kernel performance issues. +It compromises soundness because, for example, a buggy tactic may produce an invalid proof, +and the kernel will not catch it if the new option is set to true. +-/ +@[extern "lean_add_decl_without_checking"] +opaque addDeclWithoutChecking (env : Environment) (decl : @& Declaration) : Except Exception Environment + +@[export lean_environment_add] +private def add (env : Environment) (cinfo : ConstantInfo) : Environment := { env with constants := env.constants.insert cinfo.name cinfo } +@[export lean_kernel_diag_is_enabled] +def Diagnostics.isEnabled (d : Diagnostics) : Bool := + d.enabled + +/-- Enables/disables kernel diagnostics. -/ +def enableDiag (env : Environment) (flag : Bool) : Environment := + { env with diagnostics.enabled := flag } + +def isDiagnosticsEnabled (env : Environment) : Bool := + env.diagnostics.enabled + +def resetDiag (env : Environment) : Environment := + { env with diagnostics.unfoldCounter := {} } + +@[export lean_kernel_record_unfold] +def Diagnostics.recordUnfold (d : Diagnostics) (declName : Name) : Diagnostics := + if d.enabled then + let cNew := if let some c := d.unfoldCounter.find? declName then c + 1 else 1 + { d with unfoldCounter := d.unfoldCounter.insert declName cNew } + else + d + +@[export lean_kernel_get_diag] +def getDiagnostics (env : Environment) : Diagnostics := + env.diagnostics + +@[export lean_kernel_set_diag] +def setDiagnostics (env : Environment) (diag : Diagnostics) : Environment := + { env with diagnostics := diag} + +end Kernel.Environment + +@[deprecated Kernel.Exception] +abbrev KernelException := Kernel.Exception + +/-- +Elaboration-specific extension of `Kernel.Environment` that adds tracking of asynchronously +elaborated declarations. +-/ +structure Environment where + /- + Like with `Kernel.Environment`, this constructor is private to protect consistency of the + environment, though there are no soundness concerns in this case given that it is used purely for + elaboration. + -/ + private mk :: + private base : Kernel.Environment + -- TODO: async data +deriving Nonempty + +namespace Environment + +@[export lean_elab_environment_of_kernel_env] +def ofKernelEnv (env : Kernel.Environment) : Environment := + { base := env } + +@[export lean_elab_environment_to_kernel_env] +def toKernelEnv (env : Environment) : Kernel.Environment := + env.base + +/-- Type check given declaration and add it to the environment. -/ +@[extern "lean_elab_add_decl"] +opaque addDeclCore (env : Environment) (maxHeartbeats : USize) (decl : @& Declaration) + (cancelTk? : @& Option IO.CancelToken) : Except Kernel.Exception Environment + +@[inherit_doc Kernel.Environment.addDeclWithoutChecking, extern "lean_elab_add_decl_without_checking"] +opaque addDeclWithoutChecking (env : Environment) (decl : @& Declaration) : Except Kernel.Exception Environment + +@[inherit_doc Kernel.Environment.constants] +def constants (env : Environment) : ConstMap := + env.toKernelEnv.constants + +@[inherit_doc Kernel.Environment.const2ModIdx] +def const2ModIdx (env : Environment) : Std.HashMap Name ModuleIdx := + env.toKernelEnv.const2ModIdx + +@[export lean_elab_environment_add] +private def add (env : Environment) (cinfo : ConstantInfo) : Environment := + { env with base := env.base.add cinfo } + /-- Save an extra constant name that is used to populate `const2ModIdx` when we import .olean files. We use this feature to save in which module an auxiliary declaration @@ -168,9 +319,8 @@ def addExtraName (env : Environment) (name : Name) : Environment := if env.constants.contains name then env else - { env with extraConstNames := env.extraConstNames.insert name } + { env with base.extraConstNames := env.base.extraConstNames.insert name } -@[export lean_environment_find] def find? (env : Environment) (n : Name) : Option ConstantInfo := /- It is safe to use `find'` because we never overwrite imported declarations. -/ env.constants.find?' n @@ -178,34 +328,23 @@ def find? (env : Environment) (n : Name) : Option ConstantInfo := def contains (env : Environment) (n : Name) : Bool := env.constants.contains n +def header (env : Environment) : EnvironmentHeader := + env.base.header + def imports (env : Environment) : Array Import := env.header.imports def allImportedModuleNames (env : Environment) : Array Name := env.header.moduleNames -@[export lean_environment_set_main_module] def setMainModule (env : Environment) (m : Name) : Environment := - { env with header := { env.header with mainModule := m } } + { env with base.header.mainModule := m } -@[export lean_environment_main_module] def mainModule (env : Environment) : Name := env.header.mainModule -@[export lean_environment_mark_quot_init] -private def markQuotInit (env : Environment) : Environment := - { env with header := { env.header with quotInit := true } } - -@[export lean_environment_quot_init] -private def isQuotInit (env : Environment) : Bool := - env.header.quotInit - -@[export lean_environment_trust_level] -private def getTrustLevel (env : Environment) : UInt32 := - env.header.trustLevel - def getModuleIdxFor? (env : Environment) (declName : Name) : Option ModuleIdx := - env.const2ModIdx[declName]? + env.base.const2ModIdx[declName]? def isConstructor (env : Environment) (declName : Name) : Bool := match env.find? declName with @@ -222,46 +361,6 @@ def getModuleIdx? (env : Environment) (moduleName : Name) : Option ModuleIdx := end Environment -/-- Exceptions that can be raised by the Kernel when type checking new declarations. -/ -inductive KernelException where - | unknownConstant (env : Environment) (name : Name) - | alreadyDeclared (env : Environment) (name : Name) - | declTypeMismatch (env : Environment) (decl : Declaration) (givenType : Expr) - | declHasMVars (env : Environment) (name : Name) (expr : Expr) - | declHasFVars (env : Environment) (name : Name) (expr : Expr) - | funExpected (env : Environment) (lctx : LocalContext) (expr : Expr) - | typeExpected (env : Environment) (lctx : LocalContext) (expr : Expr) - | letTypeMismatch (env : Environment) (lctx : LocalContext) (name : Name) (givenType : Expr) (expectedType : Expr) - | exprTypeMismatch (env : Environment) (lctx : LocalContext) (expr : Expr) (expectedType : Expr) - | appTypeMismatch (env : Environment) (lctx : LocalContext) (app : Expr) (funType : Expr) (argType : Expr) - | invalidProj (env : Environment) (lctx : LocalContext) (proj : Expr) - | thmTypeIsNotProp (env : Environment) (name : Name) (type : Expr) - | other (msg : String) - | deterministicTimeout - | excessiveMemory - | deepRecursion - | interrupted - -namespace Environment - -/-- -Type check given declaration and add it to the environment --/ -@[extern "lean_add_decl"] -opaque addDeclCore (env : Environment) (maxHeartbeats : USize) (decl : @& Declaration) - (cancelTk? : @& Option IO.CancelToken) : Except KernelException Environment - -/-- -Add declaration to kernel without type checking it. -**WARNING** This function is meant for temporarily working around kernel performance issues. -It compromises soundness because, for example, a buggy tactic may produce an invalid proof, -and the kernel will not catch it if the new option is set to true. --/ -@[extern "lean_add_decl_without_checking"] -opaque addDeclWithoutChecking (env : Environment) (decl : @& Declaration) : Except KernelException Environment - -end Environment - namespace ConstantInfo def instantiateTypeLevelParams (c : ConstantInfo) (ls : List Level) : Expr := @@ -385,20 +484,20 @@ opaque EnvExtensionInterfaceImp : EnvExtensionInterface def EnvExtension (σ : Type) : Type := EnvExtensionInterfaceImp.ext σ private def ensureExtensionsArraySize (env : Environment) : IO Environment := do - let exts ← EnvExtensionInterfaceImp.ensureExtensionsSize env.extensions - return { env with extensions := exts } + let exts ← EnvExtensionInterfaceImp.ensureExtensionsSize env.base.extensions + return { env with base.extensions := exts } namespace EnvExtension instance {σ} [s : Inhabited σ] : Inhabited (EnvExtension σ) := EnvExtensionInterfaceImp.inhabitedExt s def setState {σ : Type} (ext : EnvExtension σ) (env : Environment) (s : σ) : Environment := - { env with extensions := EnvExtensionInterfaceImp.setState ext env.extensions s } + { env with base.extensions := EnvExtensionInterfaceImp.setState ext env.base.extensions s } def modifyState {σ : Type} (ext : EnvExtension σ) (env : Environment) (f : σ → σ) : Environment := - { env with extensions := EnvExtensionInterfaceImp.modifyState ext env.extensions f } + { env with base.extensions := EnvExtensionInterfaceImp.modifyState ext env.base.extensions f } def getState {σ : Type} [Inhabited σ] (ext : EnvExtension σ) (env : Environment) : σ := - EnvExtensionInterfaceImp.getState ext env.extensions + EnvExtensionInterfaceImp.getState ext env.base.extensions end EnvExtension @@ -418,11 +517,13 @@ def mkEmptyEnvironment (trustLevel : UInt32 := 0) : IO Environment := do if initializing then throw (IO.userError "environment objects cannot be created during initialization") let exts ← mkInitialExtensionStates pure { - const2ModIdx := {} - constants := {} - header := { trustLevel := trustLevel } - extraConstNames := {} - extensions := exts + base := { + const2ModIdx := {} + constants := {} + header := { trustLevel } + extraConstNames := {} + extensions := exts + } } structure PersistentEnvExtensionState (α : Type) (σ : Type) where @@ -710,7 +811,7 @@ def mkModuleData (env : Environment) : IO ModuleData := do let constants := env.constants.foldStage2 (fun cs _ c => cs.push c) #[] return { imports := env.header.imports - extraConstNames := env.extraConstNames.toArray + extraConstNames := env.base.extraConstNames.toArray constNames, constants, entries } @@ -873,17 +974,17 @@ def finalizeImport (s : ImportState) (imports : Array Import) (opts : Options) ( let constants : ConstMap := SMap.fromHashMap constantMap false let exts ← mkInitialExtensionStates let mut env : Environment := { - const2ModIdx := const2ModIdx - constants := constants - extraConstNames := {} - extensions := exts - header := { - quotInit := !imports.isEmpty -- We assume `core.lean` initializes quotient module - trustLevel := trustLevel - imports := imports - regions := s.regions - moduleNames := s.moduleNames - moduleData := s.moduleData + base := { + const2ModIdx, constants + quotInit := !imports.isEmpty -- We assume `core.lean` initializes quotient module + extraConstNames := {} + extensions := exts + header := { + trustLevel, imports + regions := s.regions + moduleNames := s.moduleNames + moduleData := s.moduleData + } } } env ← setImportedEntries env s.moduleData @@ -946,54 +1047,21 @@ builtin_initialize namespacesExt : SimplePersistentEnvExtension Name NameSSet addEntryFn := fun s n => s.insert n } -structure Kernel.Diagnostics where - /-- Number of times each declaration has been unfolded by the kernel. -/ - unfoldCounter : PHashMap Name Nat := {} - /-- If `enabled = true`, kernel records declarations that have been unfolded. -/ - enabled : Bool := false - deriving Inhabited - -/-- -Extension for storting diagnostic information. - -Remark: We store kernel diagnostic information in an environment extension to simplify -the interface with the kernel implemented in C/C++. Thus, we can only track -declarations in methods, such as `addDecl`, which return a new environment. -`Kernel.isDefEq` and `Kernel.whnf` do not update the statistics. We claim -this is ok since these methods are mainly used for debugging. --/ -builtin_initialize diagExt : EnvExtension Kernel.Diagnostics ← - registerEnvExtension (pure {}) +@[inherit_doc Kernel.Environment.enableDiag] +def Kernel.enableDiag (env : Lean.Environment) (flag : Bool) : Lean.Environment := + { env with base := env.base.enableDiag flag } -@[export lean_kernel_diag_is_enabled] -def Kernel.Diagnostics.isEnabled (d : Diagnostics) : Bool := - d.enabled +def Kernel.isDiagnosticsEnabled (env : Lean.Environment) : Bool := + env.base.isDiagnosticsEnabled -/-- Enables/disables kernel diagnostics. -/ -def Kernel.enableDiag (env : Environment) (flag : Bool) : Environment := - diagExt.modifyState env fun s => { s with enabled := flag } - -def Kernel.isDiagnosticsEnabled (env : Environment) : Bool := - diagExt.getState env |>.enabled - -def Kernel.resetDiag (env : Environment) : Environment := - diagExt.modifyState env fun s => { s with unfoldCounter := {} } - -@[export lean_kernel_record_unfold] -def Kernel.Diagnostics.recordUnfold (d : Diagnostics) (declName : Name) : Diagnostics := - if d.enabled then - let cNew := if let some c := d.unfoldCounter.find? declName then c + 1 else 1 - { d with unfoldCounter := d.unfoldCounter.insert declName cNew } - else - d +def Kernel.resetDiag (env : Lean.Environment) : Lean.Environment := + { env with base := env.base.resetDiag } -@[export lean_kernel_get_diag] -def Kernel.getDiagnostics (env : Environment) : Diagnostics := - diagExt.getState env +def Kernel.getDiagnostics (env : Lean.Environment) : Diagnostics := + env.base.diagnostics -@[export lean_kernel_set_diag] -def Kernel.setDiagnostics (env : Environment) (diag : Diagnostics) : Environment := - diagExt.setState env diag +def Kernel.setDiagnostics (env : Lean.Environment) (diag : Diagnostics) : Lean.Environment := + { env with base := env.base.setDiagnostics diag } namespace Environment @@ -1014,22 +1082,29 @@ private def isNamespaceName : Name → Bool | .str p _ => isNamespaceName p | _ => false -private def registerNamePrefixes : Environment → Name → Environment - | env, .str p _ => if isNamespaceName p then registerNamePrefixes (registerNamespace env p) p else env - | env, _ => env - -@[export lean_environment_add] -private def add (env : Environment) (cinfo : ConstantInfo) : Environment := - let name := cinfo.name - let env := match name with +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 - registerNamePrefixes env name + go env name | _ => env - env.addAux cinfo +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 @[export lean_display_stats] def displayStats (env : Environment) : IO Unit := do @@ -1039,7 +1114,7 @@ def displayStats (env : Environment) : IO Unit := do IO.println ("number of memory-mapped modules: " ++ toString (env.header.regions.filter (·.isMemoryMapped) |>.size)); IO.println ("number of buckets for imported consts: " ++ toString env.constants.numBuckets); IO.println ("trust level: " ++ toString env.header.trustLevel); - IO.println ("number of extensions: " ++ toString env.extensions.size); + IO.println ("number of extensions: " ++ toString env.base.extensions.size); pExtDescrs.forM fun extDescr => do IO.println ("extension '" ++ toString extDescr.name ++ "'") let s := extDescr.toEnvExtension.getState env @@ -1085,27 +1160,33 @@ namespace Kernel /-- Kernel isDefEq predicate. We use it mainly for debugging purposes. - Recall that the Kernel type checker does not support metavariables. + Recall that the kernel type checker does not support metavariables. When implementing automation, consider using the `MetaM` methods. -/ +-- We use `Lean.Environment` for ease of use; as this is a debugging function, we forgo a +-- `Kernel.Environment` base variant @[extern "lean_kernel_is_def_eq"] -opaque isDefEq (env : Environment) (lctx : LocalContext) (a b : Expr) : Except KernelException Bool +opaque isDefEq (env : Lean.Environment) (lctx : LocalContext) (a b : Expr) : Except Kernel.Exception Bool -def isDefEqGuarded (env : Environment) (lctx : LocalContext) (a b : Expr) : Bool := +def isDefEqGuarded (env : Lean.Environment) (lctx : LocalContext) (a b : Expr) : Bool := if let .ok result := isDefEq env lctx a b then result else false /-- Kernel WHNF function. We use it mainly for debugging purposes. - Recall that the Kernel type checker does not support metavariables. + Recall that the kernel type checker does not support metavariables. When implementing automation, consider using the `MetaM` methods. -/ +-- We use `Lean.Environment` for ease of use; as this is a debugging function, we forgo a +-- `Kernel.Environment` base variant @[extern "lean_kernel_whnf"] -opaque whnf (env : Environment) (lctx : LocalContext) (a : Expr) : Except KernelException Expr +opaque whnf (env : Lean.Environment) (lctx : LocalContext) (a : Expr) : Except Kernel.Exception Expr /-- Kernel typecheck function. We use it mainly for debugging purposes. Recall that the Kernel type checker does not support metavariables. When implementing automation, consider using the `MetaM` methods. -/ +-- We use `Lean.Environment` for ease of use; as this is a debugging function, we forgo a +-- `Kernel.Environment` base variant @[extern "lean_kernel_check"] -opaque check (env : Environment) (lctx : LocalContext) (a : Expr) : Except KernelException Expr +opaque check (env : Lean.Environment) (lctx : LocalContext) (a : Expr) : Except Kernel.Exception Expr end Kernel diff --git a/src/Lean/Exception.lean b/src/Lean/Exception.lean index 896052f998aa6..0d830f67cdab6 100644 --- a/src/Lean/Exception.lean +++ b/src/Lean/Exception.lean @@ -89,11 +89,11 @@ def ofExcept [Monad m] [MonadError m] [ToMessageData ε] (x : Except ε α) : m /-- Throw an error exception for the given kernel exception. -/ -def throwKernelException [Monad m] [MonadError m] [MonadOptions m] (ex : KernelException) : m α := do +def throwKernelException [Monad m] [MonadError m] [MonadOptions m] (ex : Kernel.Exception) : m α := do Lean.throwError <| ex.toMessageData (← getOptions) /-- Lift from `Except KernelException` to `m` when `m` can throw kernel exceptions. -/ -def ofExceptKernelException [Monad m] [MonadError m] [MonadOptions m] (x : Except KernelException α) : m α := +def ofExceptKernelException [Monad m] [MonadError m] [MonadOptions m] (x : Except Kernel.Exception α) : m α := match x with | .ok a => return a | .error e => throwKernelException e diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean index 15618a0ba69f4..5c4fc1d52bc1c 100644 --- a/src/Lean/Message.lean +++ b/src/Lean/Message.lean @@ -537,12 +537,12 @@ macro_rules def toMessageList (msgs : Array MessageData) : MessageData := indentD (MessageData.joinSep msgs.toList m!"\n\n") -namespace KernelException +namespace Kernel.Exception private def mkCtx (env : Environment) (lctx : LocalContext) (opts : Options) (msg : MessageData) : MessageData := - MessageData.withContext { env := env, mctx := {}, lctx := lctx, opts := opts } msg + MessageData.withContext { env := .ofKernelEnv env, mctx := {}, lctx := lctx, opts := opts } msg -def toMessageData (e : KernelException) (opts : Options) : MessageData := +def toMessageData (e : Kernel.Exception) (opts : Options) : MessageData := match e with | unknownConstant env constName => mkCtx env {} opts m!"(kernel) unknown constant '{constName}'" | alreadyDeclared env constName => mkCtx env {} opts m!"(kernel) constant has already been declared '{.ofConstName constName true}'" @@ -570,5 +570,5 @@ def toMessageData (e : KernelException) (opts : Options) : MessageData := | deepRecursion => "(kernel) deep recursion detected" | interrupted => "(kernel) interrupted" -end KernelException +end Kernel.Exception end Lean diff --git a/src/Lean/Meta/Constructions/CasesOn.lean b/src/Lean/Meta/Constructions/CasesOn.lean index 57a642ddcb70f..e4ab37384d958 100644 --- a/src/Lean/Meta/Constructions/CasesOn.lean +++ b/src/Lean/Meta/Constructions/CasesOn.lean @@ -9,13 +9,13 @@ import Lean.Meta.Basic namespace Lean -@[extern "lean_mk_cases_on"] opaque mkCasesOnImp (env : Environment) (declName : @& Name) : Except KernelException Declaration +@[extern "lean_mk_cases_on"] opaque mkCasesOnImp (env : Kernel.Environment) (declName : @& Name) : Except Kernel.Exception Declaration open Meta def mkCasesOn (declName : Name) : MetaM Unit := do let name := mkCasesOnName declName - let decl ← ofExceptKernelException (mkCasesOnImp (← getEnv) declName) + let decl ← ofExceptKernelException (mkCasesOnImp (← getEnv).toKernelEnv declName) addDecl decl setReducibleAttribute name modifyEnv fun env => markAuxRecursor env name diff --git a/src/Lean/Meta/Constructions/NoConfusion.lean b/src/Lean/Meta/Constructions/NoConfusion.lean index d3ed5033fa95b..52cf24dbcfe3e 100644 --- a/src/Lean/Meta/Constructions/NoConfusion.lean +++ b/src/Lean/Meta/Constructions/NoConfusion.lean @@ -10,8 +10,8 @@ import Lean.Meta.CompletionName namespace Lean -@[extern "lean_mk_no_confusion_type"] opaque mkNoConfusionTypeCoreImp (env : Environment) (declName : @& Name) : Except KernelException Declaration -@[extern "lean_mk_no_confusion"] opaque mkNoConfusionCoreImp (env : Environment) (declName : @& Name) : Except KernelException Declaration +@[extern "lean_mk_no_confusion_type"] opaque mkNoConfusionTypeCoreImp (env : Environment) (declName : @& Name) : Except Kernel.Exception Declaration +@[extern "lean_mk_no_confusion"] opaque mkNoConfusionCoreImp (env : Environment) (declName : @& Name) : Except Kernel.Exception Declaration open Meta diff --git a/src/Lean/Replay.lean b/src/Lean/Replay.lean index 8192bc4da77a5..93977b5c660af 100644 --- a/src/Lean/Replay.lean +++ b/src/Lean/Replay.lean @@ -49,13 +49,11 @@ def isTodo (name : Name) : M Bool := do else return false -/-- Use the current `Environment` to throw a `KernelException`. -/ -def throwKernelException (ex : KernelException) : M Unit := do - let ctx := { fileName := "", options := ({} : KVMap), fileMap := default } - let state := { env := (← get).env } - Prod.fst <$> (Lean.Core.CoreM.toIO · ctx state) do Lean.throwKernelException ex +/-- Use the current `Environment` to throw a `Kernel.Exception`. -/ +def throwKernelException (ex : Kernel.Exception) : M Unit := do + throw <| .userError <| (← ex.toMessageData {} |>.toString) -/-- Add a declaration, possibly throwing a `KernelException`. -/ +/-- Add a declaration, possibly throwing a `Kernel.Exception`. -/ def addDecl (d : Declaration) : M Unit := do match (← get).env.addDecl {} d with | .ok env => modify fun s => { s with env := env } diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index 57e0a0358ec42..1e8514eff38fc 100644 --- a/src/kernel/environment.cpp +++ b/src/kernel/environment.cpp @@ -19,16 +19,9 @@ Author: Leonardo de Moura namespace lean { extern "C" object* lean_environment_add(object*, object*); -extern "C" object* lean_mk_empty_environment(uint32, object*); extern "C" object* lean_environment_find(object*, object*); -extern "C" uint32 lean_environment_trust_level(object*); extern "C" object* lean_environment_mark_quot_init(object*); extern "C" uint8 lean_environment_quot_init(object*); -extern "C" object* lean_register_extension(object*); -extern "C" object* lean_get_extension(object*, object*); -extern "C" object* lean_set_extension(object*, object*, object*); -extern "C" object* lean_environment_set_main_module(object*, object*); -extern "C" object* lean_environment_main_module(object*); extern "C" object* lean_kernel_record_unfold (object*, object*); extern "C" object* lean_kernel_get_diag(object*); extern "C" object* lean_kernel_set_diag(object*, object*); @@ -62,14 +55,6 @@ environment scoped_diagnostics::update(environment const & env) const { return env; } -environment mk_empty_environment(uint32 trust_lvl) { - return get_io_result(lean_mk_empty_environment(trust_lvl, io_mk_world())); -} - -environment::environment(unsigned trust_lvl): - object_ref(mk_empty_environment(trust_lvl)) { -} - diagnostics environment::get_diag() const { return diagnostics(lean_kernel_get_diag(to_obj_arg())); } @@ -78,18 +63,6 @@ environment environment::set_diag(diagnostics const & diag) const { return environment(lean_kernel_set_diag(to_obj_arg(), diag.to_obj_arg())); } -void environment::set_main_module(name const & n) { - m_obj = lean_environment_set_main_module(m_obj, n.to_obj_arg()); -} - -name environment::get_main_module() const { - return name(lean_environment_main_module(to_obj_arg())); -} - -unsigned environment::trust_lvl() const { - return lean_environment_trust_level(to_obj_arg()); -} - bool environment::is_quot_initialized() const { return lean_environment_quot_init(to_obj_arg()) != 0; } @@ -297,7 +270,7 @@ environment environment::add(declaration const & d, bool check) const { } /* addDeclCore (env : Environment) (maxHeartbeats : USize) (decl : @& Declaration) - (cancelTk? : @& Option IO.CancelToken) : Except KernelException Environment + (cancelTk? : @& Option IO.CancelToken) : Except Kernel.Exception Environment */ extern "C" LEAN_EXPORT object * lean_add_decl(object * env, size_t max_heartbeat, object * decl, object * opt_cancel_tk) { @@ -321,12 +294,6 @@ void environment::for_each_constant(std::function }); } -extern "C" obj_res lean_display_stats(obj_arg env, obj_arg w); - -void environment::display_stats() const { - dec_ref(lean_display_stats(to_obj_arg(), io_mk_world())); -} - void initialize_environment() { } diff --git a/src/kernel/environment.h b/src/kernel/environment.h index d0d61a8eed9b3..88ff1496995a3 100644 --- a/src/kernel/environment.h +++ b/src/kernel/environment.h @@ -24,10 +24,6 @@ Author: Leonardo de Moura #endif namespace lean { -class environment_extension { -public: - virtual ~environment_extension() {} -}; /* Wrapper for `Kernel.Diagnostics` */ class diagnostics : public object_ref { @@ -41,7 +37,7 @@ class diagnostics : public object_ref { }; /* -Store `Kernel.Diagnostics` stored in environment extension in `m_diag` IF +Store `Kernel.Diagnostics` (to be stored in `Kernel.Environment.diagnostics`) in `m_diag` IF - `Kernel.Diagnostics.enable = true` - `collect = true`. This is a minor optimization. @@ -59,6 +55,7 @@ class scoped_diagnostics { diagnostics * get() const { return m_diag; } }; +/* Wrapper for `Lean.Kernel.Environment` */ class LEAN_EXPORT environment : public object_ref { friend class add_inductive_fn; @@ -76,7 +73,6 @@ class LEAN_EXPORT environment : public object_ref { environment add_quot() const; environment add_inductive(declaration const & d) const; public: - environment(unsigned trust_lvl = 0); environment(environment const & other):object_ref(other) {} environment(environment && other):object_ref(other) {} explicit environment(b_obj_arg o, bool b):object_ref(o, b) {} @@ -89,15 +85,8 @@ class LEAN_EXPORT environment : public object_ref { diagnostics get_diag() const; environment set_diag(diagnostics const & diag) const; - /** \brief Return the trust level of this environment. */ - unsigned trust_lvl() const; - bool is_quot_initialized() const; - void set_main_module(name const & n); - - name get_main_module() const; - /** \brief Return information for the constant with name \c n (if it is defined in this environment). */ optional find(name const & n) const; @@ -114,8 +103,6 @@ class LEAN_EXPORT environment : public object_ref { friend bool is_eqp(environment const & e1, environment const & e2) { return e1.raw() == e2.raw(); } - - void display_stats() const; }; void check_no_metavar_no_fvar(environment const & env, name const & n, expr const & e); diff --git a/src/kernel/kernel_exception.h b/src/kernel/kernel_exception.h index 793cf6403277a..243b53635fda1 100644 --- a/src/kernel/kernel_exception.h +++ b/src/kernel/kernel_exception.h @@ -152,9 +152,9 @@ class invalid_proj_exception : public kernel_exception_with_lctx { /* Helper function for interfacing C++ code with code written in Lean. It executes closure `f` which produces an object_ref of type `A` and may throw -an `kernel_exception` or `exception`. Then, convert result into `Except KernelException T` +an `kernel_exception` or `exception`. Then, convert result into `Except Kernel.Exception T` where `T` is the type of the lean objected represented by `A`. -We use the constructor `KernelException.other ` to handle C++ `exception` objects which +We use the constructor `Kernel.Exception.other ` to handle C++ `exception` objects which are not `kernel_exception`. */ template diff --git a/src/kernel/trace.cpp b/src/kernel/trace.cpp index 9cec464e5fd69..c556540612b9f 100644 --- a/src/kernel/trace.cpp +++ b/src/kernel/trace.cpp @@ -8,7 +8,7 @@ Author: Leonardo de Moura #include #include "util/io.h" #include "util/option_declarations.h" -#include "kernel/environment.h" +#include "library/elab_environment.h" #include "kernel/local_ctx.h" #include "kernel/trace.h" @@ -17,7 +17,7 @@ static name_set * g_trace_classes = nullptr; static name_map * g_trace_aliases = nullptr; MK_THREAD_LOCAL_GET_DEF(std::vector, get_enabled_trace_classes); MK_THREAD_LOCAL_GET_DEF(std::vector, get_disabled_trace_classes); -LEAN_THREAD_PTR(environment, g_env); +LEAN_THREAD_PTR(elab_environment, g_env); LEAN_THREAD_PTR(options, g_opts); void register_trace_class(name const & n, name const & decl_name) { @@ -90,7 +90,7 @@ bool is_trace_class_enabled(name const & n) { } -void scope_trace_env::init(environment * env, options * opts) { +void scope_trace_env::init(elab_environment * env, options * opts) { m_enable_sz = get_enabled_trace_classes().size(); m_disable_sz = get_disabled_trace_classes().size(); m_old_env = g_env; @@ -111,12 +111,12 @@ void scope_trace_env::init(environment * env, options * opts) { g_opts = opts; } -scope_trace_env::scope_trace_env(environment const & env, options const & o) { - init(const_cast(&env), const_cast(&o)); +scope_trace_env::scope_trace_env(elab_environment const & env, options const & o) { + init(const_cast(&env), const_cast(&o)); } scope_trace_env::~scope_trace_env() { - g_env = const_cast(m_old_env); + g_env = const_cast(m_old_env); g_opts = const_cast(m_old_opts); get_enabled_trace_classes().resize(m_enable_sz); get_disabled_trace_classes().resize(m_disable_sz); @@ -169,7 +169,7 @@ def pretty (f : Format) (w : Nat := defWidth) (indent : Nat := 0) (column := 0) */ extern "C" object * lean_format_pretty(object * f, object * w, object * i, object * c); -std::string pp_expr(environment const & env, options const & opts, local_ctx const & lctx, expr const & e) { +std::string pp_expr(elab_environment const & env, options const & opts, local_ctx const & lctx, expr const & e) { options o = opts; // o = o.update(name{"pp", "proofs"}, true); -- object_ref fmt = get_io_result(lean_pp_expr(env.to_obj_arg(), lean_mk_metavar_ctx(lean_box(0)), lctx.to_obj_arg(), o.to_obj_arg(), @@ -178,7 +178,7 @@ std::string pp_expr(environment const & env, options const & opts, local_ctx con return str.to_std_string(); } -std::string pp_expr(environment const & env, options const & opts, expr const & e) { +std::string pp_expr(elab_environment const & env, options const & opts, expr const & e) { local_ctx lctx; return pp_expr(env, opts, lctx, e); } diff --git a/src/kernel/trace.h b/src/kernel/trace.h index feac201c88e7b..e42f20f90d137 100644 --- a/src/kernel/trace.h +++ b/src/kernel/trace.h @@ -7,7 +7,7 @@ Author: Leonardo de Moura #pragma once #include #include -#include "kernel/environment.h" +#include "library/elab_environment.h" #include "util/options.h" #include "util/message_definitions.h" @@ -20,13 +20,13 @@ bool is_trace_class_enabled(name const & n); #define lean_is_trace_enabled(CName) (::lean::is_trace_enabled() && ::lean::is_trace_class_enabled(CName)) class scope_trace_env { - unsigned m_enable_sz; - unsigned m_disable_sz; - environment const * m_old_env; - options const * m_old_opts; - void init(environment * env, options * opts); + unsigned m_enable_sz; + unsigned m_disable_sz; + elab_environment const * m_old_env; + options const * m_old_opts; + void init(elab_environment * env, options * opts); public: - scope_trace_env(environment const & env, options const & opts); + scope_trace_env(elab_environment const & env, options const & opts); ~scope_trace_env(); }; diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index b0e6844dca24e..dc4034e9ffc68 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -549,7 +549,7 @@ static expr * g_lean_reduce_bool = nullptr; static expr * g_lean_reduce_nat = nullptr; namespace ir { -object * run_boxed(environment const & env, options const & opts, name const & fn, unsigned n, object **args); +object * run_boxed_kernel(environment const & env, options const & opts, name const & fn, unsigned n, object **args); } expr mk_bool_true(); @@ -560,7 +560,7 @@ optional reduce_native(environment const & env, expr const & e) { expr const & arg = app_arg(e); if (!is_constant(arg)) return none_expr(); if (app_fn(e) == *g_lean_reduce_bool) { - object * r = ir::run_boxed(env, options(), const_name(arg), 0, nullptr); + object * r = ir::run_boxed_kernel(env, options(), const_name(arg), 0, nullptr); if (!lean_is_scalar(r)) { lean_dec_ref(r); throw kernel_exception(env, "type checker failure, unexpected result value for 'Lean.reduceBool'"); @@ -568,7 +568,7 @@ optional reduce_native(environment const & env, expr const & e) { return lean_unbox(r) == 0 ? some_expr(mk_bool_false()) : some_expr(mk_bool_true()); } if (app_fn(e) == *g_lean_reduce_nat) { - object * r = ir::run_boxed(env, options(), const_name(arg), 0, nullptr); + object * r = ir::run_boxed_kernel(env, options(), const_name(arg), 0, nullptr); if (lean_is_scalar(r) || lean_is_mpz(r)) { return some_expr(mk_lit(literal(nat(r)))); } else { @@ -1193,24 +1193,6 @@ type_checker::~type_checker() { delete m_st; } -extern "C" LEAN_EXPORT lean_object * lean_kernel_is_def_eq(lean_object * env, lean_object * lctx, lean_object * a, lean_object * b) { - return catch_kernel_exceptions([&]() { - return lean_box(type_checker(environment(env), local_ctx(lctx)).is_def_eq(expr(a), expr(b))); - }); -} - -extern "C" LEAN_EXPORT lean_object * lean_kernel_whnf(lean_object * env, lean_object * lctx, lean_object * a) { - return catch_kernel_exceptions([&]() { - return type_checker(environment(env), local_ctx(lctx)).whnf(expr(a)).steal(); - }); -} - -extern "C" LEAN_EXPORT lean_object * lean_kernel_check(lean_object * env, lean_object * lctx, lean_object * a) { - return catch_kernel_exceptions([&]() { - return type_checker(environment(env), local_ctx(lctx)).check(expr(a)).steal(); - }); -} - inline static expr * new_persistent_expr_const(name const & n) { expr * e = new expr(mk_const(n)); mark_persistent(e->raw()); diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h index 3ab2ce643b72d..ac387564aa753 100644 --- a/src/kernel/type_checker.h +++ b/src/kernel/type_checker.h @@ -9,6 +9,7 @@ Author: Leonardo de Moura #include #include #include +#include "runtime/flet.h" #include "util/lbool.h" #include "util/name_set.h" #include "util/name_generator.h" @@ -104,6 +105,7 @@ class type_checker { optional reduce_pow(expr const & e); optional reduce_nat(expr const & e); public: + // The following two constructor are used only by the old compiler and should be deleted with it type_checker(state & st, local_ctx const & lctx, definition_safety ds = definition_safety::safe); type_checker(state & st, definition_safety ds = definition_safety::safe):type_checker(st, local_ctx(), ds) {} type_checker(environment const & env, local_ctx const & lctx, diagnostics * diag = nullptr, definition_safety ds = definition_safety::safe); diff --git a/src/lake/Lake/Load/Lean/Elab.lean b/src/lake/Lake/Load/Lean/Elab.lean index c83fe093df165..cf2600753d1fe 100644 --- a/src/lake/Lake/Load/Lean/Elab.lean +++ b/src/lake/Lake/Load/Lean/Elab.lean @@ -81,10 +81,10 @@ def elabConfigFile (pkgDir : FilePath) (lakeOpts : NameMap String) return s.commandState.env /-- -`Lean.Environment.add` is now private, but exported as `lean_environment_add`. +`Lean.Environment.add` is now private, but exported as `lean_elab_environment_add`. We call it here via `@[extern]` with a mock implementation. -/ -@[extern "lean_environment_add"] +@[extern "lean_elab_environment_add"] private opaque addToEnv (env : Environment) (_ : ConstantInfo) : Environment /-- diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 7fbbb41851eb9..30c2c8924af4f 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -6,4 +6,5 @@ add_library(library OBJECT expr_lt.cpp projection.cpp aux_recursors.cpp profiling.cpp time_task.cpp - formatter.cpp) + formatter.cpp + elab_environment.cpp) diff --git a/src/library/aux_recursors.cpp b/src/library/aux_recursors.cpp index 724e8c2b10444..d4134090fb75c 100644 --- a/src/library/aux_recursors.cpp +++ b/src/library/aux_recursors.cpp @@ -10,11 +10,11 @@ namespace lean { extern "C" uint8 lean_is_aux_recursor(object * env, object * n); extern "C" uint8 lean_is_no_confusion(object * env, object * n); -bool is_aux_recursor(environment const & env, name const & r) { +bool is_aux_recursor(elab_environment const & env, name const & r) { return lean_is_aux_recursor(env.to_obj_arg(), r.to_obj_arg()); } -bool is_no_confusion(environment const & env, name const & r) { +bool is_no_confusion(elab_environment const & env, name const & r) { return lean_is_no_confusion(env.to_obj_arg(), r.to_obj_arg()); } } diff --git a/src/library/aux_recursors.h b/src/library/aux_recursors.h index 49556be1f8622..1d66ee423ff7e 100644 --- a/src/library/aux_recursors.h +++ b/src/library/aux_recursors.h @@ -5,11 +5,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "kernel/environment.h" +#include "library/elab_environment.h" namespace lean { /** \brief Return true iff \c n is the name of an auxiliary recursor. \see add_aux_recursor */ -bool is_aux_recursor(environment const & env, name const & n); -bool is_no_confusion(environment const & env, name const & n); +bool is_aux_recursor(elab_environment const & env, name const & n); +bool is_no_confusion(elab_environment const & env, name const & n); } diff --git a/src/library/class.cpp b/src/library/class.cpp index f67e89f2cb59b..e37bdaf7b3e21 100644 --- a/src/library/class.cpp +++ b/src/library/class.cpp @@ -15,9 +15,9 @@ extern "C" uint8 lean_is_out_param(object* e); extern "C" uint8 lean_has_out_params(object* env, object* n); bool is_class_out_param(expr const & e) { return lean_is_out_param(e.to_obj_arg()); } -bool has_class_out_params(environment const & env, name const & c) { return lean_has_out_params(env.to_obj_arg(), c.to_obj_arg()); } -bool is_class(environment const & env, name const & c) { return lean_is_class(env.to_obj_arg(), c.to_obj_arg()); } -bool is_instance(environment const & env, name const & i) { return lean_is_instance(env.to_obj_arg(), i.to_obj_arg()); } +bool has_class_out_params(elab_environment const & env, name const & c) { return lean_has_out_params(env.to_obj_arg(), c.to_obj_arg()); } +bool is_class(elab_environment const & env, name const & c) { return lean_is_class(env.to_obj_arg(), c.to_obj_arg()); } +bool is_instance(elab_environment const & env, name const & i) { return lean_is_instance(env.to_obj_arg(), i.to_obj_arg()); } static name * g_anonymous_inst_name_prefix = nullptr; diff --git a/src/library/class.h b/src/library/class.h index ed8768cfc8455..2dd2c21c7d130 100644 --- a/src/library/class.h +++ b/src/library/class.h @@ -6,11 +6,12 @@ Author: Leonardo de Moura */ #pragma once #include "library/util.h" +#include "library/elab_environment.h" namespace lean { /** \brief Return true iff \c c was declared with \c add_class. */ -bool is_class(environment const & env, name const & c); +bool is_class(elab_environment const & env, name const & c); /** \brief Return true iff \c i was declared with \c add_instance. */ -bool is_instance(environment const & env, name const & i); +bool is_instance(elab_environment const & env, name const & i); name const & get_anonymous_instance_prefix(); name mk_anonymous_inst_name(unsigned idx); @@ -20,7 +21,7 @@ bool is_anonymous_inst_name(name const & n); bool is_class_out_param(expr const & e); /** \brief Return true iff c is a type class that contains an `outParam` */ -bool has_class_out_params(environment const & env, name const & c); +bool has_class_out_params(elab_environment const & env, name const & c); void initialize_class(); void finalize_class(); diff --git a/src/library/compiler/closed_term_cache.cpp b/src/library/compiler/closed_term_cache.cpp index 2dbdfa40dd59e..8995a95d84e9e 100644 --- a/src/library/compiler/closed_term_cache.cpp +++ b/src/library/compiler/closed_term_cache.cpp @@ -5,16 +5,17 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include "library/util.h" +#include "library/elab_environment.h" namespace lean { extern "C" object * lean_cache_closed_term_name(object * env, object * e, object * n); extern "C" object * lean_get_closed_term_name(object * env, object * e); -optional get_closed_term_name(environment const & env, expr const & e) { +optional get_closed_term_name(elab_environment const & env, expr const & e) { return to_optional(lean_get_closed_term_name(env.to_obj_arg(), e.to_obj_arg())); } -environment cache_closed_term_name(environment const & env, expr const & e, name const & n) { - return environment(lean_cache_closed_term_name(env.to_obj_arg(), e.to_obj_arg(), n.to_obj_arg())); +elab_environment cache_closed_term_name(elab_environment const & env, expr const & e, name const & n) { + return elab_environment(lean_cache_closed_term_name(env.to_obj_arg(), e.to_obj_arg(), n.to_obj_arg())); } } diff --git a/src/library/compiler/closed_term_cache.h b/src/library/compiler/closed_term_cache.h index a1397a9c64496..e4b2b506b8a1b 100644 --- a/src/library/compiler/closed_term_cache.h +++ b/src/library/compiler/closed_term_cache.h @@ -5,8 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "kernel/environment.h" +#include "library/elab_environment.h" namespace lean { -optional get_closed_term_name(environment const & env, expr const & e); -environment cache_closed_term_name(environment const & env, expr const & e, name const & n); +optional get_closed_term_name(elab_environment const & env, expr const & e); +elab_environment cache_closed_term_name(elab_environment const & env, expr const & e, name const & n); } diff --git a/src/library/compiler/compiler.cpp b/src/library/compiler/compiler.cpp index eb75c93a2737d..bed22bb5a5994 100644 --- a/src/library/compiler/compiler.cpp +++ b/src/library/compiler/compiler.cpp @@ -44,19 +44,19 @@ static name get_real_name(name const & n) { return n; } -static comp_decls to_comp_decls(environment const & env, names const & cs) { +static comp_decls to_comp_decls(elab_environment const & env, names const & cs) { bool allow_opaque = true; return map2(cs, [&](name const & n) { return comp_decl(get_real_name(n), env.get(n).get_value(allow_opaque)); }); } -static expr eta_expand(environment const & env, expr const & e) { - return type_checker(env).eta_expand(e); +static expr eta_expand(elab_environment const & env, expr const & e) { + return type_checker(env.to_kernel_env()).eta_expand(e); } template -comp_decls apply(F && f, environment const & env, comp_decls const & ds) { +comp_decls apply(F && f, elab_environment const & env, comp_decls const & ds) { return map(ds, [&](comp_decl const & d) { return comp_decl(d.fst(), f(env, d.snd())); }); } @@ -75,7 +75,7 @@ void trace_comp_decls(comp_decls const & ds) { } } -static environment cache_stage1(environment env, comp_decls const & ds) { +static elab_environment cache_stage1(elab_environment env, comp_decls const & ds) { for (comp_decl const & d : ds) { name n = d.fst(); expr v = d.snd(); @@ -94,7 +94,7 @@ static expr ensure_arity(expr const & t, unsigned arity) { return update_binding(t, binding_domain(t), ensure_arity(binding_body(t), arity-1)); } -static environment cache_stage2(environment env, comp_decls const & ds, bool only_new_ones = false) { +static elab_environment cache_stage2(elab_environment env, comp_decls const & ds, bool only_new_ones = false) { buffer ts; ll_infer_type(env, ds, ts); lean_assert(ts.size() == length(ds)); @@ -116,11 +116,11 @@ static environment cache_stage2(environment env, comp_decls const & ds, bool onl } /* Cache the declarations in `ds` that have not already been cached. */ -static environment cache_new_stage2(environment env, comp_decls const & ds) { +static elab_environment cache_new_stage2(elab_environment env, comp_decls const & ds) { return cache_stage2(env, ds, true); } -bool is_main_fn(environment const & env, name const & n) { +bool is_main_fn(elab_environment const & env, name const & n) { if (n == "main") return true; if (optional c = get_export_name_for(env, n)) { return *c == "main"; @@ -160,15 +160,15 @@ bool is_main_fn_type(expr const & type) { extern "C" object* lean_csimp_replace_constants(object* env, object* n); -expr csimp_replace_constants(environment const & env, expr const & e) { +expr csimp_replace_constants(elab_environment const & env, expr const & e) { return expr(lean_csimp_replace_constants(env.to_obj_arg(), e.to_obj_arg())); } -bool is_matcher(environment const & env, comp_decls const & ds) { +bool is_matcher(elab_environment const & env, comp_decls const & ds) { return length(ds) == 1 && is_matcher(env, head(ds).fst()); } -environment compile(environment const & env, options const & opts, names cs) { +elab_environment compile(elab_environment const & env, options const & opts, names cs) { /* Do not generate code for irrelevant decls */ cs = filter(cs, [&](name const & c) { return !is_irrelevant_type(env, env.get(c).get_type());}); if (empty(cs)) return env; @@ -202,8 +202,8 @@ environment compile(environment const & env, options const & opts, names cs) { csimp_cfg cfg(opts); // Use the following line to see compiler intermediate steps // scope_traces_as_string trace_scope; - auto simp = [&](environment const & env, expr const & e) { return csimp(env, e, cfg); }; - auto esimp = [&](environment const & env, expr const & e) { return cesimp(env, e, cfg); }; + auto simp = [&](elab_environment const & env, expr const & e) { return csimp(env, e, cfg); }; + auto esimp = [&](elab_environment const & env, expr const & e) { return cesimp(env, e, cfg); }; trace_compiler(name({"compiler", "input"}), ds); ds = apply(eta_expand, env, ds); trace_compiler(name({"compiler", "eta_expand"}), ds); @@ -218,7 +218,7 @@ environment compile(environment const & env, options const & opts, names cs) { ds = apply(simp, env, ds); trace_compiler(name({"compiler", "simp"}), ds); // trace(ds); - environment new_env = env; + elab_environment new_env = env; std::tie(new_env, ds) = eager_lambda_lifting(new_env, ds, cfg); trace_compiler(name({"compiler", "eager_lambda_lifting"}), ds); ds = apply(max_sharing, ds); @@ -274,8 +274,8 @@ environment compile(environment const & env, options const & opts, names cs) { } extern "C" LEAN_EXPORT object * lean_compile_decls(object * env, object * opts, object * decls) { - return catch_kernel_exceptions([&]() { - return compile(environment(env), options(opts, true), names(decls, true)); + return catch_kernel_exceptions([&]() { + return compile(elab_environment(env), options(opts, true), names(decls, true)); }); } diff --git a/src/library/compiler/compiler.h b/src/library/compiler/compiler.h index 16c1fe8b3b6e1..d620c53aa6443 100644 --- a/src/library/compiler/compiler.h +++ b/src/library/compiler/compiler.h @@ -5,10 +5,10 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "kernel/environment.h" +#include "library/elab_environment.h" namespace lean { -environment compile(environment const & env, options const & opts, names cs); -inline environment compile(environment const & env, options const & opts, name const & c) { +elab_environment compile(elab_environment const & env, options const & opts, names cs); +inline elab_environment compile(elab_environment const & env, options const & opts, name const & c) { return compile(env, opts, names(c)); } void initialize_compiler(); diff --git a/src/library/compiler/cse.cpp b/src/library/compiler/cse.cpp index 057b30356796b..44db877b0c8cc 100644 --- a/src/library/compiler/cse.cpp +++ b/src/library/compiler/cse.cpp @@ -8,7 +8,7 @@ Author: Leonardo de Moura #include #include "runtime/flet.h" #include "util/name_generator.h" -#include "kernel/environment.h" +#include "library/elab_environment.h" #include "kernel/instantiate.h" #include "kernel/abstract.h" #include "kernel/for_each_fn.h" @@ -21,7 +21,7 @@ namespace lean { static name * g_cse_fresh = nullptr; class cse_fn { - environment m_env; + elab_environment m_env; name_generator m_ngen; bool m_before_erasure; expr_map m_map; @@ -148,14 +148,14 @@ class cse_fn { } public: - cse_fn(environment const & env, bool before_erasure): + cse_fn(elab_environment const & env, bool before_erasure): m_env(env), m_ngen(*g_cse_fresh), m_before_erasure(before_erasure) { } expr operator()(expr const & e) { return visit(e); } }; -expr cse_core(environment const & env, expr const & e, bool before_erasure) { +expr cse_core(elab_environment const & env, expr const & e, bool before_erasure) { return cse_fn(env, before_erasure)(e); } @@ -170,6 +170,7 @@ expr cse_core(environment const & env, expr const & e, bool before_erasure) { ``` The "else"-branch is duplicated by the equation compiler for each constructor different from `expr.app`. */ class cce_fn { + elab_environment m_env; type_checker::state m_st; local_ctx m_lctx; buffer m_fvars; @@ -178,7 +179,7 @@ class cce_fn { name m_j; unsigned m_next_idx{1}; public: - environment & env() { return m_st.env(); } + elab_environment & env() { return m_env; } name_generator & ngen() { return m_st.ngen(); } @@ -394,8 +395,8 @@ class cce_fn { } public: - cce_fn(environment const & env, local_ctx const & lctx): - m_st(env), m_lctx(lctx), m_j("_j") { + cce_fn(elab_environment const & env, local_ctx const & lctx): + m_env(env), m_st(env), m_lctx(lctx), m_j("_j") { } expr operator()(expr const & e) { @@ -404,7 +405,7 @@ class cce_fn { } }; -expr cce_core(environment const & env, local_ctx const & lctx, expr const & e) { +expr cce_core(elab_environment const & env, local_ctx const & lctx, expr const & e) { return cce_fn(env, lctx)(e); } diff --git a/src/library/compiler/cse.h b/src/library/compiler/cse.h index 82bd830a75884..4488f16538fe1 100644 --- a/src/library/compiler/cse.h +++ b/src/library/compiler/cse.h @@ -5,15 +5,15 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "kernel/environment.h" +#include "library/elab_environment.h" namespace lean { /* Common subexpression elimination */ -expr cse_core(environment const & env, expr const & e, bool before_erasure); -inline expr cse(environment const & env, expr const & e) { return cse_core(env, e, true); } -inline expr ecse(environment const & env, expr const & e) { return cse_core(env, e, false); } +expr cse_core(elab_environment const & env, expr const & e, bool before_erasure); +inline expr cse(elab_environment const & env, expr const & e) { return cse_core(env, e, true); } +inline expr ecse(elab_environment const & env, expr const & e) { return cse_core(env, e, false); } /* Common case elimination */ -expr cce_core(environment const & env, local_ctx const & lctx, expr const & e); -inline expr cce(environment const & env, expr const & e) { return cce_core(env, local_ctx(), e); } +expr cce_core(elab_environment const & env, local_ctx const & lctx, expr const & e); +inline expr cce(elab_environment const & env, expr const & e) { return cce_core(env, local_ctx(), e); } void initialize_cse(); void finalize_cse(); } diff --git a/src/library/compiler/csimp.cpp b/src/library/compiler/csimp.cpp index 35bb6c375446e..1bc325dac84d0 100644 --- a/src/library/compiler/csimp.cpp +++ b/src/library/compiler/csimp.cpp @@ -64,6 +64,7 @@ optional fold_bin_op(bool before_erasure, expr const & f, expr const & a, class csimp_fn { typedef expr_pair_struct_map jp_cache; + elab_environment m_env; type_checker::state m_st; local_ctx m_lctx; bool m_before_erasure; @@ -96,7 +97,7 @@ class csimp_fn { typedef rb_expr_map expr2ctor; expr2ctor m_expr2ctor; - environment const & env() const { return m_st.env(); } + elab_environment const & env() const { return m_env; } name_generator & ngen() { return m_st.ngen(); } @@ -1625,12 +1626,12 @@ class csimp_fn { } struct is_recursive_fn { - environment const & m_env; + elab_environment const & m_env; csimp_cfg const & m_cfg; bool m_before_erasure; name m_target; - is_recursive_fn(environment const & env, csimp_cfg const & cfg, bool before_erasure): + is_recursive_fn(elab_environment const & env, csimp_cfg const & cfg, bool before_erasure): m_env(env), m_cfg(cfg), m_before_erasure(before_erasure) { } @@ -1969,8 +1970,8 @@ class csimp_fn { } public: - csimp_fn(environment const & env, local_ctx const & lctx, bool before_erasure, csimp_cfg const & cfg): - m_st(env), m_lctx(lctx), m_before_erasure(before_erasure), m_cfg(cfg), m_x("_x"), m_j("j") {} + csimp_fn(elab_environment const & env, local_ctx const & lctx, bool before_erasure, csimp_cfg const & cfg): + m_env(env), m_st(env), m_lctx(lctx), m_before_erasure(before_erasure), m_cfg(cfg), m_x("_x"), m_j("j") {} expr operator()(expr const & e) { if (is_lambda(e)) { @@ -1992,7 +1993,7 @@ bool at_most_once(expr const & e, name const & x) { /* Eliminate join-points that are used only once */ class elim_jp1_fn { - environment const & m_env; + elab_environment const & m_env; local_ctx m_lctx; bool m_before_erasure; name_generator m_ngen; @@ -2093,7 +2094,7 @@ class elim_jp1_fn { } public: - elim_jp1_fn(environment const & env, local_ctx const & lctx, bool before_erasure): + elim_jp1_fn(elab_environment const & env, local_ctx const & lctx, bool before_erasure): m_env(env), m_lctx(lctx), m_before_erasure(before_erasure) {} expr operator()(expr const & e) { m_expanded = false; @@ -2103,7 +2104,7 @@ class elim_jp1_fn { bool expanded() const { return m_expanded; } }; -expr csimp_core(environment const & env, local_ctx const & lctx, expr const & e0, bool before_erasure, csimp_cfg const & cfg) { +expr csimp_core(elab_environment const & env, local_ctx const & lctx, expr const & e0, bool before_erasure, csimp_cfg const & cfg) { csimp_fn simp(env, lctx, before_erasure, cfg); elim_jp1_fn elim_jp1(env, lctx, before_erasure); expr e = e0; diff --git a/src/library/compiler/csimp.h b/src/library/compiler/csimp.h index db3746a770d49..a4ef44b7bd0c6 100644 --- a/src/library/compiler/csimp.h +++ b/src/library/compiler/csimp.h @@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "kernel/environment.h" +#include "library/elab_environment.h" namespace lean { struct csimp_cfg { /* If `m_inline` == false, then we will not inline `c` even if it is marked with the attribute `[inline]`. */ @@ -23,11 +23,11 @@ struct csimp_cfg { csimp_cfg(); }; -expr csimp_core(environment const & env, local_ctx const & lctx, expr const & e, bool before_erasure, csimp_cfg const & cfg); -inline expr csimp(environment const & env, expr const & e, csimp_cfg const & cfg = csimp_cfg()) { +expr csimp_core(elab_environment const & env, local_ctx const & lctx, expr const & e, bool before_erasure, csimp_cfg const & cfg); +inline expr csimp(elab_environment const & env, expr const & e, csimp_cfg const & cfg = csimp_cfg()) { return csimp_core(env, local_ctx(), e, true, cfg); } -inline expr cesimp(environment const & env, expr const & e, csimp_cfg const & cfg = csimp_cfg()) { +inline expr cesimp(elab_environment const & env, expr const & e, csimp_cfg const & cfg = csimp_cfg()) { return csimp_core(env, local_ctx(), e, false, cfg); } } diff --git a/src/library/compiler/eager_lambda_lifting.cpp b/src/library/compiler/eager_lambda_lifting.cpp index 2f838dad1f2a5..3e7d1da698dc4 100644 --- a/src/library/compiler/eager_lambda_lifting.cpp +++ b/src/library/compiler/eager_lambda_lifting.cpp @@ -98,6 +98,7 @@ static bool depends_on_fvar(local_ctx const & lctx, buffer const & params, Remark: we also skip this transformation for definitions marked as `[inline]` or `[instance]`. */ class eager_lambda_lifting_fn { + elab_environment m_env; type_checker::state m_st; csimp_cfg m_cfg; local_ctx m_lctx; @@ -108,7 +109,7 @@ class eager_lambda_lifting_fn { name_set m_nonterminal_lambdas; unsigned m_next_idx{1}; - environment const & env() const { return m_st.env(); } + elab_environment const & env() const { return m_env; } name_generator & ngen() { return m_st.ngen(); } @@ -234,12 +235,13 @@ class eager_lambda_lifting_fn { } expr type = cheap_beta_reduce(type_checker(m_st).infer(code)); name n = next_name(); - /* We add the auxiliary declaration `n` as a "meta" axiom to the environment. + /* We add the auxiliary declaration `n` as a "meta" axiom to the elab_environment. This is a hack to make sure we can use `csimp` to simplify `code` and other definitions that use `n`. We used a similar hack at `specialize.cpp`. */ declaration aux_ax = mk_axiom(n, names(), type, true /* meta */); - m_st.env() = env().add(aux_ax, false); + m_env = m_env.add(aux_ax, false); + m_st.env() = m_env; m_new_decls.push_back(comp_decl(n, code)); return mk_app(mk_constant(n), new_params); } catch (exception &) { @@ -398,10 +400,10 @@ class eager_lambda_lifting_fn { } public: - eager_lambda_lifting_fn(environment const & env, csimp_cfg const & cfg): - m_st(env), m_cfg(cfg) {} + eager_lambda_lifting_fn(elab_environment const & env, csimp_cfg const & cfg): + m_env(env), m_st(env), m_cfg(cfg) {} - pair operator()(comp_decl const & cdecl) { + pair operator()(comp_decl const & cdecl) { m_base_name = cdecl.fst(); expr r = visit(cdecl.snd(), true); comp_decl new_cdecl(cdecl.fst(), r); @@ -410,7 +412,7 @@ class eager_lambda_lifting_fn { } }; -pair eager_lambda_lifting(environment env, comp_decls const & ds, csimp_cfg const & cfg) { +pair eager_lambda_lifting(elab_environment env, comp_decls const & ds, csimp_cfg const & cfg) { comp_decls r; for (comp_decl const & d : ds) { if (has_inline_attribute(env, d.fst()) || is_instance(env, d.fst())) { diff --git a/src/library/compiler/eager_lambda_lifting.h b/src/library/compiler/eager_lambda_lifting.h index 04ab99872daab..bccc9ba42b0f5 100644 --- a/src/library/compiler/eager_lambda_lifting.h +++ b/src/library/compiler/eager_lambda_lifting.h @@ -5,11 +5,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "kernel/environment.h" +#include "library/elab_environment.h" #include "library/compiler/csimp.h" namespace lean { /** \brief Eager version of lambda lifting. See comment at eager_lambda_lifting.cpp. */ -pair eager_lambda_lifting(environment env, comp_decls const & ds, csimp_cfg const & cfg); +pair eager_lambda_lifting(elab_environment env, comp_decls const & ds, csimp_cfg const & cfg); /* Return true iff `fn` is the name of an auxiliary function generated by `eager_lambda_lifting`. */ bool is_elambda_lifting_name(name fn); }; diff --git a/src/library/compiler/erase_irrelevant.cpp b/src/library/compiler/erase_irrelevant.cpp index 42057654f34aa..727ec117cc5c2 100644 --- a/src/library/compiler/erase_irrelevant.cpp +++ b/src/library/compiler/erase_irrelevant.cpp @@ -16,6 +16,7 @@ Author: Leonardo de Moura namespace lean { class erase_irrelevant_fn { typedef std::tuple let_entry; + elab_environment m_env; type_checker::state m_st; local_ctx m_lctx; buffer m_let_fvars; @@ -24,7 +25,7 @@ class erase_irrelevant_fn { unsigned m_next_idx{1}; expr_map m_irrelevant_cache; - environment & env() { return m_st.env(); } + elab_environment & env() { return m_env; } name_generator & ngen() { return m_st.ngen(); } @@ -485,14 +486,14 @@ class erase_irrelevant_fn { lean_unreachable(); } public: - erase_irrelevant_fn(environment const & env, local_ctx const & lctx): - m_st(env), m_lctx(lctx), m_x("_x") {} + erase_irrelevant_fn(elab_environment const & env, local_ctx const & lctx): + m_env(env), m_st(env), m_lctx(lctx), m_x("_x") {} expr operator()(expr const & e) { return mk_let(0, visit(e)); } }; -expr erase_irrelevant_core(environment const & env, local_ctx const & lctx, expr const & e) { +expr erase_irrelevant_core(elab_environment const & env, local_ctx const & lctx, expr const & e) { return erase_irrelevant_fn(env, lctx)(e); } } diff --git a/src/library/compiler/erase_irrelevant.h b/src/library/compiler/erase_irrelevant.h index 5ced492633216..15f3ffd7796d1 100644 --- a/src/library/compiler/erase_irrelevant.h +++ b/src/library/compiler/erase_irrelevant.h @@ -5,8 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "kernel/environment.h" +#include "library/elab_environment.h" namespace lean { -expr erase_irrelevant_core(environment const & env, local_ctx const & lctx, expr const & e); -inline expr erase_irrelevant(environment const & env, expr const & e) { return erase_irrelevant_core(env, local_ctx(), e); } +expr erase_irrelevant_core(elab_environment const & env, local_ctx const & lctx, expr const & e); +inline expr erase_irrelevant(elab_environment const & env, expr const & e) { return erase_irrelevant_core(env, local_ctx(), e); } } diff --git a/src/library/compiler/export_attribute.cpp b/src/library/compiler/export_attribute.cpp index 5ab58f6cdfc62..6388a77d97fd3 100644 --- a/src/library/compiler/export_attribute.cpp +++ b/src/library/compiler/export_attribute.cpp @@ -6,10 +6,11 @@ Author: Leonardo de Moura */ #include "library/constants.h" #include "library/util.h" +#include "library/elab_environment.h" namespace lean { extern "C" object* lean_get_export_name_for(object* env, object *n); -optional get_export_name_for(environment const & env, name const & n) { +optional get_export_name_for(elab_environment const & env, name const & n) { return to_optional(lean_get_export_name_for(env.to_obj_arg(), n.to_obj_arg())); } } diff --git a/src/library/compiler/export_attribute.h b/src/library/compiler/export_attribute.h index 81744fdd800a0..06026945c0174 100644 --- a/src/library/compiler/export_attribute.h +++ b/src/library/compiler/export_attribute.h @@ -5,8 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "kernel/environment.h" +#include "library/elab_environment.h" namespace lean { -optional get_export_name_for(environment const & env, name const & n); -inline bool has_export_name(environment const & env, name const & n) { return static_cast(get_export_name_for(env, n)); } +optional get_export_name_for(elab_environment const & env, name const & n); +inline bool has_export_name(elab_environment const & env, name const & n) { return static_cast(get_export_name_for(env, n)); } } diff --git a/src/library/compiler/extern_attribute.cpp b/src/library/compiler/extern_attribute.cpp index 447f8929209d1..5c00d3a89fe9a 100644 --- a/src/library/compiler/extern_attribute.cpp +++ b/src/library/compiler/extern_attribute.cpp @@ -23,15 +23,15 @@ Authors: Leonardo de Moura namespace lean { extern "C" object* lean_get_extern_attr_data(object* env, object* n); -optional get_extern_attr_data(environment const & env, name const & fn) { +optional get_extern_attr_data(elab_environment const & env, name const & fn) { return to_optional(lean_get_extern_attr_data(env.to_obj_arg(), fn.to_obj_arg())); } -bool is_extern_constant(environment const & env, name const & c) { +bool is_extern_constant(elab_environment const & env, name const & c) { return static_cast(get_extern_attr_data(env, c)); } -bool is_extern_or_init_constant(environment const & env, name const & c) { +bool is_extern_or_init_constant(elab_environment const & env, name const & c) { if (is_extern_constant(env, c)) { return true; } else if (auto info = env.find(c)) { @@ -44,7 +44,7 @@ bool is_extern_or_init_constant(environment const & env, name const & c) { extern "C" object * lean_get_extern_const_arity(object* env, object*, object* w); -optional get_extern_constant_arity(environment const & env, name const & c) { +optional get_extern_constant_arity(elab_environment const & env, name const & c) { auto arity = get_io_result>(lean_get_extern_const_arity(env.to_obj_arg(), c.to_obj_arg(), lean_io_mk_world())); if (optional aux = arity.get()) { return optional(aux->get_small_value()); @@ -53,7 +53,7 @@ optional get_extern_constant_arity(environment const & env, name const } } -bool get_extern_borrowed_info(environment const & env, name const & c, buffer & borrowed_args, bool & borrowed_res) { +bool get_extern_borrowed_info(elab_environment const & env, name const & c, buffer & borrowed_args, bool & borrowed_res) { if (is_extern_constant(env, c)) { /* Extract borrowed info from type */ expr type = env.get(c).get_type(); @@ -80,7 +80,7 @@ bool get_extern_borrowed_info(environment const & env, name const & c, buffer get_extern_constant_ll_type(environment const & env, name const & c) { +optional get_extern_constant_ll_type(elab_environment const & env, name const & c) { if (is_extern_or_init_constant(env, c)) { unsigned arity = 0; expr type = env.get(c).get_type(); diff --git a/src/library/compiler/extern_attribute.h b/src/library/compiler/extern_attribute.h index 84c6d3194bfa9..c254121630e29 100644 --- a/src/library/compiler/extern_attribute.h +++ b/src/library/compiler/extern_attribute.h @@ -6,15 +6,15 @@ Authors: Leonardo de Moura */ #pragma once #include -#include "kernel/environment.h" +#include "library/elab_environment.h" namespace lean { -bool is_extern_constant(environment const & env, name const & c); -bool is_extern_or_init_constant(environment const & env, name const & c); -optional get_extern_constant_ll_type(environment const & env, name const & c); -optional get_extern_constant_arity(environment const & env, name const & c); +bool is_extern_constant(elab_environment const & env, name const & c); +bool is_extern_or_init_constant(elab_environment const & env, name const & c); +optional get_extern_constant_ll_type(elab_environment const & env, name const & c); +optional get_extern_constant_arity(elab_environment const & env, name const & c); typedef object_ref extern_attr_data_value; -optional get_extern_attr_data(environment const & env, name const & c); +optional get_extern_attr_data(elab_environment const & env, name const & c); /* Return true if `c` is an extern constant, and store in borrowed_args and borrowed_res which arguments/results are marked as borrowed. */ -bool get_extern_borrowed_info(environment const & env, name const & c, buffer & borrowed_args, bool & borrowed_res); +bool get_extern_borrowed_info(elab_environment const & env, name const & c, buffer & borrowed_args, bool & borrowed_res); } diff --git a/src/library/compiler/extract_closed.cpp b/src/library/compiler/extract_closed.cpp index 929b49e6a3cd3..234ce10ecfbd5 100644 --- a/src/library/compiler/extract_closed.cpp +++ b/src/library/compiler/extract_closed.cpp @@ -25,7 +25,7 @@ bool is_extract_closed_aux_fn(name const & n) { } class extract_closed_fn { - environment m_env; + elab_environment m_env; comp_decls m_input_decls; name_generator m_ngen; local_ctx m_lctx; @@ -34,7 +34,7 @@ class extract_closed_fn { unsigned m_next_idx{1}; expr_map m_closed; - environment const & env() const { return m_env; } + elab_environment const & env() const { return m_env; } name_generator & ngen() { return m_ngen; } name next_name() { @@ -286,11 +286,11 @@ class extract_closed_fn { } public: - extract_closed_fn(environment const & env, comp_decls const & ds): + extract_closed_fn(elab_environment const & env, comp_decls const & ds): m_env(env), m_input_decls(ds) { } - pair operator()(comp_decl const & d) { + pair operator()(comp_decl const & d) { if (arity_was_reduced(d)) { /* Do nothing since `d` will be inlined. */ return mk_pair(env(), comp_decls(d)); @@ -308,11 +308,11 @@ class extract_closed_fn { } }; -pair extract_closed_core(environment const & env, comp_decls const & input_ds, comp_decl const & d) { +pair extract_closed_core(elab_environment const & env, comp_decls const & input_ds, comp_decl const & d) { return extract_closed_fn(env, input_ds)(d); } -pair extract_closed(environment env, comp_decls const & ds) { +pair extract_closed(elab_environment env, comp_decls const & ds) { comp_decls r; for (comp_decl const & d : ds) { comp_decls new_ds; diff --git a/src/library/compiler/extract_closed.h b/src/library/compiler/extract_closed.h index 1c8b39d4585fd..5c15fdb910b3d 100644 --- a/src/library/compiler/extract_closed.h +++ b/src/library/compiler/extract_closed.h @@ -5,9 +5,9 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "kernel/environment.h" +#include "library/elab_environment.h" #include "library/compiler/util.h" namespace lean { bool is_extract_closed_aux_fn(name const & n); -pair extract_closed(environment env, comp_decls const & ds); +pair extract_closed(elab_environment env, comp_decls const & ds); } diff --git a/src/library/compiler/find_jp.cpp b/src/library/compiler/find_jp.cpp index 343128c0c5195..a6279e953ef04 100644 --- a/src/library/compiler/find_jp.cpp +++ b/src/library/compiler/find_jp.cpp @@ -13,7 +13,7 @@ namespace lean { /* Find join-points */ class find_jp_fn { - environment const & m_env; + elab_environment const & m_env; local_ctx m_lctx; name_generator m_ngen; name_map m_candidates; @@ -130,7 +130,7 @@ class find_jp_fn { } public: - find_jp_fn(environment const & env): + find_jp_fn(elab_environment const & env): m_env(env) {} expr operator()(expr const & e) { @@ -138,7 +138,7 @@ class find_jp_fn { } }; -expr find_jp(environment const & env, expr const & e) { +expr find_jp(elab_environment const & env, expr const & e) { return find_jp_fn(env)(e); } } diff --git a/src/library/compiler/find_jp.h b/src/library/compiler/find_jp.h index 2b611a1b59f94..a71e2fcc55c5b 100644 --- a/src/library/compiler/find_jp.h +++ b/src/library/compiler/find_jp.h @@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "kernel/environment.h" +#include "library/elab_environment.h" namespace lean { -expr find_jp(environment const & env, expr const & e); +expr find_jp(elab_environment const & env, expr const & e); } diff --git a/src/library/compiler/implemented_by_attribute.cpp b/src/library/compiler/implemented_by_attribute.cpp index 267c60c4ccb27..8a6afe4ef032e 100644 --- a/src/library/compiler/implemented_by_attribute.cpp +++ b/src/library/compiler/implemented_by_attribute.cpp @@ -4,11 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include "kernel/environment.h" +#include "library/elab_environment.h" namespace lean { extern "C" object* lean_get_implemented_by(object*, object*); -optional get_implemented_by_attribute(environment const & env, name const & n) { +optional get_implemented_by_attribute(elab_environment const & env, name const & n) { return to_optional(lean_get_implemented_by(env.to_obj_arg(), n.to_obj_arg())); } } diff --git a/src/library/compiler/implemented_by_attribute.h b/src/library/compiler/implemented_by_attribute.h index 375cb3ba37baa..30b68954d8c65 100644 --- a/src/library/compiler/implemented_by_attribute.h +++ b/src/library/compiler/implemented_by_attribute.h @@ -5,11 +5,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "kernel/environment.h" +#include "library/elab_environment.h" namespace lean { -optional get_implemented_by_attribute(environment const & env, name const & n); -inline bool has_implemented_by_attribute(environment const & env, name const & n) { +optional get_implemented_by_attribute(elab_environment const & env, name const & n); +inline bool has_implemented_by_attribute(elab_environment const & env, name const & n) { return static_cast(get_implemented_by_attribute(env, n)); } } diff --git a/src/library/compiler/init_attribute.cpp b/src/library/compiler/init_attribute.cpp index eac9ad41f13dd..1b5a09986ab89 100644 --- a/src/library/compiler/init_attribute.cpp +++ b/src/library/compiler/init_attribute.cpp @@ -5,12 +5,12 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura */ #include "runtime/object_ref.h" -#include "kernel/environment.h" +#include "library/elab_environment.h" namespace lean { extern "C" object* lean_get_init_fn_name_for(object* env, object* fn); -optional get_init_fn_name_for(environment const & env, name const & n) { +optional get_init_fn_name_for(elab_environment const & env, name const & n) { return to_optional(lean_get_init_fn_name_for(env.to_obj_arg(), n.to_obj_arg())); } } diff --git a/src/library/compiler/init_attribute.h b/src/library/compiler/init_attribute.h index 9bfaa62a3d1d7..7a0f5707546bc 100644 --- a/src/library/compiler/init_attribute.h +++ b/src/library/compiler/init_attribute.h @@ -5,11 +5,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura */ #pragma once -#include "kernel/environment.h" +#include "library/elab_environment.h" namespace lean { -optional get_init_fn_name_for(environment const & env, name const & n); -inline bool has_init_attribute(environment const & env, name const & n) { +optional get_init_fn_name_for(elab_environment const & env, name const & n); +inline bool has_init_attribute(elab_environment const & env, name const & n) { return static_cast(get_init_fn_name_for(env, n)); } } diff --git a/src/library/compiler/ir.cpp b/src/library/compiler/ir.cpp index 2c499224f3cd1..528b28bf3b42e 100644 --- a/src/library/compiler/ir.cpp +++ b/src/library/compiler/ir.cpp @@ -100,8 +100,8 @@ std::string decl_to_string(decl const & d) { string_ref r(lean_ir_decl_to_string(d.to_obj_arg())); return r.to_std_string(); } -environment add_decl(environment const & env, decl const & d) { - return environment(lean_ir_add_decl(env.to_obj_arg(), d.to_obj_arg())); +elab_environment add_decl(elab_environment const & env, decl const & d) { + return elab_environment(lean_ir_add_decl(env.to_obj_arg(), d.to_obj_arg())); } } @@ -133,12 +133,13 @@ static ir::type to_ir_type(expr const & e) { } class to_ir_fn { + elab_environment m_env; type_checker::state m_st; local_ctx m_lctx; name m_x{"x"}; unsigned m_next_idx{1}; - environment const & env() const { return m_st.env(); } + elab_environment const & env() const { return m_env; } name_generator & ngen() { return m_st.ngen(); } @@ -493,7 +494,7 @@ class to_ir_fn { return ir::mk_decl(fn, xs, type, b); } public: - to_ir_fn(environment const & env):m_st(env) {} + to_ir_fn(elab_environment const & env):m_env(env), m_st(env) {} ir::decl operator()(comp_decl const & d) { return to_ir_decl(d); } @@ -520,7 +521,7 @@ class to_ir_fn { }; namespace ir { -decl to_ir_decl(environment const & env, comp_decl const & d) { +decl to_ir_decl(elab_environment const & env, comp_decl const & d) { return to_ir_fn(env)(d); } @@ -528,7 +529,7 @@ decl to_ir_decl(environment const & env, comp_decl const & d) { @[export lean.ir.compile_core] def compile (env : Environment) (opts : Options) (decls : Array Decl) : Log × (Except String Environment) := */ -environment compile(environment const & env, options const & opts, comp_decls const & decls) { +elab_environment compile(elab_environment const & env, options const & opts, comp_decls const & decls) { buffer ir_decls; for (comp_decl const & decl : decls) { lean_trace(name({"compiler", "lambda_pure"}), @@ -549,7 +550,7 @@ environment compile(environment const & env, options const & opts, comp_decls co dec_ref(r); throw exception(error.data()); } else { - environment new_env(cnstr_get(v, 0), true); + elab_environment new_env(cnstr_get(v, 0), true); dec_ref(r); return new_env; } @@ -560,28 +561,28 @@ environment compile(environment const & env, options const & opts, comp_decls co def addBoxedVersion (env : Environment) (decl : Decl) : Except String Environment := */ extern "C" object * lean_ir_add_boxed_version(object * env, object * decl); -environment add_boxed_version(environment const & env, decl const & d) { +elab_environment add_boxed_version(elab_environment const & env, decl const & d) { object * v = lean_ir_add_boxed_version(env.to_obj_arg(), d.to_obj_arg()); if (cnstr_tag(v) == 0) { string_ref error(cnstr_get(v, 0), true); dec_ref(v); throw exception(error.data()); } else { - environment new_env(cnstr_get(v, 0), true); + elab_environment new_env(cnstr_get(v, 0), true); dec_ref(v); return new_env; } } -environment add_extern(environment const & env, name const & fn) { +elab_environment add_extern(elab_environment const & env, name const & fn) { decl d = to_ir_fn(env)(fn); - environment new_env = ir::add_decl(env, d); + elab_environment new_env = ir::add_decl(env, d); return add_boxed_version(new_env, d); } extern "C" LEAN_EXPORT object* lean_add_extern(object * env, object * fn) { try { - environment new_env = add_extern(environment(env), name(fn)); + elab_environment new_env = add_extern(elab_environment(env), name(fn)); return mk_except_ok(new_env); } catch (exception & ex) { // throw; // We use to uncomment this line when debugging weird bugs in the Lean/C++ interface. @@ -591,7 +592,7 @@ extern "C" LEAN_EXPORT object* lean_add_extern(object * env, object * fn) { extern "C" object * lean_ir_emit_c(object * env, object * mod_name); -string_ref emit_c(environment const & env, name const & mod_name) { +string_ref emit_c(elab_environment const & env, name const & mod_name) { object * r = lean_ir_emit_c(env.to_obj_arg(), mod_name.to_obj_arg()); string_ref s(cnstr_get(r, 0), true); if (cnstr_tag(r) == 0) { @@ -639,7 +640,7 @@ object_ref to_object_ref(cnstr_info const & info) { } extern "C" LEAN_EXPORT object * lean_ir_get_ctor_layout(object * env0, object * ctor_name0) { - environment const & env = TO_REF(environment, env0); + elab_environment const & env = TO_REF(elab_environment, env0); name const & ctor_name = TO_REF(name, ctor_name0); type_checker::state st(env); try { diff --git a/src/library/compiler/ir.h b/src/library/compiler/ir.h index 8a9a092269a27..df91f21ee5b47 100644 --- a/src/library/compiler/ir.h +++ b/src/library/compiler/ir.h @@ -6,7 +6,7 @@ Author: Leonardo de Moura */ #pragma once #include -#include "kernel/environment.h" +#include "library/elab_environment.h" #include "library/compiler/util.h" namespace lean { namespace ir { @@ -35,10 +35,10 @@ typedef object_ref decl; typedef object_ref decl; std::string decl_to_string(decl const & d); void test(decl const & d); -environment compile(environment const & env, options const & opts, comp_decls const & decls); -environment add_extern(environment const & env, name const & fn); -LEAN_EXPORT string_ref emit_c(environment const & env, name const & mod_name); -void emit_llvm(environment const & env, name const & mod_name, std::string const &filepath); +elab_environment compile(elab_environment const & env, options const & opts, comp_decls const & decls); +elab_environment add_extern(elab_environment const & env, name const & fn); +LEAN_EXPORT string_ref emit_c(elab_environment const & env, name const & mod_name); +void emit_llvm(elab_environment const & env, name const & mod_name, std::string const &filepath); } void initialize_ir(); void finalize_ir(); diff --git a/src/library/compiler/ir_interpreter.cpp b/src/library/compiler/ir_interpreter.cpp index 978aa853f4584..2f32ef8621503 100644 --- a/src/library/compiler/ir_interpreter.cpp +++ b/src/library/compiler/ir_interpreter.cpp @@ -19,7 +19,7 @@ Implementation The interpreter mainly consists of a homogeneous stack of `value`s, which are either unboxed values or pointers to boxed objects. The IR type system tells us which union member is active at any time. IR variables are mapped to stack slots by adding the current base pointer to the variable index. Further stacks are used for storing join points and call -stack metadata. The interpreted IR is taken directly from the environment. Whenever possible, we try to switch to native +stack metadata. The interpreted IR is taken directly from the elab_environment. Whenever possible, we try to switch to native code by checking for the mangled symbol via dlsym/GetProcAddress, which is also how we can call external functions (which only works if the file declaring them has already been compiled). We always call the "boxed" versions of native functions, which have a (relatively) homogeneous ABI that we can use without runtime code generation; see also @@ -182,7 +182,7 @@ type decl_type(decl const & b) { return cnstr_get_type(b, 2); } fn_body const & decl_fun_body(decl const & b) { lean_assert(decl_tag(b) == decl_kind::Fun); return cnstr_get_ref_t(b, 3); } extern "C" object * lean_ir_find_env_decl(object * env, object * n); -option_ref find_ir_decl(environment const & env, name const & n) { +option_ref find_ir_decl(elab_environment const & env, name const & n) { return option_ref(lean_ir_find_env_decl(env.to_obj_arg(), n.to_obj_arg())); } @@ -213,12 +213,12 @@ static bool type_is_scalar(type t) { } extern "C" object* lean_get_regular_init_fn_name_for(object* env, object* fn); -optional get_regular_init_fn_name_for(environment const & env, name const & n) { +optional get_regular_init_fn_name_for(elab_environment const & env, name const & n) { return to_optional(lean_get_regular_init_fn_name_for(env.to_obj_arg(), n.to_obj_arg())); } extern "C" object* lean_get_builtin_init_fn_name_for(object* env, object* fn); -optional get_builtin_init_fn_name_for(environment const & env, name const & n) { +optional get_builtin_init_fn_name_for(elab_environment const & env, name const & n) { return to_optional(lean_get_builtin_init_fn_name_for(env.to_obj_arg(), n.to_obj_arg())); } @@ -355,7 +355,7 @@ class interpreter { frame(name const & mFn, size_t mArgBp, size_t mJpBp) : m_fn(mFn), m_arg_bp(mArgBp), m_jp_bp(mJpBp) {} }; std::vector m_call_stack; - environment const & m_env; + elab_environment const & m_env; options const & m_opts; // if `false`, use IR code where possible bool m_prefer_native; @@ -393,7 +393,7 @@ class interpreter { public: template - static inline T with_interpreter(environment const & env, options const & opts, name const & fn, std::function const & f) { + static inline T with_interpreter(elab_environment const & env, options const & opts, name const & fn, std::function const & f) { if (g_interpreter && is_eqp(g_interpreter->m_env, env) && is_eqp(g_interpreter->m_opts, opts)) { return f(*g_interpreter); } else { @@ -808,7 +808,7 @@ class interpreter { } } - /** \brief Retrieve Lean declaration from environment. */ + /** \brief Retrieve Lean declaration from elab_environment. */ decl get_decl(name const & fn) { option_ref d = find_ir_decl(m_env, fn); if (!d) { @@ -931,7 +931,7 @@ class interpreter { // static closure stub static object * stub_m_aux(object ** args) { - environment env(args[0]); + elab_environment env(args[0]); options opts(args[1]); return with_interpreter(env, opts, decl_fun_id(TO_REF(decl, args[2])), [&](interpreter & interp) { return interp.stub_m(args); @@ -979,7 +979,7 @@ class interpreter { } } public: - explicit interpreter(environment const & env, options const & opts) : m_env(env), m_opts(opts) { + explicit interpreter(elab_environment const & env, options const & opts) : m_env(env), m_opts(opts) { m_prefer_native = opts.get_bool(*g_interpreter_prefer_native, LEAN_DEFAULT_INTERPRETER_PREFER_NATIVE); } @@ -1090,24 +1090,34 @@ class interpreter { extern "C" object * lean_decl_get_sorry_dep(object * env, object * n); -optional get_sorry_dep(environment const & env, name const & n) { +optional get_sorry_dep(elab_environment const & env, name const & n) { return option_ref(lean_decl_get_sorry_dep(env.to_obj_arg(), n.to_obj_arg())).get(); } -object * run_boxed(environment const & env, options const & opts, name const & fn, unsigned n, object **args) { +object * run_boxed(elab_environment const & env, options const & opts, name const & fn, unsigned n, object **args) { if (optional decl_with_sorry = get_sorry_dep(env, fn)) { throw exception(sstream() << "cannot evaluate code because '" << *decl_with_sorry << "' uses 'sorry' and/or contains errors"); } return interpreter::with_interpreter(env, opts, fn, [&](interpreter & interp) { return interp.call_boxed(fn, n, args); }); } -uint32 run_main(environment const & env, options const & opts, int argv, char * argc[]) { + +extern "C" obj_res lean_elab_environment_of_kernel_env(obj_arg); +elab_environment elab_environment_of_kernel_env(environment const & env) { + return elab_environment(lean_elab_environment_of_kernel_env(env.to_obj_arg())); +} + +object * run_boxed_kernel(environment const & env, options const & opts, name const & fn, unsigned n, object **args) { + return run_boxed(elab_environment_of_kernel_env(env), opts, fn, n, args); +} + +uint32 run_main(elab_environment const & env, options const & opts, int argv, char * argc[]) { return interpreter::with_interpreter(env, opts, "main", [&](interpreter & interp) { return interp.run_main(argv, argc); }); } extern "C" LEAN_EXPORT object * lean_eval_const(object * env, object * opts, object * c) { try { - return mk_cnstr(1, run_boxed(TO_REF(environment, env), TO_REF(options, opts), TO_REF(name, c), 0, 0)).steal(); + return mk_cnstr(1, run_boxed(TO_REF(elab_environment, env), TO_REF(options, opts), TO_REF(name, c), 0, 0)).steal(); } catch (exception & ex) { return mk_cnstr(0, string_ref(ex.what())).steal(); } @@ -1134,7 +1144,7 @@ extern "C" LEAN_EXPORT object * lean_run_mod_init(object * mod, object *) { } extern "C" LEAN_EXPORT object * lean_run_init(object * env, object * opts, object * decl, object * init_decl, object *) { - return interpreter::with_interpreter(TO_REF(environment, env), TO_REF(options, opts), TO_REF(name, decl), [&](interpreter & interp) { + return interpreter::with_interpreter(TO_REF(elab_environment, env), TO_REF(options, opts), TO_REF(name, decl), [&](interpreter & interp) { return interp.run_init(TO_REF(name, decl), TO_REF(name, init_decl)); }); } diff --git a/src/library/compiler/ir_interpreter.h b/src/library/compiler/ir_interpreter.h index 00a65a34fe623..c3a0022656df0 100644 --- a/src/library/compiler/ir_interpreter.h +++ b/src/library/compiler/ir_interpreter.h @@ -5,14 +5,14 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Sebastian Ullrich */ #pragma once -#include "kernel/environment.h" +#include "library/elab_environment.h" #include "runtime/object.h" namespace lean { namespace ir { /** \brief Run `n` using the "boxed" ABI, i.e. with all-owned parameters. */ -object * run_boxed(environment const & env, options const & opts, name const & fn, unsigned n, object **args); -LEAN_EXPORT uint32 run_main(environment const & env, options const & opts, int argv, char * argc[]); +object * run_boxed(elab_environment const & env, options const & opts, name const & fn, unsigned n, object **args); +LEAN_EXPORT uint32 run_main(elab_environment const & env, options const & opts, int argv, char * argc[]); } void initialize_ir_interpreter(); void finalize_ir_interpreter(); diff --git a/src/library/compiler/lambda_lifting.cpp b/src/library/compiler/lambda_lifting.cpp index 176db6baae964..e7138092824ae 100644 --- a/src/library/compiler/lambda_lifting.cpp +++ b/src/library/compiler/lambda_lifting.cpp @@ -30,7 +30,7 @@ bool is_lambda_lifting_name(name fn) { } class lambda_lifting_fn { - environment m_env; + elab_environment m_env; name_generator m_ngen; local_ctx m_lctx; buffer m_new_decls; @@ -39,7 +39,7 @@ class lambda_lifting_fn { typedef std::unordered_set name_set; - environment const & env() { return m_env; } + elab_environment const & env() { return m_env; } name_generator & ngen() { return m_ngen; } @@ -207,10 +207,10 @@ class lambda_lifting_fn { } public: - lambda_lifting_fn(environment const & env): + lambda_lifting_fn(elab_environment const & env): m_env(env) {} - pair operator()(comp_decl const & cdecl) { + pair operator()(comp_decl const & cdecl) { m_base_name = cdecl.fst(); expr r = visit(cdecl.snd(), true); comp_decl new_cdecl(cdecl.fst(), r); @@ -219,11 +219,11 @@ class lambda_lifting_fn { } }; -pair lambda_lifting(environment const & env, comp_decl const & d) { +pair lambda_lifting(elab_environment const & env, comp_decl const & d) { return lambda_lifting_fn(env)(d); } -pair lambda_lifting(environment env, comp_decls const & ds) { +pair lambda_lifting(elab_environment env, comp_decls const & ds) { comp_decls r; for (comp_decl const & d : ds) { comp_decls new_ds; diff --git a/src/library/compiler/lambda_lifting.h b/src/library/compiler/lambda_lifting.h index c4f921467c533..ded6caee37721 100644 --- a/src/library/compiler/lambda_lifting.h +++ b/src/library/compiler/lambda_lifting.h @@ -5,11 +5,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "kernel/environment.h" +#include "library/elab_environment.h" #include "library/compiler/util.h" namespace lean { /** \brief Lift lambda expressions in `ds`. The result also contains new auxiliary declarations that have been generated. */ -pair lambda_lifting(environment env, comp_decls const & ds); +pair lambda_lifting(elab_environment env, comp_decls const & ds); /* Return true iff `fn` is the name of an auxiliary function generated by `lambda_lifting`. */ bool is_lambda_lifting_name(name fn); }; diff --git a/src/library/compiler/lcnf.cpp b/src/library/compiler/lcnf.cpp index 9bcd88d4cf593..95949e744e887 100644 --- a/src/library/compiler/lcnf.cpp +++ b/src/library/compiler/lcnf.cpp @@ -37,6 +37,7 @@ bool is_do_notation_joinpoint(name const & n) { class to_lcnf_fn { typedef rb_expr_map cache; + elab_environment m_env; type_checker::state m_st; local_ctx m_lctx; cache m_cache; @@ -44,10 +45,10 @@ class to_lcnf_fn { name m_x; unsigned m_next_idx{1}; public: - to_lcnf_fn(environment const & env, local_ctx const & lctx): - m_st(env), m_lctx(lctx), m_x("_x") {} + to_lcnf_fn(elab_environment const & env, local_ctx const & lctx): + m_env(env), m_st(env), m_lctx(lctx), m_x("_x") {} - environment & env() { return m_st.env(); } + elab_environment & env() { return m_env; } name_generator & ngen() { return m_st.ngen(); } @@ -637,7 +638,7 @@ class to_lcnf_fn { } }; -expr to_lcnf_core(environment const & env, local_ctx const & lctx, expr const & e) { +expr to_lcnf_core(elab_environment const & env, local_ctx const & lctx, expr const & e) { expr new_e = unfold_macro_defs(env, e); return to_lcnf_fn(env, lctx)(new_e); } diff --git a/src/library/compiler/lcnf.h b/src/library/compiler/lcnf.h index 58d3c9c03c602..79fbb4967d70f 100644 --- a/src/library/compiler/lcnf.h +++ b/src/library/compiler/lcnf.h @@ -5,10 +5,10 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "kernel/environment.h" +#include "library/elab_environment.h" namespace lean { -expr to_lcnf_core(environment const & env, local_ctx const & lctx, expr const & e); -inline expr to_lcnf(environment const & env, expr const & e) { return to_lcnf_core(env, local_ctx(), e); } +expr to_lcnf_core(elab_environment const & env, local_ctx const & lctx, expr const & e); +inline expr to_lcnf(elab_environment const & env, expr const & e) { return to_lcnf_core(env, local_ctx(), e); } void initialize_lcnf(); void finalize_lcnf(); } diff --git a/src/library/compiler/ll_infer_type.cpp b/src/library/compiler/ll_infer_type.cpp index 9167aeb8613bc..671c9183c5523 100644 --- a/src/library/compiler/ll_infer_type.cpp +++ b/src/library/compiler/ll_infer_type.cpp @@ -17,12 +17,13 @@ static expr * g_bot = nullptr; /* Infer type of expressions in ENF or LLNF. */ class ll_infer_type_fn { + elab_environment m_env; type_checker::state m_st; local_ctx m_lctx; buffer const * m_new_decl_names{nullptr}; buffer const * m_new_decl_types{nullptr}; - environment const & env() const { return m_st.env(); } + elab_environment const & env() const { return m_env; } name_generator & ngen() { return m_st.ngen(); } bool may_use_bot() const { return m_new_decl_types != nullptr; } @@ -227,14 +228,14 @@ class ll_infer_type_fn { } public: - ll_infer_type_fn(environment const & env, buffer const & ns, buffer const & ts): - m_st(env), m_new_decl_names(&ns), m_new_decl_types(&ts) {} - ll_infer_type_fn(environment const & env, local_ctx const & lctx): - m_st(env), m_lctx(lctx) {} + ll_infer_type_fn(elab_environment const & env, buffer const & ns, buffer const & ts): + m_env(env), m_st(env), m_new_decl_names(&ns), m_new_decl_types(&ts) {} + ll_infer_type_fn(elab_environment const & env, local_ctx const & lctx): + m_env(env), m_st(env), m_lctx(lctx) {} expr operator()(expr const & e) { return infer(e); } }; -void ll_infer_type(environment const & env, comp_decls const & ds, buffer & ts) { +void ll_infer_type(elab_environment const & env, comp_decls const & ds, buffer & ts) { buffer ns; ts.clear(); /* Initialize `ts` */ @@ -272,7 +273,7 @@ void ll_infer_type(environment const & env, comp_decls const & ds, buffer lean_assert(ts.size() == length(ds)); } -expr ll_infer_type(environment const & env, local_ctx const & lctx, expr const & e) { +expr ll_infer_type(elab_environment const & env, local_ctx const & lctx, expr const & e) { return ll_infer_type_fn(env, lctx)(e); } diff --git a/src/library/compiler/ll_infer_type.h b/src/library/compiler/ll_infer_type.h index 779f5e9583578..35bd795b77fe5 100644 --- a/src/library/compiler/ll_infer_type.h +++ b/src/library/compiler/ll_infer_type.h @@ -5,11 +5,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "kernel/environment.h" +#include "library/elab_environment.h" namespace lean { -expr ll_infer_type(environment const & env, local_ctx const & lctx, expr const & e); -inline expr ll_infer_type(environment const & env, expr const & e) { return ll_infer_type(env, local_ctx(), e); } -void ll_infer_type(environment const & env, comp_decls const & ds, buffer & ts); +expr ll_infer_type(elab_environment const & env, local_ctx const & lctx, expr const & e); +inline expr ll_infer_type(elab_environment const & env, expr const & e) { return ll_infer_type(env, local_ctx(), e); } +void ll_infer_type(elab_environment const & env, comp_decls const & ds, buffer & ts); void initialize_ll_infer_type(); void finalize_ll_infer_type(); } diff --git a/src/library/compiler/llnf.cpp b/src/library/compiler/llnf.cpp index 25a4b4f11b4c1..d5af9bbb19f7f 100644 --- a/src/library/compiler/llnf.cpp +++ b/src/library/compiler/llnf.cpp @@ -247,7 +247,7 @@ cnstr_info::cnstr_info(unsigned cidx, list const & finfo): } } -unsigned get_llnf_arity(environment const & env, name const & n) { +unsigned get_llnf_arity(elab_environment const & env, name const & n) { /* First, try to infer arity from `_cstage2` auxiliary definition. */ name c = mk_cstage2_name(n); optional info = env.find(c); @@ -334,6 +334,7 @@ class to_lambda_pure_fn { typedef name_hash_set name_set; typedef name_hash_map cnstr_info_cache; typedef name_hash_map> enum_cache; + elab_environment m_env; type_checker::state m_st; local_ctx m_lctx; buffer m_fvars; @@ -343,7 +344,7 @@ class to_lambda_pure_fn { unsigned m_next_jp_idx{1}; cnstr_info_cache m_cnstr_info_cache; - environment const & env() const { return m_st.env(); } + elab_environment const & env() const { return m_env; } name_generator & ngen() { return m_st.ngen(); } @@ -803,8 +804,8 @@ class to_lambda_pure_fn { } public: - to_lambda_pure_fn(environment const & env): - m_st(env), m_x("_x"), m_j("j") { + to_lambda_pure_fn(elab_environment const & env): + m_env(env), m_st(env), m_x("_x"), m_j("j") { } expr operator()(expr e) { @@ -815,7 +816,7 @@ class to_lambda_pure_fn { } }; -expr get_constant_ll_type(environment const & env, name const & c) { +expr get_constant_ll_type(elab_environment const & env, name const & c) { if (optional type = get_extern_constant_ll_type(env, c)) { return *type; } else { @@ -823,7 +824,7 @@ expr get_constant_ll_type(environment const & env, name const & c) { } } -environment compile_ir(environment const & env, options const & opts, comp_decls const & ds) { +elab_environment compile_ir(elab_environment const & env, options const & opts, comp_decls const & ds) { buffer new_ds; for (comp_decl const & d : ds) { expr new_v = to_lambda_pure_fn(env)(d.snd()); diff --git a/src/library/compiler/llnf.h b/src/library/compiler/llnf.h index 87c61c6ffee58..3b6bebadc1dfc 100644 --- a/src/library/compiler/llnf.h +++ b/src/library/compiler/llnf.h @@ -5,11 +5,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "kernel/environment.h" +#include "library/elab_environment.h" #include "library/compiler/util.h" namespace lean { -environment compile_ir(environment const & env, options const & opts, comp_decls const & ds); +elab_environment compile_ir(elab_environment const & env, options const & opts, comp_decls const & ds); bool is_llnf_apply(expr const & e); bool is_llnf_closure(expr const & e); @@ -49,8 +49,8 @@ inline bool is_llnf_uset(expr const & e) { unsigned d; return is_llnf_uset(e, d) inline bool is_llnf_box(expr const & e) { unsigned n; return is_llnf_box(e, n); } inline bool is_llnf_unbox(expr const & e) { unsigned n; return is_llnf_unbox(e, n); } -expr get_constant_ll_type(environment const & env, name const & c); -unsigned get_llnf_arity(environment const & env, name const & c); +expr get_constant_ll_type(elab_environment const & env, name const & c); +unsigned get_llnf_arity(elab_environment const & env, name const & c); struct field_info { /* Remark: the position of a scalar value in diff --git a/src/library/compiler/reduce_arity.cpp b/src/library/compiler/reduce_arity.cpp index 22e32381867b1..cd5135e5d2b7a 100644 --- a/src/library/compiler/reduce_arity.cpp +++ b/src/library/compiler/reduce_arity.cpp @@ -29,7 +29,7 @@ bool arity_was_reduced(comp_decl const & cdecl) { return is_reduce_arity_aux_fn(n) && n.get_prefix() == cdecl.fst(); } -comp_decls reduce_arity(environment const & env, comp_decl const & cdecl) { +comp_decls reduce_arity(elab_environment const & env, comp_decl const & cdecl) { if (has_export_name(env, cdecl.fst()) || cdecl.fst() == "main") { /* We do not modify the arity of entry points (i.e., functions with attribute [export]) */ return comp_decls(cdecl); @@ -92,7 +92,7 @@ comp_decls reduce_arity(environment const & env, comp_decl const & cdecl) { return comp_decls(red_decl, comp_decls(new_decl)); } -comp_decls reduce_arity(environment const & env, comp_decls const & ds) { +comp_decls reduce_arity(elab_environment const & env, comp_decls const & ds) { comp_decls r; for (comp_decl const & d : ds) { r = append(r, reduce_arity(env, d)); diff --git a/src/library/compiler/reduce_arity.h b/src/library/compiler/reduce_arity.h index f16a00bb58526..9c131c75dc2de 100644 --- a/src/library/compiler/reduce_arity.h +++ b/src/library/compiler/reduce_arity.h @@ -6,7 +6,7 @@ Author: Leonardo de Moura #pragma once #include "library/compiler/util.h" namespace lean { -comp_decls reduce_arity(environment const & env, comp_decls const & cdecls); +comp_decls reduce_arity(elab_environment const & env, comp_decls const & cdecls); /* Return true if the `cdecl` is of the form `f := fun xs, f._rarg ...`. That is, `f`s arity "was reduced" and an auxiliary declaration `f._rarg` was created to replace it. */ bool arity_was_reduced(comp_decl const & cdecl); diff --git a/src/library/compiler/simp_app_args.cpp b/src/library/compiler/simp_app_args.cpp index 84f34ad9c82c5..7c18d2d179f8f 100644 --- a/src/library/compiler/simp_app_args.cpp +++ b/src/library/compiler/simp_app_args.cpp @@ -11,13 +11,14 @@ Author: Leonardo de Moura namespace lean { /* Make sure every argument of applications and projections is a free variable (or neutral element). */ class simp_app_args_fn { + elab_environment m_env; type_checker::state m_st; local_ctx m_lctx; buffer m_fvars; name m_x; unsigned m_next_idx{1}; - environment const & env() const { return m_st.env(); } + elab_environment const & env() const { return m_env; } name_generator & ngen() { return m_st.ngen(); } name next_name() { @@ -125,14 +126,14 @@ class simp_app_args_fn { } public: - simp_app_args_fn(environment const & env):m_st(env), m_x("_x") {} + simp_app_args_fn(elab_environment const & env):m_env(env), m_st(env), m_x("_x") {} expr operator()(expr const & e) { return mk_let(0, visit(e)); } }; -expr simp_app_args(environment const & env, expr const & e) { +expr simp_app_args(elab_environment const & env, expr const & e) { return simp_app_args_fn(env)(e); } } diff --git a/src/library/compiler/simp_app_args.h b/src/library/compiler/simp_app_args.h index af9bb6e1d7420..35dab66e24582 100644 --- a/src/library/compiler/simp_app_args.h +++ b/src/library/compiler/simp_app_args.h @@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "kernel/environment.h" +#include "library/elab_environment.h" namespace lean { -expr simp_app_args(environment const & env, expr const & e); +expr simp_app_args(elab_environment const & env, expr const & e); } diff --git a/src/library/compiler/specialize.cpp b/src/library/compiler/specialize.cpp index 6874412c894e3..6340fabf7b2db 100644 --- a/src/library/compiler/specialize.cpp +++ b/src/library/compiler/specialize.cpp @@ -19,11 +19,11 @@ namespace lean { extern "C" uint8 lean_has_specialize_attribute(object* env, object* n); extern "C" uint8 lean_has_nospecialize_attribute(object* env, object* n); -bool has_specialize_attribute(environment const & env, name const & n) { +bool has_specialize_attribute(elab_environment const & env, name const & n) { return lean_has_specialize_attribute(env.to_obj_arg(), n.to_obj_arg()); } -bool has_nospecialize_attribute(environment const & env, name const & n) { +bool has_nospecialize_attribute(elab_environment const & env, name const & n) { return lean_has_nospecialize_attribute(env.to_obj_arg(), n.to_obj_arg()); } @@ -103,11 +103,11 @@ class spec_info : public object_ref { extern "C" object* lean_add_specialization_info(object* env, object* fn, object* info); extern "C" object* lean_get_specialization_info(object* env, object* fn); -static environment save_specialization_info(environment const & env, name const & fn, spec_info const & si) { - return environment(lean_add_specialization_info(env.to_obj_arg(), fn.to_obj_arg(), si.to_obj_arg())); +static elab_environment save_specialization_info(elab_environment const & env, name const & fn, spec_info const & si) { + return elab_environment(lean_add_specialization_info(env.to_obj_arg(), fn.to_obj_arg(), si.to_obj_arg())); } -static optional get_specialization_info(environment const & env, name const & fn) { +static optional get_specialization_info(elab_environment const & env, name const & fn) { return to_optional(lean_get_specialization_info(env.to_obj_arg(), fn.to_obj_arg())); } @@ -119,7 +119,7 @@ typedef buffer>> spec_info_buffer; Remark: we only create free variables for the header of each declaration. Then, we assume an argument of a recursive call is fixed iff it is a free variable (see `update_spec_info`). */ -static void update_info_buffer(environment const & env, expr e, name_set const & S, spec_info_buffer & info_buffer) { +static void update_info_buffer(elab_environment const & env, expr e, name_set const & S, spec_info_buffer & info_buffer) { while (true) { switch (e.kind()) { case expr_kind::Lambda: @@ -162,7 +162,7 @@ static void update_info_buffer(environment const & env, expr e, name_set const & } } -bool is_class(environment const & env, expr type) { +bool is_class(elab_environment const & env, expr type) { // This is a temporary hack. We do not unfold `type` here, but we should. We will fix it when we reimplement the compiler in Lean. while (is_pi(type)) { type = binding_body(type); @@ -171,7 +171,7 @@ bool is_class(environment const & env, expr type) { return is_constant(type) && is_class(env, const_name(type)); } -environment update_spec_info(environment const & env, comp_decls const & ds) { +elab_environment update_spec_info(elab_environment const & env, comp_decls const & ds) { name_set S; spec_info_buffer d_infos; name_generator ngen; @@ -237,7 +237,7 @@ environment update_spec_info(environment const & env, comp_decls const & ds) { update_info_buffer(env, code, S, d_infos); } /* Update extension */ - environment new_env = env; + elab_environment new_env = env; names mutual_decls = map2(ds, [&](comp_decl const & d) { return d.fst(); }); for (pair> const & info : d_infos) { name const & n = info.first; @@ -255,15 +255,16 @@ environment update_spec_info(environment const & env, comp_decls const & ds) { extern "C" object* lean_cache_specialization(object* env, object* e, object* fn); extern "C" object* lean_get_cached_specialization(object* env, object* e); -static environment cache_specialization(environment const & env, expr const & k, name const & fn) { - return environment(lean_cache_specialization(env.to_obj_arg(), k.to_obj_arg(), fn.to_obj_arg())); +static elab_environment cache_specialization(elab_environment const & env, expr const & k, name const & fn) { + return elab_environment(lean_cache_specialization(env.to_obj_arg(), k.to_obj_arg(), fn.to_obj_arg())); } -static optional get_cached_specialization(environment const & env, expr const & e) { +static optional get_cached_specialization(elab_environment const & env, expr const & e) { return to_optional(lean_get_cached_specialization(env.to_obj_arg(), e.to_obj_arg())); } class specialize_fn { + elab_environment m_env; type_checker::state m_st; csimp_cfg m_cfg; local_ctx m_lctx; @@ -274,7 +275,7 @@ class specialize_fn { unsigned m_next_idx{1}; name_set m_to_respecialize; - environment const & env() { return m_st.env(); } + elab_environment const & env() { return m_env; } name_generator & ngen() { return m_st.ngen(); } @@ -969,7 +970,8 @@ class specialize_fn { try { expr type = cheap_beta_reduce(type_checker(m_st).infer(code)); declaration aux_ax = mk_axiom(n, names(), type, true /* meta */); - m_st.env() = env().add(aux_ax, false); + m_env = m_env.add(aux_ax, false); + m_st.env() = m_env; } catch (exception &) { /* We may fail to infer the type of code, since it may be recursive This is a workaround. When we re-implement the compiler in Lean, @@ -1149,7 +1151,7 @@ class specialize_fn { for (comp_decl const & new_decl : new_decls) { m_to_respecialize.insert(new_decl.fst()); } - m_st.env() = update_spec_info(env(), new_decls); + m_env = update_spec_info(env(), new_decls); } /* It is only safe to cache when `m_params.size == 0`. See comment above. */ @@ -1162,7 +1164,7 @@ class specialize_fn { i++; } tout() << ">> key: " << trace_pp_expr(key) << "\n";); - m_st.env() = cache_specialization(env(), key, *new_fn_name); + m_env = cache_specialization(env(), key, *new_fn_name); } } expr r = mk_constant(*new_fn_name); @@ -1213,10 +1215,10 @@ class specialize_fn { } public: - specialize_fn(environment const & env, csimp_cfg const & cfg): - m_st(env), m_cfg(cfg), m_at("_at"), m_spec("_spec") {} + specialize_fn(elab_environment const & env, csimp_cfg const & cfg): + m_env(env), m_st(env), m_cfg(cfg), m_at("_at"), m_spec("_spec") {} - pair operator()(comp_decl const & d) { + pair operator()(comp_decl const & d) { m_base_name = d.fst(); lean_trace(name({"compiler", "specialize"}), tout() << "INPUT: " << d.fst() << "\n" << trace_pp_expr(d.snd()) << "\n";); expr new_v = visit(d.snd()); @@ -1225,11 +1227,11 @@ class specialize_fn { } }; -pair specialize_core(environment const & env, comp_decl const & d, csimp_cfg const & cfg) { +pair specialize_core(elab_environment const & env, comp_decl const & d, csimp_cfg const & cfg) { return specialize_fn(env, cfg)(d); } -pair specialize(environment env, comp_decls const & ds, csimp_cfg const & cfg) { +pair specialize(elab_environment env, comp_decls const & ds, csimp_cfg const & cfg) { env = update_spec_info(env, ds); comp_decls r; for (comp_decl const & d : ds) { diff --git a/src/library/compiler/specialize.h b/src/library/compiler/specialize.h index a1651e39c967d..63061244d1a6e 100644 --- a/src/library/compiler/specialize.h +++ b/src/library/compiler/specialize.h @@ -5,11 +5,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "kernel/environment.h" +#include "library/elab_environment.h" #include "library/compiler/util.h" #include "library/compiler/csimp.h" namespace lean { -pair specialize(environment env, comp_decls const & ds, csimp_cfg const & cfg); +pair specialize(elab_environment env, comp_decls const & ds, csimp_cfg const & cfg); void initialize_specialize(); void finalize_specialize(); } diff --git a/src/library/compiler/struct_cases_on.cpp b/src/library/compiler/struct_cases_on.cpp index 50d26c8749939..9f28c17cc2f06 100644 --- a/src/library/compiler/struct_cases_on.cpp +++ b/src/library/compiler/struct_cases_on.cpp @@ -15,6 +15,7 @@ Author: Leonardo de Moura namespace lean { class struct_cases_on_fn { + elab_environment m_env; type_checker::state m_st; local_ctx m_lctx; name_set m_scrutinies; /* Set of variables `x` such that there is `casesOn x ...` in the context */ @@ -23,7 +24,7 @@ class struct_cases_on_fn { name m_fld{"_d"}; unsigned m_next_idx{1}; - environment const & env() { return m_st.env(); } + elab_environment const & env() { return m_env; } name_generator & ngen() { return m_st.ngen(); } @@ -203,8 +204,8 @@ class struct_cases_on_fn { } public: - struct_cases_on_fn(environment const & env): - m_st(env) { + struct_cases_on_fn(elab_environment const & env): + m_env(env), m_st(env) { } expr operator()(expr const & e) { @@ -212,7 +213,7 @@ class struct_cases_on_fn { } }; -expr struct_cases_on(environment const & env, expr const & e) { +expr struct_cases_on(elab_environment const & env, expr const & e) { return struct_cases_on_fn(env)(e); } } diff --git a/src/library/compiler/struct_cases_on.h b/src/library/compiler/struct_cases_on.h index 5b534d95e34b3..de18defb53ece 100644 --- a/src/library/compiler/struct_cases_on.h +++ b/src/library/compiler/struct_cases_on.h @@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "kernel/environment.h" +#include "library/elab_environment.h" namespace lean { /* Insert `S.casesOn` applications for a structure `S` when @@ -50,5 +50,5 @@ namespace lean { The missing definitional equalities is problematic. For example, the whole algebraic hierarchy in Lean relies on them. */ -expr struct_cases_on(environment const & env, expr const & e); +expr struct_cases_on(elab_environment const & env, expr const & e); } diff --git a/src/library/compiler/util.cpp b/src/library/compiler/util.cpp index 96f8ed4c4da7d..5d6fa1e37476a 100644 --- a/src/library/compiler/util.cpp +++ b/src/library/compiler/util.cpp @@ -94,13 +94,13 @@ extern "C" uint8 lean_has_inline_if_reduce_attribute(object* env, object* n); extern "C" uint8 lean_has_macro_inline_attribute(object* env, object* n); extern "C" uint8 lean_has_noinline_attribute(object* env, object* n); -bool has_inline_attribute(environment const & env, name const & n) { return lean_has_inline_attribute(env.to_obj_arg(), n.to_obj_arg()); } -bool has_inline_if_reduce_attribute(environment const & env, name const & n) { return lean_has_inline_if_reduce_attribute(env.to_obj_arg(), n.to_obj_arg()); } -bool has_macro_inline_attribute(environment const & env, name const & n) { return lean_has_macro_inline_attribute(env.to_obj_arg(), n.to_obj_arg()); } -bool has_noinline_attribute(environment const & env, name const & n) { return lean_has_noinline_attribute(env.to_obj_arg(), n.to_obj_arg()); } +bool has_inline_attribute(elab_environment const & env, name const & n) { return lean_has_inline_attribute(env.to_obj_arg(), n.to_obj_arg()); } +bool has_inline_if_reduce_attribute(elab_environment const & env, name const & n) { return lean_has_inline_if_reduce_attribute(env.to_obj_arg(), n.to_obj_arg()); } +bool has_macro_inline_attribute(elab_environment const & env, name const & n) { return lean_has_macro_inline_attribute(env.to_obj_arg(), n.to_obj_arg()); } +bool has_noinline_attribute(elab_environment const & env, name const & n) { return lean_has_noinline_attribute(env.to_obj_arg(), n.to_obj_arg()); } extern "C" uint8 lean_has_never_extract_attribute(object* env, object *n); -bool has_never_extract_attribute(environment const & env, name const & n) { return lean_has_never_extract_attribute(env.to_obj_arg(), n.to_obj_arg()); } +bool has_never_extract_attribute(elab_environment const & env, name const & n) { return lean_has_never_extract_attribute(env.to_obj_arg(), n.to_obj_arg()); } bool is_lcnf_atom(expr const & e) { switch (e.kind()) { @@ -126,8 +126,8 @@ expr elim_trivial_let_decls(expr const & e) { } struct unfold_macro_defs_fn : public replace_visitor { - environment const & m_env; - unfold_macro_defs_fn(environment const & env):m_env(env) {} + elab_environment const & m_env; + unfold_macro_defs_fn(elab_environment const & env):m_env(env) {} bool should_macro_inline(name const & n) { @@ -175,15 +175,15 @@ struct unfold_macro_defs_fn : public replace_visitor { } }; -expr unfold_macro_defs(environment const & env, expr const & e) { +expr unfold_macro_defs(elab_environment const & env, expr const & e) { return unfold_macro_defs_fn(env)(e); } -bool is_cases_on_recursor(environment const & env, name const & n) { +bool is_cases_on_recursor(elab_environment const & env, name const & n) { return ::lean::is_aux_recursor(env, n) && n.get_string() == g_cases_on; } -unsigned get_cases_on_arity(environment const & env, name const & c, bool before_erasure) { +unsigned get_cases_on_arity(elab_environment const & env, name const & c, bool before_erasure) { lean_assert(is_cases_on_recursor(env, c)); inductive_val I_val = get_cases_on_inductive_val(env, c); unsigned nminors = I_val.get_ncnstrs(); @@ -196,7 +196,7 @@ unsigned get_cases_on_arity(environment const & env, name const & c, bool before } } -unsigned get_cases_on_major_idx(environment const & env, name const & c, bool before_erasure) { +unsigned get_cases_on_major_idx(elab_environment const & env, name const & c, bool before_erasure) { if (before_erasure) { inductive_val I_val = get_cases_on_inductive_val(env, c); return I_val.get_nparams() + 1 /* motive */ + I_val.get_nindices(); @@ -205,14 +205,14 @@ unsigned get_cases_on_major_idx(environment const & env, name const & c, bool be } } -expr get_cases_on_app_major(environment const & env, expr const & c, bool before_erasure) { +expr get_cases_on_app_major(elab_environment const & env, expr const & c, bool before_erasure) { lean_assert(is_cases_on_app(env, c)); buffer args; expr const & fn = get_app_args(c, args); return args[get_cases_on_major_idx(env, const_name(fn), before_erasure)]; } -pair get_cases_on_minors_range(environment const & env, name const & c, bool before_erasure) { +pair get_cases_on_minors_range(elab_environment const & env, name const & c, bool before_erasure) { inductive_val I_val = get_cases_on_inductive_val(env, c); unsigned nminors = I_val.get_ncnstrs(); if (before_erasure) { @@ -294,7 +294,7 @@ void sort_fvars(local_ctx const & lctx, buffer & fvars) { }); } -unsigned get_lcnf_size(environment const & env, expr e) { +unsigned get_lcnf_size(elab_environment const & env, expr e) { unsigned r = 0; switch (e.kind()) { case expr_kind::BVar: case expr_kind::MVar: @@ -558,16 +558,16 @@ expr mk_runtime_type(type_checker::state & st, local_ctx const & lctx, expr e) { } } -environment register_stage1_decl(environment const & env, name const & n, names const & ls, expr const & t, expr const & v) { +elab_environment register_stage1_decl(elab_environment const & env, name const & n, names const & ls, expr const & t, expr const & v) { declaration aux_decl = mk_definition(mk_cstage1_name(n), ls, t, v, reducibility_hints::mk_opaque(), definition_safety::unsafe); return env.add(aux_decl, false); } -bool is_stage2_decl(environment const & env, name const & n) { +bool is_stage2_decl(elab_environment const & env, name const & n) { return static_cast(env.find(mk_cstage2_name(n))); } -environment register_stage2_decl(environment const & env, name const & n, expr const & t, expr const & v) { +elab_environment register_stage2_decl(elab_environment const & env, name const & n, expr const & t, expr const & v) { declaration aux_decl = mk_definition(mk_cstage2_name(n), names(), t, v, reducibility_hints::mk_opaque(), definition_safety::unsafe); return env.add(aux_decl, false); @@ -608,10 +608,11 @@ we can get an irrelevant `ty`. We disabled this validator since we will delete the code generator written in C++. */ class lcnf_valid_let_decls_fn { + elab_environment m_env; type_checker::state m_st; local_ctx m_lctx; - environment const & env() const { return m_st.env(); } + elab_environment const & env() const { return m_env; } name_generator & ngen() { return m_st.ngen(); } @@ -675,19 +676,19 @@ class lcnf_valid_let_decls_fn { } public: - lcnf_valid_let_decls_fn(environment const & env, local_ctx const & lctx): - m_st(env), m_lctx(lctx) {} + lcnf_valid_let_decls_fn(elab_environment const & env, local_ctx const & lctx): + m_env(env), m_st(env), m_lctx(lctx) {} optional operator()(expr const & e) { return visit(e); } }; -optional lcnf_valid_let_decls(environment const & env, expr const & e) { +optional lcnf_valid_let_decls(elab_environment const & env, expr const & e) { return lcnf_valid_let_decls_fn(env, local_ctx())(e); } -bool lcnf_check_let_decls(environment const & env, comp_decl const & d) { +bool lcnf_check_let_decls(elab_environment const & env, comp_decl const & d) { if (optional v = lcnf_valid_let_decls(env, d.snd())) { tout() << "LCNF violation at " << d.fst() << "\n" << *v << "\n"; return false; @@ -696,7 +697,7 @@ bool lcnf_check_let_decls(environment const & env, comp_decl const & d) { } } -bool lcnf_check_let_decls(environment const & env, comp_decls const & ds) { +bool lcnf_check_let_decls(elab_environment const & env, comp_decls const & ds) { for (comp_decl const & d : ds) { if (!lcnf_check_let_decls(env, d)) return false; @@ -771,12 +772,12 @@ expr lcnf_eta_expand(type_checker::state & st, local_ctx lctx, expr e) { } } -bool is_quot_primitive_app(environment const & env, expr const & e) { +bool is_quot_primitive_app(elab_environment const & env, expr const & e) { expr const & f = get_app_fn(e); return is_constant(f) && is_quot_primitive(env, const_name(f)); } -bool must_be_eta_expanded(environment const & env, expr const & e) { +bool must_be_eta_expanded(elab_environment const & env, expr const & e) { return is_constructor_app(env, e) || is_proj(e) || diff --git a/src/library/compiler/util.h b/src/library/compiler/util.h index bb7e45788403a..49a3844e38f09 100644 --- a/src/library/compiler/util.h +++ b/src/library/compiler/util.h @@ -12,6 +12,7 @@ Author: Leonardo de Moura #include "kernel/type_checker.h" #include "library/constants.h" #include "library/util.h" +#include "library/elab_environment.h" namespace lean { /* Return the `some(n)` if `I` is the name of an inductive datatype that contains only constructors with 0-arguments, @@ -35,19 +36,19 @@ bool is_lcnf_atom(expr const & e); expr elim_trivial_let_decls(expr const & e); -bool has_inline_attribute(environment const & env, name const & n); -bool has_noinline_attribute(environment const & env, name const & n); -bool has_inline_if_reduce_attribute(environment const & env, name const & n); -bool has_never_extract_attribute(environment const & env, name const & n); +bool has_inline_attribute(elab_environment const & env, name const & n); +bool has_noinline_attribute(elab_environment const & env, name const & n); +bool has_inline_if_reduce_attribute(elab_environment const & env, name const & n); +bool has_never_extract_attribute(elab_environment const & env, name const & n); -expr unfold_macro_defs(environment const & env, expr const & e); +expr unfold_macro_defs(elab_environment const & env, expr const & e); /* Return true if the given argument is mdata relevant to the compiler Remark: we currently don't keep any metadata in the compiler. */ inline bool is_lc_mdata(expr const &) { return false; } -bool is_cases_on_recursor(environment const & env, name const & n); +bool is_cases_on_recursor(elab_environment const & env, name const & n); /* We defined the "arity" of a cases_on application as the sum: ``` number of inductive parameters + @@ -57,30 +58,30 @@ bool is_cases_on_recursor(environment const & env, name const & n); number of constructors // cases_on has a minor premise for each constructor ``` \pre is_cases_on_recursor(env, c) */ -unsigned get_cases_on_arity(environment const & env, name const & c, bool before_erasure = true); +unsigned get_cases_on_arity(elab_environment const & env, name const & c, bool before_erasure = true); /* Return the `inductive_val` for the cases_on constant `c`. */ -inline inductive_val get_cases_on_inductive_val(environment const & env, name const & c) { +inline inductive_val get_cases_on_inductive_val(elab_environment const & env, name const & c) { lean_assert(is_cases_on_recursor(env, c)); return env.get(c.get_prefix()).to_inductive_val(); } -inline inductive_val get_cases_on_inductive_val(environment const & env, expr const & c) { +inline inductive_val get_cases_on_inductive_val(elab_environment const & env, expr const & c) { lean_assert(is_constant(c)); return get_cases_on_inductive_val(env, const_name(c)); } -inline bool is_cases_on_app(environment const & env, expr const & e) { +inline bool is_cases_on_app(elab_environment const & env, expr const & e) { expr const & fn = get_app_fn(e); return is_constant(fn) && is_cases_on_recursor(env, const_name(fn)); } /* Return the major premise of a cases_on-application. \pre is_cases_on_app(env, c) */ -expr get_cases_on_app_major(environment const & env, expr const & c, bool before_erasure = true); -unsigned get_cases_on_major_idx(environment const & env, name const & c, bool before_erasure = true); +expr get_cases_on_app_major(elab_environment const & env, expr const & c, bool before_erasure = true); +unsigned get_cases_on_major_idx(elab_environment const & env, name const & c, bool before_erasure = true); /* Return the pair `(b, e)` such that `i in [b, e)` is argument `i` in a `c` cases_on application is a minor premise. \pre is_cases_on_recursor(env, c) */ -pair get_cases_on_minors_range(environment const & env, name const & c, bool before_erasure = true); +pair get_cases_on_minors_range(elab_environment const & env, name const & c, bool before_erasure = true); -inline bool is_quot_primitive(environment const & env, name const & n) { +inline bool is_quot_primitive(elab_environment const & env, name const & n) { optional info = env.find(n); return info && info->is_quot(); } @@ -119,7 +120,7 @@ expr replace_fvar(expr const & e, expr const & fvar, expr const & new_term); void sort_fvars(local_ctx const & lctx, buffer & fvars); /* Return the "code" size for `e` */ -unsigned get_lcnf_size(environment const & env, expr e); +unsigned get_lcnf_size(elab_environment const & env, expr e); // ======================================= // Auxiliary expressions for erasure. @@ -165,9 +166,9 @@ void collect_used(expr const & e, name_hash_set & S); /* Return true iff `e` contains a free variable in `s` */ bool depends_on(expr const & e, name_hash_set const & s); -bool is_stage2_decl(environment const & env, name const & n); -environment register_stage1_decl(environment const & env, name const & n, names const & ls, expr const & t, expr const & v); -environment register_stage2_decl(environment const & env, name const & n, expr const & t, expr const & v); +bool is_stage2_decl(elab_environment const & env, name const & n); +elab_environment register_stage1_decl(elab_environment const & env, name const & n, names const & ls, expr const & t, expr const & v); +elab_environment register_stage2_decl(elab_environment const & env, name const & n, expr const & t, expr const & v); /* Return `some n` iff `e` is of the forms `expr.lit (literal.nat n)` or `uint*.of_nat (expr.lit (literal.nat n))` */ optional get_num_lit_ext(expr const & e); @@ -181,8 +182,8 @@ optional is_fix_core(name const & c); Remark: this function assumes universe levels have already been erased. */ optional mk_enf_fix_core(unsigned n); -bool lcnf_check_let_decls(environment const & env, comp_decl const & d); -bool lcnf_check_let_decls(environment const & env, comp_decls const & ds); +bool lcnf_check_let_decls(elab_environment const & env, comp_decl const & d); +bool lcnf_check_let_decls(elab_environment const & env, comp_decls const & ds); // ======================================= /* Similar to `type_checker::eta_expand`, but preserves LCNF */ @@ -200,11 +201,11 @@ optional is_enum_type(environment const & env, expr const & type); extern "C" uint8 lean_is_matcher(object* env, object* n); -inline bool is_matcher(environment const & env, name const & n) { +inline bool is_matcher(elab_environment const & env, name const & n) { return lean_is_matcher(env.to_obj_arg(), n.to_obj_arg()); } -inline bool is_matcher_app(environment const & env, expr const & e) { +inline bool is_matcher_app(elab_environment const & env, expr const & e) { expr const & f = get_app_fn(e); return is_constant(f) && is_matcher(env, const_name(f)); } @@ -213,7 +214,7 @@ inline bool is_matcher_app(environment const & env, expr const & e) { Return true if the given expression must be in eta-expanded form during compilation. Example: constructors, `casesOn` applications must always be in eta-expanded form. */ -bool must_be_eta_expanded(environment const & env, expr const & e); +bool must_be_eta_expanded(elab_environment const & env, expr const & e); void initialize_compiler_util(); void finalize_compiler_util(); diff --git a/src/library/constructions/no_confusion.cpp b/src/library/constructions/no_confusion.cpp index 6710b0b0dd79c..8a3470c4d4db1 100644 --- a/src/library/constructions/no_confusion.cpp +++ b/src/library/constructions/no_confusion.cpp @@ -6,7 +6,7 @@ Author: Leonardo de Moura */ #include "runtime/sstream.h" #include "kernel/kernel_exception.h" -#include "kernel/environment.h" +#include "library/elab_environment.h" #include "kernel/instantiate.h" #include "kernel/abstract.h" #include "kernel/type_checker.h" @@ -22,7 +22,7 @@ static void throw_corrupted(name const & n) { throw exception(sstream() << "error in '" << g_no_confusion << "' generation, '" << n << "' inductive datatype declaration is corrupted"); } -static declaration mk_no_confusion_type(environment const & env, name const & n) { +static declaration mk_no_confusion_type(elab_environment const & env, name const & n) { constant_info ind_info = env.get(n); inductive_val ind_val = ind_info.to_inductive_val(); local_ctx lctx; @@ -122,10 +122,10 @@ static declaration mk_no_confusion_type(environment const & env, name const & n) } extern "C" LEAN_EXPORT object * lean_mk_no_confusion_type(object * env, object * n) { - return catch_kernel_exceptions([&]() { return mk_no_confusion_type(environment(env), name(n, true)); }); + return catch_kernel_exceptions([&]() { return mk_no_confusion_type(elab_environment(env), name(n, true)); }); } -declaration mk_no_confusion(environment const & env, name const & n) { +declaration mk_no_confusion(elab_environment const & env, name const & n) { local_ctx lctx; name_generator ngen = mk_constructions_name_generator(); constant_info ind_info = env.get(n); @@ -229,6 +229,6 @@ declaration mk_no_confusion(environment const & env, name const & n) { } extern "C" LEAN_EXPORT object * lean_mk_no_confusion(object * env, object * n) { - return catch_kernel_exceptions([&]() { return mk_no_confusion(environment(env), name(n, true)); }); + return catch_kernel_exceptions([&]() { return mk_no_confusion(elab_environment(env), name(n, true)); }); } } diff --git a/src/library/constructions/no_confusion.h b/src/library/constructions/no_confusion.h index b15317c90a24f..951959c7fb026 100644 --- a/src/library/constructions/no_confusion.h +++ b/src/library/constructions/no_confusion.h @@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "kernel/environment.h" +#include "library/elab_environment.h" namespace lean { /** \brief Given an inductive datatype \c n (which is not a proposition) in \c env, @@ -15,7 +15,7 @@ namespace lean { If the environment has an impredicative Prop, it also assumes heq is defined. If the environment does not have an impredicative Prop, then it also assumes lift is defined. */ -declaration mk_no_confusion_type(environment const & env, name const & n); +declaration mk_no_confusion_type(elab_environment const & env, name const & n); /** \brief Given an inductive datatype \c n (which is not a proposition) in \c env, returns the declaration for n.no_confusion. @@ -24,5 +24,5 @@ declaration mk_no_confusion_type(environment const & env, name const & n); If the environment has an impredicative Prop, it also assumes heq is defined. If the environment does not have an impredicative Prop, then it also assumes lift is defined. */ -declaration mk_no_confusion(environment const & env, name const & n); +declaration mk_no_confusion(elab_environment const & env, name const & n); } diff --git a/src/library/constructions/projection.cpp b/src/library/constructions/projection.cpp index a234c172fdb36..0e40d4b6ce050 100644 --- a/src/library/constructions/projection.cpp +++ b/src/library/constructions/projection.cpp @@ -30,7 +30,7 @@ static bool is_prop(expr type) { return is_sort(type) && is_zero(sort_level(type)); } -environment mk_projections(environment const & env, name const & n, buffer const & proj_names, bool inst_implicit) { +elab_environment mk_projections(elab_environment const & env, name const & n, buffer const & proj_names, bool inst_implicit) { local_ctx lctx; name_generator ngen = mk_constructions_name_generator(); constant_info ind_info = env.get(n); @@ -82,7 +82,7 @@ environment mk_projections(environment const & env, name const & n, buffer it = instantiate(binding_body(it), local); } unsigned i = 0; - environment new_env = env; + elab_environment new_env = env; for (name const & proj_name : proj_names) { if (!is_pi(cnstr_type)) throw exception(sstream() << "generating projection '" << proj_name << "', '" @@ -126,14 +126,14 @@ environment mk_projections(environment const & env, name const & n, buffer extern "C" LEAN_EXPORT object * lean_mk_projections(object * env, object * struct_name, object * proj_infos, uint8 inst_implicit) { - environment new_env(env); + elab_environment new_env(env); name n(struct_name); list_ref ps(proj_infos); buffer proj_names; for (auto p : ps) { proj_names.push_back(p); } - return catch_kernel_exceptions([&]() { return mk_projections(new_env, n, proj_names, inst_implicit != 0); }); + return catch_kernel_exceptions([&]() { return mk_projections(new_env, n, proj_names, inst_implicit != 0); }); } void initialize_def_projection() { diff --git a/src/library/elab_environment.cpp b/src/library/elab_environment.cpp new file mode 100644 index 0000000000000..537169f4ec512 --- /dev/null +++ b/src/library/elab_environment.cpp @@ -0,0 +1,74 @@ +/* +Copyright (c) 2024 Lean FRO. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Authors: Leonardo de Moura, Sebastian Ullrich +*/ +#include "runtime/interrupt.h" +#include "kernel/type_checker.h" +#include "kernel/kernel_exception.h" +#include "library/elab_environment.h" +#include "library/compiler/ir_interpreter.h" + +namespace lean { +/* updateBaseAfterKernelAdd (env : Environment) (added : Declaration) (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. + + 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); + +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())); +} + +extern "C" LEAN_EXPORT object * lean_elab_add_decl(object * env, size_t max_heartbeat, object * decl, + object * opt_cancel_tk) { + scope_max_heartbeat s(max_heartbeat); + scope_cancel_tk s2(is_scalar(opt_cancel_tk) ? nullptr : cnstr_get(opt_cancel_tk, 0)); + return catch_kernel_exceptions([&]() { + return elab_environment(env).add(declaration(decl, true)); + }); +} + +extern "C" LEAN_EXPORT object * lean_elab_add_decl_without_checking(object * env, object * decl) { + return catch_kernel_exceptions([&]() { + return elab_environment(env).add(declaration(decl, true), false); + }); +} + +extern "C" obj_res lean_elab_environment_to_kernel_env(obj_arg); +environment elab_environment::to_kernel_env() const { + return environment(lean_elab_environment_to_kernel_env(to_obj_arg())); +} + +extern "C" obj_res lean_display_stats(obj_arg env, obj_arg w); +void elab_environment::display_stats() const { + dec_ref(lean_display_stats(to_obj_arg(), io_mk_world())); +} + +extern "C" LEAN_EXPORT lean_object * lean_kernel_is_def_eq(lean_object * obj_env, lean_object * lctx, lean_object * a, lean_object * b) { + elab_environment env(obj_env); + return catch_kernel_exceptions([&]() { + return lean_box(type_checker(env.to_kernel_env(), local_ctx(lctx)).is_def_eq(expr(a), expr(b))); + }); +} + +extern "C" LEAN_EXPORT lean_object * lean_kernel_whnf(lean_object * obj_env, lean_object * lctx, lean_object * a) { + elab_environment env(obj_env); + return catch_kernel_exceptions([&]() { + return type_checker(env.to_kernel_env(), local_ctx(lctx)).whnf(expr(a)).steal(); + }); +} + +extern "C" LEAN_EXPORT lean_object * lean_kernel_check(lean_object * obj_env, lean_object * lctx, lean_object * a) { + elab_environment env(obj_env); + return catch_kernel_exceptions([&]() { + return type_checker(env.to_kernel_env(), local_ctx(lctx)).check(expr(a)).steal(); + }); +} +} diff --git a/src/library/elab_environment.h b/src/library/elab_environment.h new file mode 100644 index 0000000000000..db21ccf13b493 --- /dev/null +++ b/src/library/elab_environment.h @@ -0,0 +1,43 @@ +/* +Copyright (c) 2024 Lean FRO. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Authors: Leonardo de Moura, Sebastian Ullrich +*/ +#pragma once +#include "kernel/environment.h" + +namespace lean { +/* Wrapper for `Lean.Environment` */ +class LEAN_EXPORT elab_environment : public object_ref { +public: + elab_environment(elab_environment const & other):object_ref(other) {} + elab_environment(elab_environment && other):object_ref(other) {} + explicit elab_environment(b_obj_arg o, bool b):object_ref(o, b) {} + explicit elab_environment(obj_arg o):object_ref(o) {} + ~elab_environment() {} + + elab_environment & operator=(elab_environment const & other) { object_ref::operator=(other); return *this; } + elab_environment & operator=(elab_environment && other) { object_ref::operator=(other); return *this; } + + /** \brief Return information for the constant with name \c n (if it is defined in this environment). */ + optional find(name const & n) const { return to_kernel_env().find(n); }; + + /** \brief Return information for the constant with name \c n. Throws and exception if constant declaration does not exist in this environment. */ + constant_info get(name const & n) const { return to_kernel_env().get(n); }; + + /** \brief Extends the current environment with the given declaration */ + elab_environment add(declaration const & d, bool check = true) const; + + /** \brief Pointer equality */ + friend bool is_eqp(elab_environment const & e1, elab_environment const & e2) { + return e1.raw() == e2.raw(); + } + + void display_stats() const; + + environment to_kernel_env() const; + + operator environment() const { return to_kernel_env(); } +}; +} diff --git a/src/library/module.cpp b/src/library/module.cpp index dad1df4649065..91d65d22db0c7 100644 --- a/src/library/module.cpp +++ b/src/library/module.cpp @@ -245,7 +245,7 @@ extern "C" LEAN_EXPORT object * lean_read_module_data(object * fname, object *) def writeModule (env : Environment) (fname : String) : IO Unit := */ extern "C" object * lean_write_module(object * env, object * fname, object *); -void write_module(environment const & env, std::string const & olean_fn) { +void write_module(elab_environment const & env, std::string const & olean_fn) { consume_io_result(lean_write_module(env.to_obj_arg(), mk_string(olean_fn), io_mk_world())); } } diff --git a/src/library/module.h b/src/library/module.h index ae6e508c0d827..cbf1618347257 100644 --- a/src/library/module.h +++ b/src/library/module.h @@ -10,9 +10,9 @@ Authors: Leonardo de Moura, Gabriel Ebner, Sebastian Ullrich #include #include #include "runtime/optional.h" -#include "kernel/environment.h" +#include "library/elab_environment.h" namespace lean { /** \brief Store module using \c env. */ -LEAN_EXPORT void write_module(environment const & env, std::string const & olean_fn); +LEAN_EXPORT void write_module(elab_environment const & env, std::string const & olean_fn); } diff --git a/src/library/projection.cpp b/src/library/projection.cpp index 62a2319022dde..909b385ad0c2f 100644 --- a/src/library/projection.cpp +++ b/src/library/projection.cpp @@ -25,11 +25,11 @@ bool projection_info::is_inst_implicit() const { return lean_projection_info_fro extern "C" object* lean_add_projection_info(object* env, object* p, object* ctor, object* nparams, object* i, uint8 fromClass); extern "C" object* lean_get_projection_info(object* env, object* p); -environment save_projection_info(environment const & env, name const & p, name const & mk, unsigned nparams, unsigned i, bool inst_implicit) { - return environment(lean_add_projection_info(env.to_obj_arg(), p.to_obj_arg(), mk.to_obj_arg(), mk_nat_obj(nparams), mk_nat_obj(i), inst_implicit)); +elab_environment save_projection_info(elab_environment const & env, name const & p, name const & mk, unsigned nparams, unsigned i, bool inst_implicit) { + return elab_environment(lean_add_projection_info(env.to_obj_arg(), p.to_obj_arg(), mk.to_obj_arg(), mk_nat_obj(nparams), mk_nat_obj(i), inst_implicit)); } -optional get_projection_info(environment const & env, name const & p) { +optional get_projection_info(elab_environment const & env, name const & p) { return to_optional(lean_get_projection_info(env.to_obj_arg(), p.to_obj_arg())); } } diff --git a/src/library/projection.h b/src/library/projection.h index 3ade6827e63c2..89e88d5004476 100644 --- a/src/library/projection.h +++ b/src/library/projection.h @@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "kernel/environment.h" +#include "library/elab_environment.h" namespace lean { /** \brief Auxiliary information attached to projections. This information @@ -37,20 +37,20 @@ class projection_info : public object_ref { bool is_inst_implicit() const; }; -/** \brief Mark \c p as a projection in the given environment and store that +/** \brief Mark \c p as a projection in the given elab_environment and store that \c mk is the constructor associated with it, \c nparams is the number of parameters, and \c i says that \c p is the i-th projection. */ -environment save_projection_info(environment const & env, name const & p, name const & mk, unsigned nparams, unsigned i, +elab_environment save_projection_info(elab_environment const & env, name const & p, name const & mk, unsigned nparams, unsigned i, bool inst_implicit); -/** \brief If \c p is a projection in the given environment, then return the information +/** \brief If \c p is a projection in the given elab_environment, then return the information associated with it (constructor, number of parameters, and index). If \c p is not a projection, then return nullptr. */ -optional get_projection_info(environment const & env, name const & p); +optional get_projection_info(elab_environment const & env, name const & p); -inline bool is_projection(environment const & env, name const & n) { +inline bool is_projection(elab_environment const & env, name const & n) { return static_cast(get_projection_info(env, n)); } } diff --git a/src/library/reducible.cpp b/src/library/reducible.cpp index 16a0aad85f1a3..a2f009f6406cc 100644 --- a/src/library/reducible.cpp +++ b/src/library/reducible.cpp @@ -5,20 +5,20 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include -#include "kernel/environment.h" +#include "library/elab_environment.h" #include "library/reducible.h" namespace lean { extern "C" uint8 lean_get_reducibility_status(object * env, object * n); extern "C" object * lean_set_reducibility_status(object * env, object * n, uint8 s); -environment set_reducible(environment const & env, name const & n, reducible_status s, bool persistent) { +elab_environment set_reducible(elab_environment const & env, name const & n, reducible_status s, bool persistent) { if (!persistent) throw exception("reducibility attributes must be persistent for now, we will relax this restriction in a near future"); - return environment(lean_set_reducibility_status(env.to_obj_arg(), n.to_obj_arg(), static_cast(s))); + return elab_environment(lean_set_reducibility_status(env.to_obj_arg(), n.to_obj_arg(), static_cast(s))); } -reducible_status get_reducible_status(environment const & env, name const & n) { +reducible_status get_reducible_status(elab_environment const & env, name const & n) { return static_cast(lean_get_reducibility_status(env.to_obj_arg(), n.to_obj_arg())); } } diff --git a/src/library/reducible.h b/src/library/reducible.h index c58e210426cec..f1fa9e44d2a79 100644 --- a/src/library/reducible.h +++ b/src/library/reducible.h @@ -7,6 +7,7 @@ Author: Leonardo de Moura #pragma once #include #include "library/util.h" +#include "library/elab_environment.h" namespace lean { enum class reducible_status { Reducible, Semireducible, Irreducible }; @@ -20,10 +21,10 @@ enum class reducible_status { Reducible, Semireducible, Irreducible }; "Reducible" definitions can be freely unfolded by automation (i.e., elaborator, simplifier, etc). We should view it as a hint to automation. */ -environment set_reducible(environment const & env, name const & n, reducible_status s, bool persistent); +elab_environment set_reducible(elab_environment const & env, name const & n, reducible_status s, bool persistent); -reducible_status get_reducible_status(environment const & env, name const & n); +reducible_status get_reducible_status(elab_environment const & env, name const & n); -inline bool is_reducible(environment const & env, name const & n) { return get_reducible_status(env, n) == reducible_status::Reducible; } -inline bool is_semireducible(environment const & env, name const & n) { return get_reducible_status(env, n) == reducible_status::Semireducible; } +inline bool is_reducible(elab_environment const & env, name const & n) { return get_reducible_status(env, n) == reducible_status::Reducible; } +inline bool is_semireducible(elab_environment const & env, name const & n) { return get_reducible_status(env, n) == reducible_status::Semireducible; } } diff --git a/src/util/shell.cpp b/src/util/shell.cpp index 02027d0265f93..ebf192d59d6ad 100644 --- a/src/util/shell.cpp +++ b/src/util/shell.cpp @@ -28,7 +28,7 @@ Author: Leonardo de Moura #include "util/io.h" #include "util/options.h" #include "util/option_declarations.h" -#include "kernel/environment.h" +#include "library/elab_environment.h" #include "kernel/kernel_exception.h" #include "kernel/trace.h" #include "library/formatter.h" @@ -332,7 +332,7 @@ extern "C" object * lean_run_frontend( uint8_t json_output, object * w ); -pair_ref run_new_frontend( +pair_ref run_new_frontend( std::string const & input, options const & opts, std::string const & file_name, name const & main_module_name, @@ -344,7 +344,7 @@ pair_ref run_new_frontend( if (ilean_file_name) { oilean_file_name = mk_option_some(mk_string(*ilean_file_name)); } - return get_io_result>(lean_run_frontend( + return get_io_result>(lean_run_frontend( mk_string(input), opts.to_obj_arg(), mk_string(file_name), @@ -401,7 +401,7 @@ void print_imports_json(array_ref const & fnames) { } extern "C" object* lean_environment_free_regions(object * env, object * w); -void environment_free_regions(environment && env) { +void environment_free_regions(elab_environment && env) { consume_io_result(lean_environment_free_regions(env.steal(), io_mk_world())); } } @@ -633,7 +633,6 @@ extern "C" LEAN_EXPORT int lean_main(int argc, char ** argv) { report_profiling_time("initialization", init_time); } - environment env(trust_lvl); scoped_task_manager scope_task_man(num_threads); optional main_module_name; @@ -705,8 +704,8 @@ extern "C" LEAN_EXPORT int lean_main(int argc, char ** argv) { if (!main_module_name) main_module_name = name("_stdin"); - pair_ref r = run_new_frontend(contents, opts, mod_fn, *main_module_name, trust_lvl, ilean_fn, json_output); - env = r.fst(); + pair_ref r = run_new_frontend(contents, opts, mod_fn, *main_module_name, trust_lvl, ilean_fn, json_output); + elab_environment env = r.fst(); bool ok = unbox(r.snd().raw()); if (stats) { diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h index b647d85f376c7..a3d118fd9f112 100644 --- a/stage0/src/stdlib_flags.h +++ b/stage0/src/stdlib_flags.h @@ -9,7 +9,7 @@ options get_default_options() { opts = opts.update({"debug", "proofAsSorry"}, false); // switch to `true` for ABI-breaking changes affecting meta code; // see also next option! - opts = opts.update({"interpreter", "prefer_native"}, false); + opts = opts.update({"interpreter", "prefer_native"}, true); // switch to `false` when enabling `prefer_native` should also affect use // of built-in parsers in quotations; this is usually the case, but setting // both to `true` may be necessary for handling non-builtin parsers with diff --git a/tests/lean/ctor_layout.lean.expected.out b/tests/lean/ctor_layout.lean.expected.out index f15ad0f679bc6..bc23bfd4c04a6 100644 --- a/tests/lean/ctor_layout.lean.expected.out +++ b/tests/lean/ctor_layout.lean.expected.out @@ -4,7 +4,6 @@ scalar#1@0:u8 obj@2 --- scalar#4@0:u32 -scalar#1@4:u8 obj@0 obj@1 obj@2 diff --git a/tests/lean/prvCtor.lean b/tests/lean/prvCtor.lean index 28c1bcb2a0f82..72483faf8e747 100644 --- a/tests/lean/prvCtor.lean +++ b/tests/lean/prvCtor.lean @@ -22,7 +22,7 @@ open Lean in open Lean in #eval id (α := CoreM Unit) do -- this implementation is no longer allowed because of a private constructor - modifyEnv fun env => { env with header.mainModule := `foo } + modifyEnv fun env => { env with base.header.mainModule := `foo } #check a -- Error diff --git a/tests/lean/prvCtor.lean.expected.out b/tests/lean/prvCtor.lean.expected.out index 3b61b9f6033b1..3e75c12ab6484 100644 --- a/tests/lean/prvCtor.lean.expected.out +++ b/tests/lean/prvCtor.lean.expected.out @@ -1,5 +1,5 @@ a : Nat -prvCtor.lean:25:23-25:61: error: invalid {...} notation, constructor for `Lean.Environment` is marked as private +prvCtor.lean:25:23-25:66: error: invalid {...} notation, constructor for `Lean.Environment` is marked as private prvCtor.lean:27:7-27:8: error: unknown identifier 'a' prvCtor.lean:29:25-29:27: error: overloaded, errors failed to synthesize diff --git a/tests/lean/run/structure.lean b/tests/lean/run/structure.lean index fc2432600519a..e2780ded05f95 100644 --- a/tests/lean/run/structure.lean +++ b/tests/lean/run/structure.lean @@ -24,7 +24,7 @@ inductive D | mk (x y z : Nat) : D /-- -info: #[const2ModIdx, constants, extensions, extraConstNames, header] +info: #[constants, quotInit, diagnostics, const2ModIdx, extensions, extraConstNames, header] #[toS2, toS1, x, y, z, toS3, w, s] (some [S4.toS2, S2.toS1]) #[S2, S3] @@ -33,7 +33,7 @@ info: #[const2ModIdx, constants, extensions, extraConstNames, header] #guard_msgs in #eval show CoreM Unit from do let env ← getEnv - IO.println (getStructureFields env `Lean.Environment) + IO.println (getStructureFields env ``Kernel.Environment) check $ getStructureFields env `S4 == #[`toS2, `toS3, `s] check $ getStructureFields env `S1 == #[`x, `y] check $ isSubobjectField? env `S4 `toS2 == some `S2