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