refactor(library/init/lean/compiler/ir): move "free variable" code to separate file
This commit is contained in:
Leonardo de Moura
parent
7a5e64e52e
commit
439ce06a19
11 changed files with 4551 additions and 4489 deletions
|
|
@ -437,214 +437,5 @@ FnBody.alphaEqv ∅ b₁ b₂
|
|||
|
||||
instance FnBody.HasBeq : HasBeq FnBody := ⟨FnBody.beq⟩
|
||||
|
||||
abbrev IndexSet := RBTree Index (λ a b, a < b)
|
||||
instance vsetInh : Inhabited IndexSet := ⟨{}⟩
|
||||
|
||||
namespace FreeVariables
|
||||
abbrev Collector := IndexSet → IndexSet → IndexSet
|
||||
|
||||
@[inline] private def skip : Collector :=
|
||||
λ bv fv, fv
|
||||
|
||||
@[inline] private def collectIndex (x : Index) : Collector :=
|
||||
λ bv fv, if bv.contains x then fv else fv.insert x
|
||||
|
||||
@[inline] private def collectVar (x : VarId) : Collector :=
|
||||
collectIndex x.idx
|
||||
|
||||
@[inline] private def collectJP (x : JoinPointId) : Collector :=
|
||||
collectIndex x.idx
|
||||
|
||||
@[inline] private def withIndex (x : Index) : Collector → Collector :=
|
||||
λ k bv fv, k (bv.insert x) fv
|
||||
|
||||
@[inline] private def withVar (x : VarId) : Collector → Collector :=
|
||||
withIndex x.idx
|
||||
|
||||
@[inline] private def withJP (x : JoinPointId) : Collector → Collector :=
|
||||
withIndex x.idx
|
||||
|
||||
def insertParams (s : IndexSet) (ys : Array Param) : IndexSet :=
|
||||
ys.foldl (λ s p, s.insert p.x.idx) s
|
||||
|
||||
@[inline] private def withParams (ys : Array Param) : Collector → Collector :=
|
||||
λ k bv fv, k (insertParams bv ys) fv
|
||||
|
||||
@[inline] private def seq : Collector → Collector → Collector :=
|
||||
λ k₁ k₂ bv fv, k₂ bv (k₁ bv fv)
|
||||
|
||||
instance : HasAndthen Collector := ⟨seq⟩
|
||||
|
||||
private def collectArg : Arg → Collector
|
||||
| (Arg.var x) := collectVar x
|
||||
| irrelevant := skip
|
||||
|
||||
@[specialize] private def collectArray {α : Type} (as : Array α) (f : α → Collector) : Collector :=
|
||||
λ bv fv, as.foldl (λ fv a, f a bv fv) fv
|
||||
|
||||
private def collectArgs (as : Array Arg) : Collector :=
|
||||
collectArray as collectArg
|
||||
|
||||
private def collectExpr : Expr → Collector
|
||||
| (Expr.ctor _ ys) := collectArgs ys
|
||||
| (Expr.reset x) := collectVar x
|
||||
| (Expr.reuse x _ _ ys) := collectVar x; collectArgs ys
|
||||
| (Expr.proj _ x) := collectVar x
|
||||
| (Expr.uproj _ x) := collectVar x
|
||||
| (Expr.sproj _ _ x) := collectVar x
|
||||
| (Expr.fap _ ys) := collectArgs ys
|
||||
| (Expr.pap _ ys) := collectArgs ys
|
||||
| (Expr.ap x ys) := collectVar x; collectArgs ys
|
||||
| (Expr.box _ x) := collectVar x
|
||||
| (Expr.unbox x) := collectVar x
|
||||
| (Expr.lit v) := skip
|
||||
| (Expr.isShared x) := collectVar x
|
||||
| (Expr.isTaggedPtr x) := collectVar x
|
||||
|
||||
private def collectAlts (f : FnBody → Collector) (alts : Array Alt) : Collector :=
|
||||
collectArray alts $ λ alt, f alt.body
|
||||
|
||||
partial def collectFnBody : FnBody → Collector
|
||||
| (FnBody.vdecl x _ v b) := collectExpr v; withVar x (collectFnBody b)
|
||||
| (FnBody.jdecl j ys _ v b) := withParams ys (collectFnBody v); withJP j (collectFnBody b)
|
||||
| (FnBody.set x _ y b) := collectVar x; collectVar y; collectFnBody b
|
||||
| (FnBody.uset x _ y b) := collectVar x; collectVar y; collectFnBody b
|
||||
| (FnBody.sset x _ _ y _ b) := collectVar x; collectVar y; collectFnBody b
|
||||
| (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.mdata _ b) := collectFnBody b
|
||||
| (FnBody.case _ x alts) := collectVar x; collectAlts collectFnBody alts
|
||||
| (FnBody.jmp j ys) := collectJP j; collectArgs ys
|
||||
| (FnBody.ret x) := collectArg x
|
||||
| FnBody.unreachable := skip
|
||||
|
||||
end FreeVariables
|
||||
|
||||
def FnBody.collectFreeVars (b : FnBody) (vs : IndexSet) : IndexSet :=
|
||||
FreeVariables.collectFnBody b {} vs
|
||||
|
||||
def FnBody.freeVars (b : FnBody) : IndexSet :=
|
||||
b.collectFreeVars {}
|
||||
|
||||
namespace MaxVar
|
||||
abbrev Collector := Index → Index
|
||||
|
||||
@[inline] private def skip : Collector := id
|
||||
@[inline] private def collect (x : Index) : Collector := λ y, if x > y then x else y
|
||||
@[inline] private def collectVar (x : VarId) : Collector := collect x.idx
|
||||
@[inline] private def collectJP (j : JoinPointId) : Collector := collect j.idx
|
||||
@[inline] private def seq (k₁ k₂ : Collector) : Collector := k₂ ∘ k₁
|
||||
instance : HasAndthen Collector := ⟨seq⟩
|
||||
|
||||
private def collectArg : Arg → Collector
|
||||
| (Arg.var x) := collectVar x
|
||||
| irrelevant := skip
|
||||
|
||||
@[specialize] private def collectArray {α : Type} (as : Array α) (f : α → Collector) : Collector :=
|
||||
λ m, as.foldl (λ m a, f a m) m
|
||||
|
||||
private def collectArgs (as : Array Arg) : Collector := collectArray as collectArg
|
||||
private def collectParam (p : Param) : Collector := collectVar p.x
|
||||
private def collectParams (ps : Array Param) : Collector := collectArray ps collectParam
|
||||
|
||||
private def collectExpr : Expr → Collector
|
||||
| (Expr.ctor _ ys) := collectArgs ys
|
||||
| (Expr.reset x) := collectVar x
|
||||
| (Expr.reuse x _ _ ys) := collectVar x; collectArgs ys
|
||||
| (Expr.proj _ x) := collectVar x
|
||||
| (Expr.uproj _ x) := collectVar x
|
||||
| (Expr.sproj _ _ x) := collectVar x
|
||||
| (Expr.fap _ ys) := collectArgs ys
|
||||
| (Expr.pap _ ys) := collectArgs ys
|
||||
| (Expr.ap x ys) := collectVar x; collectArgs ys
|
||||
| (Expr.box _ x) := collectVar x
|
||||
| (Expr.unbox x) := collectVar x
|
||||
| (Expr.lit v) := skip
|
||||
| (Expr.isShared x) := collectVar x
|
||||
| (Expr.isTaggedPtr x) := collectVar x
|
||||
|
||||
private def collectAlts (f : FnBody → Collector) (alts : Array Alt) : Collector :=
|
||||
collectArray alts $ λ alt, f alt.body
|
||||
|
||||
partial def collectFnBody : FnBody → Collector
|
||||
| (FnBody.vdecl x _ v b) := collectExpr v; collectFnBody b
|
||||
| (FnBody.jdecl j ys _ v b) := collectFnBody v; collectParams ys; collectFnBody b
|
||||
| (FnBody.set x _ y b) := collectVar x; collectVar y; collectFnBody b
|
||||
| (FnBody.uset x _ y b) := collectVar x; collectVar y; collectFnBody b
|
||||
| (FnBody.sset x _ _ y _ b) := collectVar x; collectVar y; collectFnBody b
|
||||
| (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.mdata _ b) := collectFnBody b
|
||||
| (FnBody.case _ x alts) := collectVar x; collectAlts collectFnBody alts
|
||||
| (FnBody.jmp j ys) := collectJP j; collectArgs ys
|
||||
| (FnBody.ret x) := collectArg x
|
||||
| FnBody.unreachable := skip
|
||||
|
||||
partial def collectDecl : Decl → Collector
|
||||
| (Decl.fdecl _ xs _ b) := collectParams xs; collectFnBody b
|
||||
| (Decl.extern _ xs _) := collectParams xs
|
||||
|
||||
end MaxVar
|
||||
|
||||
def FnBody.maxVar (b : FnBody) : Index :=
|
||||
MaxVar.collectFnBody b 0
|
||||
|
||||
def Decl.maxVar (d : Decl) : Index :=
|
||||
MaxVar.collectDecl d 0
|
||||
|
||||
namespace HasIndex
|
||||
|
||||
def visitVar (w : Index) (x : VarId) : Bool := w == x.idx
|
||||
def visitJP (w : Index) (x : JoinPointId) : Bool := w == x.idx
|
||||
|
||||
def visitArg (w : Index) : Arg → Bool
|
||||
| (Arg.var x) := visitVar w x
|
||||
| _ := false
|
||||
|
||||
def visitArgs (w : Index) (xs : Array Arg) : Bool :=
|
||||
xs.any (visitArg w)
|
||||
|
||||
def visitParams (w : Index) (ps : Array Param) : Bool :=
|
||||
ps.any (λ p, w == p.x.idx)
|
||||
|
||||
def visitExpr (w : Index) : Expr → Bool
|
||||
| (Expr.ctor _ ys) := visitArgs w ys
|
||||
| (Expr.reset x) := visitVar w x
|
||||
| (Expr.reuse x _ _ ys) := visitVar w x || visitArgs w ys
|
||||
| (Expr.proj _ x) := visitVar w x
|
||||
| (Expr.uproj _ x) := visitVar w x
|
||||
| (Expr.sproj _ _ x) := visitVar w x
|
||||
| (Expr.fap _ ys) := visitArgs w ys
|
||||
| (Expr.pap _ ys) := visitArgs w ys
|
||||
| (Expr.ap x ys) := visitVar w x || visitArgs w ys
|
||||
| (Expr.box _ x) := visitVar w x
|
||||
| (Expr.unbox x) := visitVar w x
|
||||
| (Expr.lit v) := false
|
||||
| (Expr.isShared x) := visitVar w x
|
||||
| (Expr.isTaggedPtr x) := visitVar w x
|
||||
|
||||
partial def visitFnBody (w : Index) : FnBody → Bool
|
||||
| (FnBody.vdecl x _ v b) := visitExpr w v || (!visitVar w x && visitFnBody b)
|
||||
| (FnBody.jdecl j ys _ v b) := (!visitParams w ys && visitFnBody v) || (!visitJP w j && visitFnBody b)
|
||||
| (FnBody.set x _ y b) := visitVar w x || visitVar w y || visitFnBody b
|
||||
| (FnBody.uset x _ y b) := visitVar w x || visitVar w y || visitFnBody b
|
||||
| (FnBody.sset x _ _ y _ b) := visitVar w x || visitVar w y || visitFnBody b
|
||||
| (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.mdata _ b) := visitFnBody b
|
||||
| (FnBody.jmp j ys) := visitJP w j || visitArgs w ys
|
||||
| (FnBody.ret x) := visitArg w x
|
||||
| (FnBody.case _ x alts) := visitVar w x || alts.any (λ alt, visitFnBody alt.body)
|
||||
| (FnBody.unreachable) := false
|
||||
|
||||
end HasIndex
|
||||
|
||||
def Arg.hasFreeVar (arg : Arg) (x : VarId) : Bool := HasIndex.visitArg x.idx arg
|
||||
def Expr.hasFreeVar (e : Expr) (x : VarId) : Bool := HasIndex.visitExpr x.idx e
|
||||
def FnBody.hasFreeVar (b : FnBody) (x : VarId) : Bool := HasIndex.visitFnBody x.idx b
|
||||
|
||||
end IR
|
||||
end Lean
|
||||
|
|
|
|||
|
|
@ -5,6 +5,7 @@ Authors: Leonardo de Moura
|
|||
-/
|
||||
prelude
|
||||
import init.lean.compiler.ir.basic
|
||||
import init.lean.compiler.ir.freevars
|
||||
|
||||
namespace Lean
|
||||
namespace IR
|
||||
|
|
|
|||
222
library/init/lean/compiler/ir/freevars.lean
Normal file
222
library/init/lean/compiler/ir/freevars.lean
Normal file
|
|
@ -0,0 +1,222 @@
|
|||
/-
|
||||
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Leonardo de Moura
|
||||
-/
|
||||
prelude
|
||||
import init.lean.compiler.ir.basic
|
||||
|
||||
namespace Lean
|
||||
namespace IR
|
||||
|
||||
abbrev IndexSet := RBTree Index (λ a b, a < b)
|
||||
instance vsetInh : Inhabited IndexSet := ⟨{}⟩
|
||||
|
||||
namespace FreeVariables
|
||||
abbrev Collector := IndexSet → IndexSet → IndexSet
|
||||
|
||||
@[inline] private def skip : Collector :=
|
||||
λ bv fv, fv
|
||||
|
||||
@[inline] private def collectIndex (x : Index) : Collector :=
|
||||
λ bv fv, if bv.contains x then fv else fv.insert x
|
||||
|
||||
@[inline] private def collectVar (x : VarId) : Collector :=
|
||||
collectIndex x.idx
|
||||
|
||||
@[inline] private def collectJP (x : JoinPointId) : Collector :=
|
||||
collectIndex x.idx
|
||||
|
||||
@[inline] private def withIndex (x : Index) : Collector → Collector :=
|
||||
λ k bv fv, k (bv.insert x) fv
|
||||
|
||||
@[inline] private def withVar (x : VarId) : Collector → Collector :=
|
||||
withIndex x.idx
|
||||
|
||||
@[inline] private def withJP (x : JoinPointId) : Collector → Collector :=
|
||||
withIndex x.idx
|
||||
|
||||
def insertParams (s : IndexSet) (ys : Array Param) : IndexSet :=
|
||||
ys.foldl (λ s p, s.insert p.x.idx) s
|
||||
|
||||
@[inline] private def withParams (ys : Array Param) : Collector → Collector :=
|
||||
λ k bv fv, k (insertParams bv ys) fv
|
||||
|
||||
@[inline] private def seq : Collector → Collector → Collector :=
|
||||
λ k₁ k₂ bv fv, k₂ bv (k₁ bv fv)
|
||||
|
||||
instance : HasAndthen Collector := ⟨seq⟩
|
||||
|
||||
private def collectArg : Arg → Collector
|
||||
| (Arg.var x) := collectVar x
|
||||
| irrelevant := skip
|
||||
|
||||
@[specialize] private def collectArray {α : Type} (as : Array α) (f : α → Collector) : Collector :=
|
||||
λ bv fv, as.foldl (λ fv a, f a bv fv) fv
|
||||
|
||||
private def collectArgs (as : Array Arg) : Collector :=
|
||||
collectArray as collectArg
|
||||
|
||||
private def collectExpr : Expr → Collector
|
||||
| (Expr.ctor _ ys) := collectArgs ys
|
||||
| (Expr.reset x) := collectVar x
|
||||
| (Expr.reuse x _ _ ys) := collectVar x; collectArgs ys
|
||||
| (Expr.proj _ x) := collectVar x
|
||||
| (Expr.uproj _ x) := collectVar x
|
||||
| (Expr.sproj _ _ x) := collectVar x
|
||||
| (Expr.fap _ ys) := collectArgs ys
|
||||
| (Expr.pap _ ys) := collectArgs ys
|
||||
| (Expr.ap x ys) := collectVar x; collectArgs ys
|
||||
| (Expr.box _ x) := collectVar x
|
||||
| (Expr.unbox x) := collectVar x
|
||||
| (Expr.lit v) := skip
|
||||
| (Expr.isShared x) := collectVar x
|
||||
| (Expr.isTaggedPtr x) := collectVar x
|
||||
|
||||
private def collectAlts (f : FnBody → Collector) (alts : Array Alt) : Collector :=
|
||||
collectArray alts $ λ alt, f alt.body
|
||||
|
||||
partial def collectFnBody : FnBody → Collector
|
||||
| (FnBody.vdecl x _ v b) := collectExpr v; withVar x (collectFnBody b)
|
||||
| (FnBody.jdecl j ys _ v b) := withParams ys (collectFnBody v); withJP j (collectFnBody b)
|
||||
| (FnBody.set x _ y b) := collectVar x; collectVar y; collectFnBody b
|
||||
| (FnBody.uset x _ y b) := collectVar x; collectVar y; collectFnBody b
|
||||
| (FnBody.sset x _ _ y _ b) := collectVar x; collectVar y; collectFnBody b
|
||||
| (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.mdata _ b) := collectFnBody b
|
||||
| (FnBody.case _ x alts) := collectVar x; collectAlts collectFnBody alts
|
||||
| (FnBody.jmp j ys) := collectJP j; collectArgs ys
|
||||
| (FnBody.ret x) := collectArg x
|
||||
| FnBody.unreachable := skip
|
||||
|
||||
end FreeVariables
|
||||
|
||||
def FnBody.collectFreeVars (b : FnBody) (vs : IndexSet) : IndexSet :=
|
||||
FreeVariables.collectFnBody b {} vs
|
||||
|
||||
def FnBody.freeVars (b : FnBody) : IndexSet :=
|
||||
b.collectFreeVars {}
|
||||
|
||||
namespace MaxVar
|
||||
abbrev Collector := Index → Index
|
||||
|
||||
@[inline] private def skip : Collector := id
|
||||
@[inline] private def collect (x : Index) : Collector := λ y, if x > y then x else y
|
||||
@[inline] private def collectVar (x : VarId) : Collector := collect x.idx
|
||||
@[inline] private def collectJP (j : JoinPointId) : Collector := collect j.idx
|
||||
@[inline] private def seq (k₁ k₂ : Collector) : Collector := k₂ ∘ k₁
|
||||
instance : HasAndthen Collector := ⟨seq⟩
|
||||
|
||||
private def collectArg : Arg → Collector
|
||||
| (Arg.var x) := collectVar x
|
||||
| irrelevant := skip
|
||||
|
||||
@[specialize] private def collectArray {α : Type} (as : Array α) (f : α → Collector) : Collector :=
|
||||
λ m, as.foldl (λ m a, f a m) m
|
||||
|
||||
private def collectArgs (as : Array Arg) : Collector := collectArray as collectArg
|
||||
private def collectParam (p : Param) : Collector := collectVar p.x
|
||||
private def collectParams (ps : Array Param) : Collector := collectArray ps collectParam
|
||||
|
||||
private def collectExpr : Expr → Collector
|
||||
| (Expr.ctor _ ys) := collectArgs ys
|
||||
| (Expr.reset x) := collectVar x
|
||||
| (Expr.reuse x _ _ ys) := collectVar x; collectArgs ys
|
||||
| (Expr.proj _ x) := collectVar x
|
||||
| (Expr.uproj _ x) := collectVar x
|
||||
| (Expr.sproj _ _ x) := collectVar x
|
||||
| (Expr.fap _ ys) := collectArgs ys
|
||||
| (Expr.pap _ ys) := collectArgs ys
|
||||
| (Expr.ap x ys) := collectVar x; collectArgs ys
|
||||
| (Expr.box _ x) := collectVar x
|
||||
| (Expr.unbox x) := collectVar x
|
||||
| (Expr.lit v) := skip
|
||||
| (Expr.isShared x) := collectVar x
|
||||
| (Expr.isTaggedPtr x) := collectVar x
|
||||
|
||||
private def collectAlts (f : FnBody → Collector) (alts : Array Alt) : Collector :=
|
||||
collectArray alts $ λ alt, f alt.body
|
||||
|
||||
partial def collectFnBody : FnBody → Collector
|
||||
| (FnBody.vdecl x _ v b) := collectExpr v; collectFnBody b
|
||||
| (FnBody.jdecl j ys _ v b) := collectFnBody v; collectParams ys; collectFnBody b
|
||||
| (FnBody.set x _ y b) := collectVar x; collectVar y; collectFnBody b
|
||||
| (FnBody.uset x _ y b) := collectVar x; collectVar y; collectFnBody b
|
||||
| (FnBody.sset x _ _ y _ b) := collectVar x; collectVar y; collectFnBody b
|
||||
| (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.mdata _ b) := collectFnBody b
|
||||
| (FnBody.case _ x alts) := collectVar x; collectAlts collectFnBody alts
|
||||
| (FnBody.jmp j ys) := collectJP j; collectArgs ys
|
||||
| (FnBody.ret x) := collectArg x
|
||||
| FnBody.unreachable := skip
|
||||
|
||||
partial def collectDecl : Decl → Collector
|
||||
| (Decl.fdecl _ xs _ b) := collectParams xs; collectFnBody b
|
||||
| (Decl.extern _ xs _) := collectParams xs
|
||||
|
||||
end MaxVar
|
||||
|
||||
def FnBody.maxVar (b : FnBody) : Index :=
|
||||
MaxVar.collectFnBody b 0
|
||||
|
||||
def Decl.maxVar (d : Decl) : Index :=
|
||||
MaxVar.collectDecl d 0
|
||||
|
||||
namespace HasIndex
|
||||
|
||||
def visitVar (w : Index) (x : VarId) : Bool := w == x.idx
|
||||
def visitJP (w : Index) (x : JoinPointId) : Bool := w == x.idx
|
||||
|
||||
def visitArg (w : Index) : Arg → Bool
|
||||
| (Arg.var x) := visitVar w x
|
||||
| _ := false
|
||||
|
||||
def visitArgs (w : Index) (xs : Array Arg) : Bool :=
|
||||
xs.any (visitArg w)
|
||||
|
||||
def visitParams (w : Index) (ps : Array Param) : Bool :=
|
||||
ps.any (λ p, w == p.x.idx)
|
||||
|
||||
def visitExpr (w : Index) : Expr → Bool
|
||||
| (Expr.ctor _ ys) := visitArgs w ys
|
||||
| (Expr.reset x) := visitVar w x
|
||||
| (Expr.reuse x _ _ ys) := visitVar w x || visitArgs w ys
|
||||
| (Expr.proj _ x) := visitVar w x
|
||||
| (Expr.uproj _ x) := visitVar w x
|
||||
| (Expr.sproj _ _ x) := visitVar w x
|
||||
| (Expr.fap _ ys) := visitArgs w ys
|
||||
| (Expr.pap _ ys) := visitArgs w ys
|
||||
| (Expr.ap x ys) := visitVar w x || visitArgs w ys
|
||||
| (Expr.box _ x) := visitVar w x
|
||||
| (Expr.unbox x) := visitVar w x
|
||||
| (Expr.lit v) := false
|
||||
| (Expr.isShared x) := visitVar w x
|
||||
| (Expr.isTaggedPtr x) := visitVar w x
|
||||
|
||||
partial def visitFnBody (w : Index) : FnBody → Bool
|
||||
| (FnBody.vdecl x _ v b) := visitExpr w v || (!visitVar w x && visitFnBody b)
|
||||
| (FnBody.jdecl j ys _ v b) := (!visitParams w ys && visitFnBody v) || (!visitJP w j && visitFnBody b)
|
||||
| (FnBody.set x _ y b) := visitVar w x || visitVar w y || visitFnBody b
|
||||
| (FnBody.uset x _ y b) := visitVar w x || visitVar w y || visitFnBody b
|
||||
| (FnBody.sset x _ _ y _ b) := visitVar w x || visitVar w y || visitFnBody b
|
||||
| (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.mdata _ b) := visitFnBody b
|
||||
| (FnBody.jmp j ys) := visitJP w j || visitArgs w ys
|
||||
| (FnBody.ret x) := visitArg w x
|
||||
| (FnBody.case _ x alts) := visitVar w x || alts.any (λ alt, visitFnBody alt.body)
|
||||
| (FnBody.unreachable) := false
|
||||
|
||||
end HasIndex
|
||||
|
||||
def Arg.hasFreeVar (arg : Arg) (x : VarId) : Bool := HasIndex.visitArg x.idx arg
|
||||
def Expr.hasFreeVar (e : Expr) (x : VarId) : Bool := HasIndex.visitExpr x.idx e
|
||||
def FnBody.hasFreeVar (b : FnBody) (x : VarId) : Bool := HasIndex.visitFnBody x.idx b
|
||||
|
||||
end IR
|
||||
end Lean
|
||||
|
|
@ -5,6 +5,7 @@ Authors: Leonardo de Moura
|
|||
-/
|
||||
prelude
|
||||
import init.lean.compiler.ir.basic
|
||||
import init.lean.compiler.ir.freevars
|
||||
|
||||
namespace Lean
|
||||
namespace IR
|
||||
|
|
|
|||
|
|
@ -3,7 +3,10 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
|
|||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Leonardo de Moura
|
||||
-/
|
||||
import init.lean.compiler.ir.basic init.control.state
|
||||
prelude
|
||||
import init.control.state
|
||||
import init.lean.compiler.ir.basic
|
||||
import init.lean.compiler.ir.freevars
|
||||
|
||||
namespace Lean
|
||||
namespace IR
|
||||
|
|
|
|||
|
|
@ -1 +1 @@
|
|||
add_library (stage0 OBJECT ./init/coe.cpp ./init/control/alternative.cpp ./init/control/applicative.cpp ./init/control/combinators.cpp ./init/control/default.cpp ./init/control/estate.cpp ./init/control/except.cpp ./init/control/functor.cpp ./init/control/id.cpp ./init/control/lift.cpp ./init/control/monad.cpp ./init/control/monadfail.cpp ./init/control/option.cpp ./init/control/reader.cpp ./init/control/state.cpp ./init/core.cpp ./init/data/array/basic.cpp ./init/data/array/default.cpp ./init/data/assoclist.cpp ./init/data/basic.cpp ./init/data/char/basic.cpp ./init/data/char/default.cpp ./init/data/default.cpp ./init/data/dlist.cpp ./init/data/fin/basic.cpp ./init/data/fin/default.cpp ./init/data/hashable.cpp ./init/data/hashmap/basic.cpp ./init/data/hashmap/default.cpp ./init/data/int/basic.cpp ./init/data/int/default.cpp ./init/data/list/basic.cpp ./init/data/list/default.cpp ./init/data/list/instances.cpp ./init/data/nat/basic.cpp ./init/data/nat/bitwise.cpp ./init/data/nat/default.cpp ./init/data/nat/div.cpp ./init/data/option/basic.cpp ./init/data/option/instances.cpp ./init/data/ordering/basic.cpp ./init/data/ordering/default.cpp ./init/data/random.cpp ./init/data/rbmap/basic.cpp ./init/data/rbmap/default.cpp ./init/data/rbtree/basic.cpp ./init/data/rbtree/default.cpp ./init/data/repr.cpp ./init/data/string/basic.cpp ./init/data/string/default.cpp ./init/data/tostring.cpp ./init/data/uint.cpp ./init/default.cpp ./init/env_ext.cpp ./init/fix.cpp ./init/io.cpp ./init/lean/compiler/constfolding.cpp ./init/lean/compiler/default.cpp ./init/lean/compiler/ir/basic.cpp ./init/lean/compiler/ir/default.cpp ./init/lean/compiler/ir/elimdead.cpp ./init/lean/compiler/ir/format.cpp ./init/lean/compiler/ir/livevars.cpp ./init/lean/compiler/ir/normids.cpp ./init/lean/compiler/ir/pushproj.cpp ./init/lean/compiler/ir/resetreuse.cpp ./init/lean/compiler/ir/simpcase.cpp ./init/lean/compiler/util.cpp ./init/lean/config.cpp ./init/lean/declaration.cpp ./init/lean/default.cpp ./init/lean/disjoint_set.cpp ./init/lean/elaborator.cpp ./init/lean/expander.cpp ./init/lean/expr.cpp ./init/lean/extern.cpp ./init/lean/format.cpp ./init/lean/frontend.cpp ./init/lean/kvmap.cpp ./init/lean/level.cpp ./init/lean/message.cpp ./init/lean/name.cpp ./init/lean/name_mangling.cpp ./init/lean/options.cpp ./init/lean/parser/basic.cpp ./init/lean/parser/combinators.cpp ./init/lean/parser/command.cpp ./init/lean/parser/declaration.cpp ./init/lean/parser/identifier.cpp ./init/lean/parser/level.cpp ./init/lean/parser/module.cpp ./init/lean/parser/notation.cpp ./init/lean/parser/parsec.cpp ./init/lean/parser/pratt.cpp ./init/lean/parser/rec.cpp ./init/lean/parser/stringliteral.cpp ./init/lean/parser/syntax.cpp ./init/lean/parser/term.cpp ./init/lean/parser/token.cpp ./init/lean/parser/trie.cpp ./init/lean/position.cpp ./init/lean/trace.cpp ./init/lean/util.cpp ./init/platform.cpp ./init/util.cpp ./init/wf.cpp)
|
||||
add_library (stage0 OBJECT ./init/coe.cpp ./init/control/alternative.cpp ./init/control/applicative.cpp ./init/control/combinators.cpp ./init/control/default.cpp ./init/control/estate.cpp ./init/control/except.cpp ./init/control/functor.cpp ./init/control/id.cpp ./init/control/lift.cpp ./init/control/monad.cpp ./init/control/monadfail.cpp ./init/control/option.cpp ./init/control/reader.cpp ./init/control/state.cpp ./init/core.cpp ./init/data/array/basic.cpp ./init/data/array/default.cpp ./init/data/assoclist.cpp ./init/data/basic.cpp ./init/data/char/basic.cpp ./init/data/char/default.cpp ./init/data/default.cpp ./init/data/dlist.cpp ./init/data/fin/basic.cpp ./init/data/fin/default.cpp ./init/data/hashable.cpp ./init/data/hashmap/basic.cpp ./init/data/hashmap/default.cpp ./init/data/int/basic.cpp ./init/data/int/default.cpp ./init/data/list/basic.cpp ./init/data/list/default.cpp ./init/data/list/instances.cpp ./init/data/nat/basic.cpp ./init/data/nat/bitwise.cpp ./init/data/nat/default.cpp ./init/data/nat/div.cpp ./init/data/option/basic.cpp ./init/data/option/instances.cpp ./init/data/ordering/basic.cpp ./init/data/ordering/default.cpp ./init/data/random.cpp ./init/data/rbmap/basic.cpp ./init/data/rbmap/default.cpp ./init/data/rbtree/basic.cpp ./init/data/rbtree/default.cpp ./init/data/repr.cpp ./init/data/string/basic.cpp ./init/data/string/default.cpp ./init/data/tostring.cpp ./init/data/uint.cpp ./init/default.cpp ./init/env_ext.cpp ./init/fix.cpp ./init/io.cpp ./init/lean/compiler/constfolding.cpp ./init/lean/compiler/default.cpp ./init/lean/compiler/ir/basic.cpp ./init/lean/compiler/ir/default.cpp ./init/lean/compiler/ir/elimdead.cpp ./init/lean/compiler/ir/format.cpp ./init/lean/compiler/ir/freevars.cpp ./init/lean/compiler/ir/livevars.cpp ./init/lean/compiler/ir/normids.cpp ./init/lean/compiler/ir/pushproj.cpp ./init/lean/compiler/ir/resetreuse.cpp ./init/lean/compiler/ir/simpcase.cpp ./init/lean/compiler/util.cpp ./init/lean/config.cpp ./init/lean/declaration.cpp ./init/lean/default.cpp ./init/lean/disjoint_set.cpp ./init/lean/elaborator.cpp ./init/lean/expander.cpp ./init/lean/expr.cpp ./init/lean/extern.cpp ./init/lean/format.cpp ./init/lean/frontend.cpp ./init/lean/kvmap.cpp ./init/lean/level.cpp ./init/lean/message.cpp ./init/lean/name.cpp ./init/lean/name_mangling.cpp ./init/lean/options.cpp ./init/lean/parser/basic.cpp ./init/lean/parser/combinators.cpp ./init/lean/parser/command.cpp ./init/lean/parser/declaration.cpp ./init/lean/parser/identifier.cpp ./init/lean/parser/level.cpp ./init/lean/parser/module.cpp ./init/lean/parser/notation.cpp ./init/lean/parser/parsec.cpp ./init/lean/parser/pratt.cpp ./init/lean/parser/rec.cpp ./init/lean/parser/stringliteral.cpp ./init/lean/parser/syntax.cpp ./init/lean/parser/term.cpp ./init/lean/parser/token.cpp ./init/lean/parser/trie.cpp ./init/lean/position.cpp ./init/lean/trace.cpp ./init/lean/util.cpp ./init/platform.cpp ./init/util.cpp ./init/wf.cpp)
|
||||
|
|
|
|||
4261
src/stage0/init/lean/compiler/ir/basic.cpp
generated
4261
src/stage0/init/lean/compiler/ir/basic.cpp
generated
File diff suppressed because it is too large
Load diff
9
src/stage0/init/lean/compiler/ir/elimdead.cpp
generated
9
src/stage0/init/lean/compiler/ir/elimdead.cpp
generated
|
|
@ -1,6 +1,6 @@
|
|||
// Lean compiler output
|
||||
// Module: init.lean.compiler.ir.elimdead
|
||||
// Imports: init.lean.compiler.ir.basic
|
||||
// Imports: init.lean.compiler.ir.basic init.lean.compiler.ir.freevars
|
||||
#include "runtime/object.h"
|
||||
#include "runtime/apply.h"
|
||||
typedef lean::object obj; typedef lean::usize usize;
|
||||
|
|
@ -26,7 +26,6 @@ obj* l_Lean_IR_reshapeWithoutDeadAux(obj*, obj*, obj*);
|
|||
obj* l_Array_back___at_Lean_IR_reshapeWithoutDeadAux___main___spec__1___boxed(obj*);
|
||||
obj* l_Lean_IR_FnBody_elimDead___main(obj*);
|
||||
obj* l_Lean_IR_FnBody_freeVars(obj*);
|
||||
obj* l_RBNode_findCore___main___at___private_init_lean_compiler_ir_basic_2__collectIndex___spec__1(obj*, obj*);
|
||||
obj* l_Lean_IR_reshapeWithoutDeadAux___main(obj*, obj*, obj*);
|
||||
namespace lean {
|
||||
uint8 nat_dec_lt(obj*, obj*);
|
||||
|
|
@ -38,6 +37,7 @@ obj* nat_add(obj*, obj*);
|
|||
}
|
||||
uint8 l_Array_isEmpty___rarg(obj*);
|
||||
obj* l_Lean_IR_Decl_elimDead___main(obj*);
|
||||
obj* l_RBNode_findCore___main___at___private_init_lean_compiler_ir_freevars_2__collectIndex___spec__1(obj*, obj*);
|
||||
obj* l_Array_hmmapAux___main___at_Lean_IR_FnBody_elimDead___main___spec__2(obj*, obj*);
|
||||
obj* l_Lean_IR_FnBody_setBody___main(obj*, obj*);
|
||||
obj* l_Lean_IR_FnBody_elimDead(obj*);
|
||||
|
|
@ -107,7 +107,7 @@ lbl_9:
|
|||
{
|
||||
obj* x_21;
|
||||
lean::inc(x_2);
|
||||
x_21 = l_RBNode_findCore___main___at___private_init_lean_compiler_ir_basic_2__collectIndex___spec__1(x_2, x_8);
|
||||
x_21 = l_RBNode_findCore___main___at___private_init_lean_compiler_ir_freevars_2__collectIndex___spec__1(x_2, x_8);
|
||||
lean::dec(x_8);
|
||||
if (lean::obj_tag(x_21) == 0)
|
||||
{
|
||||
|
|
@ -418,12 +418,15 @@ return x_1;
|
|||
}
|
||||
}
|
||||
obj* initialize_init_lean_compiler_ir_basic(obj*);
|
||||
obj* initialize_init_lean_compiler_ir_freevars(obj*);
|
||||
static bool _G_initialized = false;
|
||||
obj* initialize_init_lean_compiler_ir_elimdead(obj* w) {
|
||||
if (_G_initialized) return w;
|
||||
_G_initialized = true;
|
||||
if (io_result_is_error(w)) return w;
|
||||
w = initialize_init_lean_compiler_ir_basic(w);
|
||||
if (io_result_is_error(w)) return w;
|
||||
w = initialize_init_lean_compiler_ir_freevars(w);
|
||||
if (io_result_is_error(w)) return w;
|
||||
l_Array_hmmapAux___main___at_Lean_IR_FnBody_elimDead___main___spec__2___closed__1 = _init_l_Array_hmmapAux___main___at_Lean_IR_FnBody_elimDead___main___spec__2___closed__1();
|
||||
lean::mark_persistent(l_Array_hmmapAux___main___at_Lean_IR_FnBody_elimDead___main___spec__2___closed__1);
|
||||
|
|
|
|||
4299
src/stage0/init/lean/compiler/ir/freevars.cpp
generated
Normal file
4299
src/stage0/init/lean/compiler/ir/freevars.cpp
generated
Normal file
File diff suppressed because it is too large
Load diff
21
src/stage0/init/lean/compiler/ir/pushproj.cpp
generated
21
src/stage0/init/lean/compiler/ir/pushproj.cpp
generated
|
|
@ -1,6 +1,6 @@
|
|||
// Lean compiler output
|
||||
// Module: init.lean.compiler.ir.pushproj
|
||||
// Imports: init.lean.compiler.ir.basic
|
||||
// Imports: init.lean.compiler.ir.basic init.lean.compiler.ir.freevars
|
||||
#include "runtime/object.h"
|
||||
#include "runtime/apply.h"
|
||||
typedef lean::object obj; typedef lean::usize usize;
|
||||
|
|
@ -26,11 +26,9 @@ obj* l_Lean_IR_pushProjs___main___closed__1;
|
|||
obj* l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__4___boxed(obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_Lean_IR_Decl_pushProj___main(obj*);
|
||||
obj* l_Lean_IR_FnBody_freeVars(obj*);
|
||||
obj* l_RBNode_findCore___main___at___private_init_lean_compiler_ir_basic_2__collectIndex___spec__1(obj*, obj*);
|
||||
obj* l_Lean_IR_reshape(obj*, obj*);
|
||||
uint8 l_Array_anyAux___main___at_Lean_IR_pushProjs___main___spec__2(obj*, obj*, obj*, obj*);
|
||||
obj* l_Lean_IR_FnBody_pushProj(obj*);
|
||||
obj* l_RBNode_insert___at___private_init_lean_compiler_ir_basic_2__collectIndex___spec__2(obj*, obj*, obj*);
|
||||
namespace lean {
|
||||
uint8 nat_dec_lt(obj*, obj*);
|
||||
}
|
||||
|
|
@ -47,7 +45,9 @@ obj* l_Array_reverseAux___main___rarg(obj*, obj*);
|
|||
obj* l_Lean_IR_AltCore_body___main(obj*);
|
||||
obj* l_Lean_IR_pushProjs___main(obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_Array_back___at_Lean_IR_pushProjs___main___spec__1(obj*);
|
||||
obj* l_RBNode_findCore___main___at___private_init_lean_compiler_ir_freevars_2__collectIndex___spec__1(obj*, obj*);
|
||||
obj* l_Array_hmmapAux___main___at_Lean_IR_FnBody_pushProj___main___spec__1(obj*, obj*);
|
||||
obj* l_RBNode_insert___at___private_init_lean_compiler_ir_freevars_2__collectIndex___spec__2(obj*, obj*, obj*);
|
||||
obj* l_Lean_IR_FnBody_setBody___main(obj*, obj*);
|
||||
obj* l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__4(obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_Array_miterateAux___main___at_Lean_IR_FnBody_pushProj___main___spec__2(obj*, obj*, obj*, obj*);
|
||||
|
|
@ -90,7 +90,7 @@ else
|
|||
{
|
||||
obj* x_9; obj* x_10;
|
||||
x_9 = lean::array_fget(x_2, x_3);
|
||||
x_10 = l_RBNode_findCore___main___at___private_init_lean_compiler_ir_basic_2__collectIndex___spec__1(x_9, x_1);
|
||||
x_10 = l_RBNode_findCore___main___at___private_init_lean_compiler_ir_freevars_2__collectIndex___spec__1(x_9, x_1);
|
||||
if (lean::obj_tag(x_10) == 0)
|
||||
{
|
||||
uint8 x_12;
|
||||
|
|
@ -159,7 +159,7 @@ if (lean::is_exclusive(x_11)) {
|
|||
}
|
||||
x_21 = l_Lean_IR_vsetInh;
|
||||
x_22 = lean::array_get(x_21, x_0, x_4);
|
||||
x_23 = l_RBNode_findCore___main___at___private_init_lean_compiler_ir_basic_2__collectIndex___spec__1(x_22, x_3);
|
||||
x_23 = l_RBNode_findCore___main___at___private_init_lean_compiler_ir_freevars_2__collectIndex___spec__1(x_22, x_3);
|
||||
if (lean::obj_tag(x_23) == 0)
|
||||
{
|
||||
obj* x_24; obj* x_25;
|
||||
|
|
@ -210,7 +210,7 @@ if (lean::is_exclusive(x_11)) {
|
|||
}
|
||||
x_38 = l_Lean_IR_vsetInh;
|
||||
x_39 = lean::array_get(x_38, x_0, x_4);
|
||||
x_40 = l_RBNode_findCore___main___at___private_init_lean_compiler_ir_basic_2__collectIndex___spec__1(x_39, x_3);
|
||||
x_40 = l_RBNode_findCore___main___at___private_init_lean_compiler_ir_freevars_2__collectIndex___spec__1(x_39, x_3);
|
||||
if (lean::obj_tag(x_40) == 0)
|
||||
{
|
||||
obj* x_41; obj* x_42;
|
||||
|
|
@ -270,7 +270,7 @@ x_12 = lean::array_fset(x_4, x_3, x_11);
|
|||
x_13 = lean::mk_nat_obj(1ul);
|
||||
x_14 = lean::nat_add(x_3, x_13);
|
||||
lean::inc(x_10);
|
||||
x_16 = l_RBNode_findCore___main___at___private_init_lean_compiler_ir_basic_2__collectIndex___spec__1(x_10, x_2);
|
||||
x_16 = l_RBNode_findCore___main___at___private_init_lean_compiler_ir_freevars_2__collectIndex___spec__1(x_10, x_2);
|
||||
if (lean::obj_tag(x_16) == 0)
|
||||
{
|
||||
obj* x_17;
|
||||
|
|
@ -327,7 +327,7 @@ lean::dec(x_12);
|
|||
x_15 = lean::cnstr_get(x_6, 0);
|
||||
lean::inc(x_15);
|
||||
lean::inc(x_4);
|
||||
x_18 = l_RBNode_findCore___main___at___private_init_lean_compiler_ir_basic_2__collectIndex___spec__1(x_4, x_15);
|
||||
x_18 = l_RBNode_findCore___main___at___private_init_lean_compiler_ir_freevars_2__collectIndex___spec__1(x_4, x_15);
|
||||
if (lean::obj_tag(x_18) == 0)
|
||||
{
|
||||
obj* x_19; obj* x_20; uint8 x_21;
|
||||
|
|
@ -703,7 +703,7 @@ x_19 = l_Array_miterateAux___main___at_Lean_IR_FnBody_pushProj___main___spec__2(
|
|||
x_20 = lean::box(0);
|
||||
x_21 = lean::box(0);
|
||||
lean::inc(x_11);
|
||||
x_23 = l_RBNode_insert___at___private_init_lean_compiler_ir_basic_2__collectIndex___spec__2(x_20, x_11, x_21);
|
||||
x_23 = l_RBNode_insert___at___private_init_lean_compiler_ir_freevars_2__collectIndex___spec__2(x_20, x_11, x_21);
|
||||
x_24 = l_Array_empty___closed__1;
|
||||
x_25 = l_Lean_IR_pushProjs___main(x_8, x_13, x_19, x_24, x_23);
|
||||
x_26 = lean::cnstr_get(x_25, 0);
|
||||
|
|
@ -797,12 +797,15 @@ return x_1;
|
|||
}
|
||||
}
|
||||
obj* initialize_init_lean_compiler_ir_basic(obj*);
|
||||
obj* initialize_init_lean_compiler_ir_freevars(obj*);
|
||||
static bool _G_initialized = false;
|
||||
obj* initialize_init_lean_compiler_ir_pushproj(obj* w) {
|
||||
if (_G_initialized) return w;
|
||||
_G_initialized = true;
|
||||
if (io_result_is_error(w)) return w;
|
||||
w = initialize_init_lean_compiler_ir_basic(w);
|
||||
if (io_result_is_error(w)) return w;
|
||||
w = initialize_init_lean_compiler_ir_freevars(w);
|
||||
if (io_result_is_error(w)) return w;
|
||||
l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__3___closed__1 = _init_l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__3___closed__1();
|
||||
lean::mark_persistent(l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__3___closed__1);
|
||||
|
|
|
|||
10
src/stage0/init/lean/compiler/ir/resetreuse.cpp
generated
10
src/stage0/init/lean/compiler/ir/resetreuse.cpp
generated
|
|
@ -1,6 +1,6 @@
|
|||
// Lean compiler output
|
||||
// Module: init.lean.compiler.ir.resetreuse
|
||||
// Imports: init.default init.lean.compiler.ir.basic init.control.state
|
||||
// Imports: init.control.state init.lean.compiler.ir.basic init.lean.compiler.ir.freevars
|
||||
#include "runtime/object.h"
|
||||
#include "runtime/apply.h"
|
||||
typedef lean::object obj; typedef lean::usize usize;
|
||||
|
|
@ -1506,19 +1506,19 @@ x_1 = l_Lean_IR_Decl_insertResetReuse___main(x_0);
|
|||
return x_1;
|
||||
}
|
||||
}
|
||||
obj* initialize_init_default(obj*);
|
||||
obj* initialize_init_lean_compiler_ir_basic(obj*);
|
||||
obj* initialize_init_control_state(obj*);
|
||||
obj* initialize_init_lean_compiler_ir_basic(obj*);
|
||||
obj* initialize_init_lean_compiler_ir_freevars(obj*);
|
||||
static bool _G_initialized = false;
|
||||
obj* initialize_init_lean_compiler_ir_resetreuse(obj* w) {
|
||||
if (_G_initialized) return w;
|
||||
_G_initialized = true;
|
||||
if (io_result_is_error(w)) return w;
|
||||
w = initialize_init_default(w);
|
||||
w = initialize_init_control_state(w);
|
||||
if (io_result_is_error(w)) return w;
|
||||
w = initialize_init_lean_compiler_ir_basic(w);
|
||||
if (io_result_is_error(w)) return w;
|
||||
w = initialize_init_control_state(w);
|
||||
w = initialize_init_lean_compiler_ir_freevars(w);
|
||||
if (io_result_is_error(w)) return w;
|
||||
l_Array_hmmapAux___main___at___private_init_lean_compiler_ir_resetreuse_2__S___main___spec__1___closed__1 = _init_l_Array_hmmapAux___main___at___private_init_lean_compiler_ir_resetreuse_2__S___main___spec__1___closed__1();
|
||||
lean::mark_persistent(l_Array_hmmapAux___main___at___private_init_lean_compiler_ir_resetreuse_2__S___main___spec__1___closed__1);
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue