arduino-copilot-1.2.0: src/Copilot/Arduino.hs

-- | Programming the Arduino with Copilot, in functional reactive style.
--
-- 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 #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE UndecidableInstances #-}

module Copilot.Arduino (
	-- * Arduino sketch generation
	arduino,
	Sketch,
	Pin,
	-- * Functional reactive programming
	Behavior,
	Event,
	(@:),
	-- * Inputs
	Input,
	readfrom,
	readfrom',
	pullup,
	Voltage,
	readvoltage,
	readvoltage',
	-- * Outputs
	--
	-- | Only a few common outputs are included in this module.
	-- Import a module such as Copilot.Arduino.Uno for `Pin`
	-- definitions etc.
	Output,
	led,
	(=:),
	PWMDutyCycle(..),
	delay,
	MilliSeconds(..),
	MicroSeconds(..),
	-- * 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/>
	Stream,
	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

-- | 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 :: Behavior Bool
blinking = clk (period (2 :: Integer)) (phase (1 :: Integer))

-- | True on the first iteration of the `Sketch`, and False thereafter.
firstIteration :: Behavior Bool
firstIteration = [True]++false

-- | A stream of milliseconds.
data MilliSeconds = MilliSeconds (Stream Word16)

-- | A stream of microseconds.
data MicroSeconds = MicroSeconds (Stream Word16)

-- | 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 := MilliSeconds (constant 100)
delay :: Delay
delay = Delay

data Delay = Delay

instance Output Delay MilliSeconds where
	Delay =: (MilliSeconds n) = tell
		[(trigger "delay" true [arg n], mempty)]

instance Output Delay MicroSeconds where
	Delay =: (MicroSeconds n) = tell
		[(trigger "delayMicroseconds" true [arg n], mempty)]

-- | Reading a Bool from a `Pin`.
--
-- > 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

-- | Use this to do PWM output to a pin.
--
-- > pin3 =: PWMDutyCycle (constant 128)
-- 
-- Each Word8 from the Stream describes a PWM square wave.
-- 0 is always off and 255 is always on.
data PWMDutyCycle = PWMDutyCycle (Behavior Word8)

instance IsPWMPin t => Output (Pin t) (Event PWMDutyCycle) where
	(Pin (PinId n)) =: (Event (PWMDutyCycle v) c) = tell [(go, f)]
	  where
		go = trigger triggername c [arg (constant n), arg v]
		-- analogWrite does not need any pinmodes set up
		(f, triggername) = defineTriggerAlias (show n) "analogWrite" mempty

instance IsPWMPin t => Output (Pin t) PWMDutyCycle where
	(=:) o s = o =: alwaysEvent s

-- | The on-board LED.
led :: Pin '[ 'DigitalIO ]
led = Pin (PinId 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)