chore: derive more type classes for IR data structures (#7085)
This commit is contained in:
parent
6c42cb353a
commit
cdc2731401
2 changed files with 3 additions and 1 deletions
|
|
@ -180,7 +180,7 @@ structure CtorInfo where
|
|||
size : Nat
|
||||
usize : Nat
|
||||
ssize : Nat
|
||||
deriving Repr
|
||||
deriving Inhabited, Repr
|
||||
|
||||
def CtorInfo.beq : CtorInfo → CtorInfo → Bool
|
||||
| ⟨n₁, cidx₁, size₁, usize₁, ssize₁⟩, ⟨n₂, cidx₂, size₂, usize₂, ssize₂⟩ =>
|
||||
|
|
@ -223,6 +223,7 @@ inductive Expr where
|
|||
| lit (v : LitVal)
|
||||
/-- Return `1 : uint8` Iff `RC(x) > 1` -/
|
||||
| isShared (x : VarId)
|
||||
deriving Inhabited
|
||||
|
||||
@[export lean_ir_mk_ctor_expr] def mkCtorExpr (n : Name) (cidx : Nat) (size : Nat) (usize : Nat) (ssize : Nat) (ys : Array Arg) : Expr :=
|
||||
Expr.ctor ⟨n, cidx, size, usize, ssize⟩ ys
|
||||
|
|
|
|||
|
|
@ -15,6 +15,7 @@ inductive CtorFieldInfo where
|
|||
| object (i : Nat)
|
||||
| usize (i : Nat)
|
||||
| scalar (sz : Nat) (offset : Nat) (type : IRType)
|
||||
deriving Inhabited
|
||||
|
||||
namespace CtorFieldInfo
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue