Lean.Compiler.IR.Basic

Lean.IR.IRType.isScalar x = match x with | Lean.IR.IRType.float => true | Lean.IR.IRType.uint8 => true | Lean.IR.IRType.uint16 => true | Lean.IR.IRType.uint32 => true | Lean.IR.IRType.uint64 => true | Lean.IR.IRType.usize => true | x => false

source

def Lean.IR.IRType.isObj :

Lean.IR.IRType → Bool

Equations

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

source

def Lean.IR.IRType.isIrrelevant :

Lean.IR.IRType → Bool

Equations

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

source

def Lean.IR.IRType.isStruct :

Lean.IR.IRType → Bool

Equations

Lean.IR.IRType.isStruct x = match x with | Lean.IR.IRType.struct x x_1 => true | x => false

source

def Lean.IR.IRType.isUnion :

Lean.IR.IRType → Bool

Equations

Lean.IR.IRType.isUnion x = match x with | Lean.IR.IRType.union x x_1 => true | x => false

source

inductive Lean.IR.Arg :

Type

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

source

instance Lean.IR.instInhabitedArg :

Inhabited Lean.IR.Arg

Equations

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

source

def Lean.IR.Arg.beq :

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

Equations

Lean.IR.Arg.beq x x = match x, x with | Lean.IR.Arg.var x, Lean.IR.Arg.var y => x == y | Lean.IR.Arg.irrelevant, Lean.IR.Arg.irrelevant => true | x, x_1 => false

source

instance Lean.IR.instBEqArg :

BEq Lean.IR.Arg

Equations

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

source

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

Lean.IR.Arg

Equations

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

source

inductive Lean.IR.LitVal :

Type

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

source

def Lean.IR.LitVal.beq :

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

Equations

Lean.IR.LitVal.beq x x = match x, x with | Lean.IR.LitVal.num v₁, Lean.IR.LitVal.num v₂ => v₁ == v₂ | Lean.IR.LitVal.str v₁, Lean.IR.LitVal.str v₂ => v₁ == v₂ | x, x_1 => false

source

instance Lean.IR.instBEqLitVal :

BEq Lean.IR.LitVal

Equations

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

source

structure Lean.IR.CtorInfo :

Type

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

source

instance Lean.IR.instReprCtorInfo :

Repr Lean.IR.CtorInfo

Equations

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

source

def Lean.IR.CtorInfo.beq :

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

Equations

Lean.IR.CtorInfo.beq x x = match x, x with | { name := n₁, cidx := cidx₁, size := size₁, usize := usize₁, ssize := ssize₁ }, { name := n₂, cidx := cidx₂, size := size₂, usize := usize₂, ssize := ssize₂ } => n₁ == n₂ && cidx₁ == cidx₂ && size₁ == size₂ && usize₁ == usize₂ && ssize₁ == ssize₂

source

instance Lean.IR.instBEqCtorInfo :

BEq Lean.IR.CtorInfo

Equations

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

source

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

Bool

Equations

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

source

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

Bool

Equations

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

source

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

source

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

Lean.IR.Expr

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

source

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

Lean.IR.Expr

Equations

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

source

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

Lean.IR.Expr

Equations

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

source

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

Lean.IR.Expr

Equations

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

source

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

Lean.IR.Expr

Equations

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

source

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

Lean.IR.Expr

Equations

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

source

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

Lean.IR.Expr

Equations

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

source

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

Lean.IR.Expr

Equations

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

source

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

Lean.IR.Expr

Equations

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

source

structure Lean.IR.Param :

Type

x : Lean.IR.VarId
borrow : Bool
ty : Lean.IR.IRType

source

instance Lean.IR.instInhabitedParam :

Inhabited Lean.IR.Param

Equations

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

source

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

Lean.IR.Param

Equations

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

source

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

source

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

source

instance Lean.IR.instInhabitedFnBody :

Inhabited Lean.IR.FnBody

Equations

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

source

@[inline]

abbrev Lean.IR.FnBody.nil :

Lean.IR.FnBody

Equations

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

source

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

Lean.IR.FnBody

Equations

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

source

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

Lean.IR.FnBody

Equations

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

source

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

Lean.IR.FnBody

Equations

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

source

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

Lean.IR.FnBody

Equations

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

source

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

Lean.IR.FnBody

Equations

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

source

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

Lean.IR.FnBody

Equations

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

source

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

Lean.IR.FnBody

Equations

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

source

def Lean.IR.mkUnreachable :

Unit → Lean.IR.FnBody

Equations

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

source

@[inline]

abbrev Lean.IR.Alt :

Type

Equations

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

source

@[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

source

@[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

source

instance Lean.IR.instInhabitedAlt :

Inhabited Lean.IR.Alt

Equations

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

source

def Lean.IR.FnBody.isTerminal :

Lean.IR.FnBody → Bool

Equations

Lean.IR.FnBody.isTerminal x = match x with | Lean.IR.FnBody.case x x_1 x_2 x_3 => true | Lean.IR.FnBody.ret x => true | Lean.IR.FnBody.jmp x x_1 => true | Lean.IR.FnBody.unreachable => true | x => false

source

def Lean.IR.FnBody.body :

Lean.IR.FnBody → Lean.IR.FnBody

Equations

Lean.IR.FnBody.body x = match x with | Lean.IR.FnBody.vdecl x x_1 x_2 b => b | Lean.IR.FnBody.jdecl x x_1 x_2 b => b | Lean.IR.FnBody.set x x_1 x_2 b => b | Lean.IR.FnBody.uset x x_1 x_2 b => b | Lean.IR.FnBody.sset x x_1 x_2 x_3 x_4 b => b | Lean.IR.FnBody.setTag x x_1 b => b | Lean.IR.FnBody.inc x x_1 x_2 x_3 b => b | Lean.IR.FnBody.dec x x_1 x_2 x_3 b => b | Lean.IR.FnBody.del x b => b | Lean.IR.FnBody.mdata x b => b | other => other

source

def Lean.IR.FnBody.setBody :

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

Equations

Lean.IR.FnBody.setBody x x = match x, x with | Lean.IR.FnBody.vdecl x t v x_1, b => Lean.IR.FnBody.vdecl x t v b | Lean.IR.FnBody.jdecl j xs v x, b => Lean.IR.FnBody.jdecl j xs v b | Lean.IR.FnBody.set x i y x_1, b => Lean.IR.FnBody.set x i y b | Lean.IR.FnBody.uset x i y x_1, b => Lean.IR.FnBody.uset x i y b | Lean.IR.FnBody.sset x i o y t x_1, b => Lean.IR.FnBody.sset x i o y t b | Lean.IR.FnBody.setTag x i x_1, b => Lean.IR.FnBody.setTag x i b | Lean.IR.FnBody.inc x n c p x_1, b => Lean.IR.FnBody.inc x n c p b | Lean.IR.FnBody.dec x n c p x_1, b => Lean.IR.FnBody.dec x n c p b | Lean.IR.FnBody.del x x_1, b => Lean.IR.FnBody.del x b | Lean.IR.FnBody.mdata d x, b => Lean.IR.FnBody.mdata d b | other, b => other

source

@[inline]

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

Lean.IR.FnBody

Equations

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

source

@[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')

source

def Lean.IR.AltCore.body :

Lean.IR.Alt → Lean.IR.FnBody

Equations

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

source

def Lean.IR.AltCore.setBody :

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

Equations

Lean.IR.AltCore.setBody x x = match x, x with | Lean.IR.AltCore.ctor c x, b => Lean.IR.Alt.ctor c b | Lean.IR.AltCore.default x, b => Lean.IR.Alt.default b

source

@[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 x = match x 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)

source

@[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 x = match x 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

source

def Lean.IR.Alt.isDefault :

Lean.IR.Alt → Bool

Equations

Lean.IR.Alt.isDefault x = match x with | Lean.IR.AltCore.ctor x x_1 => false | Lean.IR.AltCore.default x => true

source

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

source

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

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

source

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 #[]

source

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

Lean.IR.FnBody

source

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

Lean.IR.FnBody

Equations

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

source

@[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

source

@[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

Lean.IR.mmodifyJPs bs f = Array.mapM (fun b => match b with | Lean.IR.FnBody.jdecl j xs v k => do let a ← f v pure (Lean.IR.FnBody.jdecl j xs a k) | other => pure other) bs

source

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

Lean.IR.Alt

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

source

structure Lean.IR.DeclInfo :

Type

sorryDep? : Option Lean.Name

source

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

source

instance Lean.IR.instInhabitedDecl :

Inhabited Lean.IR.Decl

Equations

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

source

def Lean.IR.Decl.name :

Lean.IR.Decl → Lean.IR.FunId

Equations

Lean.IR.Decl.name x = match x with | Lean.IR.Decl.fdecl f x x_1 x_2 x_3 => f | Lean.IR.Decl.extern f x x_1 x_2 => f

source

def Lean.IR.Decl.params :

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

Equations

Lean.IR.Decl.params x = match x with | Lean.IR.Decl.fdecl x xs x_1 x_2 x_3 => xs | Lean.IR.Decl.extern x xs x_1 x_2 => xs

source

def Lean.IR.Decl.resultType :

Lean.IR.Decl → Lean.IR.IRType

Equations

Lean.IR.Decl.resultType x = match x with | Lean.IR.Decl.fdecl x x_1 t x_2 x_3 => t | Lean.IR.Decl.extern x x_1 t x_2 => t

source

def Lean.IR.Decl.isExtern :

Lean.IR.Decl → Bool

Equations

Lean.IR.Decl.isExtern x = match x with | Lean.IR.Decl.extern x x_1 x_2 x_3 => true | x => false

source

def Lean.IR.Decl.getInfo :

Lean.IR.Decl → Lean.IR.DeclInfo

Equations

Lean.IR.Decl.getInfo x = match x with | Lean.IR.Decl.fdecl x x_1 x_2 x_3 info => info | x => { sorryDep? := none }

source

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

Lean.IR.Decl

Equations

Lean.IR.Decl.updateBody! d bNew = match d with | Lean.IR.Decl.fdecl f xs t b info => Lean.IR.Decl.fdecl f xs t bNew info | x => panicWithPosWithDecl "Lean.Compiler.IR.Basic" "Lean.IR.Decl.updateBody!" 431 9 "expected definition"

source

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

Lean.IR.Decl

Equations

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

source

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

Lean.IR.Decl

Equations

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

source

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

Lean.IR.Decl

Equations

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

source

@[inline]

abbrev Lean.IR.IndexSet :

Type

Equations

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

source

instance Lean.IR.instInhabitedIndexSet :

Inhabited Lean.IR.IndexSet

Equations

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

source

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

Lean.IR.IndexSet

Equations

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

source

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

source

@[inline]

abbrev Lean.IR.LocalContext :

Type

Equations

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

source

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)

source

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)

source

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)

source

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)

source

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

Bool

Equations

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

source

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 x b) => some b | other => none

source

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 x) => some ys | other => none

source

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

Bool

Equations

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

source

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

Bool

Equations

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

source

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

Bool

Equations

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

source

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

source

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

Option Lean.IR.IRType

Equations

Lean.IR.LocalContext.getType ctx x = match Std.RBMap.find? ctx x.idx with | some (Lean.IR.LocalContextEntry.param t) => some t | some (Lean.IR.LocalContextEntry.localVar t x) => some t | other => none

source

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 x v) => some v | other => none

source

@[inline]

abbrev Lean.IR.IndexRenaming :

Type

Equations

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

source

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

Type

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

Instances

source

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

Bool

Equations

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

source

instance Lean.IR.instAlphaEqvVarId :

Lean.IR.AlphaEqv Lean.IR.VarId

Equations

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

source

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

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

Equations

Lean.IR.Arg.alphaEqv ρ x x = match x, x with | Lean.IR.Arg.var v₁, Lean.IR.Arg.var v₂ => Lean.IR.aeqv ρ v₁ v₂ | Lean.IR.Arg.irrelevant, Lean.IR.Arg.irrelevant => true | x, x_1 => false

source

instance Lean.IR.instAlphaEqvArg :

Lean.IR.AlphaEqv Lean.IR.Arg

Equations

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

source

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

Bool

Equations

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

source

instance Lean.IR.instAlphaEqvArrayArg :

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

Equations

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

source

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

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

Equations

Lean.IR.Expr.alphaEqv ρ x x = match x, x with | Lean.IR.Expr.ctor i₁ ys₁, Lean.IR.Expr.ctor i₂ ys₂ => i₁ == i₂ && Lean.IR.aeqv ρ ys₁ ys₂ | Lean.IR.Expr.reset n₁ x₁, Lean.IR.Expr.reset n₂ x₂ => n₁ == n₂ && Lean.IR.aeqv ρ x₁ x₂ | Lean.IR.Expr.reuse x₁ i₁ u₁ ys₁, Lean.IR.Expr.reuse x₂ i₂ u₂ ys₂ => Lean.IR.aeqv ρ x₁ x₂ && i₁ == i₂ && u₁ == u₂ && Lean.IR.aeqv ρ ys₁ ys₂ | Lean.IR.Expr.proj i₁ x₁, Lean.IR.Expr.proj i₂ x₂ => i₁ == i₂ && Lean.IR.aeqv ρ x₁ x₂ | Lean.IR.Expr.uproj i₁ x₁, Lean.IR.Expr.uproj i₂ x₂ => i₁ == i₂ && Lean.IR.aeqv ρ x₁ x₂ | Lean.IR.Expr.sproj n₁ o₁ x₁, Lean.IR.Expr.sproj n₂ o₂ x₂ => n₁ == n₂ && o₁ == o₂ && Lean.IR.aeqv ρ x₁ x₂ | Lean.IR.Expr.fap c₁ ys₁, Lean.IR.Expr.fap c₂ ys₂ => c₁ == c₂ && Lean.IR.aeqv ρ ys₁ ys₂ | Lean.IR.Expr.pap c₁ ys₁, Lean.IR.Expr.pap c₂ ys₂ => c₁ == c₂ && Lean.IR.aeqv ρ ys₁ ys₂ | Lean.IR.Expr.ap x₁ ys₁, Lean.IR.Expr.ap x₂ ys₂ => Lean.IR.aeqv ρ x₁ x₂ && Lean.IR.aeqv ρ ys₁ ys₂ | Lean.IR.Expr.box ty₁ x₁, Lean.IR.Expr.box ty₂ x₂ => ty₁ == ty₂ && Lean.IR.aeqv ρ x₁ x₂ | Lean.IR.Expr.unbox x₁, Lean.IR.Expr.unbox x₂ => Lean.IR.aeqv ρ x₁ x₂ | Lean.IR.Expr.lit v₁, Lean.IR.Expr.lit v₂ => v₁ == v₂ | Lean.IR.Expr.isShared x₁, Lean.IR.Expr.isShared x₂ => Lean.IR.aeqv ρ x₁ x₂ | Lean.IR.Expr.isTaggedPtr x₁, Lean.IR.Expr.isTaggedPtr x₂ => Lean.IR.aeqv ρ x₁ x₂ | x, x_1 => false

source

instance Lean.IR.instAlphaEqvExpr :

Lean.IR.AlphaEqv Lean.IR.Expr

Equations

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

source

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₂

source

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

source

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

Option Lean.IR.IndexRenaming

Equations

Lean.IR.addParamsRename ρ ps₁ ps₂ = OptionM.run (if (Array.size ps₁ != Array.size ps₂) = true then failure else let ρ := ρ; do let r ← let col := { start := 0, stop := Array.size ps₁, step := 1 }; forIn col ρ fun i r => let ρ := r; do let r ← Lean.IR.addParamRename ρ (Array.getOp ps₁ i) (Array.getOp ps₂ i) let ρ : Lean.IR.IndexRenaming := r pure PUnit.unit pure (ForInStep.yield ρ) let x : Lean.IR.IndexRenaming := r let ρ : Lean.IR.IndexRenaming := x pure ρ)

source

partial def Lean.IR.FnBody.alphaEqv :

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

source

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

Bool

Equations

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

source

instance Lean.IR.instBEqFnBody :

BEq Lean.IR.FnBody

Equations

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

source

@[inline]

abbrev Lean.IR.VarIdSet :

Type

Equations

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

source

instance Lean.IR.instInhabitedVarIdSet :

Inhabited Lean.IR.VarIdSet

Equations

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

source

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

Lean.IR.FnBody

Equations

Lean.IR.mkIf x t e = Lean.IR.FnBody.case `Bool x Lean.IR.IRType.uint8 #[Lean.IR.Alt.ctor { name := `Bool.false, cidx := 0, size := 0, usize := 0, ssize := 0 } e, Lean.IR.Alt.ctor { name := `Bool.true, cidx := 1, size := 0, usize := 0, ssize := 0 } t]