This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
./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) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Intrp. CUDA | |
1 1 | |
2 2 | |
3 3 | |
4 4 | |
5 5 | |
6 6 | |
7 7 | |
8 8 | |
9 9 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# 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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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), |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 := |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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), |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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). | |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(* 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}. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
! 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;; |