ctford

(ns ture.cdr-police
  (:require [overtone.live :refer :all :exclude [stop]]
            [leipzig.melody :refer :all]
            [leipzig.scale :as scale]
            [leipzig.canon :as canon]
            [leipzig.live :as live]
            [leipzig.live :refer [stop]]
            [leipzig.chord :as chord]
            [leipzig.temperament :as temperament]))

ctford

module Data.FSM.Entropy
%default total

data Solfege = Do | Re | Mi | Fa | So | La | Ti

entropy : Solfege -> Solfege -> Nat
entropy Do Do = 1
entropy Do Re = 2
entropy Re Do = 2
entropy Re Re = 1

ctford

module Entropy
import Data.List

%default total

data Probability : a -> Nat -> Type where
  Occurred : (x : a) -> Probability x bits

begin : Probability [] 0
begin = Occurred []

ctford

module Optic.Prism

import Data.List
%default total

-- Const
data Const a b = Constant a

implementation Functor (Const a) where
  map _ (Constant x) = (Constant x)

ctford

module Data.Chain
%default total

data Chain : Type -> Type -> Type
where
  Link : (a -> b) -> Chain a b
  Section : (a -> b) -> Chain b c -> Chain a c

fuse : Chain a b -> a -> b
fuse (Link f) x = f x

ctford

module Data.FSM.Channel
import Data.List
%default total

data Protocol : Type
where
  Out    : a -> Protocol -> Protocol
  In     : a -> Protocol -> Protocol
  Accept : Protocol -> Protocol -> Protocol
  Select : Protocol -> Protocol -> Protocol

ctford

%default total

data Channel : (result :Type ) -> Type
where
  Send     : a -> Channel a
  Receive  : a -> Channel a
  Finished : Channel ()
  (>>=)    : Channel a -> ((x:a) -> Channel b) -> Channel b

dual : Channel a -> Channel a

ctford

(ns whilst.song
  (:require [overtone.live :refer :all]
            [leipzig.melody :refer :all]
            [leipzig.scale :as scale]
            [leipzig.live :as live]
            [leipzig.chord :as chord]
            [leipzig.temperament :as temperament]))

; Instruments
(definst bass [freq 110 dur 1 volume 1.0]

ctford

when : (test : Bool) -> a -> b -> if test then a else b
when True x _ = x
when False _ y = y

ctford

locate : Eq a => (key : a) -> (entries : List (a, b)) -> {auto membership : Elem key (map Prelude.Basics.fst entries)} -> b
locate {membership} _ [] = absurd membership
locate {membership = Here} key ((key, value) :: _) = value
locate {membership = (There later)} key (_ :: entries) = locate key entries {membership = later}