Types.hs

{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}

module Sketch.FRP.Copilot.Types where

import Language.Copilot
import Control.Monad.Writer
import Control.Monad.State.Strict
import qualified Data.Map as M
import qualified Data.Set as S
import Data.Type.Bool
import GHC.TypeLits

-- | A value that changes over time.
--
-- This is implemented as a `Stream` in the Copilot DSL.
-- Copilot 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 Behavior t = Stream t

-- | A Behavior with an additional phantom type `p`.
--
-- The Compilot DSL only lets a Stream contain basic C types,
-- a limitation that `Behavior` also has. When more type safely
-- is needed, this can be used.
data TypedBehavior p t = TypedBehavior (Behavior t)

-- | A discrete event, that occurs at particular points in time.
data Event p v = Event v (Stream Bool)

-- | A sketch, implemented using Copilot.
--
-- It's best to think of the `Sketch` as a description of the state of the
-- board at any point in time.
--
-- Under the hood, the `Sketch` is run in a loop. On each iteration, it first
-- reads inputs and then updates outputs as needed.
--
-- While it is a monad, a Sketch's outputs are not updated in any
-- particular order, because Copilot does not guarantee any order.
--
-- This is a generalized Sketch that can operate on any type of context.
newtype GenSketch ctx t = GenSketch (WriterT [(TriggerLimit -> Spec, TriggerLimit -> GenFramework ctx)] (State UniqueIds) t)
	deriving 
		( Monad
		, Applicative
		, Functor
		, MonadWriter [(TriggerLimit -> Spec, TriggerLimit -> GenFramework ctx)]
		, MonadState UniqueIds
		)

instance Monoid (GenSketch ctx ()) where
	mempty = GenSketch (return ())

instance Semigroup (GenSketch ctx t) where
	(GenSketch a) <> (GenSketch b) = GenSketch (a >> b)

class Ord ctx => Context ctx

-- | Things that can have a `Behavior` or `Event` output to them.
class Output ctx o t where
	(=:) :: o -> t -> GenSketch ctx ()
	-- ^ Connect a `Behavior` or `Event` to an `Output`
	-- 
	-- > led =: blinking
	-- 
	-- When a `Behavior` is used, its current value is written 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, because `true`
	-- is a `Behavior` (that is always True).
	-- 
	-- > led =: true
	-- 
	-- To avoid unncessary work being done, you can use an `Event`
	-- instead. Then the write only happens at the points in time
	-- when the `Event` occurs. To turn a `Behavior` into an `Event`,
	-- use `@:`
	-- 
	-- 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 =: true @: firstIteration

-- Same fixity as =<<
infixr 1 =:

instance Output ctx o (Event () (Stream v)) => Output ctx o (Behavior v) where
	(=:) o b = o =: te
	  where
	  	te :: Event () (Stream v)
		te = Event b true

instance Output ctx o (Event p (Stream v)) => Output ctx o (TypedBehavior p v) where
	(=:) o (TypedBehavior b) = o =: te
	  where
		te :: Event p (Stream v)
		te = Event b true

class Input ctx o t where
	-- | The list is input to use when simulating the Sketch.
	input' :: o -> [t] -> GenSketch ctx (Behavior t)

-- | The framework of a sketch.
--
-- This is a generalized Framework that can operate on any type of
-- context.
data GenFramework ctx = Framework
	{ defines :: [CChunk]
	-- ^ Things that come before the C code generated by Copilot.
	, setups :: [CChunk]
	-- ^ Things to do at setup, not including configuring pins.
	, earlySetups :: [CChunk]
	-- ^ Things to do at setup, before the setups.
	, pinmodes :: M.Map ctx (S.Set PinMode)
	-- ^ How pins are used.
	, loops :: [CChunk]
	-- ^ Things to run in `loop`.
	}

instance Context ctx => Semigroup (GenFramework ctx) where
	a <> b = Framework
		{ defines = defines a <> defines b
		, setups = setups a <> setups b
		, earlySetups = earlySetups a <> earlySetups b
		, pinmodes = M.unionWith S.union (pinmodes a) (pinmodes b)
		, loops = loops a  <> loops b
		}

instance Context ctx => Monoid (GenFramework ctx) where
	mempty = Framework mempty mempty mempty mempty mempty

newtype UniqueIds = UniqueIds (M.Map String Integer)

newtype UniqueId = UniqueId Integer

data TriggerLimit
	= TriggerLimit (Behavior Bool)
	| NoTriggerLimit

instance Monoid TriggerLimit where
	mempty = NoTriggerLimit

instance Semigroup TriggerLimit where
	TriggerLimit a <> TriggerLimit b =
		TriggerLimit (a Language.Copilot.&& b)
	a <> NoTriggerLimit = a
	NoTriggerLimit <> b = b

data PinMode = InputMode | InputPullupMode | OutputMode
	deriving (Show, Eq, Ord)

-- | A line of C code.
newtype CLine = CLine { fromCLine :: String }
	deriving (Eq, Show, Ord)

-- | A chunk of C code. Identical chunks get deduplicated.
newtype CChunk = CChunk [CLine]
	deriving (Eq, Show, Ord, Semigroup, Monoid)

-- | This type family is open, so it can be extended when adding other data
-- types to the IsBehavior class.
type family BehaviorToEvent a
type instance BehaviorToEvent (Behavior v) = Event () (Stream v)
type instance BehaviorToEvent (TypedBehavior p v) = Event p (Stream v)

class IsBehavior behavior where
	-- | Generate an Event, from some type of behavior,
	-- that only occurs when the `Behavior` Bool is True.
	(@:) :: behavior -> Behavior Bool -> BehaviorToEvent behavior

instance IsBehavior (Behavior v) where
	b @: c = Event b c

instance IsBehavior (TypedBehavior p v) where
	(@:) (TypedBehavior b) c = Event b c

data PinCapabilities
	= DigitalIO
	| AnalogInput
	| PWM
	deriving (Show, Eq, Ord)

type family IsDigitalIOPin t where
	IsDigitalIOPin t = 
		'True ~ If (HasPinCapability 'DigitalIO t)
			('True)
			(TypeError ('Text "This Pin does not support digital IO"))

type family IsAnalogInputPin t where
	IsAnalogInputPin t = 
		'True ~ If (HasPinCapability 'AnalogInput t)
			('True)
			(TypeError ('Text "This Pin does not support analog input"))

type family IsPWMPin t where
	IsPWMPin t = 
		'True ~ If (HasPinCapability 'PWM t)
			('True)
			(TypeError ('Text "This Pin does not support PWM"))

type family HasPinCapability (c :: t) (list :: [t]) :: Bool where
	HasPinCapability c '[] = 'False
	HasPinCapability c (x ': xs) = SameCapability c x || HasPinCapability c xs

type family SameCapability a b :: Bool where
	SameCapability 'DigitalIO 'DigitalIO = 'True
	SameCapability 'AnalogInput 'AnalogInput = 'True
	SameCapability 'PWM 'PWM = 'True
	SameCapability _ _ = 'False