michel-steuwer

import scala.collection._

val checkEnv = mutable.Map[Ref[_], Thread]()
def check[A](thread: Thread)(ref: Ref[A]): Unit = {
  checkEnv.get(ref) match {
    case Some(priorThread) =>
      if (thread != priorThread)
        println(s"$thread overriding $ref previously written by $priorThread")
    case None =>
      checkEnv.addOne(ref, thread)

michel-steuwer

# Naive algorithm
k = tvm.reduce_axis((0, K), 'k')
A = tvm.placeholder((M, K), name='A')
B = tvm.placeholder((K, N), name='B')
C = tvm.compute((M, N),lambda x, y: tvm.sum(A[x, k] * B[k, y], axis=k),name='C')
# Default schedule
s = tvm.create_schedule(C.op)

michel-steuwer

# Optimized algorithm
k = tvm.reduce_axis((0, K), 'k')
A = tvm.placeholder((M, K), name='A')
B = tvm.placeholder((K, N), name='B')
pB = tvm.compute((N / 32, K, 32), lambda x, y, z: B[y, x * 32 + z], name='pB')
C = tvm.compute((M,N), lambda x,y:tvm.sum(A[x,k] * pB[y//32,k,tvm.indexmod(y,32)], axis=k),name='C')
# Parallel schedule
s = tvm.create_schedule(C.op)
CC = s.cache_write(C, 'global')
xo, yo, xi, yi = s[C].tile(C.op.axis[0], C.op.axis[1], 32, 32)

michel-steuwer

open import Agda.Builtin.Nat

data Vec (F : Nat → Set) : Nat → Set where
  []  : Vec F 0
  _∷_ : ∀ {n} (xs : Vec F n) (x : F (suc n)) → Vec F (suc n)

map : {!   !}
map f [] = []
map f (xs ∷ x) = (map f xs) ∷ (f x)

michel-steuwer

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_)
-- open import Data.Nat.DivMod using (_div_)
open import Data.Nat.Properties
open import Data.Char
open import Data.Product using (_×_; _,_)

coerce : ∀ {ℓ} {A B : Set ℓ} → A ≡ B → A → B

michel-steuwer

Keybase proof

I hereby claim:

• I am michel-steuwer on github.
• I am michelsteuwer (https://keybase.io/michelsteuwer) on keybase.
• I have a public key ASClq9CkKkrkwZ3c309gumosurMzoFFKWOyQvgcFZ0k7Awo

To claim this, I am signing this object:

michel-steuwer

module GeneralisedDependentMatrix

import Data.Vect

neg : Int -> Int
neg x = -x

-- Vect (len: Nat) (elemt: Type)

-- A generalisation of the TriangularMatrix type

michel-steuwer

#include <iostream>

template <typename T>
concept bool
JustEqualityComparable() {
  return requires(T a, T b) {
    { a == b } -> bool;
  };
}

michel-steuwer

module my

import Syntax.PreorderReasoning
import Data.Vect

total
add_mult_suc : (n: Nat) -> (m: Nat) -> n * (S m) = n + (n * m)
add_mult_suc Z      m = Refl
add_mult_suc (S n') m =
  ( S ( m  + (n' * (S m)))    ) ={ cong {f = \x => S (m + x)        } (add_mult_suc n' m)                   }=