From 85560da3e484d08a507683e3c7d2a49e3790df95 Mon Sep 17 00:00:00 2001 From: Cameron Zwarich Date: Mon, 13 Jan 2025 10:51:06 -0800 Subject: [PATCH] chore: remove functions for compiling decls from Environment (#6600) This PR removes functions from compiling decls from Environment, and moves all users to functions on CoreM. This is required for supporting the new code generator, since its implementation uses CoreM. --- src/Lean/AddDecl.lean | 5 ----- src/Lean/Compiler/InitAttr.lean | 8 ++------ src/Lean/Compiler/Old.lean | 15 --------------- src/Lean/CoreM.lean | 7 +++++-- src/Lean/ParserCompiler.lean | 7 ++----- tests/lean/run/toExpr.lean | 21 +++++++++++---------- 6 files changed, 20 insertions(+), 43 deletions(-) diff --git a/src/Lean/AddDecl.lean b/src/Lean/AddDecl.lean index 128fb20a00..08386f4c9b 100644 --- a/src/Lean/AddDecl.lean +++ b/src/Lean/AddDecl.lean @@ -21,11 +21,6 @@ def Environment.addDecl (env : Environment) (opts : Options) (decl : Declaration 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 - let env ← addDecl env opts decl cancelTk? - compileDecl env opts decl - def addDecl (decl : Declaration) : CoreM Unit := do profileitM Exception "type checking" (← getOptions) do withTraceNode `Kernel (fun _ => return m!"typechecking declaration") do diff --git a/src/Lean/Compiler/InitAttr.lean b/src/Lean/Compiler/InitAttr.lean index 212e3c6de3..ce27e263d3 100644 --- a/src/Lean/Compiler/InitAttr.lean +++ b/src/Lean/Compiler/InitAttr.lean @@ -144,11 +144,7 @@ def declareBuiltin (forDecl : Name) (value : Expr) : CoreM Unit := do let type := mkApp (mkConst `IO) (mkConst `Unit) let decl := Declaration.defnDecl { name, levelParams := [], type, value, hints := ReducibilityHints.opaque, safety := DefinitionSafety.safe } - match (← getEnv).addAndCompile {} decl with - -- TODO: pretty print error - | Except.error e => do - let msg ← (e.toMessageData {}).toString - throwError "failed to emit registration code for builtin '{forDecl}': {msg}" - | Except.ok env => IO.ofExcept (setBuiltinInitAttr env name) >>= setEnv + addAndCompile decl + IO.ofExcept (setBuiltinInitAttr (← getEnv) name) >>= setEnv end Lean diff --git a/src/Lean/Compiler/Old.lean b/src/Lean/Compiler/Old.lean index 52908bc84e..66f79ad1a2 100644 --- a/src/Lean/Compiler/Old.lean +++ b/src/Lean/Compiler/Old.lean @@ -53,18 +53,3 @@ def isUnsafeRecName? : Name → Option Name | _ => none end Compiler - -namespace Environment - -/-- -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 - -/-- 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 := - compileDecls env opt (Compiler.getDeclNamesForCodeGen decl) - -end Environment diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean index f6d34ca804..d541bb1951 100644 --- a/src/Lean/CoreM.lean +++ b/src/Lean/CoreM.lean @@ -514,13 +514,16 @@ register_builtin_option compiler.enableNew : Bool := { @[extern "lean_lcnf_compile_decls"] opaque compileDeclsNew (declNames : List Name) : CoreM Unit +@[extern "lean_compile_decls"] +opaque compileDeclsOld (env : Environment) (opt : @& Options) (decls : @& List Name) : Except KernelException Environment + def compileDecl (decl : Declaration) : CoreM Unit := do let opts ← getOptions let decls := Compiler.getDeclNamesForCodeGen decl if compiler.enableNew.get opts then compileDeclsNew decls let res ← withTraceNode `compiler (fun _ => return m!"compiling old: {decls}") do - return (← getEnv).compileDecl opts decl + return compileDeclsOld (← getEnv) opts decls match res with | Except.ok env => setEnv env | Except.error (KernelException.other msg) => @@ -533,7 +536,7 @@ def compileDecls (decls : List Name) : CoreM Unit := do let opts ← getOptions if compiler.enableNew.get opts then compileDeclsNew decls - match (← getEnv).compileDecls opts decls with + match compileDeclsOld (← getEnv) opts decls with | Except.ok env => setEnv env | Except.error (KernelException.other msg) => throwError msg diff --git a/src/Lean/ParserCompiler.lean b/src/Lean/ParserCompiler.lean index 3d15ea6436..6cdc9ce46a 100644 --- a/src/Lean/ParserCompiler.lean +++ b/src/Lean/ParserCompiler.lean @@ -103,11 +103,8 @@ partial def compileParserExpr (e : Expr) : MetaM Expr := do name := c', levelParams := [] type := ty, value := value, hints := ReducibilityHints.opaque, safety := DefinitionSafety.safe } - let env ← getEnv - let env ← match env.addAndCompile {} decl with - | Except.ok env => pure env - | Except.error kex => do throwError (← (kex.toMessageData {}).toString) - setEnv <| ctx.combinatorAttr.setDeclFor env c c' + addAndCompile decl + modifyEnv (ctx.combinatorAttr.setDeclFor · c c') if cinfo.type.isConst then if let some kind ← parserNodeKind? cinfo.value! then -- If the parser is parameter-less and produces a node of kind `kind`, diff --git a/tests/lean/run/toExpr.lean b/tests/lean/run/toExpr.lean index e44c93603a..6131320902 100644 --- a/tests/lean/run/toExpr.lean +++ b/tests/lean/run/toExpr.lean @@ -14,16 +14,17 @@ let decl := Declaration.defnDecl { safety := DefinitionSafety.safe }; IO.println (toExpr a); -(match env.addAndCompile {} decl with -| Except.error _ => throwError "addDecl failed" -| Except.ok env => - match env.evalConst α {} auxName with - | Except.error ex => throwError ex - | Except.ok b => do - IO.println b; - unless a == b do - throwError "toExpr failed"; - pure ()) +let oldEnv ← getEnv; +addAndCompile decl; +let newEnv ← getEnv +setEnv oldEnv +match newEnv.evalConst α {} auxName with +| Except.error ex => throwError ex +| Except.ok b => do + IO.println b; + unless a == b do + throwError "toExpr failed"; + pure () #eval test #[(1, 2), (3, 4)] #eval test ['a', 'b', 'c']