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

refactor: remove questionable defaults in Context structure (#9458)

Browse source
This commit is contained in:
Cameron Zwarich 2025-07-21 15:16:14 -07:00 • committed by GitHub
parent f3e1795175
commit 9a34f6bc95
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 3 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/Lean/Compiler/IR/Boxing.lean
View file

@ -85,9 +85,9 @@ def eqvTypes (t₁ t₂ : IRType) : Bool :=
(t₁.isScalar == t₂.isScalar) && (!t₁.isScalar || t₁ == t₂)
structure BoxingContext where
f : FunId := default
f : FunId
localCtx : LocalContext := {}
resultType : IRType := .erased
resultType : IRType
decls : Array Decl
env : Environment
@ -315,12 +315,11 @@ partial def visitFnBody : FnBody → M FnBody
pure other
def run (env : Environment) (decls : Array Decl) : Array Decl :=
let ctx : BoxingContext := { decls := decls, env := env }
let decls := decls.foldl (init := #[]) fun newDecls decl =>
match decl with
| .fdecl f xs resultType b _ =>
let nextIdx := decl.maxIndex + 1
let (b, s) := withParams xs (visitFnBody b) { ctx with f, resultType } |>.run { nextIdx }
let (b, s) := withParams xs (visitFnBody b) { f, resultType, decls, env } |>.run { nextIdx }
let newDecls := newDecls ++ s.auxDecls
let newDecl := decl.updateBody! b
let newDecl := newDecl.elimDead