Skip to content

Instantly share code, notes, and snippets.

@bmsherman
bmsherman / StreamSemantics.asd
Created March 21, 2019 05:33
Computable semantics of random streams
! Standard operations
let tt : bool = mkbool True False;;
let ff : bool = mkbool False True;;
let log (x : real) : real = dedekind_cut (fun q : real => exp q <b x);;
let pi2 : real = 3 * (cut q : [1.0, 1.1] left cos q > 0.5 right cos q < 0.5);;
let pi : real = cut q : [3.1415926, 3.1415927] left sin q > 0 right sin q < 0;;
let twopi : real = cut q : [6.28318, 6.28319] left sin q < 0 right sin q > 0;;
(* Categories *)
Class Cat {C : Type} :=
{ arr : C -> C -> Type
; eq : forall {A B : C}, arr A B -> arr A B -> Prop }.
Arguments Cat : clear implicits.
Section Functor.
Context {C D : Type} `{Cat C} `{Cat D}.
@bmsherman
bmsherman / RealLEM.v
Created May 28, 2016 12:01
Coq's classical real numbers imply the weak law of excluded middle
Require Import Reals.
Definition WeakLEM := forall (P : Prop), {~~P} + {~P}.
Local Open Scope R_scope.
Definition ind (P : Prop) (x : R) : Prop :=
(x = 0) \/ (x = 1 /\ P).
@bmsherman
bmsherman / Semideciders.v
Created May 18, 2016 13:07
Semideciders
CoInductive Partial {A : Type} : Type :=
| Now : A -> Partial
| Later : Partial -> Partial.
Arguments Partial : clear implicits.
(** We can use this to loop. *)
CoFixpoint loop {A : Type} := @Later A loop.
Definition unfold_Partial {A : Type} : forall (px : Partial A),
@bmsherman
bmsherman / InhabitedIso.v
Created March 28, 2016 16:44
An isomorphism of types involving truncation.
Record T { A B : Type } : Type :=
{ to : A -> B
; from : B -> A
; from_to : forall (a : A), from (to a) = a
; to_from : forall (b : B), to (from b) = b
}.
Arguments T : clear implicits.
Inductive inhabited {A : Type} : Prop :=
@bmsherman
bmsherman / Tree_indices.v
Created January 6, 2016 17:24
Tree indices
Inductive Tree :=
| Branch : forall {n}, Vector.t Tree n -> Tree.
Inductive TreeNode : Tree -> Type :=
| Root : forall {t : Tree}, TreeNode t
| InBranch : forall {n : nat} {xs : Vector.t Tree n}
(i : Fin.t n),
TreeNode (Vector.nth xs i) -> TreeNode (Branch xs).
Lemma fin_dec : forall {n : nat} (x y : Fin.t n),
@bmsherman
bmsherman / Sampler.hs
Last active December 31, 2015 19:29
The Sampler monad
{-# LANGUAGE Rank2Types #-}
module Sampler where
import Control.Applicative
import System.Random
data Sampler a = Sampler { sample :: RandomGen g => g -> (a, g) }
instance Monad Sampler where
(Sampler f) >>= g = Sampler $ \r -> let (x, r2) = f r; Sampler h = g x in h r2
@bmsherman
bmsherman / cuda-fold-failures
Created November 6, 2013 17:02
Results from summing a vector of length n with constant 1s using accelerate for values of n ranging from 1 to 1025. Left: interpreter, Right: CUDA.
Intrp. CUDA
1 1
2 2
3 3
4 4
5 5
6 6
7 7
8 8
9 9
@bmsherman
bmsherman / device-query
Created November 6, 2013 16:56
CUDA device query
./deviceQuery Starting...
CUDA Device Query (Runtime API) version (CUDART static linking)
Detected 1 CUDA Capable device(s)
Device 0: "GeForce GTX 580"
CUDA Driver Version / Runtime Version 5.5 / 5.5
CUDA Capability Major/Minor version number: 2.0
Total amount of global memory: 3072 MBytes (3220766720 bytes)
@bmsherman
bmsherman / accelerate-examples-cuda-failure
Created November 6, 2013 16:53
Output of running accelerate-examples --cuda -k There are failures.
running with CUDA backend
to display available options, rerun with '--help'
map-abs: Ok
map-plus: Ok
map-square: Ok
zip: Ok
zipWith-plus: Ok
fold-sum: Ok
fold-product: Ok