diff --git a/src/Lean/Compiler/LCNF/ElimDeadBranches.lean b/src/Lean/Compiler/LCNF/ElimDeadBranches.lean index 82c070a1fa..703ebb16dc 100644 --- a/src/Lean/Compiler/LCNF/ElimDeadBranches.lean +++ b/src/Lean/Compiler/LCNF/ElimDeadBranches.lean @@ -642,7 +642,7 @@ where eraseCode alt.getCode return alt.updateCode <| .unreach typ | .default body => return alt.updateCode (← go body) - return code.updateCases! cs.resultType cs.discr (← cs.alts.mapM <| processAlt cs.resultType) + return code.updateAlts! (← cs.alts.mapMonoM <| processAlt cs.resultType) | .jmp .. | .return .. | .unreach .. => return code end UnreachableBranches diff --git a/src/Lean/Compiler/LCNF/ExplicitBoxing.lean b/src/Lean/Compiler/LCNF/ExplicitBoxing.lean index 0133e1977f..c5aa689c25 100644 --- a/src/Lean/Compiler/LCNF/ExplicitBoxing.lean +++ b/src/Lean/Compiler/LCNF/ExplicitBoxing.lean @@ -311,7 +311,15 @@ where | .pap .. => return object | .uproj .. => return usize | .erased => return tagged - | .fvar .. | .lit .. | .sproj .. | .oproj .. | .reset .. | .ctor .. | .reuse .. => + | .lit (.nat n) => + if n ≤ maxSmallNat then + return tagged + else + return currentType + | .lit (.str ..) => + return object + | .ctor i _ => return i.type + | .fvar .. | .lit .. | .sproj .. | .oproj .. | .reset .. | .reuse .. => return currentType | .box .. | .unbox .. => unreachable! diff --git a/src/Lean/Compiler/LCNF/ExtractClosed.lean b/src/Lean/Compiler/LCNF/ExtractClosed.lean index 3ccd4a26ae..3aa07df7c6 100644 --- a/src/Lean/Compiler/LCNF/ExtractClosed.lean +++ b/src/Lean/Compiler/LCNF/ExtractClosed.lean @@ -145,7 +145,7 @@ partial def visitCode (code : Code .pure) : M (Code .pure) := do let decl ← decl.updateValue (← visitCode decl.value) return code.updateFun! decl (← visitCode k) | .cases cases => - let alts ← cases.alts.mapM (fun alt => do return alt.updateCode (← visitCode alt.getCode)) + let alts ← cases.alts.mapMonoM (fun alt => do return alt.updateCode (← visitCode alt.getCode)) return code.updateAlts! alts | .jmp .. | .return _ | .unreach .. => return code diff --git a/src/Lean/Compiler/LCNF/FVarUtil.lean b/src/Lean/Compiler/LCNF/FVarUtil.lean index 74247fa8be..dab681e5e1 100644 --- a/src/Lean/Compiler/LCNF/FVarUtil.lean +++ b/src/Lean/Compiler/LCNF/FVarUtil.lean @@ -132,7 +132,7 @@ partial def Code.mapFVarM [MonadLiftT CompilerM m] [Monad m] (f : FVarId → m F let decl ← decl.update (← Expr.mapFVarM f decl.type) params (← mapFVarM f decl.value) return Code.updateFun! c decl (← mapFVarM f k) | .cases cs => - return Code.updateCases! c (← Expr.mapFVarM f cs.resultType) (← f cs.discr) (← cs.alts.mapM (·.mapCodeM (mapFVarM f))) + return Code.updateCases! c (← Expr.mapFVarM f cs.resultType) (← f cs.discr) (← cs.alts.mapMonoM (·.mapCodeM (mapFVarM f))) | .jmp fn args => return Code.updateJmp! c (← f fn) (← args.mapM (Arg.mapFVarM f)) | .return var => diff --git a/src/Lean/Compiler/LCNF/FloatLetIn.lean b/src/Lean/Compiler/LCNF/FloatLetIn.lean index 0a4d5ebeb3..013948b5a8 100644 --- a/src/Lean/Compiler/LCNF/FloatLetIn.lean +++ b/src/Lean/Compiler/LCNF/FloatLetIn.lean @@ -320,7 +320,7 @@ where } let (_, res) ← goCases |>.run base let remainders := res.newArms[Decision.dont]! - let newAlts ← cs.alts.mapM fun alt => do + let newAlts ← cs.alts.mapMonoM fun alt => do let decision := Decision.ofAlt alt let newCode := res.newArms[decision]! trace[Compiler.floatLetIn] "Size of code that was pushed into arm: {repr decision} {newCode.length}" diff --git a/src/Lean/Compiler/LCNF/InferBorrow.lean b/src/Lean/Compiler/LCNF/InferBorrow.lean index 9e7ff0b5be..b28836a1e8 100644 --- a/src/Lean/Compiler/LCNF/InferBorrow.lean +++ b/src/Lean/Compiler/LCNF/InferBorrow.lean @@ -118,7 +118,7 @@ where let ps ← updateParams decl.params map[ParamMap.Key.jp declName decl.fvarId]! let decl ← decl.update decl.type ps (← go declName decl.value) return code.updateFun! decl (← go declName k) - | .cases cs => return code.updateAlts! <| ← cs.alts.mapM (·.mapCodeM (go declName)) + | .cases cs => return code.updateAlts! <| ← cs.alts.mapMonoM (·.mapCodeM (go declName)) | .let _ k | .uset _ _ _ k _ | .sset _ _ _ _ _ k _ => return code.updateCont! (← go declName k) | .return .. | .jmp .. | .unreach .. => return code | .inc .. | .dec .. => unreachable! diff --git a/src/Lean/Compiler/LCNF/JoinPoints.lean b/src/Lean/Compiler/LCNF/JoinPoints.lean index 3b0ad560a9..4e7b71069e 100644 --- a/src/Lean/Compiler/LCNF/JoinPoints.lean +++ b/src/Lean/Compiler/LCNF/JoinPoints.lean @@ -240,7 +240,7 @@ where let newDecl ← decl.updateValue (← go decl.value) return Code.updateFun! code newDecl (← go k) | .cases cs => - return Code.updateCases! code cs.resultType cs.discr (← cs.alts.mapM (·.mapCodeM go)) + return Code.updateCases! code cs.resultType cs.discr (← cs.alts.mapMonoM (·.mapCodeM go)) | .jmp .. | .return .. | .unreach .. => return code @@ -452,7 +452,7 @@ where let visitor := fun alt => do withNewAltScope alt do alt.mapCodeM go - let alts ← cs.alts.mapM visitor + let alts ← cs.alts.mapMonoM visitor return Code.updateCases! code cs.resultType discr alts | .jmp fn args => let mut newArgs ← args.mapM (mapFVarM goFVar) @@ -624,7 +624,7 @@ where let decl ← decl.updateValue (← goReduce decl.value) return Code.updateFun! code decl (← goReduce k) | .cases cs => - let alts ← cs.alts.mapM (·.mapCodeM goReduce) + let alts ← cs.alts.mapMonoM (·.mapCodeM goReduce) return Code.updateCases! code cs.resultType cs.discr alts | .return .. | .unreach .. => return code diff --git a/src/Lean/Compiler/LCNF/PushProj.lean b/src/Lean/Compiler/LCNF/PushProj.lean index 1eed19bdaa..e131220296 100644 --- a/src/Lean/Compiler/LCNF/PushProj.lean +++ b/src/Lean/Compiler/LCNF/PushProj.lean @@ -78,7 +78,7 @@ partial def Cases.pushProjs (c : Cases .impure) (decls : Array (CodeDecl .impure let altsUsed := c.alts.map (·.getCode.collectUsed) let ctxUsed := ({} : FVarIdHashSet) |>.insert c.discr let (bs, alts) ← go decls c.alts altsUsed #[] ctxUsed - let alts ← alts.mapM (·.mapCodeM Code.pushProj) + let alts ← alts.mapMonoM (·.mapCodeM Code.pushProj) let c := c.updateAlts alts return attachCodeDecls bs (.cases c) where diff --git a/src/Lean/Compiler/LCNF/ResetReuse.lean b/src/Lean/Compiler/LCNF/ResetReuse.lean index 562fe46d96..1f870928c9 100644 --- a/src/Lean/Compiler/LCNF/ResetReuse.lean +++ b/src/Lean/Compiler/LCNF/ResetReuse.lean @@ -204,7 +204,7 @@ where | .cases cs => if ← c.isFVarLiveIn x then /- If `x` is live in `c`, we recursively process each branch. -/ - let alts ← cs.alts.mapM (·.mapCodeM (D x info)) + let alts ← cs.alts.mapMonoM (·.mapCodeM (D x info)) return (c.updateAlts! alts, true) else return (c, false) diff --git a/src/Lean/Compiler/LCNF/StructProjCases.lean b/src/Lean/Compiler/LCNF/StructProjCases.lean index 2190b8b06e..bdbe651a2c 100644 --- a/src/Lean/Compiler/LCNF/StructProjCases.lean +++ b/src/Lean/Compiler/LCNF/StructProjCases.lean @@ -101,7 +101,7 @@ partial def visitCode (code : Code .pure) : M (Code .pure) := do -- a variable above while also destructuring an array doesn't work. return code.updateCases! cases.resultType discr #[.alt ctorName params k] else - let alts ← cases.alts.mapM (visitAlt ·) + let alts ← cases.alts.mapMonoM (visitAlt ·) return code.updateCases! cases.resultType discr alts | .return fvarId => return code.updateReturn! (← remapFVar fvarId) | .unreach .. => return code diff --git a/src/Lean/Compiler/LCNF/ToLCNF.lean b/src/Lean/Compiler/LCNF/ToLCNF.lean index 8171dcf45b..fb63bc8cad 100644 --- a/src/Lean/Compiler/LCNF/ToLCNF.lean +++ b/src/Lean/Compiler/LCNF/ToLCNF.lean @@ -74,7 +74,7 @@ partial def bindCases (jpDecl : FunDecl .pure) (cases : Cases .pure) : CompilerM return .jp jpDecl result where visitAlts (alts : Array (Alt .pure)) : BindCasesM (Array (Alt .pure)) := - alts.mapM fun alt => return alt.updateCode (← go alt.getCode) + alts.mapMonoM (·.mapCodeM go) findFun? (f : FVarId) : CompilerM (Option (FunDecl .pure)) := do if let some funDecl ← findFunDecl? (pu := .pure) f then