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
data Selection : Type where | |
Empty : Selection | |
InHand : Nat -> Selection | |
Tower : Type | |
Tower = List Nat | |
data Hanoi : Selection -> Tower -> Tower -> Tower -> Type where | |
Start : Hanoi Empty [1,2,3,4,5] [] [] | |
Take1 : Hanoi Empty (x::xs) ys zs -> Hanoi (InHand x) xs ys zs |
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
import Data.Fin | |
import Data.List | |
%default total | |
Surjective : {A,B:Type} -> (A -> B) -> Type | |
Surjective {A} {B} f = (y:B) -> (x:A ** f x = y) | |
||| A listing of size n of a type A is a surjective map from the first n numbers | |
||| to A. If such a listing exists, then A is finite. |
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
import qualified Sound.JACK.MIDI as MIDI | |
import Sound.JACK (NFrames(NFrames), ) | |
import qualified Sound.MIDI.Message as Msg | |
import qualified Sound.MIDI.Message.Channel as Ch | |
import Data.IORef | |
startMidiListener :: IO () | |
startMidiListener = do | |
counter <- newIORef 0 |
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
import qualified Sound.JACK.MIDI as MIDI | |
import Sound.JACK (NFrames(NFrames), ) | |
import qualified Sound.MIDI.Message as Msg | |
import qualified Sound.MIDI.Message.Channel as Ch | |
import Data.IORef | |
mutableValue :: IO (IORef Int) | |
mutableValue = newIORef (0 :: Int) |
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
pick :: [a] -> IO a | |
pick urn = do | |
let n = length urn | |
when (n < 1) (throwIO (userError "nothing in the urn")) | |
i <- randomRIO (0,n-1) | |
return (urn !! i) |
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
minn a@(x:xs) b@(y:ys) = case compare x y of | |
LT -> a | |
GT -> b | |
EQ -> x : minn xs ys |
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
def sum(ptr, n, a) | |
n ? sum(ptr, n-1, a + ptr[n-1]) : a | |
ifz n goto L | |
r1 = r1 - 1 | |
r4 = r1 - 1 # without CSE | |
r3 = ptr[r4] | |
r2 = r2 + r3 | |
goto 0 # loopification | |
L: |
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
== procs == | |
proc 0: | |
0: r0,r1 = 19 div 3 | |
1: sleep | |
== heap == | |
== stack == | |
(empty) |
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
-- translate this language | |
-- e = w | x | -e | e + e | let x = e in e | |
-- into this language | |
-- a = [code] | |
-- code = t = t + t (add) | |
-- | t = -t (negate) | |
-- | t = t (copy) | |
-- > example |
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
foldr f z [] = z | |
foldr f z (x:xs) = f x (foldr f z xs) | |
foldl f z [] = z | |
foldl f z (x:xs) = foldl f (f z x) xs |
NewerOlder