-- | Programming the Arduino with Copilot.
--
-- This module should work on any model of Arduino.
-- See Copilot.Arduino.Uno and Copilot.Arduino.Nano for model-specific code.
--
-- There are also libraries like Copilot.Arduino.Library.Serial to support
-- additional hardware.
{-# LANGUAGE RebindableSyntax #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
module Copilot.Arduino (
-- * Arduino sketch generation
arduino,
Sketch,
Input,
Output,
-- | 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/>
Stream,
Pin,
PinCapabilities(..),
-- * Combinators
(=:),
(@:),
-- * Inputs
readfrom,
readfrom',
pullup,
Voltage,
readvoltage,
readvoltage',
-- * Outputs
--
-- | Only outputs that work on all Arduino boards are included
-- here. Import a module such as Copilot.Arduino.Uno for
-- model-specific outputs.
led,
writeto,
DutyCycle,
pwm,
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 X,
) where
import Language.Copilot as X hiding (Stream)
import Language.Copilot (Stream)
import Copilot.Arduino.Internals
import Copilot.Arduino.Main
import Control.Monad.Writer
import qualified Data.Map as M
import qualified Data.Set as S
-- | 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 =: constant 100
delay :: Output MicroSeconds
delay = Output
{ setupOutput = []
, outputBehavior = \c n -> trigger "delay" c [arg n]
, outputCond = true
, outputPinmode = mempty
}
-- | Reading a Bool from a `Pin`.
--
-- > do
-- > buttonpressed <- readfrom pin12
-- > led =: buttonpressed
readfrom :: IsDigitalIOPin t => Pin t -> Input Bool
readfrom p = readfrom' p []
-- | The list is used as simulated input when interpreting the program.
readfrom' :: IsDigitalIOPin t => Pin t -> [Bool] -> Input Bool
readfrom' (Pin p@(PinId n)) interpretvalues = mkInput $ InputSource
{ defineVar = [CLine $ "bool " <> varname <> ";"]
, setupInput = []
, inputPinmode = M.singleton p InputMode
, readInput = [CLine $ varname <> " = digitalRead(" <> show n <> ");"]
, inputStream = extern varname interpretvalues'
}
where
varname = "arduino_digital_pin_input" <> show n
interpretvalues'
| null interpretvalues = Nothing
| otherwise = Just interpretvalues
-- | Normally when a `Pin` is read with `readfrom`, it is configured
-- without the internal pullup resistor being enabled. Use this to enable
-- the pullup register for all reads from the `Pin`.
--
-- Bear in mind that enabling the pullup resistor inverts the value that
-- will be read from the pin.
--
-- > pullup pin3
pullup :: Pin t -> Sketch ()
pullup (Pin p) = tell [(return (), f)]
where
f = mempty
{ pinmodes = M.singleton p (S.singleton InputPullupMode)
}
-- | Voltage read from an Arduino's ADC. Ranges from 0-1023.
type Voltage = Int16
-- | Measuring the voltage of a `Pin`.
readvoltage :: IsAnalogInputPin t => Pin t -> Input Voltage
readvoltage p = readvoltage' p []
readvoltage' :: IsAnalogInputPin t => Pin t -> [Int16] -> Input Voltage
readvoltage' (Pin (PinId n)) interpretvalues = mkInput $ InputSource
{ defineVar = [CLine $ "int " <> varname <> ";"]
, setupInput = []
, inputPinmode = mempty
, readInput = [CLine $ varname <> " = analogRead(" <> show n <> ");"]
, inputStream = extern varname interpretvalues'
}
where
varname = "arduino_analog_pin_input" <> show n
interpretvalues'
| null interpretvalues = Nothing
| otherwise = Just interpretvalues
-- | Writing to a pin.
--
-- > writeto pin3 =: blinking
writeto :: IsDigitalIOPin t => Pin t -> Output Bool
writeto (Pin p@(PinId n)) = Output
{ setupOutput = []
, outputPinmode = M.singleton p OutputMode
, outputBehavior =
\c v -> trigger "digitalWrite" c [arg (constant n), arg v]
, outputCond = true
}
-- | PWM output to a pin.
--
-- > pwm pin3 =: constant 128
pwm :: IsPWMPin t => Pin t -> Output DutyCycle
pwm (Pin (PinId n)) = Output
{ setupOutput = []
, outputPinmode = mempty -- analogWrite does not need pinMode
, outputBehavior =
\c v -> trigger "analogWrite" c [arg (constant n), arg v]
, outputCond = true
}
-- | Describes a PWM square wave. Between 0 (always off) and 255 (always on).
type DutyCycle = Word8
-- | The on-board LED.
led :: Output Bool
led = writeto p
where
p :: Pin '[ 'DigitalIO ]
p = Pin (PinId 13)
-- | An 8 bit character.
-- | 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)