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:
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) |
# 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) |
# 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) |
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) |
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 |
I hereby claim:
To claim this, I am signing this object:
module GeneralisedDependentMatrix | |
import Data.Vect | |
neg : Int -> Int | |
neg x = -x | |
-- Vect (len: Nat) (elemt: Type) | |
-- A generalisation of the TriangularMatrix type |
#include <iostream> | |
template <typename T> | |
concept bool | |
JustEqualityComparable() { | |
return requires(T a, T b) { | |
{ a == b } -> bool; | |
}; | |
} |
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) }= |