chore: remove unused isTaggedPtr from IR.

This reduces the surface area of `unimplemented` in the LLVM backend,
and also removes dead code in the compiler.

src/Lean/Compiler/IR/Basic.lean

@@ -219,8 +219,6 @@ inductive Expr where
   | lit (v : LitVal)
   /-- Return `1 : uint8` Iff `RC(x) > 1` -/
   | isShared (x : VarId)
-  /-- Return `1 : uint8` Iff `x : tobject` is a tagged pointer (storing a scalar value). -/
-  | isTaggedPtr (x : VarId)
 
 @[export lean_ir_mk_ctor_expr]  def mkCtorExpr (n : Name) (cidx : Nat) (size : Nat) (usize : Nat) (ssize : Nat) (ys : Array Arg) : Expr :=
   Expr.ctor ⟨n, cidx, size, usize, ssize⟩ ys
@@ -550,7 +548,6 @@ def Expr.alphaEqv (ρ : IndexRenaming) : Expr → Expr → Bool
   | Expr.unbox x₁,           Expr.unbox x₂           => aeqv ρ x₁ x₂
   | Expr.lit v₁,             Expr.lit v₂             => v₁ == v₂
   | Expr.isShared x₁,        Expr.isShared x₂        => aeqv ρ x₁ x₂
-  | Expr.isTaggedPtr x₁,     Expr.isTaggedPtr x₂     => aeqv ρ x₁ x₂
   | _,                        _                      => false
 
 instance : AlphaEqv Expr:= ⟨Expr.alphaEqv⟩

src/Lean/Compiler/IR/Checker.lean

@@ -134,7 +134,6 @@ def checkExpr (ty : IRType) : Expr → M Unit
   | Expr.uproj _ x          => checkObjVar x *> checkType ty (fun t => t == IRType.usize)
   | Expr.sproj _ _ x        => checkObjVar x *> checkScalarType ty
   | Expr.isShared x         => checkObjVar x *> checkType ty (fun t => t == IRType.uint8)
-  | Expr.isTaggedPtr x      => checkObjVar x *> checkType ty (fun t => t == IRType.uint8)
   | Expr.lit (LitVal.str _) => checkObjType ty
   | Expr.lit _              => pure ()
 

src/Lean/Compiler/IR/EmitC.lean

@@ -460,9 +460,6 @@ def emitUnbox (z : VarId) (t : IRType) (x : VarId) : M Unit := do
 def emitIsShared (z : VarId) (x : VarId) : M Unit := do
   emitLhs z; emit "!lean_is_exclusive("; emit x; emitLn ");"
 
-def emitIsTaggedPtr (z : VarId) (x : VarId) : M Unit := do
-  emitLhs z; emit "!lean_is_scalar("; emit x; emitLn ");"
-
 def toHexDigit (c : Nat) : String :=
   String.singleton c.digitChar
 
@@ -511,7 +508,6 @@ def emitVDecl (z : VarId) (t : IRType) (v : Expr) : M Unit :=
   | Expr.box t x        => emitBox z x t
   | Expr.unbox x        => emitUnbox z t x
   | Expr.isShared x     => emitIsShared z x
-  | Expr.isTaggedPtr x  => emitIsTaggedPtr z x
   | Expr.lit v          => emitLit z t v
 
 def isTailCall (x : VarId) (v : Expr) (b : FnBody) : M Bool := do

src/Lean/Compiler/IR/EmitLLVM.lean

@@ -896,7 +896,6 @@ def emitVDecl (builder : LLVM.Builder llvmctx) (z : VarId) (t : IRType) (v : Exp
   | Expr.box t x        => emitBox builder z x t
   | Expr.unbox x        => emitUnbox builder z t x
   | Expr.isShared x     => emitIsShared builder z x
-  | Expr.isTaggedPtr _x => throw "unimplemented: emitIsTaggedPtr z x" -- TODO(bollu): implement emitIsTaggedPtr
   | Expr.lit v          => let _ ← emitLit builder z t v
 
 def declareVar (builder : LLVM.Builder llvmctx) (x : VarId) (t : IRType) : M llvmctx Unit := do

src/Lean/Compiler/IR/Format.lean

@@ -48,7 +48,6 @@ private def formatExpr : Expr → Format
   | Expr.unbox x        => "unbox " ++ format x
   | Expr.lit v          => format v
   | Expr.isShared x     => "isShared " ++ format x
-  | Expr.isTaggedPtr x  => "isTaggedPtr " ++ format x
 
 instance : ToFormat Expr := ⟨formatExpr⟩
 instance : ToString Expr := ⟨fun e => Format.pretty (format e)⟩

src/Lean/Compiler/IR/FreeVars.lean

@@ -51,7 +51,6 @@ private def collectExpr : Expr → Collector
   | Expr.unbox x        => collectVar x
   | Expr.lit _          => skip
   | Expr.isShared x     => collectVar x
-  | Expr.isTaggedPtr x  => collectVar x
 
 private def collectAlts (f : FnBody → Collector) (alts : Array Alt) : Collector :=
   collectArray alts fun alt => f alt.body
@@ -147,7 +146,6 @@ private def collectExpr : Expr → Collector
   | Expr.unbox x        => collectVar x
   | Expr.lit _          => skip
   | Expr.isShared x     => collectVar x
-  | Expr.isTaggedPtr x  => collectVar x
 
 private def collectAlts (f : FnBody → Collector) (alts : Array Alt) : Collector :=
   collectArray alts fun alt => f alt.body
@@ -208,7 +206,6 @@ def visitExpr (w : Index) : Expr → Bool
   | Expr.unbox x        => visitVar w x
   | Expr.lit _          => false
   | Expr.isShared x     => visitVar w x
-  | Expr.isTaggedPtr x  => visitVar w x
 
 partial def visitFnBody (w : Index) : FnBody → Bool
   | FnBody.vdecl _ _ v b    => visitExpr w v || visitFnBody w b

src/Lean/Compiler/IR/LiveVars.lean

@@ -132,7 +132,6 @@ def collectExpr : Expr → Collector
   | Expr.unbox x        => collectVar x
   | Expr.lit _          => skip
   | Expr.isShared x     => collectVar x
-  | Expr.isTaggedPtr x  => collectVar x
 
 partial def collectFnBody : FnBody → JPLiveVarMap → Collector
   | FnBody.vdecl x _ v b,    m => collectExpr v ∘ bindVar x ∘ collectFnBody b m

src/Lean/Compiler/IR/NormIds.lean

@@ -68,7 +68,6 @@ def normExpr : Expr → M Expr
   | Expr.box t x,        m => Expr.box t (normVar x m)
   | Expr.unbox x,        m => Expr.unbox (normVar x m)
   | Expr.isShared x,     m => Expr.isShared (normVar x m)
-  | Expr.isTaggedPtr x,  m => Expr.isTaggedPtr (normVar x m)
   | e@(Expr.lit _),      _ =>  e
 
 abbrev N := ReaderT IndexRenaming (StateM Nat)
@@ -147,7 +146,6 @@ def mapExpr (f : VarId → VarId) : Expr → Expr
   | Expr.box t x        => Expr.box t (f x)
   | Expr.unbox x        => Expr.unbox (f x)
   | Expr.isShared x     => Expr.isShared (f x)
-  | Expr.isTaggedPtr x  => Expr.isTaggedPtr (f x)
   | e@(Expr.lit _)      =>  e
 
 partial def mapFnBody (f : VarId → VarId) : FnBody → FnBody

src/Lean/Compiler/IR/PushProj.lean

@@ -32,7 +32,6 @@ partial def pushProjs (bs : Array FnBody) (alts : Array Alt) (altsF : Array Inde
       | Expr.uproj _ _     => push x
       | Expr.sproj _ _ _   => push x
       | Expr.isShared _    => skip ()
-      | Expr.isTaggedPtr _ => skip ()
       | _                  => done ()
     | _ => done ()