chore: use mutual inductives for data structures in the new compiler (#8332)

This PR changes the types `AltCore`, `FunDeclCore` and `CasesCore` used
in the IRs of the new compiler into the mutual inductives `Alt`,
`FunDecl` and `Cases`.

Author: Rob23oba

src/Lean/Compiler/IR/Basic.lean

@@ -245,9 +245,11 @@ structure Param where
 @[export lean_ir_mk_param]
 def mkParam (x : VarId) (borrow : Bool) (ty : IRType) : Param := ⟨x, borrow, ty⟩
 
-inductive AltCore (FnBody : Type) : Type where
-  | ctor (info : CtorInfo) (b : FnBody) : AltCore FnBody
-  | default (b : FnBody) : AltCore FnBody
+mutual
+
+inductive Alt where
+  | ctor (info : CtorInfo) (b : FnBody) : Alt
+  | default (b : FnBody) : Alt
 
 inductive FnBody where
   /-- `let x : ty := e; b` -/
@@ -271,12 +273,14 @@ inductive FnBody where
   | dec (x : VarId) (n : Nat) (c : Bool) (persistent : Bool) (b : FnBody)
   | del (x : VarId) (b : FnBody)
   | mdata (d : MData) (b : FnBody)
-  | case (tid : Name) (x : VarId) (xType : IRType) (cs : Array (AltCore FnBody))
+  | case (tid : Name) (x : VarId) (xType : IRType) (cs : Array Alt)
   | ret (x : Arg)
   /-- Jump to join point `j` -/
   | jmp (j : JoinPointId) (ys : Array Arg)
   | unreachable
 
+end
+
 instance : Inhabited FnBody := ⟨FnBody.unreachable⟩
 
 abbrev FnBody.nil := FnBody.unreachable
@@ -285,17 +289,13 @@ abbrev FnBody.nil := FnBody.unreachable
 @[export lean_ir_mk_jdecl] def mkJDecl (j : JoinPointId) (xs : Array Param) (v : FnBody) (b : FnBody) : FnBody := FnBody.jdecl j xs v b
 @[export lean_ir_mk_uset] def mkUSet (x : VarId) (i : Nat) (y : VarId) (b : FnBody) : FnBody := FnBody.uset x i y b
 @[export lean_ir_mk_sset] def mkSSet (x : VarId) (i : Nat) (offset : Nat) (y : VarId) (ty : IRType) (b : FnBody) : FnBody := FnBody.sset x i offset y ty b
-@[export lean_ir_mk_case] def mkCase (tid : Name) (x : VarId) (cs : Array (AltCore FnBody)) : FnBody :=
+@[export lean_ir_mk_case] def mkCase (tid : Name) (x : VarId) (cs : Array Alt) : FnBody :=
   -- Type field `xType` is set by `explicitBoxing` compiler pass.
   FnBody.case tid x IRType.object cs
 @[export lean_ir_mk_ret] def mkRet (x : Arg) : FnBody := FnBody.ret x
 @[export lean_ir_mk_jmp] def mkJmp (j : JoinPointId) (ys : Array Arg) : FnBody := FnBody.jmp j ys
 @[export lean_ir_mk_unreachable] def mkUnreachable : Unit → FnBody := fun _ => FnBody.unreachable
 
-abbrev Alt := AltCore FnBody
-@[match_pattern] abbrev Alt.ctor    := @AltCore.ctor FnBody
-@[match_pattern] abbrev Alt.default := @AltCore.default FnBody
-
 instance : Inhabited Alt := ⟨Alt.default default⟩
 
 def FnBody.isTerminal : FnBody → Bool
@@ -341,19 +341,19 @@ def FnBody.setBody : FnBody → FnBody → FnBody
   let c  := b.resetBody
   (c, b')
 
-def AltCore.body : Alt → FnBody
+def Alt.body : Alt → FnBody
   | Alt.ctor _ b  => b
   | Alt.default b => b
 
-def AltCore.setBody : Alt → FnBody → Alt
+def Alt.setBody : Alt → FnBody → Alt
   | Alt.ctor c _, b  => Alt.ctor c b
   | Alt.default _, b => Alt.default b
 
-@[inline] def AltCore.modifyBody (f : FnBody → FnBody) : AltCore FnBody → Alt
+@[inline] def Alt.modifyBody (f : FnBody → FnBody) : Alt → Alt
   | Alt.ctor c b  => Alt.ctor c (f b)
   | Alt.default b => Alt.default (f b)
 
-@[inline] def AltCore.mmodifyBody {m : Type → Type} [Monad m] (f : FnBody → m FnBody) : AltCore FnBody → m Alt
+@[inline] def Alt.mmodifyBody {m : Type → Type} [Monad m] (f : FnBody → m FnBody) : Alt → m Alt
   | Alt.ctor c b  => Alt.ctor c <$> f b
   | Alt.default b => Alt.default <$> f b
 

src/Lean/Compiler/IR/ToIR.lean

@@ -15,7 +15,7 @@ import Lean.Environment
 
 namespace Lean.IR
 
-open Lean.Compiler (LCNF.AltCore LCNF.Arg LCNF.Code LCNF.Decl LCNF.DeclValue LCNF.LCtx LCNF.LetDecl
+open Lean.Compiler (LCNF.Alt LCNF.Arg LCNF.Code LCNF.Decl LCNF.DeclValue LCNF.LCtx LCNF.LetDecl
                     LCNF.LetValue LCNF.LitValue LCNF.Param LCNF.getMonoDecl?)
 
 namespace ToIR
@@ -346,7 +346,7 @@ partial def lowerLet (decl : LCNF.LetDecl) (k : LCNF.Code) : M FnBody := do
     | some (.joinPoint ..) | none => panic! "unexpected value"
   | .erased => mkErased ()
 
-partial def lowerAlt (discr : VarId) (a : LCNF.AltCore LCNF.Code) : M (AltCore FnBody) := do
+partial def lowerAlt (discr : VarId) (a : LCNF.Alt) : M Alt := do
   match a with
   | .alt ctorName params code =>
     let ⟨ctorInfo, fields⟩ ← getCtorInfo ctorName

src/Lean/Compiler/LCNF/Basic.lean

@@ -33,11 +33,6 @@ structure Param where
 def Param.toExpr (p : Param) : Expr :=
   .fvar p.fvarId
 
-inductive AltCore (Code : Type) where
-  | alt (ctorName : Name) (params : Array Param) (code : Code)
-  | default (code : Code)
-  deriving Inhabited
-
 inductive LitValue where
   | natVal (val : Nat)
   | strVal (val : String)
@@ -136,42 +131,48 @@ structure LetDecl where
   value : LetValue
   deriving Inhabited, BEq
 
-structure FunDeclCore (Code : Type) where
+mutual
+
+inductive Alt where
+  | alt (ctorName : Name) (params : Array Param) (code : Code)
+  | default (code : Code)
+
+structure FunDecl where
   fvarId : FVarId
   binderName : Name
   params : Array Param
   type : Expr
   value : Code
-  deriving Inhabited
-
-def FunDeclCore.getArity (decl : FunDeclCore Code) : Nat :=
-  decl.params.size
 
-structure CasesCore (Code : Type) where
+structure Cases where
   typeName : Name
   resultType : Expr
   discr : FVarId
-  alts : Array (AltCore Code)
+  alts : Array Alt
   deriving Inhabited
 
 inductive Code where
   | let (decl : LetDecl) (k : Code)
-  | fun (decl : FunDeclCore Code) (k : Code)
-  | jp (decl : FunDeclCore Code) (k : Code)
+  | fun (decl : FunDecl) (k : Code)
+  | jp (decl : FunDecl) (k : Code)
   | jmp (fvarId : FVarId) (args : Array Arg)
-  | cases (cases : CasesCore Code)
+  | cases (cases : Cases)
   | return (fvarId : FVarId)
   | unreach (type : Expr)
   deriving Inhabited
 
-abbrev Alt := AltCore Code
-abbrev FunDecl := FunDeclCore Code
-abbrev Cases := CasesCore Code
+end
+
+deriving instance Inhabited for Alt
+deriving instance Inhabited for FunDecl
+
+def FunDecl.getArity (decl : FunDecl) : Nat :=
+  decl.params.size
 
 /--
 Return the constructor names that have an explicit (non-default) alternative.
 -/
-def CasesCore.getCtorNames (c : Cases) : NameSet :=
+def Cases.getCtorNames (c : Cases) : NameSet :=
   c.alts.foldl (init := {}) fun ctorNames alt =>
     match alt with
     | .default _ => ctorNames
@@ -241,15 +242,15 @@ instance : BEq Code where
 instance : BEq FunDecl where
   beq := FunDecl.beq
 
-def AltCore.getCode : Alt → Code
+def Alt.getCode : Alt → Code
   | .default k => k
   | .alt _ _ k => k
 
-def AltCore.getParams : Alt → Array Param
+def Alt.getParams : Alt → Array Param
   | .default _ => #[]
   | .alt _ ps _ => ps
 
-def AltCore.forCodeM [Monad m] (alt : Alt) (f : Code → m Unit) : m Unit := do
+def Alt.forCodeM [Monad m] (alt : Alt) (f : Code → m Unit) : m Unit := do
   match alt with
   | .default k => f k
   | .alt _ _ k => f k
@@ -259,14 +260,14 @@ private unsafe def updateAltCodeImp (alt : Alt) (k' : Code) : Alt :=
   | .default k => if ptrEq k k' then alt else .default k'
   | .alt ctorName ps k => if ptrEq k k' then alt else .alt ctorName ps k'
 
-@[implemented_by updateAltCodeImp] opaque AltCore.updateCode (alt : Alt) (c : Code) : Alt
+@[implemented_by updateAltCodeImp] opaque Alt.updateCode (alt : Alt) (c : Code) : Alt
 
 private unsafe def updateAltImp (alt : Alt) (ps' : Array Param) (k' : Code) : Alt :=
   match alt with
   | .alt ctorName ps k => if ptrEq k k' && ptrEq ps ps' then alt else .alt ctorName ps' k'
   | _ => unreachable!
 
-@[implemented_by updateAltImp] opaque AltCore.updateAlt! (alt : Alt) (ps' : Array Param) (k' : Code) : Alt
+@[implemented_by updateAltImp] opaque Alt.updateAlt! (alt : Alt) (ps' : Array Param) (k' : Code) : Alt
 
 @[inline] private unsafe def updateAltsImp (c : Code) (alts : Array Alt) : Code :=
   match c with
@@ -364,9 +365,9 @@ Low-level update `FunDecl` function. It does not update the local context.
 Consider using `FunDecl.update : LetDecl → Expr → Array Param → Code → CompilerM FunDecl` if you want the local context
 to be updated.
 -/
-@[implemented_by updateFunDeclCoreImp] opaque FunDeclCore.updateCore (decl: FunDecl) (type : Expr) (params : Array Param) (value : Code) : FunDecl
+@[implemented_by updateFunDeclCoreImp] opaque FunDecl.updateCore (decl : FunDecl) (type : Expr) (params : Array Param) (value : Code) : FunDecl
 
-def CasesCore.extractAlt! (cases : Cases) (ctorName : Name) : Alt × Cases :=
+def Cases.extractAlt! (cases : Cases) (ctorName : Name) : Alt × Cases :=
   let found i := (cases.alts[i], { cases with alts := cases.alts.eraseIdx i })
   if let some i := cases.alts.findFinIdx? fun | .alt ctorName' .. => ctorName == ctorName' | _ => false then
     found i
@@ -375,7 +376,7 @@ def CasesCore.extractAlt! (cases : Cases) (ctorName : Name) : Alt × Cases :=
   else
     unreachable!
 
-def AltCore.mapCodeM [Monad m] (alt : Alt) (f : Code → m Code) : m Alt := do
+def Alt.mapCodeM [Monad m] (alt : Alt) (f : Code → m Code) : m Alt := do
   return alt.updateCode (← f alt.getCode)
 
 def Code.isDecl : Code → Bool
@@ -678,7 +679,7 @@ private partial def collectParams (ps : Array Param) (s : FVarIdSet) : FVarIdSet
   ps.foldl (init := s) fun s p => collectType p.type s
 
 mutual
-partial def FunDeclCore.collectUsed (decl : FunDecl) (s : FVarIdSet := {}) : FVarIdSet :=
+partial def FunDecl.collectUsed (decl : FunDecl) (s : FVarIdSet := {}) : FVarIdSet :=
   decl.value.collectUsed <| collectParams decl.params <| collectType decl.type s
 
 partial def Code.collectUsed (code : Code) (s : FVarIdSet := {}) : FVarIdSet :=

src/Lean/Compiler/LCNF/Bind.lean

@@ -99,7 +99,7 @@ def isEtaExpandCandidateCore (type : Expr) (params : Array Param) : Bool :=
   let valueArity := params.size
   typeArity > valueArity
 
-abbrev FunDeclCore.isEtaExpandCandidate (decl : FunDecl) : Bool :=
+abbrev FunDecl.isEtaExpandCandidate (decl : FunDecl) : Bool :=
   isEtaExpandCandidateCore decl.type decl.params
 
 def etaExpandCore (type : Expr) (params : Array Param) (value : Code) : CompilerM (Array Param × Code) := do
@@ -118,7 +118,7 @@ def etaExpandCore? (type : Expr) (params : Array Param) (value : Code) : Compile
   else
     return none
 
-def FunDeclCore.etaExpand (decl : FunDecl) : CompilerM FunDecl := do
+def FunDecl.etaExpand (decl : FunDecl) : CompilerM FunDecl := do
   let some (params, value) ← etaExpandCore? decl.type decl.params decl.value | return decl
   decl.update decl.type params value
 

src/Lean/Compiler/LCNF/CompilerM.lean

@@ -395,20 +395,20 @@ private unsafe def updateLetDeclImp (decl : LetDecl) (type : Expr) (value : LetV
 def LetDecl.updateValue (decl : LetDecl) (value : LetValue) : CompilerM LetDecl :=
   decl.update decl.type value
 
-private unsafe def updateFunDeclImp (decl: FunDecl) (type : Expr) (params : Array Param) (value : Code) : CompilerM FunDecl := do
+private unsafe def updateFunDeclImp (decl : FunDecl) (type : Expr) (params : Array Param) (value : Code) : CompilerM FunDecl := do
   if ptrEq type decl.type && ptrEq params decl.params && ptrEq value decl.value then
     return decl
   else
     let decl := { decl with type, params, value }
     modifyLCtx fun lctx => lctx.addFunDecl decl
     return decl
 
-@[implemented_by updateFunDeclImp] opaque FunDeclCore.update (decl: FunDecl) (type : Expr) (params : Array Param) (value : Code) : CompilerM FunDecl
+@[implemented_by updateFunDeclImp] opaque FunDecl.update (decl : FunDecl) (type : Expr) (params : Array Param) (value : Code) : CompilerM FunDecl
 
-abbrev FunDeclCore.update' (decl : FunDecl) (type : Expr) (value : Code) : CompilerM FunDecl :=
+abbrev FunDecl.update' (decl : FunDecl) (type : Expr) (value : Code) : CompilerM FunDecl :=
   decl.update type decl.params value
 
-abbrev FunDeclCore.updateValue (decl : FunDecl) (value : Code) : CompilerM FunDecl :=
+abbrev FunDecl.updateValue (decl : FunDecl) (value : Code) : CompilerM FunDecl :=
   decl.update decl.type decl.params value
 
 @[inline] def normParam [MonadLiftT CompilerM m] [Monad m] [MonadFVarSubst m t] (p : Param) : m Param := do

src/Lean/Compiler/LCNF/InferType.lean

@@ -262,7 +262,7 @@ def Code.inferParamType (params : Array Param) (code : Code) : CompilerM Expr :=
   let xs := params.map fun p => .fvar p.fvarId
   InferType.mkForallFVars xs type |>.run {}
 
-def AltCore.inferType (alt : Alt) : CompilerM Expr :=
+def Alt.inferType (alt : Alt) : CompilerM Expr :=
   alt.getCode.inferType
 
 def mkAuxLetDecl (e : LetValue) (prefixName := `_x) : CompilerM LetDecl := do

src/Lean/Compiler/LCNF/Probing.lean

@@ -54,7 +54,7 @@ where
     | .fun decl k | .jp decl k =>
       go decl.value
       go k
-    | .cases (cases : CasesCore Code) => cases.alts.forM (go ·.getCode)
+    | .cases cs => cs.alts.forM (go ·.getCode)
     | .jmp .. | .return .. | .unreach .. => return ()
   start (decls : Array Decl) : StateRefT (Array LetValue) CompilerM Unit :=
     decls.forM (·.value.forCodeM go)

src/Lean/Compiler/LCNF/Renaming.lean

@@ -29,7 +29,7 @@ def LetDecl.applyRenaming (decl : LetDecl) (r : Renaming) : CompilerM LetDecl :=
     return decl
 
 mutual
-partial def FunDeclCore.applyRenaming (decl : FunDecl) (r : Renaming) : CompilerM FunDecl := do
+partial def FunDecl.applyRenaming (decl : FunDecl) (r : Renaming) : CompilerM FunDecl := do
   if let some binderName := r.find? decl.fvarId then
     let decl := { decl with binderName }
     modifyLCtx fun lctx => lctx.addFunDecl decl

src/Lean/Compiler/LCNF/ToExpr.lean

@@ -79,7 +79,7 @@ private def Arg.toExprM (arg : Arg) : ToExprM Expr :=
   return arg.toExpr.abstract' (← read) (← get)
 
 mutual
-partial def FunDeclCore.toExprM (decl : FunDecl) : ToExprM Expr :=
+partial def FunDecl.toExprM (decl : FunDecl) : ToExprM Expr :=
   withParams decl.params do mkLambdaM decl.params (← decl.value.toExprM)
 
 partial def Code.toExprM (code : Code) : ToExprM Expr := do
@@ -107,7 +107,7 @@ end
 def Code.toExpr (code : Code) (xs : Array FVarId := #[]) : Expr :=
   run' code.toExprM xs
 
-def FunDeclCore.toExpr (decl : FunDecl) (xs : Array FVarId := #[]) : Expr :=
+def FunDecl.toExpr (decl : FunDecl) (xs : Array FVarId := #[]) : Expr :=
   run' decl.toExprM xs
 
 end Lean.Compiler.LCNF

src/Lean/Compiler/LCNF/ToMono.lean

@@ -83,7 +83,7 @@ def LetDecl.toMono (decl : LetDecl) : ToMonoM LetDecl := do
 
 mutual
 
-partial def FunDeclCore.toMono (decl : FunDecl) : ToMonoM FunDecl := do
+partial def FunDecl.toMono (decl : FunDecl) : ToMonoM FunDecl := do
   let type ← toMonoType decl.type
   let params ← decl.params.mapM (·.toMono)
   let value ← decl.value.toMono