def InstcombineTransformDialect.mkUnaryOp {φ : ℕ} {Γ : Ctxt (InstCombine.MetaLLVM φ).Ty} {w : InstCombine.Width φ} (op : InstCombine.MOp.UnaryOp) (e : Γ.Var (InstCombine.MTy.bitvec w)) : Expr (InstCombine.MetaLLVM φ) Γ EffectKind.pure (InstCombine.MTy.bitvec w)

Equations

• InstcombineTransformDialect.mkUnaryOp op e = Expr.mk (InstCombine.MOp.unary w op) ⋯ ⋯ (e::ₕHVector.nil) HVector.nil

def InstcombineTransformDialect.mkBinOp {φ : ℕ} {Γ : Ctxt (InstCombine.MetaLLVM φ).Ty} {w : InstCombine.Width φ} (op : InstCombine.MOp.BinaryOp) (e₁ : Γ.Var (InstCombine.MTy.bitvec w)) (e₂ : Γ.Var (InstCombine.MTy.bitvec w)) : Expr (InstCombine.MetaLLVM φ) Γ EffectKind.pure (InstCombine.MTy.bitvec w)

Equations

• InstcombineTransformDialect.mkBinOp op e₁ e₂ = Expr.mk (InstCombine.MOp.binary w op) ⋯ ⋯ (e₁::ₕ(e₂::ₕHVector.nil)) HVector.nil

def InstcombineTransformDialect.mkIcmp {φ : ℕ} {Γ : Ctxt (InstCombine.MetaLLVM φ).Ty} {w : InstCombine.Width φ} (p : LLVM.IntPredicate) (e₁ : Γ.Var (InstCombine.MTy.bitvec w)) (e₂ : Γ.Var (InstCombine.MTy.bitvec w)) : Expr (InstCombine.MetaLLVM φ) Γ EffectKind.pure (InstCombine.MTy.bitvec 1)

Equations

• InstcombineTransformDialect.mkIcmp p e₁ e₂ = Expr.mk (InstCombine.MOp.icmp p w) ⋯ ⋯ (e₁::ₕ(e₂::ₕHVector.nil)) HVector.nil

def InstcombineTransformDialect.mkSelect {φ : ℕ} {Γ : Ctxt (InstCombine.MetaLLVM φ).Ty} {ty : (InstCombine.MetaLLVM φ).Ty} (op : InstCombine.MOp φ) (c : Γ.Var (InstCombine.MTy.bitvec 1)) (e₁ : Γ.Var ty) (e₂ : Γ.Var ty) : MLIR.AST.ExceptM (InstCombine.MetaLLVM φ) (Expr (InstCombine.MetaLLVM φ) Γ EffectKind.pure ty)

Equations

• One or more equations did not get rendered due to their size.
• InstcombineTransformDialect.mkSelect op c e₁_2 e₂_2 = throw (MLIR.AST.TransformError.unsupportedOp "Unsupported select operation")

def InstcombineTransformDialect.mkTy {φ : ℕ} : MLIR.AST.MLIRType φ → MLIR.AST.ExceptM (InstCombine.MetaLLVM φ) (InstCombine.MetaLLVM φ).Ty

Equations

• InstcombineTransformDialect.mkTy (MLIR.AST.MLIRType.int MLIR.AST.Signedness.Signless w) = pure (InstCombine.MTy.bitvec w)
• InstcombineTransformDialect.mkTy x = throw MLIR.AST.TransformError.unsupportedType

instance InstcombineTransformDialect.instTransformTy {φ : ℕ} : MLIR.AST.TransformTy (InstCombine.MetaLLVM φ) φ

Equations

• InstcombineTransformDialect.instTransformTy = { mkTy := InstcombineTransformDialect.mkTy }

def InstcombineTransformDialect.mkExpr {φ : ℕ} (Γ : Ctxt (InstCombine.MetaLLVM φ).Ty) (opStx : MLIR.AST.Op φ) : MLIR.AST.ReaderM (InstCombine.MetaLLVM φ) ((eff : EffectKind) × (ty : (InstCombine.MetaLLVM φ).Ty) × Expr (InstCombine.MetaLLVM φ) Γ eff ty)

Equations

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

instance InstcombineTransformDialect.instTransformExprMetaLLVM {φ : ℕ} : MLIR.AST.TransformExpr (InstCombine.MetaLLVM φ) φ

Equations

• InstcombineTransformDialect.instTransformExprMetaLLVM = { mkExpr := InstcombineTransformDialect.mkExpr }

def InstcombineTransformDialect.mkReturn {φ : ℕ} (Γ : Ctxt (InstCombine.MetaLLVM φ).Ty) (opStx : MLIR.AST.Op φ) : MLIR.AST.ReaderM (InstCombine.MetaLLVM φ) ((eff : EffectKind) × (ty : (InstCombine.MetaLLVM φ).Ty) × Com (InstCombine.MetaLLVM φ) Γ eff ty)

Equations

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

instance InstcombineTransformDialect.instTransformReturnMetaLLVM {φ : ℕ} : MLIR.AST.TransformReturn (InstCombine.MetaLLVM φ) φ

Equations

• InstcombineTransformDialect.instTransformReturnMetaLLVM = { mkReturn := InstcombineTransformDialect.mkReturn }

Instantiation

Finally, we show how to instantiate a family of programs to a concrete program

def InstcombineTransformDialect.instantiateMTy {φ : ℕ} (vals : Mathlib.Vector ℕ φ) : (InstCombine.MetaLLVM φ).Ty → InstCombine.LLVM.Ty

Equations

• InstcombineTransformDialect.instantiateMTy vals (InstCombine.MTy.bitvec w) = InstCombine.Ty.bitvec (ConcreteOrMVar.instantiate vals w)

def InstcombineTransformDialect.instantiateMOp {φ : ℕ} (vals : Mathlib.Vector ℕ φ) : (InstCombine.MetaLLVM φ).Op → InstCombine.LLVM.Op

Equations

• InstcombineTransformDialect.instantiateMOp vals (InstCombine.MOp.binary w binOp) = InstCombine.Op.binary (ConcreteOrMVar.instantiate vals w) binOp
• InstcombineTransformDialect.instantiateMOp vals (InstCombine.MOp.unary w unOp) = InstCombine.Op.unary (ConcreteOrMVar.instantiate vals w) unOp
• InstcombineTransformDialect.instantiateMOp vals (InstCombine.MOp.select w) = InstCombine.Op.select (ConcreteOrMVar.instantiate vals w)
• InstcombineTransformDialect.instantiateMOp vals (InstCombine.MOp.icmp c w) = InstCombine.Op.icmp c (ConcreteOrMVar.instantiate vals w)
• InstcombineTransformDialect.instantiateMOp vals (InstCombine.MOp.const w val) = InstCombine.Op.const (ConcreteOrMVar.instantiate vals w) val

def InstcombineTransformDialect.instantiateCtxt {φ : ℕ} (vals : Mathlib.Vector ℕ φ) (Γ : Ctxt (InstCombine.MetaLLVM φ).Ty) : Ctxt InstCombine.Ty

Equations

• InstcombineTransformDialect.instantiateCtxt vals Γ = Ctxt.map (InstcombineTransformDialect.instantiateMTy vals) Γ

def InstcombineTransformDialect.MOp.instantiateCom {φ : ℕ} (vals : Mathlib.Vector ℕ φ) : DialectMorphism (InstCombine.MetaLLVM φ) InstCombine.LLVM

Equations

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

def InstcombineTransformDialect.mkComInstantiate {φ : ℕ} (reg : MLIR.AST.Region φ) : MLIR.AST.ExceptM (InstCombine.MetaLLVM φ) (Mathlib.Vector ℕ φ → (Γ : Ctxt InstCombine.LLVM.Ty) × (eff : EffectKind) × (ty : InstCombine.LLVM.Ty) × Com InstCombine.LLVM Γ eff ty)

Equations

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

def «term[llvm_(_,,)|_]» : Lean.ParserDescr

Equations

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

def «term[llvm|_]» : Lean.ParserDescr

Equations

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

def «commandDeftest_:=_» : Lean.ParserDescr

Equations

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