From 9a34f6bc95e40a4a3491e22ef49b85d1008ebdc6 Mon Sep 17 00:00:00 2001 From: Cameron Zwarich Date: Mon, 21 Jul 2025 15:16:14 -0700 Subject: [PATCH] refactor: remove questionable defaults in Context structure (#9458) --- src/Lean/Compiler/IR/Boxing.lean | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/src/Lean/Compiler/IR/Boxing.lean b/src/Lean/Compiler/IR/Boxing.lean index 609053f5b3..338992c415 100644 --- a/src/Lean/Compiler/IR/Boxing.lean +++ b/src/Lean/Compiler/IR/Boxing.lean @@ -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