CopilotSing.hs

--
-- Play a song and flash LEDs on alternate notes.
-- Lee Pike <lee pike @ gmail . com> (remove spaces)
-- See http://leepike.wordpress.com/?p=427
-- BSD3 License
-- 
-- Note timing issues: http://www.arduino.cc/en/Tutorial/PlayMelody
--

module CopilotSing where

import Prelude 
  ( String, ($), unlines, map, unwords, Char, error, show
  , IO, fromIntegral, Show, length, Maybe(..))
import qualified Prelude as P
import Data.Int
import Data.List (intersperse, replicate)
import Data.Map (fromList)
import System.Directory (copyFile)

import Language.Atom (Type(..))
import Language.Copilot
import Language.Copilot.AdHocC

-- for interpreting
import Language.Copilot.Interpreter
import Language.Copilot.Core

-- pin numbers
speaker, red, green :: Spec Int32
speaker = 13
red     = 12
green   = 11

-- The main control loop.
cycleSong :: Streams
cycleSong = do
  -- Copilot vars
  let idx       = varI32 "idx"
      notes     = varI32 "notes"
      duration  = varI32 "duration"
      odd       = varI32 "odd"
      even      = varI32 "even"
      playNote  = varB   "playNote"
  -- external vars
      note = extArrI32 "notes" idx
      beat = extArrI32 "beats" idx 

  idx       .= [0] ++ (idx + 1) `mod` (fromIntegral $ length notesLst)
  notes     .= note
  duration  .= beat * 300
  odd       .= mux (idx `mod` 2 == 1) green red
  even      .= mux (idx `mod` 2 == 1) red green
  playNote  .= true 

  trigger playNote "digitalWrite" (odd <> true)
  trigger playNote "digitalWrite" (even <> false)
  trigger playNote "playtone" (speaker <> notes <> duration)


----------------------------------------------------------------------
-- Compilation
----------------------------------------------------------------------
name :: String
name = "CopilotSing"

main :: IO ()
main = do
  compile cycleSong name 
    $ setPP cCode  -- C code for above/below the Copilot program
    $ setV Verbose -- Verbose compilation
    baseOpts
  copyFile (name P.++ ".c") (name P.++ ".pde") -- SConstruct expects .pde

interpreter :: IO ()
interpreter = 
  interpret cycleSong 20 
    $ setE (emptySM {i32Map = fromList [ ("notes", notesLst)
                                       , ("beats", beatsLst)]
                    })
    $ setV Verbose 
    baseOpts

verifying :: IO ()
verifying = 
  verify (name P.++ ".c") (length notesLst * 4 + 3)
    (   "-DCBMC -I/Applications/Arduino.app/Contents/Resources/Java/hardware/arduino/cores/arduino/ "
     P.++ "-I/Applications/Arduino.app/Contents/Resources/Java/hardware/tools/avr/avr-4/include "
     P.++ "--function cbmc") 


----------------------------------------------------------------------
-- Code to place above and below the generated code.
----------------------------------------------------------------------
freq :: Char -> Int32
freq note  = 
  case note of
    'c' -> 1915
    'd' -> 1700
    'e' -> 1519
    'f' -> 1432
    'g' -> 1275
    'a' -> 1136
    'b' -> 1014
    'C' -> 956
    ' ' -> 0
    x   -> error $ "Unexpected note " P.++ show x 

-- The notes.  Replace for a new song.
notesLst :: [Int32]
notesLst = map freq jingleBellsNotes

jingleBellsNotes, happyBirthdayNotes :: String
jingleBellsNotes = "eeeeeeegcdefffffeeeddedgeeeeeeegcdefffffeeggfdc"
happyBirthdayNotes = "ccdcfe ccdcfe ccCafed aaafgf"

-- The corresponding beats.  Replace for a new song.
beatsLst, jingleBellsBeats, happyBirthdayBeats :: [Int32]
beatsLst = jingleBellsBeats
jingleBellsBeats = 
  [ 1,1,2  , 1,1,2, 1,1,1,1, 4
  , 1,1,1,1, 1,1,2, 1,1,1,1, 2,2
  , 1,1,2  , 1,1,2, 1,1,1,1, 4
  , 1,1,1,1, 1,1,2, 1,1,1,1, 4 
  ]
happyBirthdayBeats = 
  [ 1, 1, 2, 2, 2, 2,  2,  1, 1, 2, 2, 2, 2,  2
  , 1, 1, 2, 2, 2, 2, 4,  2,  1, 1, 2, 2, 2, 8]

cCode :: (String, String)
cCode =
    (unlines
    [ "#include \"WProgram.h\""
    , ""
    , arrayInit Int32 "notes" notesLst
    , arrayInit Int32 "beats" beatsLst
    , funcDecl Nothing "playtone" (replicate 3 Int32)
    ]

    , unlines
    [ function "void" "playtone" ["int32_t speaker", "int32_t tone", "int32_t duration"] P.++ "{"
    , "#ifdef CBMC"
    , "  for (int32_t i = 0; i < 1; i ++) {"
    , "#else"
    , "  for (int32_t i = 0; i < duration * 1000; i += tone * 2) {"
    , "#endif"
    , "    digitalWrite(speaker, HIGH);"
    , "    delayMicroseconds(tone);"
    , "    digitalWrite(speaker, LOW);"
    , "    delayMicroseconds(tone);"
    , "  }"
    , "}"
    , ""
    , function "void" "setup" [] P.++ "{"
    , "  " P.++ pinOut speaker
    , "  " P.++ pinOut red
    , "  " P.++ pinOut green
    , "}"
    , ""
    , function "void" "loop" [] P.++ "{"
    , " " P.++ function "  " name [] P.++ ";"
    , "    delay(3);"
    , "}"
    , ""
    , "//Just for calling CBMC."
    , function "void" "cbmc" [] P.++ "{"
    , "  setup();"
    , "  while(1) {"
    , " " P.++ function "  " name [] P.++ ";"
    , "    delay(3);"
    , "  }"
    , "}"
    ]
    )

----------------------------------------------------------------------
-- Pretty-printing C.
----------------------------------------------------------------------

function :: String -> String -> [String] -> String
function ftype nm args = 
  ftype P.++ " " P.++ nm P.++ "(" P.++ unwords (intersperse "," args) P.++ ")"

pinOut :: Spec Int32 -> String
pinOut device = function "" "pinMode" [show device, "OUTPUT"] P.++ ";"