evanrinehart

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

evanrinehart

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.

evanrinehart

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

evanrinehart

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)

evanrinehart

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)

evanrinehart

minn a@(x:xs) b@(y:ys) = case compare x y of
  LT -> a
  GT -> b
  EQ -> x : minn xs ys

evanrinehart

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:

evanrinehart

== procs ==
proc 0:
0: r0,r1 = 19 div 3
1: sleep

== heap ==

== stack ==
(empty)

evanrinehart

-- 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

evanrinehart

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