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