max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/init/lean/compiler/ir): add del instruction for releasing memory

Browse source
This commit is contained in:
Leonardo de Moura 2019-05-23 08:01:15 -07:00
parent c6433460fb
commit 8ba7dd4cff
7 changed files with 16 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
library/init/lean/compiler/ir/basic.lean
View file

@ -225,6 +225,7 @@ inductive FnBody
| inc (x : VarId) (n : Nat) (c : Bool) (b : FnBody)
/- RC decrement for `object`. If c == `true`, then `inc` must check whether `x` is a tagged pointer or not. -/
| dec (x : VarId) (n : Nat) (c : Bool) (b : FnBody)
| del (x : VarId) (b : FnBody)
| mdata (d : MData) (b : FnBody)
| case (tid : Name) (x : VarId) (cs : Array (AltCore FnBody))
| ret (x : Arg)
@ -268,6 +269,7 @@ def FnBody.body : FnBody → FnBody
| (FnBody.release _ _ b) := b
| (FnBody.inc _ _ _ b) := b
| (FnBody.dec _ _ _ b) := b
| (FnBody.del _ b) := b
| (FnBody.mdata _ b) := b
| other := other
@ -280,6 +282,7 @@ def FnBody.setBody : FnBody → FnBody → FnBody
| (FnBody.release x i _) b := FnBody.release x i b
| (FnBody.inc x n c _) b := FnBody.inc x n c b
| (FnBody.dec x n c _) b := FnBody.dec x n c b
| (FnBody.del x _) b := FnBody.del x b
| (FnBody.mdata d _) b := FnBody.mdata d b
| other b := other
@ -535,6 +538,7 @@ partial def FnBody.alphaEqv : IndexRenaming → FnBody → FnBody → Bool
| ρ (FnBody.release x₁ i₁ b₁) (FnBody.release x₂ i₂ b₂) := x₁ =[ρ]= x₂ && i₁ == i₂ && FnBody.alphaEqv ρ b₁ b₂
| ρ (FnBody.inc x₁ n₁ c₁ b₁) (FnBody.inc x₂ n₂ c₂ b₂) := x₁ =[ρ]= x₂ && n₁ == n₂ && c₁ == c₂ && FnBody.alphaEqv ρ b₁ b₂
| ρ (FnBody.dec x₁ n₁ c₁ b₁) (FnBody.dec x₂ n₂ c₂ b₂) := x₁ =[ρ]= x₂ && n₁ == n₂ && c₁ == c₂ && FnBody.alphaEqv ρ b₁ b₂
| ρ (FnBody.del x₁ b₁) (FnBody.del x₂ b₂) := x₁ =[ρ]= x₂ && FnBody.alphaEqv ρ b₁ b₂
| ρ (FnBody.mdata m₁ b₁) (FnBody.mdata m₂ b₂) := m₁ == m₂ && FnBody.alphaEqv ρ b₁ b₂
| ρ (FnBody.case n₁ x₁ alts₁) (FnBody.case n₂ x₂ alts₂) := n₁ == n₂ && x₁ =[ρ]= x₂ && Array.isEqv alts₁ alts₂ (λ alt₁ alt₂,
match alt₁, alt₂ with

1
library/init/lean/compiler/ir/checker.lean
View file

@ -110,6 +110,7 @@ partial def checkFnBody : FnBody → M Unit
| (FnBody.release x _ b) := checkVar x *> checkFnBody b
| (FnBody.inc x _ _ b) := checkVar x *> checkFnBody b
| (FnBody.dec x _ _ b) := checkVar x *> checkFnBody b
| (FnBody.del x b) := checkVar x *> checkFnBody b
| (FnBody.mdata _ b) := checkFnBody b
| (FnBody.jmp j ys) := checkJP j *> checkArgs ys
| (FnBody.ret x) := checkArg x

4
library/init/lean/compiler/ir/emitcpp.lean
View file

@ -322,6 +322,9 @@ emit "(" *> emit x,
when (n != 1) (emit ", " *> emit n),
emitLn ");"
def emitDel (x : VarId) : M Unit :=
do emit "lean::free_heap_obj(", emit x, emitLn ");"
def emitRelease (x : VarId) (i : Nat) : M Unit :=
do emit "lean::cnstr_release(", emit x, emit ", ", emit i, emitLn ");"
@ -587,6 +590,7 @@ partial def emitBlock (emitBody : FnBody → M Unit) : FnBody → M Unit
| (FnBody.vdecl x t v b) := do isTail ← isTailCall x v b, if isTail then emitTailCall v else emitVDecl x t v *> emitBlock b
| (FnBody.inc x n c b) := emitInc x n c *> emitBlock b
| (FnBody.dec x n c b) := emitDec x n c *> emitBlock b
| (FnBody.del x b) := emitDel x *> emitBlock b
| (FnBody.release x i b) := emitRelease x i *> emitBlock b
| (FnBody.set x i y b) := emitSet x i y *> emitBlock b
| (FnBody.uset x i y b) := emitUSet x i y *> emitBlock b

1
library/init/lean/compiler/ir/format.lean
View file

@ -86,6 +86,7 @@ partial def formatFnBody (indent : Nat := 2) : FnBody → Format
| (FnBody.release x i b) := "release " ++ format x ++ "[" ++ format i ++ "];" ++ Format.line ++ formatFnBody b
| (FnBody.inc x n c b) := "inc" ++ (if n != 1 then Format.sbracket (format n) else "") ++ " " ++ format x ++ ";" ++ Format.line ++ formatFnBody b
| (FnBody.dec x n c b) := "dec" ++ (if n != 1 then Format.sbracket (format n) else "") ++ " " ++ format x ++ ";" ++ Format.line ++ formatFnBody b
| (FnBody.del x b) := "del " ++ format x ++ ";" ++ Format.line ++ formatFnBody b
| (FnBody.mdata d b) := "mdata " ++ format d ++ ";" ++ Format.line ++ formatFnBody b
| (FnBody.case tid x cs) := "case " ++ format x ++ " of" ++ cs.foldl (λ r c, r ++ Format.line ++ formatAlt formatFnBody indent c) Format.nil
| (FnBody.jmp j ys) := "jmp " ++ format j ++ formatArray ys

3
library/init/lean/compiler/ir/freevars.lean
View file

@ -66,6 +66,7 @@ partial def collectFnBody : FnBody → Collector
| (FnBody.release x _ b) := collectVar x; collectFnBody b
| (FnBody.inc x _ _ b) := collectVar x; collectFnBody b
| (FnBody.dec x _ _ b) := collectVar x; collectFnBody b
| (FnBody.del x b) := collectVar x; collectFnBody b
| (FnBody.mdata _ b) := collectFnBody b
| (FnBody.case _ x alts) := collectVar x; collectAlts collectFnBody alts
| (FnBody.jmp j ys) := collectJP j; collectArgs ys
@ -160,6 +161,7 @@ partial def collectFnBody : FnBody → Collector
| (FnBody.release x _ b) := collectVar x; collectFnBody b
| (FnBody.inc x _ _ b) := collectVar x; collectFnBody b
| (FnBody.dec x _ _ b) := collectVar x; collectFnBody b
| (FnBody.del x b) := collectVar x; collectFnBody b
| (FnBody.mdata _ b) := collectFnBody b
| (FnBody.case _ x alts) := collectVar x; collectAlts collectFnBody alts
| (FnBody.jmp j ys) := collectJP j; collectArgs ys
@ -217,6 +219,7 @@ partial def visitFnBody (w : Index) : FnBody → Bool
| (FnBody.release x _ b) := visitVar w x || visitFnBody b
| (FnBody.inc x _ _ b) := visitVar w x || visitFnBody b
| (FnBody.dec x _ _ b) := visitVar w x || visitFnBody b
| (FnBody.del x b) := visitVar w x || visitFnBody b
| (FnBody.mdata _ b) := visitFnBody b
| (FnBody.jmp j ys) := visitJP w j || visitArgs w ys
| (FnBody.ret x) := visitArg w x

2
library/init/lean/compiler/ir/livevars.lean
View file

@ -55,6 +55,7 @@ partial def visitFnBody (w : Index) : FnBody → M Bool
| (FnBody.release x _ b) := visitVar w x <||> visitFnBody b
| (FnBody.inc x _ _ b) := visitVar w x <||> visitFnBody b
| (FnBody.dec x _ _ b) := visitVar w x <||> visitFnBody b
| (FnBody.del x b) := visitVar w x <||> visitFnBody b
| (FnBody.mdata _ b) := visitFnBody b
| (FnBody.jmp j ys) := visitArgs w ys <||> do {
ctx ← get,
@ -141,6 +142,7 @@ partial def collectFnBody : FnBody → JPLiveVarMap → Collector
| (FnBody.release x _ b) m := collectVar x >> collectFnBody b m
| (FnBody.inc x _ _ b) m := collectVar x >> collectFnBody b m
| (FnBody.dec x _ _ b) m := collectVar x >> collectFnBody b m
| (FnBody.del x b) m := collectVar x >> collectFnBody b m
| (FnBody.mdata _ b) m := collectFnBody b m
| (FnBody.ret x) m := collectArg x
| (FnBody.case _ x alts) m := collectVar x >> collectArray alts (λ alt, collectFnBody alt.body m)

1
library/init/lean/compiler/ir/normids.lean
View file

@ -108,6 +108,7 @@ partial def normFnBody : FnBody → N FnBody
| (FnBody.release x i b) := do x ← normVar x, FnBody.release x i <$> normFnBody b
| (FnBody.inc x n c b) := do x ← normVar x, FnBody.inc x n c <$> normFnBody b
| (FnBody.dec x n c b) := do x ← normVar x, FnBody.dec x n c <$> normFnBody b
| (FnBody.del x b) := do x ← normVar x, FnBody.del x <$> normFnBody b
| (FnBody.mdata d b) := FnBody.mdata d <$> normFnBody b
| (FnBody.case tid x alts) := do
x ← normVar x,