copilot-frp-sketch-1.0.0: src/Copilot/FRPSketch.hs

{-# LANGUAGE RebindableSyntax #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Copilot.FRPSketch where

import Copilot.FRPSketch.Internals
import Language.Copilot hiding (ifThenElse)
import qualified Language.Copilot
import Data.Maybe

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

-- | Use this to make an event occur 1 time out of n.
--
-- This is implemented using Copilot's `clk`:
--
-- > frequency = clk (period n) (phase 1)
frequency :: Integer -> Behavior Bool
frequency n = clk (period n) (phase 1)

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

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

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

class IfThenElse t a where
	-- | This allows "if then else" expressions to be written
	-- that choose between two Streams, or Behaviors, or TypedBehaviors,
	-- or Sketches, when the RebindableSyntax language extension is
	-- enabled.
	--
	-- > {-# LANGUAGE RebindableSyntax #-}
	-- > buttonpressed <- input pin3
	-- > if buttonpressed then ... else ...
	ifThenElse :: Behavior Bool -> t a -> t a -> t a

instance Typed a => IfThenElse Stream a where
	ifThenElse = Language.Copilot.ifThenElse

instance Typed a => IfThenElse (TypedBehavior p) a where
	ifThenElse c (TypedBehavior a) (TypedBehavior b) =
		TypedBehavior (ifThenElse c a b)

instance Ord pinid => IfThenElse (GenSketch pinid) () where
	ifThenElse c a b = do
		whenB c a
		whenB (not c) b

instance (Ord pinid, Typed a) => IfThenElse (GenSketch pinid) (Behavior a) where
	ifThenElse c a b = do
		ra <- whenB c a
		rb <- whenB (not c) b
		return $ Language.Copilot.ifThenElse c ra rb

-- | Schedule when to perform different Sketches.
scheduleB
	:: (Typed t, Eq t, Ord pinid)
	=> Behavior t
	-> [(t, GenSketch pinid ())]
	-> GenSketch pinid ()
scheduleB b = sequence_ . map go
  where
	go (v, s) = whenB (b == constant v) s

-- | Extracts a copilot `Spec` from a `Sketch`.
--
-- This can be useful to intergrate with other libraries 
-- such as copilot-theorem.
sketchSpec :: Ord pinid => GenSketch pinid a -> Spec
sketchSpec = fromMaybe (return ()) . fst . evalSketch

-- | Apply a Copilot DSL function to a `TypedBehavior`.
liftB
	:: (Behavior a -> Behavior r)
	-> TypedBehavior t a
	-> Behavior r
liftB f (TypedBehavior b) = f b

-- | Apply a Copilot DSL function to two `TypedBehavior`s.
liftB2
	:: (Behavior a -> Behavior b -> Behavior r)
	-> TypedBehavior t a
	-> TypedBehavior t b
	-> Behavior r
liftB2 f (TypedBehavior a) (TypedBehavior b) = f a b