Equations
- ToyNoRegion.instDecidableEqTy x y = if h : x.toCtorIdx = y.toCtorIdx then isTrue ⋯ else isFalse ⋯
Equations
- ToyNoRegion.instReprTy = { reprPrec := ToyNoRegion.reprTy✝ }
@[reducible]
Equations
- ToyNoRegion.instTyDenoteTy = { toType := fun (x : ToyNoRegion.Ty) => match x with | ToyNoRegion.Ty.int => BitVec 32 }
Equations
- ToyNoRegion.instReprOp = { reprPrec := ToyNoRegion.reprOp✝ }
@[reducible, inline]
Simple
is a very basic example dialect
Equations
- ToyNoRegion.Simple = { Op := ToyNoRegion.Op, Ty := ToyNoRegion.Ty, m := Id }
Instances For
Equations
- One or more equations did not get rendered due to their size.
@[reducible]
Equations
- One or more equations did not get rendered due to their size.
Equations
- ToyNoRegion.cst n = Expr.mk (ToyNoRegion.Op.const n) ToyNoRegion.cst.proof_1 ⋯ HVector.nil HVector.nil
Instances For
def
ToyNoRegion.add
{Γ : Ctxt ToyNoRegion.Simple.Ty}
(e₁ : Γ.Var ToyNoRegion.Ty.int)
(e₂ : Γ.Var ToyNoRegion.Ty.int)
:
Equations
- ToyNoRegion.add e₁ e₂ = Expr.mk ToyNoRegion.Op.add ToyNoRegion.add.proof_1 ⋯ (e₁::ₕ(e₂::ₕHVector.nil)) HVector.nil
Instances For
Equations
- ToyNoRegion.MLIR2Simple.mkTy (MLIR.AST.MLIRType.int MLIR.AST.Signedness.Signless a) = pure ToyNoRegion.Ty.int
- ToyNoRegion.MLIR2Simple.mkTy x = throw MLIR.AST.TransformError.unsupportedType
Instances For
Equations
- ToyNoRegion.MLIR2Simple.instTransformTy = { mkTy := ToyNoRegion.MLIR2Simple.mkTy }
def
ToyNoRegion.MLIR2Simple.mkExpr
(Γ : Ctxt ToyNoRegion.Simple.Ty)
(opStx : MLIR.AST.Op 0)
:
MLIR.AST.ReaderM ToyNoRegion.Simple
((eff : EffectKind) × (ty : ToyNoRegion.Simple.Ty) × Expr ToyNoRegion.Simple Γ eff ty)
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
ToyNoRegion.MLIR2Simple.mkReturn
(Γ : Ctxt ToyNoRegion.Simple.Ty)
(opStx : MLIR.AST.Op 0)
:
MLIR.AST.ReaderM ToyNoRegion.Simple
((eff : EffectKind) × (ty : ToyNoRegion.Simple.Ty) × Com ToyNoRegion.Simple Γ eff ty)
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- ToyNoRegion.eg₀val = ToyNoRegion.eg₀.denote Ctxt.Valuation.nil
Instances For
x + 0
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- ToyNoRegion.p1 = { lhs := ToyNoRegion.lhs, rhs := ToyNoRegion.rhs, correct := ToyNoRegion.p1.proof_1 }
Instances For
theorem
ToyNoRegion.hex1_rewritePeephole :
ToyNoRegion.ex1_rewritePeepholeAt = Com.var (ToyNoRegion.cst 0) (Com.var (ToyNoRegion.add ⟨1, ⋯⟩ ⟨0, ⋯⟩) (Com.ret ⟨2, ⋯⟩))
theorem
ToyNoRegion.Hex1_rewritePeephole :
ToyNoRegion.ex1_rewritePeephole = Com.var (ToyNoRegion.cst 0) (Com.var (ToyNoRegion.add ⟨1, ⋯⟩ ⟨0, ⋯⟩) (Com.ret ⟨2, ⋯⟩))
Equations
- ToyRegion.instDecidableEqTy x y = if h : x.toCtorIdx = y.toCtorIdx then isTrue ⋯ else isFalse ⋯
Equations
- ToyRegion.instReprTy = { reprPrec := ToyRegion.reprTy✝ }
@[reducible]
Equations
- ToyRegion.instTyDenoteTy = { toType := fun (x : ToyRegion.Ty) => match x with | ToyRegion.Ty.int => BitVec 32 }
Equations
- ToyRegion.instInhabitedToTypeTy = { default := ToyRegion.Ty.casesOn (motive := fun (t_1 : ToyRegion.Ty) => t = t_1 → ⟦t⟧) t (fun (h : t = ToyRegion.Ty.int) => ⋯ ▸ 0#32) ⋯ }
- add: ToyRegion.Op
- const: ℤ → ToyRegion.Op
- iterate: ℕ → ToyRegion.Op
Instances For
Equations
- ToyRegion.instReprOp = { reprPrec := ToyRegion.reprOp✝ }
@[reducible, inline]
A simple example dialect with regions
Equations
- ToyRegion.SimpleReg = { Op := ToyRegion.Op, Ty := ToyRegion.Ty, m := Id }
Instances For
@[reducible, inline]
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
@[reducible]
Equations
- One or more equations did not get rendered due to their size.
Equations
- ToyRegion.cst n = Expr.mk (ToyRegion.Op.const n) ToyRegion.cst.proof_1 ⋯ HVector.nil HVector.nil
Instances For
def
ToyRegion.add
{Γ : Ctxt ToyRegion.SimpleReg.Ty}
(e₁ : Γ.Var ToyRegion.SimpleReg.int)
(e₂ : Γ.Var ToyRegion.SimpleReg.int)
:
Equations
- ToyRegion.add e₁ e₂ = Expr.mk ToyRegion.Op.add ToyRegion.add.proof_1 ⋯ (e₁::ₕ(e₂::ₕHVector.nil)) HVector.nil
Instances For
def
ToyRegion.iterate
{Γ : Ctxt ToyRegion.SimpleReg.Ty}
(k : ℕ)
(input : Γ.Var ToyRegion.SimpleReg.int)
(body : Com ToyRegion.SimpleReg [ToyRegion.SimpleReg.int] EffectKind.impure ToyRegion.SimpleReg.int)
:
Equations
- ToyRegion.iterate k input body = Expr.mk (ToyRegion.Op.iterate k) ToyRegion.iterate.proof_1 ⋯ (input::ₕHVector.nil) (body::ₕHVector.nil)
Instances For
running f(x) = x + x
0 times is the identity.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- ToyRegion.P1.p1 = { lhs := ToyRegion.P1.lhs, rhs := ToyRegion.P1.rhs, correct := ToyRegion.P1.p1.proof_1 }
Instances For
running f(x) = x + 0
0 times is the identity.
Equations
- ToyRegion.P2.lhs = Com.var (ToyRegion.cst 0) (Com.var (ToyRegion.add ⟨0, ToyRegion.P2.lhs.proof_1⟩ ⟨1, ToyRegion.P2.lhs.proof_2⟩) (Com.ret ⟨0, ToyRegion.P2.lhs.proof_3⟩))
Instances For
Equations
- ToyRegion.P2.p2 = { lhs := ToyRegion.P2.lhs, rhs := ToyRegion.P2.rhs, correct := ToyRegion.P2.p2.proof_1 }
Instances For
example program that has the pattern 'x + 0' both at the top level, and inside a region in an iterate.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.