Documentation

Lean.Compiler.IR.Basic

@[inline]

abbrev Lean.IR.FunId:

Type

Equations

Lean.IR.FunId = Lean.Name

@[inline]

abbrev Lean.IR.Index:

Type

Equations

Lean.IR.Index = Nat

structure Lean.IR.VarId:

Type

idx : Lean.IR.Index

instance Lean.IR.instInhabitedVarId:

Inhabited Lean.IR.VarId

Equations

Lean.IR.instInhabitedVarId = { default := { idx := default } }

structure Lean.IR.JoinPointId:

Type

idx : Lean.IR.Index

instance Lean.IR.instInhabitedJoinPointId:

Inhabited Lean.IR.JoinPointId

Equations

Lean.IR.instInhabitedJoinPointId = { default := { idx := default } }

@[inline]

abbrev Lean.IR.Index.lt (a : Lean.IR.Index) (b : Lean.IR.Index) :

Equations

Lean.IR.Index.lt a b = decide (a < b)

instance Lean.IR.instBEqVarId:

BEq Lean.IR.VarId

Equations

Lean.IR.instBEqVarId = { beq := fun a b => a.idx == b.idx }

instance Lean.IR.instToStringVarId:

ToString Lean.IR.VarId

Equations

Lean.IR.instToStringVarId = { toString := fun a => "x_" ++ toString a.idx }

instance Lean.IR.instToFormatVarId:

Lean.ToFormat Lean.IR.VarId

Equations

Lean.IR.instToFormatVarId = { format := fun a => Std.Format.text (toString a) }

instance Lean.IR.instHashableVarId:

Hashable Lean.IR.VarId

Equations

Lean.IR.instHashableVarId = { hash := fun a => hash a.idx }

instance Lean.IR.instBEqJoinPointId:

BEq Lean.IR.JoinPointId

Equations

Lean.IR.instBEqJoinPointId = { beq := fun a b => a.idx == b.idx }

instance Lean.IR.instToStringJoinPointId:

ToString Lean.IR.JoinPointId

Equations

Lean.IR.instToStringJoinPointId = { toString := fun a => "block_" ++ toString a.idx }

instance Lean.IR.instToFormatJoinPointId:

Lean.ToFormat Lean.IR.JoinPointId

Equations

Lean.IR.instToFormatJoinPointId = { format := fun a => Std.Format.text (toString a) }

instance Lean.IR.instHashableJoinPointId:

Hashable Lean.IR.JoinPointId

Equations

Lean.IR.instHashableJoinPointId = { hash := fun a => hash a.idx }

@[inline]

abbrev Lean.IR.MData:

Type

Equations

Lean.IR.MData = Lean.KVMap

@[inline]

abbrev Lean.IR.MData.empty:

Equations

Lean.IR.MData.empty = { entries := [] }

inductive Lean.IR.IRType:

Type

float: Lean.IR.IRType
uint8: Lean.IR.IRType
uint16: Lean.IR.IRType
uint32: Lean.IR.IRType
uint64: Lean.IR.IRType
usize: Lean.IR.IRType
irrelevant: Lean.IR.IRType
object: Lean.IR.IRType
tobject: Lean.IR.IRType
struct: Option Lean.Name → Array Lean.IR.IRType → Lean.IR.IRType
union: Lean.Name → Array Lean.IR.IRType → Lean.IR.IRType

instance Lean.IR.instInhabitedIRType:

Inhabited Lean.IR.IRType

Equations

Lean.IR.instInhabitedIRType = { default := Lean.IR.IRType.float }

partial def Lean.IR.IRType.beq:

Lean.IR.IRType → Lean.IR.IRType → Bool

instance Lean.IR.IRType.instBEqIRType:

BEq Lean.IR.IRType

Equations

Lean.IR.IRType.instBEqIRType = { beq := Lean.IR.IRType.beq }

def Lean.IR.IRType.isScalar:

Lean.IR.IRType → Bool

Equations

One or more equations did not get rendered due to their size.

def Lean.IR.IRType.isObj:

Lean.IR.IRType → Bool

Equations

Lean.IR.IRType.isObj _fun_discr = match _fun_discr with | Lean.IR.IRType.object => true | Lean.IR.IRType.tobject => true | x => false

def Lean.IR.IRType.isIrrelevant:

Lean.IR.IRType → Bool

Equations

Lean.IR.IRType.isIrrelevant _fun_discr = match _fun_discr with | Lean.IR.IRType.irrelevant => true | x => false

def Lean.IR.IRType.isStruct:

Lean.IR.IRType → Bool

Equations

Lean.IR.IRType.isStruct _fun_discr = match _fun_discr with | Lean.IR.IRType.struct leanTypeName types => true | x => false

def Lean.IR.IRType.isUnion:

Lean.IR.IRType → Bool

Equations

Lean.IR.IRType.isUnion _fun_discr = match _fun_discr with | Lean.IR.IRType.union leanTypeName types => true | x => false

inductive Lean.IR.Arg:

Type

var: Lean.IR.VarId → Lean.IR.Arg
irrelevant: Lean.IR.Arg

instance Lean.IR.instInhabitedArg:

Inhabited Lean.IR.Arg

Equations

Lean.IR.instInhabitedArg = { default := Lean.IR.Arg.var default }

def Lean.IR.Arg.beq:

Lean.IR.Arg → Lean.IR.Arg → Bool

Equations

One or more equations did not get rendered due to their size.

instance Lean.IR.instBEqArg:

BEq Lean.IR.Arg

Equations

Lean.IR.instBEqArg = { beq := Lean.IR.Arg.beq }

@[export lean_ir_mk_var_arg]

def Lean.IR.mkVarArg (id : Lean.IR.VarId) :

Equations

Lean.IR.mkVarArg id = Lean.IR.Arg.var id

inductive Lean.IR.LitVal:

Type

num: Nat → Lean.IR.LitVal
str: String → Lean.IR.LitVal

def Lean.IR.LitVal.beq:

Lean.IR.LitVal → Lean.IR.LitVal → Bool

Equations

One or more equations did not get rendered due to their size.

instance Lean.IR.instBEqLitVal:

BEq Lean.IR.LitVal

Equations

Lean.IR.instBEqLitVal = { beq := Lean.IR.LitVal.beq }

structure Lean.IR.CtorInfo:

Type

name : Lean.Name
cidx : Nat
size : Nat
usize : Nat
ssize : Nat

instance Lean.IR.instReprCtorInfo:

Repr Lean.IR.CtorInfo

Equations

Lean.IR.instReprCtorInfo = { reprPrec := [anonymous] }

def Lean.IR.CtorInfo.beq:

Lean.IR.CtorInfo → Lean.IR.CtorInfo → Bool

Equations

One or more equations did not get rendered due to their size.

instance Lean.IR.instBEqCtorInfo:

BEq Lean.IR.CtorInfo

Equations

Lean.IR.instBEqCtorInfo = { beq := Lean.IR.CtorInfo.beq }

def Lean.IR.CtorInfo.isRef (info : Lean.IR.CtorInfo) :

Equations

Lean.IR.CtorInfo.isRef info = (decide (info.size > 0) || decide (info.usize > 0) || decide (info.ssize > 0))

def Lean.IR.CtorInfo.isScalar (info : Lean.IR.CtorInfo) :

Equations

Lean.IR.CtorInfo.isScalar info = !Lean.IR.CtorInfo.isRef info

inductive Lean.IR.Expr:

Type

ctor: Lean.IR.CtorInfo → Array Lean.IR.Arg → Lean.IR.Expr
reset: Nat → Lean.IR.VarId → Lean.IR.Expr
reuse: Lean.IR.VarId → Lean.IR.CtorInfo → Bool → Array Lean.IR.Arg → Lean.IR.Expr
proj: Nat → Lean.IR.VarId → Lean.IR.Expr
uproj: Nat → Lean.IR.VarId → Lean.IR.Expr
sproj: Nat → Nat → Lean.IR.VarId → Lean.IR.Expr
fap: Lean.IR.FunId → Array Lean.IR.Arg → Lean.IR.Expr
pap: Lean.IR.FunId → Array Lean.IR.Arg → Lean.IR.Expr
ap: Lean.IR.VarId → Array Lean.IR.Arg → Lean.IR.Expr
box: Lean.IR.IRType → Lean.IR.VarId → Lean.IR.Expr
unbox: Lean.IR.VarId → Lean.IR.Expr
lit: Lean.IR.LitVal → Lean.IR.Expr
isShared: Lean.IR.VarId → Lean.IR.Expr
isTaggedPtr: Lean.IR.VarId → Lean.IR.Expr

@[export lean_ir_mk_ctor_expr]

def Lean.IR.mkCtorExpr (n : Lean.Name) (cidx : Nat) (size : Nat) (usize : Nat) (ssize : Nat) (ys : Array Lean.IR.Arg) :

Equations

Lean.IR.mkCtorExpr n cidx size usize ssize ys = Lean.IR.Expr.ctor { name := n, cidx := cidx, size := size, usize := usize, ssize := ssize } ys

@[export lean_ir_mk_proj_expr]

def Lean.IR.mkProjExpr (i : Nat) (x : Lean.IR.VarId) :

Equations

Lean.IR.mkProjExpr i x = Lean.IR.Expr.proj i x

@[export lean_ir_mk_uproj_expr]

def Lean.IR.mkUProjExpr (i : Nat) (x : Lean.IR.VarId) :

Equations

Lean.IR.mkUProjExpr i x = Lean.IR.Expr.uproj i x

@[export lean_ir_mk_sproj_expr]

def Lean.IR.mkSProjExpr (n : Nat) (offset : Nat) (x : Lean.IR.VarId) :

Equations

Lean.IR.mkSProjExpr n offset x = Lean.IR.Expr.sproj n offset x

@[export lean_ir_mk_fapp_expr]

def Lean.IR.mkFAppExpr (c : Lean.IR.FunId) (ys : Array Lean.IR.Arg) :

Equations

Lean.IR.mkFAppExpr c ys = Lean.IR.Expr.fap c ys

@[export lean_ir_mk_papp_expr]

def Lean.IR.mkPAppExpr (c : Lean.IR.FunId) (ys : Array Lean.IR.Arg) :

Equations

Lean.IR.mkPAppExpr c ys = Lean.IR.Expr.pap c ys

@[export lean_ir_mk_app_expr]

def Lean.IR.mkAppExpr (x : Lean.IR.VarId) (ys : Array Lean.IR.Arg) :

Equations

Lean.IR.mkAppExpr x ys = Lean.IR.Expr.ap x ys

@[export lean_ir_mk_num_expr]

def Lean.IR.mkNumExpr (v : Nat) :

Equations

Lean.IR.mkNumExpr v = Lean.IR.Expr.lit (Lean.IR.LitVal.num v)

@[export lean_ir_mk_str_expr]

def Lean.IR.mkStrExpr (v : String) :

Equations

Lean.IR.mkStrExpr v = Lean.IR.Expr.lit (Lean.IR.LitVal.str v)

structure Lean.IR.Param:

Type

instance Lean.IR.instInhabitedParam:

Inhabited Lean.IR.Param

Equations

Lean.IR.instInhabitedParam = { default := { x := default, borrow := default, ty := default } }

@[export lean_ir_mk_param]

def Lean.IR.mkParam (x : Lean.IR.VarId) (borrow : Bool) (ty : Lean.IR.IRType) :

Equations

Lean.IR.mkParam x borrow ty = { x := x, borrow := borrow, ty := ty }

inductive Lean.IR.AltCore (FnBody : Type) :

Type

ctor: {FnBody : Type} → Lean.IR.CtorInfo → FnBody → Lean.IR.AltCore FnBody
default: {FnBody : Type} → FnBody → Lean.IR.AltCore FnBody

inductive Lean.IR.FnBody:

Type

vdecl: Lean.IR.VarId → Lean.IR.IRType → Lean.IR.Expr → Lean.IR.FnBody → Lean.IR.FnBody
jdecl: Lean.IR.JoinPointId → Array Lean.IR.Param → Lean.IR.FnBody → Lean.IR.FnBody → Lean.IR.FnBody
set: Lean.IR.VarId → Nat → Lean.IR.Arg → Lean.IR.FnBody → Lean.IR.FnBody
setTag: Lean.IR.VarId → Nat → Lean.IR.FnBody → Lean.IR.FnBody
uset: Lean.IR.VarId → Nat → Lean.IR.VarId → Lean.IR.FnBody → Lean.IR.FnBody
sset: Lean.IR.VarId → Nat → Nat → Lean.IR.VarId → Lean.IR.IRType → Lean.IR.FnBody → Lean.IR.FnBody
inc: Lean.IR.VarId → Nat → Bool → Bool → Lean.IR.FnBody → Lean.IR.FnBody
dec: Lean.IR.VarId → Nat → Bool → Bool → Lean.IR.FnBody → Lean.IR.FnBody
del: Lean.IR.VarId → Lean.IR.FnBody → Lean.IR.FnBody
mdata: Lean.IR.MData → Lean.IR.FnBody → Lean.IR.FnBody
case: Lean.Name → Lean.IR.VarId → Lean.IR.IRType → Array (Lean.IR.AltCore Lean.IR.FnBody) → Lean.IR.FnBody
ret: Lean.IR.Arg → Lean.IR.FnBody
jmp: Lean.IR.JoinPointId → Array Lean.IR.Arg → Lean.IR.FnBody
unreachable: Lean.IR.FnBody

instance Lean.IR.instInhabitedFnBody:

Inhabited Lean.IR.FnBody

Equations

Lean.IR.instInhabitedFnBody = { default := Lean.IR.FnBody.unreachable }

@[inline]

abbrev Lean.IR.FnBody.nil:

Equations

Lean.IR.FnBody.nil = Lean.IR.FnBody.unreachable

@[export lean_ir_mk_vdecl]

def Lean.IR.mkVDecl (x : Lean.IR.VarId) (ty : Lean.IR.IRType) (e : Lean.IR.Expr) (b : Lean.IR.FnBody) :

Equations

Lean.IR.mkVDecl x ty e b = Lean.IR.FnBody.vdecl x ty e b

@[export lean_ir_mk_jdecl]

def Lean.IR.mkJDecl (j : Lean.IR.JoinPointId) (xs : Array Lean.IR.Param) (v : Lean.IR.FnBody) (b : Lean.IR.FnBody) :

Equations

Lean.IR.mkJDecl j xs v b = Lean.IR.FnBody.jdecl j xs v b

@[export lean_ir_mk_uset]

def Lean.IR.mkUSet (x : Lean.IR.VarId) (i : Nat) (y : Lean.IR.VarId) (b : Lean.IR.FnBody) :

Equations

Lean.IR.mkUSet x i y b = Lean.IR.FnBody.uset x i y b

@[export lean_ir_mk_sset]

def Lean.IR.mkSSet (x : Lean.IR.VarId) (i : Nat) (offset : Nat) (y : Lean.IR.VarId) (ty : Lean.IR.IRType) (b : Lean.IR.FnBody) :

Equations

Lean.IR.mkSSet x i offset y ty b = Lean.IR.FnBody.sset x i offset y ty b

@[export lean_ir_mk_case]

def Lean.IR.mkCase (tid : Lean.Name) (x : Lean.IR.VarId) (cs : Array (Lean.IR.AltCore Lean.IR.FnBody)) :

Equations

Lean.IR.mkCase tid x cs = Lean.IR.FnBody.case tid x Lean.IR.IRType.object cs

@[export lean_ir_mk_ret]

def Lean.IR.mkRet (x : Lean.IR.Arg) :

Equations

Lean.IR.mkRet x = Lean.IR.FnBody.ret x

@[export lean_ir_mk_jmp]

def Lean.IR.mkJmp (j : Lean.IR.JoinPointId) (ys : Array Lean.IR.Arg) :

Equations

Lean.IR.mkJmp j ys = Lean.IR.FnBody.jmp j ys

@[export lean_ir_mk_unreachable]

def Lean.IR.mkUnreachable:

Unit → Lean.IR.FnBody

Equations

Lean.IR.mkUnreachable x = Lean.IR.FnBody.unreachable

@[inline]

abbrev Lean.IR.Alt:

Type

Equations

Lean.IR.Alt = Lean.IR.AltCore Lean.IR.FnBody

@[matchPattern, inline]

abbrev Lean.IR.Alt.ctor (info : Lean.IR.CtorInfo) (b : Lean.IR.FnBody) :

Lean.IR.AltCore Lean.IR.FnBody

Equations

Lean.IR.Alt.ctor = Lean.IR.AltCore.ctor

@[matchPattern, inline]

abbrev Lean.IR.Alt.default (b : Lean.IR.FnBody) :

Lean.IR.AltCore Lean.IR.FnBody

Equations

Lean.IR.Alt.default = Lean.IR.AltCore.default

instance Lean.IR.instInhabitedAlt:

Inhabited Lean.IR.Alt

Equations

Lean.IR.instInhabitedAlt = { default := Lean.IR.Alt.default default }

def Lean.IR.FnBody.isTerminal:

Lean.IR.FnBody → Bool

Equations

One or more equations did not get rendered due to their size.

def Lean.IR.FnBody.body:

Lean.IR.FnBody → Lean.IR.FnBody

Equations

One or more equations did not get rendered due to their size.

def Lean.IR.FnBody.setBody:

Lean.IR.FnBody → Lean.IR.FnBody → Lean.IR.FnBody

Equations

One or more equations did not get rendered due to their size.

@[inline]

def Lean.IR.FnBody.resetBody (b : Lean.IR.FnBody) :

Equations

Lean.IR.FnBody.resetBody b = Lean.IR.FnBody.setBody b Lean.IR.FnBody.nil

@[inline]

def Lean.IR.FnBody.split (b : Lean.IR.FnBody) :

Lean.IR.FnBody × Lean.IR.FnBody

Equations

Lean.IR.FnBody.split b = let b' := Lean.IR.FnBody.body b; let c := Lean.IR.FnBody.resetBody b; (c, b')

def Lean.IR.AltCore.body:

Lean.IR.Alt → Lean.IR.FnBody

Equations

Lean.IR.AltCore.body _fun_discr = match _fun_discr with | Lean.IR.AltCore.ctor info b => b | Lean.IR.AltCore.default b => b

def Lean.IR.AltCore.setBody:

Lean.IR.Alt → Lean.IR.FnBody → Lean.IR.Alt

Equations

One or more equations did not get rendered due to their size.

@[inline]

def Lean.IR.AltCore.modifyBody (f : Lean.IR.FnBody → Lean.IR.FnBody) :

Lean.IR.AltCore Lean.IR.FnBody → Lean.IR.Alt

Equations

Lean.IR.AltCore.modifyBody f _fun_discr = match _fun_discr with | Lean.IR.AltCore.ctor c b => Lean.IR.Alt.ctor c (f b) | Lean.IR.AltCore.default b => Lean.IR.Alt.default (f b)

@[inline]

def Lean.IR.AltCore.mmodifyBody {m : Type → Type} [inst : Monad m] (f : Lean.IR.FnBody → m Lean.IR.FnBody) :

Lean.IR.AltCore Lean.IR.FnBody → m Lean.IR.Alt

Equations

Lean.IR.AltCore.mmodifyBody f _fun_discr = match _fun_discr with | Lean.IR.AltCore.ctor c b => Lean.IR.Alt.ctor c <$> f b | Lean.IR.AltCore.default b => Lean.IR.Alt.default <$> f b

def Lean.IR.Alt.isDefault:

Lean.IR.Alt → Bool

Equations

Lean.IR.Alt.isDefault _fun_discr = match _fun_discr with | Lean.IR.AltCore.ctor info b => false | Lean.IR.AltCore.default b => true

def Lean.IR.push (bs : Array Lean.IR.FnBody) (b : Lean.IR.FnBody) :

Array Lean.IR.FnBody

Equations

Lean.IR.push bs b = let b := Lean.IR.FnBody.resetBody b; Array.push bs b

partial def Lean.IR.flattenAux (b : Lean.IR.FnBody) (r : Array Lean.IR.FnBody) :

Array Lean.IR.FnBody × Lean.IR.FnBody

def Lean.IR.FnBody.flatten (b : Lean.IR.FnBody) :

Array Lean.IR.FnBody × Lean.IR.FnBody

Equations

Lean.IR.FnBody.flatten b = Lean.IR.flattenAux b #[]

partial def Lean.IR.reshapeAux (a : Array Lean.IR.FnBody) (i : Nat) (b : Lean.IR.FnBody) :

def Lean.IR.reshape (bs : Array Lean.IR.FnBody) (term : Lean.IR.FnBody) :

Equations

Lean.IR.reshape bs term = Lean.IR.reshapeAux bs (Array.size bs) term

@[inline]

def Lean.IR.modifyJPs (bs : Array Lean.IR.FnBody) (f : Lean.IR.FnBody → Lean.IR.FnBody) :

Array Lean.IR.FnBody

Equations

Lean.IR.modifyJPs bs f = Array.map (fun b => match b with | Lean.IR.FnBody.jdecl j xs v k => Lean.IR.FnBody.jdecl j xs (f v) k | other => other) bs

@[inline]

def Lean.IR.mmodifyJPs {m : Type → Type} [inst : Monad m] (bs : Array Lean.IR.FnBody) (f : Lean.IR.FnBody → m Lean.IR.FnBody) :

m (Array Lean.IR.FnBody)

Equations

One or more equations did not get rendered due to their size.

@[export lean_ir_mk_alt]

def Lean.IR.mkAlt (n : Lean.Name) (cidx : Nat) (size : Nat) (usize : Nat) (ssize : Nat) (b : Lean.IR.FnBody) :

Equations

Lean.IR.mkAlt n cidx size usize ssize b = Lean.IR.Alt.ctor { name := n, cidx := cidx, size := size, usize := usize, ssize := ssize } b

structure Lean.IR.DeclInfo:

Type

If some , then declaration depends on which uses a sorry axiom.
sorryDep? : Option Lean.Name

Extra information associated with a declaration.

inductive Lean.IR.Decl:

Type

fdecl: Lean.IR.FunId → Array Lean.IR.Param → Lean.IR.IRType → Lean.IR.FnBody → Lean.IR.DeclInfo → Lean.IR.Decl
extern: Lean.IR.FunId → Array Lean.IR.Param → Lean.IR.IRType → Lean.ExternAttrData → Lean.IR.Decl

instance Lean.IR.instInhabitedDecl:

Inhabited Lean.IR.Decl

Equations

Lean.IR.instInhabitedDecl = { default := Lean.IR.Decl.extern default default default default }

def Lean.IR.Decl.name:

Lean.IR.Decl → Lean.IR.FunId

Equations

Lean.IR.Decl.name _fun_discr = match _fun_discr with | Lean.IR.Decl.fdecl f xs type body info => f | Lean.IR.Decl.extern f xs type ext => f

def Lean.IR.Decl.params:

Lean.IR.Decl → Array Lean.IR.Param

Equations

Lean.IR.Decl.params _fun_discr = match _fun_discr with | Lean.IR.Decl.fdecl f xs type body info => xs | Lean.IR.Decl.extern f xs type ext => xs

def Lean.IR.Decl.resultType:

Lean.IR.Decl → Lean.IR.IRType

Equations

Lean.IR.Decl.resultType _fun_discr = match _fun_discr with | Lean.IR.Decl.fdecl f xs t body info => t | Lean.IR.Decl.extern f xs t ext => t

def Lean.IR.Decl.isExtern:

Lean.IR.Decl → Bool

Equations

Lean.IR.Decl.isExtern _fun_discr = match _fun_discr with | Lean.IR.Decl.extern f xs type ext => true | x => false

def Lean.IR.Decl.getInfo:

Lean.IR.Decl → Lean.IR.DeclInfo

Equations

Lean.IR.Decl.getInfo _fun_discr = match _fun_discr with | Lean.IR.Decl.fdecl f xs type body info => info | x => { sorryDep? := none }

def Lean.IR.Decl.updateBody! (d : Lean.IR.Decl) (bNew : Lean.IR.FnBody) :

Equations

One or more equations did not get rendered due to their size.

@[export lean_ir_mk_decl]

def Lean.IR.mkDecl (f : Lean.IR.FunId) (xs : Array Lean.IR.Param) (ty : Lean.IR.IRType) (b : Lean.IR.FnBody) :

Equations

Lean.IR.mkDecl f xs ty b = Lean.IR.Decl.fdecl f xs ty b { sorryDep? := none }

@[export lean_ir_mk_extern_decl]

def Lean.IR.mkExternDecl (f : Lean.IR.FunId) (xs : Array Lean.IR.Param) (ty : Lean.IR.IRType) (e : Lean.ExternAttrData) :

Equations

Lean.IR.mkExternDecl f xs ty e = Lean.IR.Decl.extern f xs ty e

@[export lean_ir_mk_dummy_extern_decl]

def Lean.IR.mkDummyExternDecl (f : Lean.IR.FunId) (xs : Array Lean.IR.Param) (ty : Lean.IR.IRType) :

Equations

Lean.IR.mkDummyExternDecl f xs ty = Lean.IR.Decl.fdecl f xs ty Lean.IR.FnBody.unreachable { sorryDep? := none }

@[inline]

abbrev Lean.IR.IndexSet:

Type

Set of variable and join point names

Equations

Lean.IR.IndexSet = Std.RBTree Lean.IR.Index compare

instance Lean.IR.instInhabitedIndexSet:

Inhabited Lean.IR.IndexSet

Equations

Lean.IR.instInhabitedIndexSet = { default := ∅ }

def Lean.IR.mkIndexSet (idx : Lean.IR.Index) :

Lean.IR.IndexSet

Equations

Lean.IR.mkIndexSet idx = Std.RBTree.insert Std.RBTree.empty idx

inductive Lean.IR.LocalContextEntry:

Type

param: Lean.IR.IRType → Lean.IR.LocalContextEntry
localVar: Lean.IR.IRType → Lean.IR.Expr → Lean.IR.LocalContextEntry
joinPoint: Array Lean.IR.Param → Lean.IR.FnBody → Lean.IR.LocalContextEntry

@[inline]

abbrev Lean.IR.LocalContext:

Type

Equations

Lean.IR.LocalContext = Std.RBMap Lean.IR.Index Lean.IR.LocalContextEntry compare

def Lean.IR.LocalContext.addLocal (ctx : Lean.IR.LocalContext) (x : Lean.IR.VarId) (t : Lean.IR.IRType) (v : Lean.IR.Expr) :

Lean.IR.LocalContext

Equations

Lean.IR.LocalContext.addLocal ctx x t v = Std.RBMap.insert ctx x.idx (Lean.IR.LocalContextEntry.localVar t v)

def Lean.IR.LocalContext.addJP (ctx : Lean.IR.LocalContext) (j : Lean.IR.JoinPointId) (xs : Array Lean.IR.Param) (b : Lean.IR.FnBody) :

Lean.IR.LocalContext

Equations

Lean.IR.LocalContext.addJP ctx j xs b = Std.RBMap.insert ctx j.idx (Lean.IR.LocalContextEntry.joinPoint xs b)

def Lean.IR.LocalContext.addParam (ctx : Lean.IR.LocalContext) (p : Lean.IR.Param) :

Lean.IR.LocalContext

Equations

Lean.IR.LocalContext.addParam ctx p = Std.RBMap.insert ctx p.x.idx (Lean.IR.LocalContextEntry.param p.ty)

def Lean.IR.LocalContext.addParams (ctx : Lean.IR.LocalContext) (ps : Array Lean.IR.Param) :

Lean.IR.LocalContext

Equations

Lean.IR.LocalContext.addParams ctx ps = Array.foldl Lean.IR.LocalContext.addParam ctx ps 0 (Array.size ps)

def Lean.IR.LocalContext.isJP (ctx : Lean.IR.LocalContext) (idx : Lean.IR.Index) :

Equations

Lean.IR.LocalContext.isJP ctx idx = match Std.RBMap.find? ctx idx with | some (Lean.IR.LocalContextEntry.joinPoint a a_1) => true | x => false

def Lean.IR.LocalContext.getJPBody (ctx : Lean.IR.LocalContext) (j : Lean.IR.JoinPointId) :

Option Lean.IR.FnBody

Equations

Lean.IR.LocalContext.getJPBody ctx j = match Std.RBMap.find? ctx j.idx with | some (Lean.IR.LocalContextEntry.joinPoint a b) => some b | x => none

def Lean.IR.LocalContext.getJPParams (ctx : Lean.IR.LocalContext) (j : Lean.IR.JoinPointId) :

Option (Array Lean.IR.Param)

Equations

Lean.IR.LocalContext.getJPParams ctx j = match Std.RBMap.find? ctx j.idx with | some (Lean.IR.LocalContextEntry.joinPoint ys a) => some ys | x => none

def Lean.IR.LocalContext.isParam (ctx : Lean.IR.LocalContext) (idx : Lean.IR.Index) :

Equations

Lean.IR.LocalContext.isParam ctx idx = match Std.RBMap.find? ctx idx with | some (Lean.IR.LocalContextEntry.param a) => true | x => false

def Lean.IR.LocalContext.isLocalVar (ctx : Lean.IR.LocalContext) (idx : Lean.IR.Index) :

Equations

Lean.IR.LocalContext.isLocalVar ctx idx = match Std.RBMap.find? ctx idx with | some (Lean.IR.LocalContextEntry.localVar a a_1) => true | x => false

def Lean.IR.LocalContext.contains (ctx : Lean.IR.LocalContext) (idx : Lean.IR.Index) :

Equations

Lean.IR.LocalContext.contains ctx idx = Std.RBMap.contains ctx idx

def Lean.IR.LocalContext.eraseJoinPointDecl (ctx : Lean.IR.LocalContext) (j : Lean.IR.JoinPointId) :

Lean.IR.LocalContext

Equations

Lean.IR.LocalContext.eraseJoinPointDecl ctx j = Std.RBMap.erase ctx j.idx

def Lean.IR.LocalContext.getType (ctx : Lean.IR.LocalContext) (x : Lean.IR.VarId) :

Option Lean.IR.IRType

Equations

One or more equations did not get rendered due to their size.

def Lean.IR.LocalContext.getValue (ctx : Lean.IR.LocalContext) (x : Lean.IR.VarId) :

Option Lean.IR.Expr

Equations

Lean.IR.LocalContext.getValue ctx x = match Std.RBMap.find? ctx x.idx with | some (Lean.IR.LocalContextEntry.localVar a v) => some v | x => none

@[inline]

abbrev Lean.IR.IndexRenaming:

Type

Equations

Lean.IR.IndexRenaming = Std.RBMap Lean.IR.Index Lean.IR.Index compare

class Lean.IR.AlphaEqv (α : Type) :

Type

aeqv : Lean.IR.IndexRenaming → α → α → Bool

Instances

def Lean.IR.VarId.alphaEqv (ρ : Lean.IR.IndexRenaming) (v₁ : Lean.IR.VarId) (v₂ : Lean.IR.VarId) :

Equations

Lean.IR.VarId.alphaEqv ρ v₁ v₂ = match Std.RBMap.find? ρ v₁.idx with | some v => v == v₂.idx | none => v₁ == v₂

instance Lean.IR.instAlphaEqvVarId:

Lean.IR.AlphaEqv Lean.IR.VarId

Equations

Lean.IR.instAlphaEqvVarId = { aeqv := Lean.IR.VarId.alphaEqv }

def Lean.IR.Arg.alphaEqv (ρ : Lean.IR.IndexRenaming) :

Lean.IR.Arg → Lean.IR.Arg → Bool

Equations

One or more equations did not get rendered due to their size.

instance Lean.IR.instAlphaEqvArg:

Lean.IR.AlphaEqv Lean.IR.Arg

Equations

Lean.IR.instAlphaEqvArg = { aeqv := Lean.IR.Arg.alphaEqv }

def Lean.IR.args.alphaEqv (ρ : Lean.IR.IndexRenaming) (args₁ : Array Lean.IR.Arg) (args₂ : Array Lean.IR.Arg) :

Equations

Lean.IR.args.alphaEqv ρ args₁ args₂ = Array.isEqv args₁ args₂ fun a b => Lean.IR.aeqv ρ a b

instance Lean.IR.instAlphaEqvArrayArg:

Lean.IR.AlphaEqv (Array Lean.IR.Arg)

Equations

Lean.IR.instAlphaEqvArrayArg = { aeqv := Lean.IR.args.alphaEqv }

def Lean.IR.Expr.alphaEqv (ρ : Lean.IR.IndexRenaming) :

Lean.IR.Expr → Lean.IR.Expr → Bool

Equations

One or more equations did not get rendered due to their size.

instance Lean.IR.instAlphaEqvExpr:

Lean.IR.AlphaEqv Lean.IR.Expr

Equations

Lean.IR.instAlphaEqvExpr = { aeqv := Lean.IR.Expr.alphaEqv }

def Lean.IR.addVarRename (ρ : Lean.IR.IndexRenaming) (x₁ : Nat) (x₂ : Nat) :

Lean.IR.IndexRenaming

Equations

Lean.IR.addVarRename ρ x₁ x₂ = if (x₁ == x₂) = true then ρ else Std.RBMap.insert ρ x₁ x₂

def Lean.IR.addParamRename (ρ : Lean.IR.IndexRenaming) (p₁ : Lean.IR.Param) (p₂ : Lean.IR.Param) :

Option Lean.IR.IndexRenaming

Equations

Lean.IR.addParamRename ρ p₁ p₂ = if (p₁.ty == p₂.ty && decide (p₁.borrow = p₂.borrow)) = true then some (Lean.IR.addVarRename ρ p₁.x.idx p₂.x.idx) else none

def Lean.IR.addParamsRename (ρ : Lean.IR.IndexRenaming) (ps₁ : Array Lean.IR.Param) (ps₂ : Array Lean.IR.Param) :

Option Lean.IR.IndexRenaming

Equations

One or more equations did not get rendered due to their size.

partial def Lean.IR.FnBody.alphaEqv:

Lean.IR.IndexRenaming → Lean.IR.FnBody → Lean.IR.FnBody → Bool

def Lean.IR.FnBody.beq (b₁ : Lean.IR.FnBody) (b₂ : Lean.IR.FnBody) :

Equations

Lean.IR.FnBody.beq b₁ b₂ = Lean.IR.FnBody.alphaEqv ∅ b₁ b₂

instance Lean.IR.instBEqFnBody:

BEq Lean.IR.FnBody

Equations

Lean.IR.instBEqFnBody = { beq := Lean.IR.FnBody.beq }

@[inline]

abbrev Lean.IR.VarIdSet:

Type

Equations

Lean.IR.VarIdSet = Std.RBTree Lean.IR.VarId fun x y => compare x.idx y.idx

instance Lean.IR.instInhabitedVarIdSet:

Inhabited Lean.IR.VarIdSet

Equations

Lean.IR.instInhabitedVarIdSet = { default := ∅ }

def Lean.IR.mkIf (x : Lean.IR.VarId) (t : Lean.IR.FnBody) (e : Lean.IR.FnBody) :

Equations

One or more equations did not get rendered due to their size.