feat: unbox inductives in the compiler

src/Init/Prelude.lean

@@ -535,6 +535,8 @@ structure PProd (α : Sort u) (β : Sort v) where
   /-- The second element of a pair. -/
   snd : β
 
+attribute [unbox] PProd
+
 /--
 A product type in which both `α` and `β` are in the same universe.
 
@@ -546,6 +548,8 @@ structure MProd (α β : Type u) where
   /-- The second element of a pair. -/
   snd : β
 
+attribute [unbox] MProd
+
 /--
 `And a b`, or `a ∧ b`, is the conjunction of propositions. It can be
 constructed and destructed like a pair: if `ha : a` and `hb : b` then

src/Init/System/ST.lean

@@ -65,6 +65,7 @@ instance {σ : Type} : MonadAttach (ST σ) where
   CanReturn x a := ∃ s s', x s = ⟨a, s'⟩
   attach x s := match h : x s with | ⟨a, s'⟩ => ⟨⟨a, s, s', h⟩, s'⟩
 
+@[unbox]
 inductive EST.Out (ε : Type) (σ : Type) (α : Type) where
   | ok : α → Void σ → EST.Out ε σ α
   | error : ε → Void σ → EST.Out ε σ α

src/Lean/Compiler/IR.lean

@@ -48,18 +48,22 @@ def compile (decls : Array Decl) : CompilerM (Array Decl) := do
   let mut decls := decls
   decls := decls.map Decl.pushProj
   logDecls `push_proj decls
+  decls := prepareBoxParams (← getEnv) decls
+  logDecls `box_params decls
+  decls ← explicitBoxing decls
+  logDecls `boxing decls
   if compiler.reuse.get (← getOptions) then
     decls := decls.map (Decl.insertResetReuse (← getEnv))
     logDecls `reset_reuse decls
-  decls := decls.map Decl.elimDead
-  logDecls `elim_dead decls
   decls := decls.map Decl.simpCase
   logDecls `simp_case decls
   decls := decls.map Decl.normalizeIds
+  decls := decls.map Decl.elimDead
+  logDecls `elim_dead decls
   decls ← inferBorrow decls
   logDecls `borrow decls
-  decls ← explicitBoxing decls
-  logDecls `boxing decls
+  decls := ExplicitBoxing.addBoxedVersions (← getEnv) decls
+  logDecls `boxed_versions decls
   decls ← explicitRC decls
   logDecls `rc decls
   if compiler.reuse.get (← getOptions) then
@@ -70,6 +74,10 @@ def compile (decls : Array Decl) : CompilerM (Array Decl) := do
   decls ← updateSorryDep decls
   logDecls `result decls
   checkDecls decls
+  if (← getOptions).getBool (tracePrefixOptionName ++ `struct_rc) ||
+      (← getOptions).getBool tracePrefixOptionName then
+    let decls2 := decls.map StructRC.visitDecl
+    log (LogEntry.step `struct_rc decls2)
   decls ← toposortDecls decls
   addDecls decls
   inferMeta decls

src/Lean/Compiler/IR/Borrow.lean

@@ -231,7 +231,7 @@ def ownArgsIfParam (xs : Array Arg) : M Unit := do
     | .var x => if ctx.paramSet.contains x.idx then ownVar x
     | .erased => pure ()
 
-def collectExpr (z : VarId) (e : Expr) : M Unit := do
+def collectExpr (z : VarId) (t : IRType) (e : Expr) : M Unit := do
   match e with
   | .reset _ x =>
     ownVar z
@@ -243,9 +243,10 @@ def collectExpr (z : VarId) (e : Expr) : M Unit := do
   | .ctor _ xs =>
     ownVar z
     ownArgsIfParam xs
-  | .proj _ x =>
+  | .proj _ _ x | .unbox x =>
     if (← isOwned x) then ownVar z
-    if (← isOwned z) then ownVar x
+    if (← isOwned z) then
+      unless t.isScalar do ownVar x
   | .fap g xs =>
     let ps ← getParamInfo (.decl g)
     ownVar z
@@ -257,7 +258,10 @@ def collectExpr (z : VarId) (e : Expr) : M Unit := do
   | .pap _ xs =>
     ownVar z
     ownArgs xs
-  | _ => pure ()
+  | .box _ x =>
+    ownVar z
+    ownVar x
+  | .lit _ | .isShared _ | .sproj .. | .uproj .. => pure ()
 
 def preserveTailCall (x : VarId) (v : Expr) (b : FnBody) : M Unit := do
   let ctx ← read
@@ -279,9 +283,9 @@ partial def collectFnBody (b : FnBody) : M Unit := do
     let ctx ← read
     updateParamMap (.jp ctx.currFn j)
     collectFnBody b
-  | .vdecl x _ v b =>
+  | .vdecl x t v b =>
     collectFnBody b
-    collectExpr x v
+    collectExpr x t v
     preserveTailCall x v b
   | .jmp j ys =>
     let ctx ← read