sketch-frp-copilot (empty) → 1.0.0

raw patch · 7 files changed

+614/−0 lines, 7 filesdep +basedep +containersdep +copilot

Dependencies added: base, containers, copilot, copilot-c99, copilot-language, mtl, optparse-applicative

Files

• CHANGELOG +5/−0
• LICENSE +22/−0
• TODO +27/−0
• sketch-frp-copilot.cabal +47/−0
• src/Sketch/FRP/Copilot.hs +152/−0
• src/Sketch/FRP/Copilot/Internals.hs +143/−0
• src/Sketch/FRP/Copilot/Types.hs +218/−0

@@ -0,0 +1,5 @@+sketch-frp-copilot (1.0.0) upstream; urgency=medium++  * First release, factored out of arduino-copilot and zephyr-copilot.++ -- Joey Hess <id@joeyh.name>  Mon, 14 Feb 2022 14:27:37 -0400

@@ -0,0 +1,22 @@+Copyright 2020-2022 Joey Hess <id@joeyh.name>.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions+are met:+1. Redistributions of source code must retain the above copyright+   notice, this list of conditions and the following disclaimer.+2. Redistributions in binary form must reproduce the above copyright+   notice, this list of conditions and the following disclaimer in the+   documentation and/or other materials provided with the distribution.++THIS SOFTWARE IS PROVIDED BY AUTHORS AND CONTRIBUTORS ``AS IS'' AND+ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE+ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHORS OR CONTRIBUTORS BE LIABLE+FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS+OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)+HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT+LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY+OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF+SUCH DAMAGE.

@@ -0,0 +1,27 @@+* liftB and liftB2 imply liftB[3..5] at least ought to exist.++  Really, want something like Applicative. But apparently TypedBehavior+  is not a Functor, and so cannot be Applicative. There might be some+  way to use type classes to do arbitrary arity lifting. Take a look+  at QuickCheck and printf for ideas. Also see+  https://www.seas.upenn.edu/~sweirich/papers/aritygen++  Alternative might be to wrap all of Copilot DSL's functions like (>)+  with ones that operate on TypedBehavior and Event. +  (Then rename TypedBehavior to Behavior and make everything produce+  and consume that, rather than the underlying Stream?)++  Alternativly, copilot could be improved, see+  https://github.com/Copilot-Language/copilot/issues/56+  https://github.com/Copilot-Language/copilot/issues/59++* using whenB with an input' makes the interpretation see+  each value from the list, even when the whenB is supposed to prevent the+  input' from having run, and the value should be whatever was input+  previously. This may not be fixable w/o Copilot DSL support+  for limiting when inputs happen, at least as far as what the interpreter+  displays as values of the input goes. But, it should be fixable+  as far as the value that is input, at least in theory, by ignoring+  the input values that should not have been input. The  Copilot+  DSL code used to do that may increase the size of the C program+  unncessarily though.

@@ -0,0 +1,47 @@+Name: sketch-frp-copilot+Version: 1.0.0+Cabal-Version: >= 1.10+License: BSD3+Maintainer: Joey Hess <id@joeyh.name>+Author: Joey Hess+Stability: Experimental+Copyright: 2020-2022 Joey Hess+License-File: LICENSE+Build-Type: Simple+Category: Embedded, Language+Synopsis: FRP sketch programming with Copilot+Description:+ This extends Copilot with a FRP-like interface which can be used to+ implement simple standalone programs (sketches) for embedded boards.+ .+ It is used by arduino-copilot and zephyr-copilot.+ .+ Copilot is a stream (i.e., infinite lists) domain-specific language+ (DSL) in Haskell that compiles into embedded C. Copilot contains an+ interpreter, multiple back-end compilers, and other verification tools.+ <https://copilot-language.github.io/>++Extra-Source-Files:+ TODO+ CHANGELOG++Library+  GHC-Options: -Wall -fno-warn-tabs+  Default-Language: Haskell2010+  Hs-Source-Dirs: src+  Exposed-Modules:+    Sketch.FRP.Copilot+    Sketch.FRP.Copilot.Types+    Sketch.FRP.Copilot.Internals+  Build-Depends:+    base (>= 4.5 && < 5),+    copilot (== 3.7.*),+    copilot-c99 (== 3.7.*),+    copilot-language (== 3.7.*),+    mtl,+    optparse-applicative (>= 0.14.1),+    containers++source-repository head+  type: git+  location: git://git.joeyh.name/sketch-frp-copilot.git

@@ -0,0 +1,152 @@+{-# LANGUAGE RebindableSyntax #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE FlexibleInstances #-}++module Sketch.FRP.Copilot where++import Sketch.FRP.Copilot.Types+import Language.Copilot hiding (ifThenElse)+import qualified Language.Copilot+import Control.Monad.Writer+import Control.Monad.State.Strict+import Data.Functor.Identity++-- | 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)++-- | 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++-- | 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++-- | Limit the effects of a `Sketch` to times when a `Behavior` `Bool` is True.+--+-- When applied to `=:`, this does the same thing as `@:` but without+-- the FRP style conversion the input `Behavior` into an `Event`. So `@:`+-- is generally better to use than this.+--+-- But, this can also be applied to `input`, to limit how often input+-- gets read. Useful to avoid performing slow input operations on every+-- iteration of a Sketch.+--+-- > v <- whenB (frequency 10) $ input pin12+--+-- (It's best to think of the value returned by that as an Event,+-- but it's currently represented as a Behavior, since the Copilot DSL+-- cannot operate on Events.)+whenB :: Ord pinid => Behavior Bool -> GenSketch pinid t -> GenSketch pinid t+whenB c (GenSketch s) = do+	ids <- get+	let ((r, w), ids') = runIdentity $ runStateT (runWriterT s) ids+	put ids'+	let (is, fs) = unzip w+	let spec = combinetl $ \c' -> sequence_ (map (\i -> i c') is)+	tell [(spec, mempty)]+	forM_ fs $ \f -> tell [(\_tl -> (return ()), combinetl f)]+	return r+  where+	combinetl :: (TriggerLimit -> a) -> TriggerLimit -> a+	combinetl g tl = g (TriggerLimit c <> tl)++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++-- | Use this to read a value from a component of the board.+--+-- For example, to read a digital value from pin12 and turn on the +-- led when the pin is high:+--+-- > buttonpressed <- input pin12+-- > led =: buttonpressed+--+-- Some pins support multiple types of reads, for example a pin may+-- support a digital read (`Bool`), and an analog to digital converter+-- read (`ADC`). In such cases you may need to specify the type of+-- data to read:+--+-- > v <- input a0 :: Sketch (Behavior ADC)+input :: Input pinid o t => o -> GenSketch pinid (Behavior t)+input o = input' o []++-- | A stream of milliseconds.+data MilliSeconds = MilliSeconds (Stream Word32)++-- | A stream of microseconds.+data MicroSeconds = MicroSeconds (Stream Word32)++data Delay = Delay++-- | 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

@@ -0,0 +1,143 @@+module Sketch.FRP.Copilot.Internals where++import Sketch.FRP.Copilot.Types+import Language.Copilot+import Control.Monad.Writer+import Control.Monad.State.Strict+import Data.Functor.Identity+import qualified Data.Map as M+import qualified Data.Set as S+import Data.Maybe++getTriggerLimit :: TriggerLimit -> Behavior Bool+getTriggerLimit (TriggerLimit b) = b+getTriggerLimit NoTriggerLimit = true++addTriggerLimit :: TriggerLimit -> Behavior Bool -> Behavior Bool+addTriggerLimit tl c = getTriggerLimit (tl <> TriggerLimit c)++-- | Gets a unique id.+getUniqueId :: String -> GenSketch pinid UniqueId+getUniqueId s = do+	UniqueIds m <- get+	let u = maybe 1 succ (M.lookup s m)+	put $ UniqueIds $ M.insert s u m+	return (UniqueId u)++-- | Generates a unique name.+uniqueName :: String -> UniqueId -> String+uniqueName s (UniqueId i)+	| i Prelude.== 1 = s+	| otherwise = s <> "_" <>  show i++uniqueName' :: String -> UniqueId -> String+uniqueName' s (UniqueId i) = s <> "_" <>  show i++-- | Use to create an empty framework. +--+-- It helps to specify the type of pinid to use:+--+-- > (emptyFramework @PinId) { ... }+emptyFramework :: Ord pinid => GenFramework pinid+emptyFramework = mempty++mkCChunk :: [CLine] -> [CChunk]+mkCChunk l = [CChunk l]++-- | Copilot only supports calling a trigger with a given name once+-- per Spec; the generated C code will fail to build if the same name is+-- used in two triggers. This generates a unique alias that can be +-- used in a trigger.+defineTriggerAlias+	:: String+	-> GenFramework pinid+	-> GenSketch pinid (GenFramework pinid, String)+defineTriggerAlias = defineTriggerAlias' ""++defineTriggerAlias'+	:: String+	-> String+	-> GenFramework pinid+	-> GenSketch pinid (GenFramework pinid, String)+defineTriggerAlias' suffix cfuncname f = do+	let basetname = if null suffix +		then cfuncname+		else cfuncname <> "_" <> suffix+	u <- getUniqueId basetname+	let triggername = uniqueName basetname u+	let define = if cfuncname Prelude./= triggername+		then mkCChunk [ CLine $ "#define " <> triggername <> " " <> cfuncname	]+		else mempty+	return (f { defines = define <> defines f }, triggername)++data MkInputSource pinid t = InputSource+	{ defineVar :: [CChunk]+	-- ^ Added to the `Framework`'s `defines`, this typically+	-- defines a C variable.+	, setupInput :: [CChunk]+	-- ^ How to set up the input, not including pin mode.+	, inputPinmode :: M.Map pinid PinMode+	-- ^ How pins are used by the input.+	, readInput :: [CChunk]+	-- ^ How to read a value from the input, this typically+	-- reads a value into a C variable.+	, inputStream :: Stream t+	-- ^ How to use Copilot's extern to access the input values.+	}++mkInput :: MkInputSource pinid t -> GenSketch pinid (Behavior t)+mkInput i = do+	u <- getUniqueId "input"+	tell [(mkspec u, f u)]+	return (inputStream i)+  where+	f u ratelimited = Framework+		{ defines = defineVar i <> mkdefine u ratelimited+		, setups = setupInput i+		, earlySetups = mempty+		, pinmodes = M.map S.singleton (inputPinmode i)+		, loops = mkloops u ratelimited (readInput i)+		}++	varname = uniqueName "update_input"+	triggername = uniqueName "input"+	+	mkdefine _ NoTriggerLimit = []+	mkdefine u (TriggerLimit _) = mkCChunk $ map CLine+		[ "bool " <> varname u <> " = true;"+		, "void " <> triggername u <> " (bool v) {"+		, "  " <> varname u <> " = v;"+		, "}"+		]+	+	mkloops _ NoTriggerLimit reader = reader+	mkloops u (TriggerLimit _) reader = mkCChunk $ concat+		[ [ CLine $ "if (" <> varname u <> ") {" ]+		, map (\(CLine l) -> CLine $ "  " <> l ) readerlines+		, [ CLine "}" ]+		]+	  where+		readerlines = concatMap (\(CChunk l) -> l) reader++	mkspec _ NoTriggerLimit = return ()+	mkspec u (TriggerLimit c) = trigger (triggername u) true [arg c]++evalSketch :: Ord pinid => GenSketch pinid a -> (Maybe Spec, GenFramework pinid)+evalSketch (GenSketch s) = (spec, f)+  where+	(is, fs) = unzip $ +		runIdentity $ evalStateT (execWriterT s) (UniqueIds mempty)+	f = mconcat (map (\f' -> f' NoTriggerLimit) fs)+	-- Copilot will throw an ugly error if given a spec that does+	-- nothing at all, so return Nothing to avoid that.+	spec :: Maybe Spec+	spec = if null is+		then Nothing+		else Just $ sequence_ $ map (\i -> i NoTriggerLimit) is++-- | 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

@@ -0,0 +1,218 @@+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE FlexibleInstances #-}+{-# 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 pinid.+newtype GenSketch pinid t = GenSketch (WriterT [(TriggerLimit -> Spec, TriggerLimit -> GenFramework pinid)] (State UniqueIds) t)+	deriving +		( Monad+		, Applicative+		, Functor+		, MonadWriter [(TriggerLimit -> Spec, TriggerLimit -> GenFramework pinid)]+		, MonadState UniqueIds+		)++instance Monoid (GenSketch pinid ()) where+	mempty = GenSketch (return ())++instance Semigroup (GenSketch pinid t) where+	(GenSketch a) <> (GenSketch b) = GenSketch (a >> b)++-- | Things that can have a `Behavior` or `Event` output to them.+class Output pinid o t where+	(=:) :: o -> t -> GenSketch pinid ()+	-- ^ 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 pinid o (Event () (Stream v)) => Output pinid o (Behavior v) where+	(=:) o b = o =: te+	  where+	  	te :: Event () (Stream v)+		te = Event b true++instance Output pinid o (Event p (Stream v)) => Output pinid o (TypedBehavior p v) where+	(=:) o (TypedBehavior b) = o =: te+	  where+		te :: Event p (Stream v)+		te = Event b true++class Input pinid o t where+	-- | The list is input to use when simulating the Sketch.+	input' :: o -> [t] -> GenSketch pinid (Behavior t)++-- | The framework of a sketch.+--+-- This is a generalized Framework that can operate on any type of pinid.+data GenFramework pinid = 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 pinid (S.Set PinMode)+	-- ^ How pins are used.+	, loops :: [CChunk]+	-- ^ Things to run in `loop`.+	}++instance Ord pinid => Semigroup (GenFramework pinid) 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 Ord pinid => Monoid (GenFramework pinid) 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