From 26edfc33f524fc4feb0bec30b1f2bf0f04ad3f67 Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Mon, 9 Jan 2023 10:52:46 +0000 Subject: [PATCH] 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 | 3 --- src/Lean/Compiler/IR/Checker.lean | 1 - src/Lean/Compiler/IR/EmitC.lean | 4 ---- src/Lean/Compiler/IR/EmitLLVM.lean | 1 - src/Lean/Compiler/IR/Format.lean | 1 - src/Lean/Compiler/IR/FreeVars.lean | 3 --- src/Lean/Compiler/IR/LiveVars.lean | 1 - src/Lean/Compiler/IR/NormIds.lean | 2 -- src/Lean/Compiler/IR/PushProj.lean | 1 - 9 files changed, 17 deletions(-) diff --git a/src/Lean/Compiler/IR/Basic.lean b/src/Lean/Compiler/IR/Basic.lean index 97d4760a17..a9a84268ad 100644 --- a/src/Lean/Compiler/IR/Basic.lean +++ b/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⟩ diff --git a/src/Lean/Compiler/IR/Checker.lean b/src/Lean/Compiler/IR/Checker.lean index 0eae0668ef..2759aa3cbb 100644 --- a/src/Lean/Compiler/IR/Checker.lean +++ b/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 () diff --git a/src/Lean/Compiler/IR/EmitC.lean b/src/Lean/Compiler/IR/EmitC.lean index 5bd7656381..085281a06d 100644 --- a/src/Lean/Compiler/IR/EmitC.lean +++ b/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 diff --git a/src/Lean/Compiler/IR/EmitLLVM.lean b/src/Lean/Compiler/IR/EmitLLVM.lean index 79f84734d0..3a2e87015e 100644 --- a/src/Lean/Compiler/IR/EmitLLVM.lean +++ b/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 diff --git a/src/Lean/Compiler/IR/Format.lean b/src/Lean/Compiler/IR/Format.lean index ddd7cf7eea..39f9798081 100644 --- a/src/Lean/Compiler/IR/Format.lean +++ b/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)⟩ diff --git a/src/Lean/Compiler/IR/FreeVars.lean b/src/Lean/Compiler/IR/FreeVars.lean index 8a1aae2c64..1d14df4b17 100644 --- a/src/Lean/Compiler/IR/FreeVars.lean +++ b/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 diff --git a/src/Lean/Compiler/IR/LiveVars.lean b/src/Lean/Compiler/IR/LiveVars.lean index 64ce289551..e4c707943b 100644 --- a/src/Lean/Compiler/IR/LiveVars.lean +++ 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 diff --git a/src/Lean/Compiler/IR/NormIds.lean b/src/Lean/Compiler/IR/NormIds.lean index e9eafe8f3b..624e34982b 100644 --- a/src/Lean/Compiler/IR/NormIds.lean +++ b/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 diff --git a/src/Lean/Compiler/IR/PushProj.lean b/src/Lean/Compiler/IR/PushProj.lean index 178d8f24c3..63f73393f0 100644 --- a/src/Lean/Compiler/IR/PushProj.lean +++ b/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 ()