chore(library/init/lean/compiler/ir): Context ==> LocalContext
This commit is contained in:
Leonardo de Moura
parent
c9bcd4990c
commit
d2f6befc15
5 changed files with 39 additions and 39 deletions
|
|
@ -398,60 +398,60 @@ partial def FnBody.isPure : FnBody → Bool
|
|||
abbrev IndexSet := RBTree Index Index.lt
|
||||
instance vsetInh : Inhabited IndexSet := ⟨{}⟩
|
||||
|
||||
inductive ContextEntry
|
||||
| param : IRType → ContextEntry
|
||||
| localVar : IRType → Expr → ContextEntry
|
||||
| joinPoint : Array Param → FnBody → ContextEntry
|
||||
inductive LocalContextEntry
|
||||
| param : IRType → LocalContextEntry
|
||||
| localVar : IRType → Expr → LocalContextEntry
|
||||
| joinPoint : Array Param → FnBody → LocalContextEntry
|
||||
|
||||
abbrev Context := RBMap Index ContextEntry Index.lt
|
||||
abbrev LocalContext := RBMap Index LocalContextEntry Index.lt
|
||||
|
||||
def Context.addLocal (ctx : Context) (x : VarId) (t : IRType) (v : Expr) : Context :=
|
||||
ctx.insert x.idx (ContextEntry.localVar t v)
|
||||
def LocalContext.addLocal (ctx : LocalContext) (x : VarId) (t : IRType) (v : Expr) : LocalContext :=
|
||||
ctx.insert x.idx (LocalContextEntry.localVar t v)
|
||||
|
||||
def Context.addJP (ctx : Context) (j : JoinPointId) (xs : Array Param) (b : FnBody) : Context :=
|
||||
ctx.insert j.idx (ContextEntry.joinPoint xs b)
|
||||
def LocalContext.addJP (ctx : LocalContext) (j : JoinPointId) (xs : Array Param) (b : FnBody) : LocalContext :=
|
||||
ctx.insert j.idx (LocalContextEntry.joinPoint xs b)
|
||||
|
||||
def Context.addParam (ctx : Context) (p : Param) : Context :=
|
||||
ctx.insert p.x.idx (ContextEntry.param p.ty)
|
||||
def LocalContext.addParam (ctx : LocalContext) (p : Param) : LocalContext :=
|
||||
ctx.insert p.x.idx (LocalContextEntry.param p.ty)
|
||||
|
||||
def Context.addParams (ctx : Context) (ps : Array Param) : Context :=
|
||||
ps.foldl Context.addParam ctx
|
||||
def LocalContext.addParams (ctx : LocalContext) (ps : Array Param) : LocalContext :=
|
||||
ps.foldl LocalContext.addParam ctx
|
||||
|
||||
def Context.isJP (ctx : Context) (idx : Index) : Bool :=
|
||||
def LocalContext.isJP (ctx : LocalContext) (idx : Index) : Bool :=
|
||||
match ctx.find idx with
|
||||
| some (ContextEntry.joinPoint _ _) := true
|
||||
| some (LocalContextEntry.joinPoint _ _) := true
|
||||
| other := false
|
||||
|
||||
def Context.getJPBody (ctx : Context) (j : JoinPointId) : Option FnBody :=
|
||||
def LocalContext.getJPBody (ctx : LocalContext) (j : JoinPointId) : Option FnBody :=
|
||||
match ctx.find j.idx with
|
||||
| some (ContextEntry.joinPoint _ b) := some b
|
||||
| some (LocalContextEntry.joinPoint _ b) := some b
|
||||
| other := none
|
||||
|
||||
def Context.getJPParams (ctx : Context) (j : JoinPointId) : Option (Array Param) :=
|
||||
def LocalContext.getJPParams (ctx : LocalContext) (j : JoinPointId) : Option (Array Param) :=
|
||||
match ctx.find j.idx with
|
||||
| some (ContextEntry.joinPoint ys _) := some ys
|
||||
| some (LocalContextEntry.joinPoint ys _) := some ys
|
||||
| other := none
|
||||
|
||||
def Context.isParam (ctx : Context) (idx : Index) : Bool :=
|
||||
def LocalContext.isParam (ctx : LocalContext) (idx : Index) : Bool :=
|
||||
match ctx.find idx with
|
||||
| some (ContextEntry.param _) := true
|
||||
| some (LocalContextEntry.param _) := true
|
||||
| other := false
|
||||
|
||||
def Context.isLocalVar (ctx : Context) (idx : Index) : Bool :=
|
||||
def LocalContext.isLocalVar (ctx : LocalContext) (idx : Index) : Bool :=
|
||||
match ctx.find idx with
|
||||
| some (ContextEntry.localVar _ _) := true
|
||||
| some (LocalContextEntry.localVar _ _) := true
|
||||
| other := false
|
||||
|
||||
def Context.contains (ctx : Context) (idx : Index) : Bool :=
|
||||
def LocalContext.contains (ctx : LocalContext) (idx : Index) : Bool :=
|
||||
ctx.contains idx
|
||||
|
||||
def Context.eraseJoinPointDecl (ctx : Context) (j : JoinPointId) : Context :=
|
||||
def LocalContext.eraseJoinPointDecl (ctx : LocalContext) (j : JoinPointId) : LocalContext :=
|
||||
ctx.erase j.idx
|
||||
|
||||
def Context.getType (ctx : Context) (x : VarId) : Option IRType :=
|
||||
def LocalContext.getType (ctx : LocalContext) (x : VarId) : Option IRType :=
|
||||
match ctx.find x.idx with
|
||||
| some (ContextEntry.param t) := some t
|
||||
| some (ContextEntry.localVar t _) := some t
|
||||
| some (LocalContextEntry.param t) := some t
|
||||
| some (LocalContextEntry.localVar t _) := some t
|
||||
| other := none
|
||||
|
||||
abbrev IndexRenaming := RBMap Index Index Index.lt
|
||||
|
|
|
|||
|
|
@ -48,7 +48,7 @@ def eqvTypes (t₁ t₂ : IRType) : Bool :=
|
|||
(t₁.isScalar == t₂.isScalar) && (!t₁.isScalar || t₁ == t₂)
|
||||
|
||||
structure Env :=
|
||||
(ctx: Context) (resultType : IRType) (decls : FunId → Decl)
|
||||
(ctx: LocalContext) (resultType : IRType) (decls : FunId → Decl)
|
||||
|
||||
abbrev M := ReaderT Env (StateT Index Id)
|
||||
|
||||
|
|
@ -57,7 +57,7 @@ do idx ← getModify (+1),
|
|||
pure { idx := idx }
|
||||
|
||||
def getEnv : M Env := read
|
||||
def getCtx : M Context := Env.ctx <$> getEnv
|
||||
def getCtx : M LocalContext := Env.ctx <$> getEnv
|
||||
def getResultType : M IRType := Env.resultType <$> getEnv
|
||||
def getVarType (x : VarId) : M IRType :=
|
||||
do ctx ← getCtx,
|
||||
|
|
|
|||
|
|
@ -11,7 +11,7 @@ namespace IR
|
|||
|
||||
namespace Checker
|
||||
|
||||
abbrev M := ExceptT String (ReaderT Context Id)
|
||||
abbrev M := ExceptT String (ReaderT LocalContext Id)
|
||||
|
||||
def checkVar (x : VarId) : M Unit :=
|
||||
do ctx ← read,
|
||||
|
|
@ -67,7 +67,7 @@ def checkExpr (ty : IRType) : Expr → M Unit
|
|||
|
||||
@[inline] def withParams (ps : Array Param) (k : M Unit) : M Unit :=
|
||||
do ctx ← read,
|
||||
ctx ← ps.mfoldl (λ (ctx : Context) p, do
|
||||
ctx ← ps.mfoldl (λ (ctx : LocalContext) p, do
|
||||
when (ctx.contains p.x.idx) $ throw ("invalid parameter declaration, shadowing is not allowed"),
|
||||
pure $ ctx.addParam p) ctx,
|
||||
adaptReader (λ _, ctx) k
|
||||
|
|
@ -79,12 +79,12 @@ partial def checkFnBody : FnBody → M Unit
|
|||
checkExpr t v,
|
||||
ctx ← read,
|
||||
when (ctx.contains x.idx) $ throw ("invalid variable declaration, shadowing is not allowed"),
|
||||
adaptReader (λ ctx : Context, ctx.addLocal x t v) (checkFnBody b)
|
||||
adaptReader (λ ctx : LocalContext, ctx.addLocal x t v) (checkFnBody b)
|
||||
| (FnBody.jdecl j ys v b) := do
|
||||
withParams ys (checkFnBody v),
|
||||
ctx ← read,
|
||||
when (ctx.contains j.idx) $ throw ("invalid join point declaration, shadowing is not allowed"),
|
||||
adaptReader (λ ctx : Context, ctx.addJP j ys v) (checkFnBody b)
|
||||
adaptReader (λ ctx : LocalContext, ctx.addJP j ys v) (checkFnBody b)
|
||||
| (FnBody.set x _ y b) := checkVar x *> checkVar y *> checkFnBody b
|
||||
| (FnBody.uset x _ y b) := checkVar x *> checkVar y *> checkFnBody b
|
||||
| (FnBody.sset x _ _ y _ b) := checkVar x *> checkVar y *> checkFnBody b
|
||||
|
|
|
|||
|
|
@ -38,7 +38,7 @@ namespace IsLive
|
|||
Remark: we don't need to track local join points because we assume there is
|
||||
no variable or join point shadowing in our IR.
|
||||
-/
|
||||
abbrev M := State Context
|
||||
abbrev M := State LocalContext
|
||||
|
||||
@[inline] def visitVar (w : Index) (x : VarId) : M Bool := pure (HasIndex.visitVar w x)
|
||||
@[inline] def visitJP (w : Index) (x : JoinPointId) : M Bool := pure (HasIndex.visitJP w x)
|
||||
|
|
@ -81,7 +81,7 @@ end IsLive
|
|||
|
||||
Recall that we say that a join point `j` is free in `b` if `b` contains
|
||||
`FnBody.jmp j ys` and `j` is not local. -/
|
||||
def FnBody.hasLiveVar (b : FnBody) (ctx : Context) (x : VarId) : Bool :=
|
||||
def FnBody.hasLiveVar (b : FnBody) (ctx : LocalContext) (x : VarId) : Bool :=
|
||||
(IsLive.visitFnBody x.idx b).run' ctx
|
||||
|
||||
end IR
|
||||
|
|
|
|||
|
|
@ -55,7 +55,7 @@ private partial def S (w : VarId) (c : CtorInfo) : FnBody → FnBody
|
|||
instr <;> S b
|
||||
|
||||
/- We use `Context` to track join points in scope. -/
|
||||
abbrev M := ReaderT Context (StateT Index Id)
|
||||
abbrev M := ReaderT LocalContext (StateT Index Id)
|
||||
local attribute [instance] monadInhabited
|
||||
|
||||
private def mkFresh : M VarId :=
|
||||
|
|
@ -87,7 +87,7 @@ private partial def Dmain (x : VarId) (c : CtorInfo) : FnBody → M (FnBody × B
|
|||
pure (FnBody.case tid y alts, true)
|
||||
else pure (e, false)
|
||||
| (FnBody.jdecl j ys v b) := do
|
||||
(b, _) ← adaptReader (λ ctx : Context, ctx.addJP j ys v) (Dmain b),
|
||||
(b, _) ← adaptReader (λ ctx : LocalContext, ctx.addJP j ys v) (Dmain b),
|
||||
(v, found) ← Dmain v,
|
||||
/- If `found == true`, then `Dmain b` must also have returned `(b, true)` since
|
||||
we assume the IR does not have dead join points. So, if `x` is live in `j`,
|
||||
|
|
@ -138,7 +138,7 @@ partial def R : FnBody → M FnBody
|
|||
pure $ FnBody.case tid x alts
|
||||
| (FnBody.jdecl j ys v b) := do
|
||||
v ← R v,
|
||||
b ← adaptReader (λ ctx : Context, ctx.addJP j ys v) (R b),
|
||||
b ← adaptReader (λ ctx : LocalContext, ctx.addJP j ys v) (R b),
|
||||
pure $ FnBody.jdecl j ys v b
|
||||
| e := do
|
||||
if e.isTerminal then pure e
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue