diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,22 @@ +Copyright 2020-2022 Joey Hess . + +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. diff --git a/TODO b/TODO new file mode 100644 --- /dev/null +++ b/TODO @@ -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. diff --git a/copilot-frp-sketch.cabal b/copilot-frp-sketch.cabal new file mode 100644 --- /dev/null +++ b/copilot-frp-sketch.cabal @@ -0,0 +1,48 @@ +Name: copilot-frp-sketch +Version: 1.0.0 +Cabal-Version: >= 1.10 +License: BSD3 +Maintainer: Joey Hess +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. + + +Extra-Source-Files: + TODO + +Library + GHC-Options: -Wall -fno-warn-tabs + Default-Language: Haskell2010 + Hs-Source-Dirs: src + Exposed-Modules: + Copilot.FRPSketch + Copilot.FRPSketch.Internals + Build-Depends: + base (>= 4.5 && < 5), + copilot (== 3.7.*), + copilot-c99 (== 3.7.*), + copilot-language (== 3.7.*), + filepath, + directory, + mtl, + temporary, + optparse-applicative (>= 0.14.1), + containers + +source-repository head + type: git + location: git://git.joeyh.name/copilot-frp-sketch.git diff --git a/src/Copilot/FRPSketch.hs b/src/Copilot/FRPSketch.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/FRPSketch.hs @@ -0,0 +1,114 @@ +{-# 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 diff --git a/src/Copilot/FRPSketch/Internals.hs b/src/Copilot/FRPSketch/Internals.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/FRPSketch/Internals.hs @@ -0,0 +1,383 @@ +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE ScopedTypeVariables #-} + +module Copilot.FRPSketch.Internals where + +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.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 +-- +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 = Sketch (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 = Sketch (return ()) + +instance Semigroup (GenSketch pinid t) where + (Sketch a) <> (Sketch b) = Sketch (a >> b) + +newtype UniqueIds = UniqueIds (M.Map String Integer) + +newtype UniqueId = UniqueId Integer + +data TriggerLimit + = TriggerLimit (Behavior Bool) + | NoTriggerLimit + +getTriggerLimit :: TriggerLimit -> Behavior Bool +getTriggerLimit (TriggerLimit b) = b +getTriggerLimit NoTriggerLimit = true + +addTriggerLimit :: TriggerLimit -> Behavior Bool -> Behavior Bool +addTriggerLimit tl c = getTriggerLimit (tl <> TriggerLimit c) + +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 + +evalSketch :: Ord pinid => GenSketch pinid a -> (Maybe Spec, GenFramework pinid) +evalSketch (Sketch 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 + +-- | 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 (Sketch 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 [(const (return ()), combinetl f)] + return r + where + combinetl :: (TriggerLimit -> a) -> TriggerLimit -> a + combinetl g tl = g (TriggerLimit c <> tl) + +-- | 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 + +-- | 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 + +-- | 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) + +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] + +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 + +data PinMode = InputMode | InputPullupMode | OutputMode + deriving (Show, Eq, Ord) + +-- | Things that can have a `Behavior` or `Event` output to them. +class Output 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 o (Event () (Stream v)) => Output o (Behavior v) where + (=:) o b = o =: te + where + te :: Event () (Stream v) + te = Event b true + +instance Output o (Event p (Stream v)) => Output o (TypedBehavior p v) where + (=:) o (TypedBehavior b) = o =: te + where + te :: Event p (Stream v) + te = Event b true + +-- | 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 + +class Input o t where + -- | The list is input to use when simulating the Sketch. + input' :: o -> [t] -> GenSketch pinid (Behavior t) + +-- | 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 o t => o -> GenSketch pinid (Behavior t) +input o = input' o []