-- | Programming the Arduino with Copilot.
--
-- This module should work on any model of Arduino.
-- See Arduino.Uno and Arduino.Nano for model-specific code.
{-# LANGUAGE RebindableSyntax #-}
module Copilot.Arduino (
-- * Arduino sketch generation
arduino,
Sketch,
Input,
Output,
Stream,
GPIO,
-- * Combinators
(=:),
(@:),
-- * Inputs
readfrom,
readfrom',
-- * Outputs
--
-- | Only outputs that work on all Arduino boards are included
-- here. Load a module such as Arduino.Uno for model-specific
-- outputs.
led,
writeto,
MicroSeconds,
delay,
-- * Utilities
blinking,
firstIteration,
sketchSpec,
-- * Copilot DSL
--
-- | The Copilot.Language module is re-exported here, including
-- a version of the Prelude modified for it. You should enable
-- the RebindableSyntax language extension in your program
-- to use the Copilot DSL.
--
-- > {-# LANGUAGE RebindableSyntax #-}
--
-- For documentation on using the Copilot DSL, see
-- <https://copilot-language.github.io/>
module Language.Copilot,
) where
import qualified Language.Copilot
import Language.Copilot hiding (Stream)
import Copilot.Arduino.Internals
import Copilot.Arduino.Main
import Control.Monad.Writer
-- | A value that varies over time.
--
-- The Copilot DSL provides many operations on streams, for example
-- `Language.Copilot.&&` to combine two streams of Bools.
--
-- For documentation on using the Copilot DSL, see
-- <https://copilot-language.github.io/>
type Stream t = Language.Copilot.Stream t
-- | Connect a `Stream` to an `Output`.
--
-- > led := blinking
(=:) :: Output t -> Stream t -> Sketch ()
o =: s = tell [(go, toFramework o)]
where
go = (outputBehavior o) (outputCond o) s
-- | Use this to make a LED blink on and off.
--
-- On each iteration of the `Sketch`, this changes to the opposite of its
-- previous value.
--
-- This is implemented using Copilot's `clk`, so to get other blinking
-- behaviors, just pick different numbers, or use Copilot `Stream`
-- combinators.
--
-- > blinking = clk (period 2) (phase 1)
blinking :: Stream Bool
blinking = clk (period (2 :: Integer)) (phase (1 :: Integer))
-- Same fixity as =<<
infixr 1 =:
-- | By default, an `Output` is written to on each iteration of the `Sketch`.
--
-- For example, this constantly turns on the LED, even though it will
-- already be on after the first iteration.
--
-- > led =: true
--
-- To avoid unnecessary work being done, this combinator can make an
-- `Output` only be written to when the current value of the provided
-- `Stream` is True.
--
-- So to make the LED only be turned on in the first iteration,
-- and allow it to remain on thereafter without doing extra work:
--
-- > led @: firstIteration =: true
(@:) :: Output t -> Stream Bool -> Output t
(@:) o c = o { outputCond = c }
-- | True on the first iteration of the `Sketch`, and False thereafter.
firstIteration :: Stream Bool
firstIteration = [True]++false
-- | Use this to add a delay between each iteration of the `Sketch`.
-- A `Sketch` with no delay will run as fast as the hardware can run it.
delay :: Output MicroSeconds
delay = Output
{ setupOutput = []
, outputBehavior = \c n -> trigger "delay" c [arg n]
, outputCond = true
}
-- | Reading from a GPIO pin.
--
-- > do
-- > buttonpressed <- readfrom pin12
-- > led := buttonpressed
readfrom :: GPIO -> Input Bool
readfrom n = readfrom' n []
-- | The list is used as simulated input when interpreting the program.
readfrom' :: GPIO -> [Bool] -> Input Bool
readfrom' (GPIO n) interpretvalues = mkInput $ InputSource
{ defineVar = ["bool " <> varname]
, setupInput = ["pinMode(" <> show n <> ", INPUT)"]
, readInput = [varname <> " = digitalRead(" <> show n <> ")"]
, inputStream = extern varname interpretvalues'
}
where
varname = "arduino_gpio_input" <> show n
interpretvalues'
| null interpretvalues = Nothing
| otherwise = Just interpretvalues
-- | Writing to a GPIO pin.
writeto :: GPIO -> Output Bool
writeto (GPIO n) = Output
{ setupOutput = ["pinMode(" <> sn <> ", OUTPUT)"]
, outputBehavior =
\c v -> trigger "digitalWrite" c [arg (constant n), arg v]
, outputCond = true
}
where
sn = show n
-- | The on-board LED.
led :: Output Bool
led = writeto (GPIO 13)
-- | Extracts a copilot `Spec` from a `Sketch`.
--
-- This can be useful to intergrate with other libraries
-- such as copilot-theorem.
sketchSpec :: Sketch a -> Spec
sketchSpec (Sketch s) = sequence_ is
where
(is, _fs) = unzip (execWriter s)