InstCombine Dialect

This file defines a dialect of basic arithmetic and bitwise operations on bitvectors.

The dialect supports types of arbitrary-width bitvectors. Thus, some definitions wil be parameterized by φ, the number of width meta-variables there are. This parameter will usually be either 0, indicating that all widths are known, concrete values, or 1, indicating there is exactly one distinct width meta-variable.

In particular, we only define a denotational semantics for concrete programs (i.e., where φ = 0)

see https://releases.llvm.org/14.0.0/docs/LangRef.html#bitwise-binary-operations

@[reducible, inline]

abbrev InstCombine.Width (φ : ℕ) : Type

Equations

• InstCombine.Width φ = ConcreteOrMVar ℕ φ

inductive InstCombine.MTy (φ : ℕ) : Type

• bitvec: {φ : ℕ} → InstCombine.Width φ → InstCombine.MTy φ

instance InstCombine.instDecidableEqMTy : {φ : ℕ} → DecidableEq (InstCombine.MTy φ)

Equations

• InstCombine.instDecidableEqMTy = InstCombine.decEqMTy✝

instance InstCombine.instInhabitedMTy : {a : ℕ} → Inhabited (InstCombine.MTy a)

Equations

• InstCombine.instInhabitedMTy = { default := InstCombine.MTy.bitvec default }

@[reducible, inline]

abbrev InstCombine.Ty : Type

Equations

• InstCombine.Ty = InstCombine.MTy 0

@[reducible, match_pattern, inline]

abbrev InstCombine.Ty.bitvec (w : ℕ) : InstCombine.Ty

Equations

• InstCombine.Ty.bitvec w = InstCombine.MTy.bitvec (ConcreteOrMVar.concrete w)

instance InstCombine.instReprMTy {φ : ℕ} : Repr (InstCombine.MTy φ)

Equations

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

instance InstCombine.instToFormatMTy {φ : ℕ} : Lean.ToFormat (InstCombine.MTy φ)

Equations

• InstCombine.instToFormatMTy = { format := repr }

instance InstCombine.instToStringMTy {φ : ℕ} : ToString (InstCombine.MTy φ)

Equations

• InstCombine.instToStringMTy = { toString := fun (t : InstCombine.MTy φ) => (repr t).pretty }

def InstCombine.Ty.width : InstCombine.Ty → ℕ

Equations

• InstCombine.Ty.width (InstCombine.MTy.bitvec (ConcreteOrMVar.concrete w)) = w

@[simp]

theorem InstCombine.Ty.width_eq (ty : InstCombine.Ty) : InstCombine.Ty.bitvec ty.width = ty

def InstCombine.BitVec.width {n : ℕ} : BitVec n → ℕ

Equations

• InstCombine.BitVec.width x = n

instance InstCombine.instTyDenoteTy : TyDenote InstCombine.Ty

Equations

• InstCombine.instTyDenoteTy = { toType := fun (x : InstCombine.Ty) => match x with | InstCombine.MTy.bitvec (ConcreteOrMVar.concrete w) => LLVM.IntW w }

instance InstCombine.instCoeIntToTypeTy (ty : InstCombine.Ty) : Coe ℤ ⟦ty⟧

Equations

• InstCombine.instCoeIntToTypeTy ty = { coe := fun (z : ℤ) => match ty with | InstCombine.MTy.bitvec (ConcreteOrMVar.concrete w) => some (BitVec.ofInt w z) }

instance InstCombine.instInhabitedToTypeTy (ty : InstCombine.Ty) : Inhabited ⟦ty⟧

Equations

• InstCombine.instInhabitedToTypeTy (InstCombine.MTy.bitvec (ConcreteOrMVar.concrete w)) = { default := pure default }

instance InstCombine.instReprBitVec_sSA {n : ℕ} : Repr (BitVec n)

Equations

• InstCombine.instReprBitVec_sSA = { reprPrec := fun (x : BitVec n) (x_1 : ℕ) => match x, x_1 with | v, n_1 => reprPrec v.toInt n_1 }

inductive InstCombine.MOp.UnaryOp : Type

Homogeneous, unary operations

• neg: InstCombine.MOp.UnaryOp
• not: InstCombine.MOp.UnaryOp
• copy: InstCombine.MOp.UnaryOp

instance InstCombine.MOp.instReprUnaryOp : Repr InstCombine.MOp.UnaryOp

Equations

• InstCombine.MOp.instReprUnaryOp = { reprPrec := InstCombine.MOp.reprUnaryOp✝ }

instance InstCombine.MOp.instDecidableEqUnaryOp : DecidableEq InstCombine.MOp.UnaryOp

Equations

• InstCombine.MOp.instDecidableEqUnaryOp x y = if h : x.toCtorIdx = y.toCtorIdx then isTrue ⋯ else isFalse ⋯

instance InstCombine.MOp.instInhabitedUnaryOp : Inhabited InstCombine.MOp.UnaryOp

Equations

• InstCombine.MOp.instInhabitedUnaryOp = { default := InstCombine.MOp.UnaryOp.neg }

inductive InstCombine.MOp.BinaryOp : Type

Homogeneous, binary operations

• and: InstCombine.MOp.BinaryOp
• or: optParam LLVM.DisjointFlag { disjoint := false } → InstCombine.MOp.BinaryOp
• xor: InstCombine.MOp.BinaryOp
• shl: optParam LLVM.NoWrapFlags { nsw := false, nuw := false } → InstCombine.MOp.BinaryOp
• lshr: optParam LLVM.ExactFlag { exact := false } → InstCombine.MOp.BinaryOp
• ashr: optParam LLVM.ExactFlag { exact := false } → InstCombine.MOp.BinaryOp
• urem: InstCombine.MOp.BinaryOp
• srem: InstCombine.MOp.BinaryOp
• add: optParam LLVM.NoWrapFlags { nsw := false, nuw := false } → InstCombine.MOp.BinaryOp
• mul: optParam LLVM.NoWrapFlags { nsw := false, nuw := false } → InstCombine.MOp.BinaryOp
• sub: optParam LLVM.NoWrapFlags { nsw := false, nuw := false } → InstCombine.MOp.BinaryOp
• sdiv: optParam LLVM.ExactFlag { exact := false } → InstCombine.MOp.BinaryOp
• udiv: optParam LLVM.ExactFlag { exact := false } → InstCombine.MOp.BinaryOp

instance InstCombine.MOp.instDecidableEqBinaryOp : DecidableEq InstCombine.MOp.BinaryOp

Equations

• InstCombine.MOp.instDecidableEqBinaryOp = InstCombine.MOp.decEqBinaryOp✝

instance InstCombine.MOp.instInhabitedBinaryOp : Inhabited InstCombine.MOp.BinaryOp

Equations

• InstCombine.MOp.instInhabitedBinaryOp = { default := InstCombine.MOp.BinaryOp.and }

def InstCombine.reprWithoutFlags (op : InstCombine.MOp.BinaryOp) (prec : ℕ) : Lean.Format

If both the nuw and nsw flags are the default value (false,false), then we should not print them. This should be the default behavior in Lean, but it isn't

Equations

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

instance InstCombine.instReprBinaryOp : Repr InstCombine.MOp.BinaryOp

Equations

• InstCombine.instReprBinaryOp = { reprPrec := InstCombine.reprWithoutFlags }

inductive InstCombine.MOp (φ : ℕ) : Type

• unary: {φ : ℕ} → InstCombine.Width φ → InstCombine.MOp.UnaryOp → InstCombine.MOp φ
• binary: {φ : ℕ} → InstCombine.Width φ → InstCombine.MOp.BinaryOp → InstCombine.MOp φ
• select: {φ : ℕ} → InstCombine.Width φ → InstCombine.MOp φ
• icmp: {φ : ℕ} → LLVM.IntPredicate → InstCombine.Width φ → InstCombine.MOp φ
• const: {φ : ℕ} → InstCombine.Width φ → ℤ → InstCombine.MOp φ

  Since the width of the const might not be known, we just store the value as an Int

instance InstCombine.instReprMOp : {φ : ℕ} → Repr (InstCombine.MOp φ)

Equations

• InstCombine.instReprMOp = { reprPrec := InstCombine.reprMOp✝ }

instance InstCombine.instDecidableEqMOp : {φ : ℕ} → DecidableEq (InstCombine.MOp φ)

Equations

• InstCombine.instDecidableEqMOp = InstCombine.decEqMOp✝

instance InstCombine.instInhabitedMOp : {a : ℕ} → Inhabited (InstCombine.MOp a)

Equations

• InstCombine.instInhabitedMOp = { default := InstCombine.MOp.unary default default }

@[match_pattern]

def InstCombine.MOp.neg {φ : ℕ} (w : InstCombine.Width φ) : InstCombine.MOp φ

Equations

• InstCombine.MOp.neg w = InstCombine.MOp.unary w InstCombine.MOp.UnaryOp.neg

@[match_pattern]

def InstCombine.MOp.not {φ : ℕ} (w : InstCombine.Width φ) : InstCombine.MOp φ

Equations

• InstCombine.MOp.not w = InstCombine.MOp.unary w InstCombine.MOp.UnaryOp.not

@[match_pattern]

def InstCombine.MOp.copy {φ : ℕ} (w : InstCombine.Width φ) : InstCombine.MOp φ

Equations

• InstCombine.MOp.copy w = InstCombine.MOp.unary w InstCombine.MOp.UnaryOp.copy

@[match_pattern]

def InstCombine.MOp.and {φ : ℕ} (w : InstCombine.Width φ) : InstCombine.MOp φ

Equations

• InstCombine.MOp.and w = InstCombine.MOp.binary w InstCombine.MOp.BinaryOp.and

@[match_pattern]

def InstCombine.MOp.xor {φ : ℕ} (w : InstCombine.Width φ) : InstCombine.MOp φ

Equations

• InstCombine.MOp.xor w = InstCombine.MOp.binary w InstCombine.MOp.BinaryOp.xor

@[match_pattern]

def InstCombine.MOp.urem {φ : ℕ} (w : InstCombine.Width φ) : InstCombine.MOp φ

Equations

• InstCombine.MOp.urem w = InstCombine.MOp.binary w InstCombine.MOp.BinaryOp.urem

@[match_pattern]

def InstCombine.MOp.srem {φ : ℕ} (w : InstCombine.Width φ) : InstCombine.MOp φ

Equations

• InstCombine.MOp.srem w = InstCombine.MOp.binary w InstCombine.MOp.BinaryOp.srem

@[match_pattern]

def InstCombine.MOp.or {φ : ℕ} (w : InstCombine.Width φ) (DisjointFlag : optParam LLVM.DisjointFlag { disjoint := false }) : InstCombine.MOp φ

Equations

• InstCombine.MOp.or w DisjointFlag = InstCombine.MOp.binary w (InstCombine.MOp.BinaryOp.or DisjointFlag)

@[match_pattern]

def InstCombine.MOp.shl {φ : ℕ} (w : InstCombine.Width φ) (NoWrapFlags : optParam LLVM.NoWrapFlags { nsw := false, nuw := false }) : InstCombine.MOp φ

Equations

• InstCombine.MOp.shl w NoWrapFlags = InstCombine.MOp.binary w (InstCombine.MOp.BinaryOp.shl NoWrapFlags)

@[match_pattern]

def InstCombine.MOp.add {φ : ℕ} (w : InstCombine.Width φ) (NoWrapFlags : optParam LLVM.NoWrapFlags { nsw := false, nuw := false }) : InstCombine.MOp φ

Equations

• InstCombine.MOp.add w NoWrapFlags = InstCombine.MOp.binary w (InstCombine.MOp.BinaryOp.add NoWrapFlags)

@[match_pattern]

def InstCombine.MOp.mul {φ : ℕ} (w : InstCombine.Width φ) (NoWrapFlags : optParam LLVM.NoWrapFlags { nsw := false, nuw := false }) : InstCombine.MOp φ

Equations

• InstCombine.MOp.mul w NoWrapFlags = InstCombine.MOp.binary w (InstCombine.MOp.BinaryOp.mul NoWrapFlags)

@[match_pattern]

def InstCombine.MOp.sub {φ : ℕ} (w : InstCombine.Width φ) (NoWrapFlags : optParam LLVM.NoWrapFlags { nsw := false, nuw := false }) : InstCombine.MOp φ

Equations

• InstCombine.MOp.sub w NoWrapFlags = InstCombine.MOp.binary w (InstCombine.MOp.BinaryOp.sub NoWrapFlags)

@[match_pattern]

def InstCombine.MOp.lshr {φ : ℕ} (w : InstCombine.Width φ) (ExactFlag : optParam LLVM.ExactFlag { exact := false }) : InstCombine.MOp φ

Equations

• InstCombine.MOp.lshr w ExactFlag = InstCombine.MOp.binary w (InstCombine.MOp.BinaryOp.lshr ExactFlag)

@[match_pattern]

def InstCombine.MOp.ashr {φ : ℕ} (w : InstCombine.Width φ) (ExactFlag : optParam LLVM.ExactFlag { exact := false }) : InstCombine.MOp φ

Equations

• InstCombine.MOp.ashr w ExactFlag = InstCombine.MOp.binary w (InstCombine.MOp.BinaryOp.ashr ExactFlag)

@[match_pattern]

def InstCombine.MOp.sdiv {φ : ℕ} (w : InstCombine.Width φ) (ExactFlag : optParam LLVM.ExactFlag { exact := false }) : InstCombine.MOp φ

Equations

• InstCombine.MOp.sdiv w ExactFlag = InstCombine.MOp.binary w (InstCombine.MOp.BinaryOp.sdiv ExactFlag)

@[match_pattern]

def InstCombine.MOp.udiv {φ : ℕ} (w : InstCombine.Width φ) (ExactFlag : optParam LLVM.ExactFlag { exact := false }) : InstCombine.MOp φ

Equations

• InstCombine.MOp.udiv w ExactFlag = InstCombine.MOp.binary w (InstCombine.MOp.BinaryOp.udiv ExactFlag)

def InstCombine.MOp.deepCasesOn {motive : {φ : ℕ} → InstCombine.MOp φ → Sort u_1} (neg : {φ : ℕ} → {w : InstCombine.Width φ} → motive (InstCombine.MOp.neg w)) (not : {φ : ℕ} → {w : InstCombine.Width φ} → motive (InstCombine.MOp.not w)) (copy : {φ : ℕ} → {w : InstCombine.Width φ} → motive (InstCombine.MOp.copy w)) (and : {φ : ℕ} → {w : InstCombine.Width φ} → motive (InstCombine.MOp.and w)) (or : {φ : ℕ} → {DisjointFlag : LLVM.DisjointFlag} → {w : InstCombine.Width φ} → motive (InstCombine.MOp.or w DisjointFlag)) (xor : {φ : ℕ} → {w : InstCombine.Width φ} → motive (InstCombine.MOp.xor w)) (shl : {φ : ℕ} → {NoWrapFlags : LLVM.NoWrapFlags} → {w : InstCombine.Width φ} → motive (InstCombine.MOp.shl w NoWrapFlags)) (lshr : {φ : ℕ} → {ExactFlag : LLVM.ExactFlag} → {w : InstCombine.Width φ} → motive (InstCombine.MOp.lshr w ExactFlag)) (ashr : {φ : ℕ} → {ExactFlag : LLVM.ExactFlag} → {w : InstCombine.Width φ} → motive (InstCombine.MOp.ashr w ExactFlag)) (urem : {φ : ℕ} → {w : InstCombine.Width φ} → motive (InstCombine.MOp.urem w)) (srem : {φ : ℕ} → {w : InstCombine.Width φ} → motive (InstCombine.MOp.srem w)) (add : {φ : ℕ} → {NoWrapFlags : LLVM.NoWrapFlags} → {w : InstCombine.Width φ} → motive (InstCombine.MOp.add w NoWrapFlags)) (mul : {φ : ℕ} → {NoWrapFlags : LLVM.NoWrapFlags} → {w : InstCombine.Width φ} → motive (InstCombine.MOp.mul w NoWrapFlags)) (sub : {φ : ℕ} → {NoWrapFlags : LLVM.NoWrapFlags} → {w : InstCombine.Width φ} → motive (InstCombine.MOp.sub w NoWrapFlags)) (sdiv : {φ : ℕ} → {ExactFlag : LLVM.ExactFlag} → {w : InstCombine.Width φ} → motive (InstCombine.MOp.sdiv w ExactFlag)) (udiv : {φ : ℕ} → {ExactFlag : LLVM.ExactFlag} → {w : InstCombine.Width φ} → motive (InstCombine.MOp.udiv w ExactFlag)) (select : {φ : ℕ} → {w : InstCombine.Width φ} → motive (InstCombine.MOp.select w)) (icmp : {φ : ℕ} → {c : LLVM.IntPredicate} → {w : InstCombine.Width φ} → motive (InstCombine.MOp.icmp c w)) (const : {φ : ℕ} → {v : ℤ} → {w : InstCombine.Width φ} → motive (InstCombine.MOp.const w v)) {φ : ℕ} (op : InstCombine.MOp φ) : motive op

Recursion principle in terms of individual operations, rather than unary or binary

Equations

• InstCombine.MOp.deepCasesOn neg not copy and or xor shl lshr ashr urem srem add mul sub sdiv udiv select icmp const (InstCombine.MOp.unary w InstCombine.MOp.UnaryOp.neg) = neg
• InstCombine.MOp.deepCasesOn neg not copy and or xor shl lshr ashr urem srem add mul sub sdiv udiv select icmp const (InstCombine.MOp.unary w InstCombine.MOp.UnaryOp.not) = not
• InstCombine.MOp.deepCasesOn neg not copy and or xor shl lshr ashr urem srem add mul sub sdiv udiv select icmp const (InstCombine.MOp.unary w InstCombine.MOp.UnaryOp.copy) = copy
• InstCombine.MOp.deepCasesOn neg not copy and or xor shl lshr ashr urem srem add mul sub sdiv udiv select icmp const (InstCombine.MOp.binary w InstCombine.MOp.BinaryOp.and) = and
• InstCombine.MOp.deepCasesOn neg not copy and or xor shl lshr ashr urem srem add mul sub sdiv udiv select icmp const (InstCombine.MOp.binary w (InstCombine.MOp.BinaryOp.or disjoint)) = or
• InstCombine.MOp.deepCasesOn neg not copy and or xor shl lshr ashr urem srem add mul sub sdiv udiv select icmp const (InstCombine.MOp.binary w InstCombine.MOp.BinaryOp.xor) = xor
• InstCombine.MOp.deepCasesOn neg not copy and or xor shl lshr ashr urem srem add mul sub sdiv udiv select icmp const (InstCombine.MOp.binary w (InstCombine.MOp.BinaryOp.shl nswnuw)) = shl
• InstCombine.MOp.deepCasesOn neg not copy and or xor shl lshr ashr urem srem add mul sub sdiv udiv select icmp const (InstCombine.MOp.binary w (InstCombine.MOp.BinaryOp.lshr exact)) = lshr
• InstCombine.MOp.deepCasesOn neg not copy and or xor shl lshr ashr urem srem add mul sub sdiv udiv select icmp const (InstCombine.MOp.binary w (InstCombine.MOp.BinaryOp.ashr exact)) = ashr
• InstCombine.MOp.deepCasesOn neg not copy and or xor shl lshr ashr urem srem add mul sub sdiv udiv select icmp const (InstCombine.MOp.binary w InstCombine.MOp.BinaryOp.urem) = urem
• InstCombine.MOp.deepCasesOn neg not copy and or xor shl lshr ashr urem srem add mul sub sdiv udiv select icmp const (InstCombine.MOp.binary w InstCombine.MOp.BinaryOp.srem) = srem
• InstCombine.MOp.deepCasesOn neg not copy and or xor shl lshr ashr urem srem add mul sub sdiv udiv select icmp const (InstCombine.MOp.binary w (InstCombine.MOp.BinaryOp.add nswnuw)) = add
• InstCombine.MOp.deepCasesOn neg not copy and or xor shl lshr ashr urem srem add mul sub sdiv udiv select icmp const (InstCombine.MOp.binary w (InstCombine.MOp.BinaryOp.mul nswnuw)) = mul
• InstCombine.MOp.deepCasesOn neg not copy and or xor shl lshr ashr urem srem add mul sub sdiv udiv select icmp const (InstCombine.MOp.binary w (InstCombine.MOp.BinaryOp.sub nswnuw)) = sub
• InstCombine.MOp.deepCasesOn neg not copy and or xor shl lshr ashr urem srem add mul sub sdiv udiv select icmp const (InstCombine.MOp.binary w (InstCombine.MOp.BinaryOp.sdiv exact)) = sdiv
• InstCombine.MOp.deepCasesOn neg not copy and or xor shl lshr ashr urem srem add mul sub sdiv udiv select icmp const (InstCombine.MOp.binary w (InstCombine.MOp.BinaryOp.udiv exact)) = udiv
• InstCombine.MOp.deepCasesOn neg not copy and or xor shl lshr ashr urem srem add mul sub sdiv udiv select icmp const (InstCombine.MOp.select w) = select
• InstCombine.MOp.deepCasesOn neg not copy and or xor shl lshr ashr urem srem add mul sub sdiv udiv select icmp const (InstCombine.MOp.icmp c w) = icmp
• InstCombine.MOp.deepCasesOn neg not copy and or xor shl lshr ashr urem srem add mul sub sdiv udiv select icmp const (InstCombine.MOp.const w val) = const

instance InstCombine.instToStringMOp {φ : ℕ} : ToString (InstCombine.MOp φ)

Equations

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

@[reducible, inline]

abbrev InstCombine.Op : Type

Equations

• InstCombine.Op = InstCombine.MOp 0

@[reducible, match_pattern, inline]

abbrev InstCombine.Op.unary (w : ℕ) (op : InstCombine.MOp.UnaryOp) : InstCombine.Op

Equations

• InstCombine.Op.unary w op = InstCombine.MOp.unary (ConcreteOrMVar.concrete w) op

@[reducible, match_pattern, inline]

abbrev InstCombine.Op.binary (w : ℕ) (op : InstCombine.MOp.BinaryOp) : InstCombine.Op

Equations

• InstCombine.Op.binary w op = InstCombine.MOp.binary (ConcreteOrMVar.concrete w) op

@[reducible, match_pattern, inline]

abbrev InstCombine.Op.and : ℕ → InstCombine.Op

Equations

• InstCombine.Op.and = InstCombine.MOp.and ∘ ConcreteOrMVar.concrete

@[reducible, match_pattern, inline]

abbrev InstCombine.Op.not : ℕ → InstCombine.Op

Equations

• InstCombine.Op.not = InstCombine.MOp.not ∘ ConcreteOrMVar.concrete

@[reducible, match_pattern, inline]

abbrev InstCombine.Op.xor : ℕ → InstCombine.Op

Equations

• InstCombine.Op.xor = InstCombine.MOp.xor ∘ ConcreteOrMVar.concrete

@[reducible, match_pattern, inline]

abbrev InstCombine.Op.urem : ℕ → InstCombine.Op

Equations

• InstCombine.Op.urem = InstCombine.MOp.urem ∘ ConcreteOrMVar.concrete

@[reducible, match_pattern, inline]

abbrev InstCombine.Op.srem : ℕ → InstCombine.Op

Equations

• InstCombine.Op.srem = InstCombine.MOp.srem ∘ ConcreteOrMVar.concrete

@[reducible, match_pattern, inline]

abbrev InstCombine.Op.select : ℕ → InstCombine.Op

Equations

• InstCombine.Op.select = InstCombine.MOp.select ∘ ConcreteOrMVar.concrete

@[reducible, match_pattern, inline]

abbrev InstCombine.Op.neg : ℕ → InstCombine.Op

Equations

• InstCombine.Op.neg = InstCombine.MOp.neg ∘ ConcreteOrMVar.concrete

@[reducible, match_pattern, inline]

abbrev InstCombine.Op.copy : ℕ → InstCombine.Op

Equations

• InstCombine.Op.copy = InstCombine.MOp.copy ∘ ConcreteOrMVar.concrete

@[reducible, match_pattern, inline]

abbrev InstCombine.Op.icmp (c : LLVM.IntPredicate) : ℕ → InstCombine.Op

Equations

• InstCombine.Op.icmp c = InstCombine.MOp.icmp c ∘ ConcreteOrMVar.concrete

@[reducible, match_pattern, inline]

abbrev InstCombine.Op.const (w : ℕ) (val : ℤ) : InstCombine.Op

Equations

• InstCombine.Op.const w val = InstCombine.MOp.const (ConcreteOrMVar.concrete w) val

@[reducible, match_pattern, inline]

abbrev InstCombine.Op.or (w : ℕ) (flag : optParam LLVM.DisjointFlag { disjoint := false }) : InstCombine.Op

Equations

• InstCombine.Op.or w flag = InstCombine.MOp.or (ConcreteOrMVar.concrete w) flag

@[reducible, match_pattern, inline]

abbrev InstCombine.Op.shl (w : ℕ) (flags : optParam LLVM.NoWrapFlags { nsw := false, nuw := false }) : InstCombine.Op

Equations

• InstCombine.Op.shl w flags = InstCombine.MOp.shl (ConcreteOrMVar.concrete w) flags

@[reducible, match_pattern, inline]

abbrev InstCombine.Op.add (w : ℕ) (flags : optParam LLVM.NoWrapFlags { nsw := false, nuw := false }) : InstCombine.Op

Equations

• InstCombine.Op.add w flags = InstCombine.MOp.add (ConcreteOrMVar.concrete w) flags

@[reducible, match_pattern, inline]

abbrev InstCombine.Op.mul (w : ℕ) (flags : optParam LLVM.NoWrapFlags { nsw := false, nuw := false }) : InstCombine.Op

Equations

• InstCombine.Op.mul w flags = InstCombine.MOp.mul (ConcreteOrMVar.concrete w) flags

@[reducible, match_pattern, inline]

abbrev InstCombine.Op.sub (w : ℕ) (flags : optParam LLVM.NoWrapFlags { nsw := false, nuw := false }) : InstCombine.Op

Equations

• InstCombine.Op.sub w flags = InstCombine.MOp.sub (ConcreteOrMVar.concrete w) flags

@[reducible, match_pattern, inline]

abbrev InstCombine.Op.lshr (w : ℕ) (flag : optParam LLVM.ExactFlag { exact := false }) : InstCombine.Op

Equations

• InstCombine.Op.lshr w flag = InstCombine.MOp.lshr (ConcreteOrMVar.concrete w) flag

@[reducible, match_pattern, inline]

abbrev InstCombine.Op.ashr (w : ℕ) (flag : optParam LLVM.ExactFlag { exact := false }) : InstCombine.Op

Equations

• InstCombine.Op.ashr w flag = InstCombine.MOp.ashr (ConcreteOrMVar.concrete w) flag

@[reducible, match_pattern, inline]

abbrev InstCombine.Op.sdiv (w : ℕ) (flag : optParam LLVM.ExactFlag { exact := false }) : InstCombine.Op

Equations

• InstCombine.Op.sdiv w flag = InstCombine.MOp.sdiv (ConcreteOrMVar.concrete w) flag

@[reducible, match_pattern, inline]

abbrev InstCombine.Op.udiv (w : ℕ) (flag : optParam LLVM.ExactFlag { exact := false }) : InstCombine.Op

Equations

• InstCombine.Op.udiv w flag = InstCombine.MOp.udiv (ConcreteOrMVar.concrete w) flag

instance InstCombine.instToStringOp : ToString InstCombine.Op

Equations

• InstCombine.instToStringOp = { toString := fun (o : InstCombine.Op) => (repr o).pretty }

@[reducible]

def InstCombine.MOp.sig {φ : ℕ} : InstCombine.MOp φ → List (InstCombine.MTy φ)

Equations

• (InstCombine.MOp.binary w op).sig = [InstCombine.MTy.bitvec w, InstCombine.MTy.bitvec w]
• (InstCombine.MOp.icmp c w).sig = [InstCombine.MTy.bitvec w, InstCombine.MTy.bitvec w]
• (InstCombine.MOp.unary w op).sig = [InstCombine.MTy.bitvec w]
• (InstCombine.MOp.select w).sig = [InstCombine.MTy.bitvec 1, InstCombine.MTy.bitvec w, InstCombine.MTy.bitvec w]
• (InstCombine.MOp.const w val).sig = []

@[reducible]

def InstCombine.MOp.outTy {φ : ℕ} : InstCombine.MOp φ → InstCombine.MTy φ

Equations

• (InstCombine.MOp.binary w op).outTy = InstCombine.MTy.bitvec w
• (InstCombine.MOp.unary w op).outTy = InstCombine.MTy.bitvec w
• (InstCombine.MOp.select w).outTy = InstCombine.MTy.bitvec w
• (InstCombine.MOp.const w val).outTy = InstCombine.MTy.bitvec w
• (InstCombine.MOp.icmp c w).outTy = InstCombine.MTy.bitvec 1

@[reducible, inline]

abbrev InstCombine.MetaLLVM (φ : ℕ) : Dialect

MetaLLVM φ is the LLVM dialect with at most φ metavariables

Equations

• InstCombine.MetaLLVM φ = { Op := InstCombine.MOp φ, Ty := InstCombine.MTy φ, m := Id }

@[reducible, inline]

abbrev InstCombine.LLVM : Dialect

Equations

• InstCombine.LLVM = { Op := InstCombine.Op, Ty := InstCombine.Ty, m := Id }

instance InstCombine.instDialectSignatureMetaLLVM {φ : ℕ} : DialectSignature (InstCombine.MetaLLVM φ)

Equations

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

instance InstCombine.instDialectSignatureLLVM : DialectSignature InstCombine.LLVM

Equations

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

def InstCombine.Op.denote (o : InstCombine.LLVM.Op) (op : HVector TyDenote.toType (DialectSignature.sig o)) : ⟦DialectSignature.outTy o⟧

Equations

• One or more equations did not get rendered due to their size.
• InstCombine.Op.denote (InstCombine.MOp.const (ConcreteOrMVar.concrete a) val) op_2 = LLVM.const? val
• InstCombine.Op.denote (InstCombine.MOp.unary (ConcreteOrMVar.concrete a) InstCombine.MOp.UnaryOp.copy) op_2 = op_2.getN 0 InstCombine.Op.denote.proof_1
• InstCombine.Op.denote (InstCombine.MOp.unary (ConcreteOrMVar.concrete a) InstCombine.MOp.UnaryOp.not) op_2 = LLVM.not (op_2.getN 0 InstCombine.Op.denote.proof_1)
• InstCombine.Op.denote (InstCombine.MOp.unary (ConcreteOrMVar.concrete a) InstCombine.MOp.UnaryOp.neg) op_2 = LLVM.neg (op_2.getN 0 InstCombine.Op.denote.proof_1)
• InstCombine.Op.denote (InstCombine.MOp.icmp c (ConcreteOrMVar.concrete a)) op_2 = LLVM.icmp c (op_2.getN 0 InstCombine.Op.denote.proof_2) (op_2.getN 1 InstCombine.Op.denote.proof_3)

instance InstCombine.instDialectDenoteLLVM : DialectDenote InstCombine.LLVM

Equations

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