Skip to content

Commit dd45a21

Browse files
zwarichzwarich
authored
chore: remove unused FnBody.mdata constructor (#9564)
1 parent 8177de8 commit dd45a21

File tree

12 files changed

+2
-32
lines changed

12 files changed

+2
-32
lines changed

‎src/Lean/Compiler/IR/Basic.lean

Lines changed: 0 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -40,9 +40,6 @@ abbrev Index.lt (a b : Index) : Bool := a < b
4040
instance : ToString VarId := ⟨fun a => "x_" ++ toString a.idx⟩
4141
instance : ToString JoinPointId := ⟨fun a => "block_" ++ toString a.idx⟩
4242

43-
abbrev MData := KVMap
44-
abbrev MData.empty : MData := {}
45-
4643
/-- Low Level IR types. Most are self explanatory.
4744
4845
- `usize` represents the C++ `size_t` Type. We have it here
@@ -234,7 +231,6 @@ inductive FnBody where
234231
If `persistent == true` then `x` is statically known to be a persistent object. -/
235232
| dec (x : VarId) (n : Nat) (c : Bool) (persistent : Bool) (b : FnBody)
236233
| del (x : VarId) (b : FnBody)
237-
| mdata (d : MData) (b : FnBody)
238234
| case (tid : Name) (x : VarId) (xType : IRType) (cs : Array Alt)
239235
| ret (x : Arg)
240236
/-- Jump to join point `j` -/
@@ -265,7 +261,6 @@ def FnBody.body : FnBody → FnBody
265261
| FnBody.inc _ _ _ _ b => b
266262
| FnBody.dec _ _ _ _ b => b
267263
| FnBody.del _ b => b
268-
| FnBody.mdata _ b => b
269264
| other => other
270265

271266
def FnBody.setBody : FnBody → FnBody → FnBody
@@ -278,7 +273,6 @@ def FnBody.setBody : FnBody → FnBody → FnBody
278273
| FnBody.inc x n c p _, b => FnBody.inc x n c p b
279274
| FnBody.dec x n c p _, b => FnBody.dec x n c p b
280275
| FnBody.del x _, b => FnBody.del x b
281-
| FnBody.mdata d _, b => FnBody.mdata d b
282276
| other, _ => other
283277

284278
@[inline] def FnBody.resetBody (b : FnBody) : FnBody :=
@@ -528,7 +522,6 @@ partial def FnBody.alphaEqv : IndexRenaming → FnBody → FnBody → Bool
528522
| ρ, FnBody.inc x₁ n₁ c₁ p₁ b₁, FnBody.inc x₂ n₂ c₂ p₂ b₂ => aeqv ρ x₁ x₂ && n₁ == n₂ && c₁ == c₂ && p₁ == p₂ && alphaEqv ρ b₁ b₂
529523
| ρ, FnBody.dec x₁ n₁ c₁ p₁ b₁, FnBody.dec x₂ n₂ c₂ p₂ b₂ => aeqv ρ x₁ x₂ && n₁ == n₂ && c₁ == c₂ && p₁ == p₂ && alphaEqv ρ b₁ b₂
530524
| ρ, FnBody.del x₁ b₁, FnBody.del x₂ b₂ => aeqv ρ x₁ x₂ && alphaEqv ρ b₁ b₂
531-
| ρ, FnBody.mdata m₁ b₁, FnBody.mdata m₂ b₂ => m₁ == m₂ && alphaEqv ρ b₁ b₂
532525
| ρ, FnBody.case n₁ x₁ _ alts₁, FnBody.case n₂ x₂ _ alts₂ => n₁ == n₂ && aeqv ρ x₁ x₂ && Array.isEqv alts₁ alts₂ (fun alt₁ alt₂ =>
533526
match alt₁, alt₂ with
534527
| Alt.ctor i₁ b₁, Alt.ctor i₂ b₂ => i₁ == i₂ && alphaEqv ρ b₁ b₂

‎src/Lean/Compiler/IR/Boxing.lean

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -302,8 +302,6 @@ partial def visitFnBody : FnBody → M FnBody
302302
let b ← visitFnBody b
303303
castVarIfNeeded y ty fun y =>
304304
return FnBody.sset x i o y ty b
305-
| FnBody.mdata d b =>
306-
FnBody.mdata d <$> visitFnBody b
307305
| FnBody.case tid x _ alts => do
308306
let expected := getScrutineeType alts
309307
let alts ← alts.mapM fun alt => alt.modifyBodyM visitFnBody

‎src/Lean/Compiler/IR/Checker.lean

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -223,8 +223,6 @@ partial def checkFnBody (fnBody : FnBody) : M Unit := do
223223
| .del x b =>
224224
checkVar x
225225
checkFnBody b
226-
| .mdata _ b =>
227-
checkFnBody b
228226
| .jmp j ys =>
229227
checkJP j
230228
checkArgs ys

‎src/Lean/Compiler/IR/EmitC.lean

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -640,7 +640,6 @@ partial def emitBlock (b : FnBody) : M Unit := do
640640
| FnBody.set x i y b => emitSet x i y; emitBlock b
641641
| FnBody.uset x i y b => emitUSet x i y; emitBlock b
642642
| FnBody.sset x i o y t b => emitSSet x i o y t; emitBlock b
643-
| FnBody.mdata _ b => emitBlock b
644643
| FnBody.ret x => emit "return "; emitArg x; emitLn ";"
645644
| FnBody.case _ x xType alts => emitCase x xType alts
646645
| FnBody.jmp j xs => emitJmp j xs

‎src/Lean/Compiler/IR/EmitLLVM.lean

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1161,7 +1161,6 @@ partial def emitBlock (builder : LLVM.Builder llvmctx) (b : FnBody) : M llvmctx
11611161
| FnBody.set x i y b => emitSet builder x i y; emitBlock builder b
11621162
| FnBody.uset x i y b => emitUSet builder x i y; emitBlock builder b
11631163
| FnBody.sset x i o y t b => emitSSet builder x i o y t; emitBlock builder b
1164-
| FnBody.mdata _ b => emitBlock builder b
11651164
| FnBody.ret x => do
11661165
let (_xty, xv) ← emitArgVal builder x "ret_val"
11671166
let _ ← LLVM.buildRet builder xv

‎src/Lean/Compiler/IR/Format.lean

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -101,7 +101,6 @@ def formatFnBodyHead : FnBody → Format
101101
| FnBody.inc x n _ _ _ => "inc" ++ (if n != 1 then Format.sbracket (format n) else "") ++ " " ++ format x
102102
| FnBody.dec x n _ _ _ => "dec" ++ (if n != 1 then Format.sbracket (format n) else "") ++ " " ++ format x
103103
| FnBody.del x _ => "del " ++ format x
104-
| FnBody.mdata d _ => "mdata " ++ format d
105104
| FnBody.case _ x _ _ => "case " ++ format x ++ " of ..."
106105
| FnBody.jmp j ys => "jmp " ++ format j ++ formatArray ys
107106
| FnBody.ret x => "ret " ++ format x
@@ -122,7 +121,6 @@ partial def formatFnBody (fnBody : FnBody) (indent : Nat := 2) : Format :=
122121
| FnBody.inc x n _ _ b => "inc" ++ (if n != 1 then Format.sbracket (format n) else "") ++ " " ++ format x ++ ";" ++ Format.line ++ loop b
123122
| FnBody.dec x n _ _ b => "dec" ++ (if n != 1 then Format.sbracket (format n) else "") ++ " " ++ format x ++ ";" ++ Format.line ++ loop b
124123
| FnBody.del x b => "del " ++ format x ++ ";" ++ Format.line ++ loop b
125-
| FnBody.mdata d b => "mdata " ++ format d ++ ";" ++ Format.line ++ loop b
126124
| FnBody.case _ x xType cs => "case " ++ format x ++ " : " ++ format xType ++ " of" ++ cs.foldl (fun r c => r ++ Format.line ++ formatAlt loop indent c) Format.nil
127125
| FnBody.jmp j ys => "jmp " ++ format j ++ formatArray ys
128126
| FnBody.ret x => "ret " ++ format x

‎src/Lean/Compiler/IR/FreeVars.lean

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -70,7 +70,6 @@ partial def collectFnBody : FnBody → Collector
7070
| FnBody.inc x _ _ _ b => collectVar x >> collectFnBody b
7171
| FnBody.dec x _ _ _ b => collectVar x >> collectFnBody b
7272
| FnBody.del x b => collectVar x >> collectFnBody b
73-
| FnBody.mdata _ b => collectFnBody b
7473
| FnBody.case _ x _ alts => collectVar x >> collectAlts collectFnBody alts
7574
| FnBody.jmp j ys => collectJP j >> collectArgs ys
7675
| FnBody.ret x => collectArg x
@@ -165,7 +164,6 @@ partial def collectFnBody : FnBody → Collector
165164
| FnBody.inc x _ _ _ b => collectVar x >> collectFnBody b
166165
| FnBody.dec x _ _ _ b => collectVar x >> collectFnBody b
167166
| FnBody.del x b => collectVar x >> collectFnBody b
168-
| FnBody.mdata _ b => collectFnBody b
169167
| FnBody.case _ x _ alts => collectVar x >> collectAlts collectFnBody alts
170168
| FnBody.jmp j ys => collectJP j >> collectArgs ys
171169
| FnBody.ret x => collectArg x
@@ -222,7 +220,6 @@ partial def visitFnBody (w : Index) : FnBody → Bool
222220
| FnBody.inc x _ _ _ b => visitVar w x || visitFnBody w b
223221
| FnBody.dec x _ _ _ b => visitVar w x || visitFnBody w b
224222
| FnBody.del x b => visitVar w x || visitFnBody w b
225-
| FnBody.mdata _ b => visitFnBody w b
226223
| FnBody.jmp j ys => visitJP w j || visitArgs w ys
227224
| FnBody.ret x => visitArg w x
228225
| FnBody.case _ x _ alts => visitVar w x || alts.any (fun alt => visitFnBody w alt.body)

‎src/Lean/Compiler/IR/LiveVars.lean

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -57,7 +57,6 @@ partial def visitFnBody (w : Index) : FnBody → M Bool
5757
| FnBody.inc x _ _ _ b => visitVar w x <||> visitFnBody w b
5858
| FnBody.dec x _ _ _ b => visitVar w x <||> visitFnBody w b
5959
| FnBody.del x b => visitVar w x <||> visitFnBody w b
60-
| FnBody.mdata _ b => visitFnBody w b
6160
| FnBody.jmp j ys => visitArgs w ys <||> do
6261
let ctx ← get
6362
match ctx.getJPBody j with
@@ -148,7 +147,6 @@ partial def collectFnBody : FnBody → JPLiveVarMap → Collector
148147
| FnBody.inc x _ _ _ b, m => collectVar x ∘ collectFnBody b m
149148
| FnBody.dec x _ _ _ b, m => collectVar x ∘ collectFnBody b m
150149
| FnBody.del x b, m => collectVar x ∘ collectFnBody b m
151-
| FnBody.mdata _ b, m => collectFnBody b m
152150
| FnBody.ret x, _ => collectArg x
153151
| FnBody.case _ x _ alts, m => collectVar x ∘ collectArray alts (fun alt => collectFnBody alt.body m)
154152
| FnBody.unreachable, _ => skip

‎src/Lean/Compiler/IR/NormIds.lean

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -107,7 +107,6 @@ partial def normFnBody : FnBody → N FnBody
107107
| FnBody.inc x n c p b => return FnBody.inc (← normVar x) n c p (← normFnBody b)
108108
| FnBody.dec x n c p b => return FnBody.dec (← normVar x) n c p (← normFnBody b)
109109
| FnBody.del x b => return FnBody.del (← normVar x) (← normFnBody b)
110-
| FnBody.mdata d b => return FnBody.mdata d (← normFnBody b)
111110
| FnBody.case tid x xType alts => do
112111
let x ← normVar x
113112
let alts ← alts.mapM fun alt => alt.modifyBodyM normFnBody
@@ -163,7 +162,6 @@ partial def mapFnBody (f : VarId → VarId) : FnBody → FnBody
163162
| FnBody.inc x n c p b => FnBody.inc (f x) n c p (mapFnBody f b)
164163
| FnBody.dec x n c p b => FnBody.dec (f x) n c p (mapFnBody f b)
165164
| FnBody.del x b => FnBody.del (f x) (mapFnBody f b)
166-
| FnBody.mdata d b => FnBody.mdata d (mapFnBody f b)
167165
| FnBody.case tid x xType alts => FnBody.case tid (f x) xType (alts.map fun alt => alt.modifyBody (mapFnBody f))
168166
| FnBody.jmp j ys => FnBody.jmp j (mapArgs f ys)
169167
| FnBody.ret x => FnBody.ret (mapArg f x)

‎src/Lean/Compiler/IR/RC.lean

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -241,9 +241,6 @@ partial def visitFnBody : FnBody → Context → (FnBody × LiveVarSet)
241241
-- We don't need to insert `y` since we only need to track live variables that are references at runtime
242242
let s := s.insert x
243243
(FnBody.sset x i o y t b, s)
244-
| FnBody.mdata m b, ctx =>
245-
let (b, s) := visitFnBody b ctx
246-
(FnBody.mdata m b, s)
247244
| b@(FnBody.case tid x xType alts), ctx =>
248245
let caseLiveVars := collectLiveVars b ctx.jpLiveVarMap
249246
let alts := alts.map fun alt => match alt with

0 commit comments

Comments
 (0)