void

Author: hargoniX

src/Lean/Compiler/IR/Basic.lean

@@ -54,6 +54,9 @@ instance : ToString JoinPointId := ⟨fun a => "block_" ++ toString a.idx⟩
 
    - `tobject` an `object` or a `tagged` pointer
 
+   - `void` is used to identify uses of the state token from `BaseIO` which do no longer need
+     to be passed around etc. at this point in the pipeline.
+
    - `struct` and `union` are used to return small values (e.g., `Option`, `Prod`, `Except`)
       on the stack.
 
@@ -80,7 +83,7 @@ inductive IRType where
   | struct (leanTypeName : Option Name) (types : Array IRType) : IRType
   | union (leanTypeName : Name) (types : Array IRType) : IRType
   -- TODO: Move this upwards after a stage0 update.
-  | tagged
+  | tagged | void
   deriving Inhabited, BEq, Repr
 
 namespace IRType
@@ -99,6 +102,7 @@ def isObj : IRType → Bool
   | object  => true
   | tagged  => true
   | tobject => true
+  | void    => true
   | _       => false
 
 def isPossibleRef : IRType → Bool
@@ -115,7 +119,7 @@ def isErased : IRType → Bool
 
 def boxed : IRType → IRType
   | object | float | float32 => object
-  | tagged | uint8 | uint16 => tagged
+  | void | tagged | uint8 | uint16 => tagged
   | _ => tobject
 
 end IRType

src/Lean/Compiler/IR/EmitC.lean

@@ -69,6 +69,7 @@ def toCType : IRType → String
   | IRType.tagged     => "lean_object*"
   | IRType.tobject    => "lean_object*"
   | IRType.erased     => "lean_object*"
+  | IRType.void       => "lean_object*"
   | IRType.struct _ _ => panic! "not implemented yet"
   | IRType.union _ _  => panic! "not implemented yet"
 

src/Lean/Compiler/IR/EmitLLVM.lean

@@ -329,6 +329,7 @@ def toLLVMType (t : IRType) : M llvmctx (LLVM.LLVMType llvmctx) := do
   | IRType.tagged     => do LLVM.pointerType (← LLVM.i8Type llvmctx)
   | IRType.tobject    => do LLVM.pointerType (← LLVM.i8Type llvmctx)
   | IRType.erased     => do LLVM.pointerType (← LLVM.i8Type llvmctx)
+  | .void             => do LLVM.pointerType (← LLVM.i8Type llvmctx)
   | IRType.struct _ _ => panic! "not implemented yet"
   | IRType.union _ _  => panic! "not implemented yet"
 

src/Lean/Compiler/IR/Format.lean

@@ -66,6 +66,7 @@ private partial def formatIRType : IRType → Format
   | IRType.uint64       => "u64"
   | IRType.usize        => "usize"
   | IRType.erased       => "◾"
+  | IRType.void         => "void"
   | IRType.object       => "obj"
   | IRType.tagged       => "tagged"
   | IRType.tobject      => "tobj"

src/Lean/Compiler/IR/ToIR.lean

@@ -89,6 +89,7 @@ def lowerArg (a : LCNF.Arg) : M Arg := do
 inductive TranslatedProj where
   | expr (e : Expr)
   | erased
+  | void
   deriving Inhabited
 
 def lowerProj (base : VarId) (ctorInfo : CtorInfo) (field : CtorFieldInfo)
@@ -98,6 +99,7 @@ def lowerProj (base : VarId) (ctorInfo : CtorInfo) (field : CtorFieldInfo)
   | .usize i => ⟨.expr (.uproj i base), .usize⟩
   | .scalar _ offset irType => ⟨.expr (.sproj (ctorInfo.size + ctorInfo.usize) offset base), irType⟩
   | .erased => ⟨.erased, .erased⟩
+  | .void => ⟨.void, .void⟩
 
 def lowerParam (p : LCNF.Param) : M Param := do
   let x ← bindVar p.fvarId
@@ -148,6 +150,7 @@ partial def lowerLet (decl : LCNF.LetDecl) (k : LCNF.Code) : M FnBody := do
       | .erased =>
         bindErased decl.fvarId
         lowerCode k
+      | .void => unreachable!
     | .erased =>
       bindErased decl.fvarId
       lowerCode k
@@ -178,7 +181,7 @@ partial def lowerLet (decl : LCNF.LetDecl) (k : LCNF.Code) : M FnBody := do
           match fields[i] with
           | .object .. =>
             result := result.push irArgs[i]!
-          | .usize .. | .scalar .. | .erased => pure ()
+          | .usize .. | .scalar .. | .erased | .void => pure ()
         pure result
       let objVar ← bindVar decl.fvarId
       let rec lowerNonObjectFields (_ : Unit) : M FnBody :=
@@ -192,7 +195,7 @@ partial def lowerLet (decl : LCNF.LetDecl) (k : LCNF.Code) : M FnBody := do
             | .scalar _ offset argType =>
               let k ← loop (i + 1)
               return .sset objVar (ctorInfo.size + ctorInfo.usize) offset varId argType k
-            | .object .. | .erased => loop (i + 1)
+            | .object .. | .erased | .void => loop (i + 1)
           | some .erased => loop (i + 1)
           | none => lowerCode k
         loop 0
@@ -270,6 +273,12 @@ partial def lowerAlt (discr : VarId) (a : LCNF.Alt) : M Alt := do
           | .erased =>
             bindErased param.fvarId
             loop (i + 1)
+          | .void =>
+            let info ← getCtorLayout ``PUnit.unit
+            return .vdecl (← bindVar param.fvarId)
+                          .void
+                          (.ctor info.ctorInfo #[])
+                          (← loop (i + 1))
         | none, none => lowerCode code
         | _, _ => panic! "mismatched fields and params"
       loop 0

src/Lean/Compiler/IR/ToIRType.lean

@@ -54,7 +54,7 @@ where fillCache : CoreM IRType := do
     -- `Int` is specified as an inductive type with two constructors that have relevant arguments,
     -- but it has the same runtime representation as `Nat` and thus needs to be special-cased here.
     | ``Int => return .tobject
-    | ``lcRealWorld => return .tagged
+    | ``lcRealWorld => return .void
     | _ =>
       let env ← Lean.getEnv
       let some (.inductInfo inductiveVal) := env.find? name | return .tobject
@@ -110,12 +110,14 @@ inductive CtorFieldInfo where
   | object (i : Nat) (type : IRType)
   | usize  (i : Nat)
   | scalar (sz : Nat) (offset : Nat) (type : IRType)
+  | void
   deriving Inhabited
 
 namespace CtorFieldInfo
 
 def format : CtorFieldInfo → Format
   | erased => "◾"
+  | void => "void"
   | object i type => f!"obj@{i}:{type}"
   | usize i    => f!"usize@{i}"
   | scalar sz offset type => f!"scalar#{sz}@{offset}:{type}"
@@ -160,6 +162,7 @@ where fillCache := do
         pure <| .object i irFieldType
       | .usize => pure <| .usize 0
       | .erased => .pure <| .erased
+      | .void => .pure <| .void
       | .uint8 =>
         has1BScalar := true
         .pure <| .scalar 1 0 .uint8
@@ -186,7 +189,7 @@ where fillCache := do
       | .usize _ => do
         let i ← modifyGet fun nextIdx => (nextIdx, nextIdx + 1)
         return .usize i
-      | .object .. | .scalar .. | .erased => return field
+      | .object .. | .scalar .. | .erased | .void => return field
     let numUSize := nextIdx - numObjs
     let adjustScalarsForSize (fields : Array CtorFieldInfo) (size : Nat) (nextOffset : Nat)
         : Array CtorFieldInfo × Nat :=
@@ -198,7 +201,7 @@ where fillCache := do
             return .scalar sz offset type
           else
             return field
-        | .object .. | .usize _ | .erased => return field
+        | .object .. | .usize _ | .erased | .void => return field
     let mut nextOffset := 0
     if has8BScalar then
       ⟨fields, nextOffset⟩ := adjustScalarsForSize fields 8 nextOffset