max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor: remove unused addBoxedVersion variants (#9289)

Browse source
This commit is contained in:
Cameron Zwarich 2025-07-09 16:44:18 -07:00 • committed by GitHub
parent d3a4bb29a7
commit 3e37eef9ea
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 0 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
src/Lean/Compiler/IR.lean
View file

@ -73,23 +73,6 @@ def compile (env : Environment) (opts : Options) (decls : Array Decl) : Log × (
| EStateM.Result.ok _ s => (s.log, Except.ok s.env)
| EStateM.Result.error msg s => (s.log, Except.error msg)
def addBoxedVersionAux (decl : Decl) : CompilerM Unit := do
let env ← getEnv
if !ExplicitBoxing.requiresBoxedVersion env decl then
pure ()
else
let decl := ExplicitBoxing.mkBoxedVersion decl
let decls : Array Decl := #[decl]
let decls ← explicitRC decls
decls.forM fun decl => modifyEnv fun env => addDeclAux env decl
pure ()
-- Remark: we are ignoring the `Log` here. This should be fine.
def addBoxedVersion (env : Environment) (decl : Decl) : Except String Environment :=
match (addBoxedVersionAux decl Options.empty).run { env := env } with
| EStateM.Result.ok _ s => Except.ok s.env
| EStateM.Result.error msg _ => Except.error msg
builtin_initialize
registerTraceClass `compiler.ir
registerTraceClass `compiler.ir.init (inherited := true)