@[reducible, inline]

abbrev Tensor1D.Index : Type

Type of tensor dimensions and indexes into tensor dimensions. NOTE: see interaction with linarith where we need to unfold Index into ℕ https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Ergonomics.3A.20linarith.20does.20not.20work.20on.20Nat.20alias/near/365631549

Equations

• Tensor1D.Index = ℕ

structure Tensor1D.Tensor1d (α : Type) [Inhabited α] : Type

• size : Tensor1D.Index
• val : Tensor1D.Index → α
• spec : ∀ ix ≥ self.size, self.val ix = default

theorem Tensor1D.Tensor1d.spec {α : Type} [Inhabited α] (self : Tensor1D.Tensor1d α) (ix : Tensor1D.Index) : ix ≥ self.size → self.val ix = default

def Tensor1D.Tensor1d.empty {α : Type} [Inhabited α] : Tensor1D.Tensor1d α

Equations

• Tensor1D.Tensor1d.empty = { size := 0, val := fun (x : Tensor1D.Index) => default, spec := ⋯ }

def Tensor1D.Tensor1d.extract {α : Type} [Inhabited α] (t : Tensor1D.Tensor1d α) (left : Tensor1D.Index) (len : Tensor1D.Index) : Tensor1D.Tensor1d α

Equations

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

def Tensor1D.Tensor1d.map {α : Type} [Inhabited α] (f : α → α) (t : Tensor1D.Tensor1d α) : Tensor1D.Tensor1d α

Equations

• Tensor1D.Tensor1d.map f t = { size := t.size, val := fun (ix : Tensor1D.Index) => if ix < t.size then f (t.val ix) else default, spec := ⋯ }

theorem Tensor1D.Tensor1d.extract_map {α : Type} {f : α → α} [Inhabited α] (t : Tensor1D.Tensor1d α) (left : Tensor1D.Index) (len : Tensor1D.Index) : Tensor1D.Tensor1d.map f (t.extract left len) = (Tensor1D.Tensor1d.map f t).extract left len

def Tensor1D.Tensor1d.fill {α : Type} [Inhabited α] (t : Tensor1D.Tensor1d α) (v : α) : Tensor1D.Tensor1d α

Equations

• t.fill v = { size := t.size, val := fun (ix : Tensor1D.Index) => if ix < t.size then v else default, spec := ⋯ }

theorem Tensor1D.Tensor1d.extract_fill {α : Type} {left : Tensor1D.Index} {len : Tensor1D.Index} {v : α} [Inhabited α] (t : Tensor1D.Tensor1d α) : (t.extract left len).fill v = (t.fill v).extract left len

def Tensor1D.Tensor1d.insertslice {α : Type} [Inhabited α] (t : Tensor1D.Tensor1d α) (sliceix : ℕ) (slice : Tensor1D.Tensor1d α) : Tensor1D.Tensor1d α

Equations

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

theorem Tensor1D.not_lt_is_geq {a : ℕ} {b : ℕ} (NOT_LT : ¬a < b) : a ≥ b

theorem Tensor1D.extractslice_insertslice {α : Type} [Inhabited α] (t : Tensor1D.Tensor1d α) (sliceix : ℕ) (slice : Tensor1D.Tensor1d α) (CORRECT : ((t.insertslice sliceix slice).extract sliceix slice.size).size ≠ 0) : (t.insertslice sliceix slice).extract sliceix slice.size = slice

structure Tensor1D.Tensor2d (α : Type) : Type

• size0 : ℕ
• size1 : ℕ
• val : Fin self.size0 → Fin self.size1 → α

def Tensor1D.Tensor2d.transpose {α : Type} (t : Tensor1D.Tensor2d α) : Tensor1D.Tensor2d α

Equations

• t.transpose = { size0 := t.size1, size1 := t.size0, val := fun (ix0 : Fin t.size1) (ix1 : Fin t.size0) => t.val ix1 ix0 }

theorem Tensor1D.Tensor2d.transpose_involutive {α : Type} (t : Tensor1D.Tensor2d α) : t.transpose.transpose = t

theorem Tensor1D.Tensor1d.map_fusion {α : Type} {g : α → α} {f : α → α} [Inhabited α] (t : Tensor1D.Tensor1d α) : Tensor1D.Tensor1d.map (g ∘ f) t = Tensor1D.Tensor1d.map g (Tensor1D.Tensor1d.map f t)

def Tensor1D.scf.for.loop {β : Sort u_1} (f : ℕ → β → β) (n : ℕ) (n_minus_i : ℕ) (acc : β) : β

Equations

• Tensor1D.scf.for.loop f n 0 acc = acc
• Tensor1D.scf.for.loop f n n_minus_i'.succ acc = Tensor1D.scf.for.loop f n n_minus_i' (f (n - n_minus_i'.succ) acc)

def Tensor1D.scf.for {β : Sort u_1} (n : ℕ) (f : ℕ → β → β) (seed : β) : β

Equations

• Tensor1D.scf.for n f seed = Tensor1D.scf.for.loop f n (n - 0) seed

theorem Tensor1D.scf.for.peel_begin {β : Sort u_1} (n : ℕ) (f : ℕ → β → β) (seed : β) : Tensor1D.scf.for.loop f (n + 1) n (f 0 seed) = Tensor1D.scf.for.loop f (n + 1) (n + 1) seed

theorem Tensor1D.scf.for.peel_end {β : Sort u_1} (n : ℕ) (f : ℕ → β → β) (seed : β) : Tensor1D.scf.for.loop f (n + 1) 0 (f n seed) = f n (Tensor1D.scf.for.loop f n 0 seed)

theorem Tensor1D.scf.for.zero_n {β : Sort u_1} (f : ℕ → β → β) (seed : β) : Tensor1D.scf.for 0 f seed = seed

def Tensor1D.scf.for.one_n {β : Sort u_1} (f : ℕ → β → β) (seed : β) : Tensor1D.scf.for 1 f seed = f 0 seed

Equations

• ⋯ = ⋯

inductive Tensor1D.Op : Type

We make the following simplifying assumptions in the IR:

• Currently, there is no way to build a tensor, we only have operations on them.
• Constants are only natural numbers, which represent indexing into tensors.
• 1D tensors are functions from indexes (natural) to tensor values (integers).

This matches the MLIR model, which has a separate index type for indexing and iXX/f32/f64 types for values held in tensors.

• add_int: Tensor1D.Op

  add two integers

• const_ix: Tensor1D.Index → Tensor1D.Op

  create a constant index

• sub_int: Tensor1D.Op

  subtract two integers

• map1d: Tensor1D.Op

  map a function onto a tensor

• extract1d: Tensor1D.Op

  extract a value at an index of a tensor

instance Tensor1D.instDecidableEqOp : DecidableEq Tensor1D.Op

Equations

• Tensor1D.instDecidableEqOp = Tensor1D.decEqOp✝

inductive Tensor1D.Ty : Type

• int: Tensor1D.Ty

  values held in tensors

• ix: Tensor1D.Ty

  shapes and indexes of tensors

• tensor1d: Tensor1D.Ty

  tensor type

instance Tensor1D.instDecidableEqTy : DecidableEq Tensor1D.Ty

Equations

• Tensor1D.instDecidableEqTy x y = if h : x.toCtorIdx = y.toCtorIdx then isTrue ⋯ else isFalse ⋯

instance Tensor1D.instInhabitedTy : Inhabited Tensor1D.Ty

Equations

• Tensor1D.instInhabitedTy = { default := Tensor1D.Ty.int }

instance Tensor1D.instTyDenoteTy : TyDenote Tensor1D.Ty

Equations

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

@[reducible]

def Tensor1D.Op.outTy : Tensor1D.Op → Tensor1D.Ty

Equations

• Tensor1D.Op.add_int.outTy = Tensor1D.Ty.int
• Tensor1D.Op.sub_int.outTy = Tensor1D.Ty.int
• (Tensor1D.Op.const_ix v).outTy = Tensor1D.Ty.ix
• Tensor1D.Op.map1d.outTy = Tensor1D.Ty.tensor1d
• Tensor1D.Op.extract1d.outTy = Tensor1D.Ty.tensor1d

@[reducible]

def Tensor1D.Op.sig : Tensor1D.Op → List Tensor1D.Ty

Equations

• Tensor1D.Op.add_int.sig = [Tensor1D.Ty.int, Tensor1D.Ty.int]
• Tensor1D.Op.sub_int.sig = [Tensor1D.Ty.int, Tensor1D.Ty.int]
• Tensor1D.Op.map1d.sig = [Tensor1D.Ty.tensor1d]
• Tensor1D.Op.extract1d.sig = [Tensor1D.Ty.tensor1d, Tensor1D.Ty.ix, Tensor1D.Ty.ix]
• (Tensor1D.Op.const_ix v).sig = []

@[reducible]

def Tensor1D.Op.regSig : Tensor1D.Op → RegionSignature Tensor1D.Ty

Equations

• Tensor1D.Op.map1d.regSig = [([Tensor1D.Ty.int], Tensor1D.Ty.int)]
• x.regSig = []

def Tensor1D.Tensor1D : Dialect

Equations

• Tensor1D.Tensor1D = { Op := Tensor1D.Op, Ty := Tensor1D.Ty, m := Id }

instance Tensor1D.instDialectSignatureTensor1D : DialectSignature Tensor1D.Tensor1D

Equations

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