diff --git a/CHANGELOG b/CHANGELOG new file mode 100644 --- /dev/null +++ b/CHANGELOG @@ -0,0 +1,5 @@ +zephyr-copilot (1.0.0) unstable; urgency=medium + + * First release. + + -- Joey Hess Fri, 11 Feb 2022 14:07:02 -0400 diff --git a/Examples/Blink/Demo.cabal b/Examples/Blink/Demo.cabal new file mode 100644 --- /dev/null +++ b/Examples/Blink/Demo.cabal @@ -0,0 +1,10 @@ +Name: Demo +Cabal-Version: >= 1.10 +Build-Type: Simple +Version: 0.0 + +Library + GHC-Options: -Wall -fno-warn-tabs + Default-Language: Haskell2010 + Exposed-Modules: Demo + Build-Depends: zephyr-copilot, base (>= 4.5 && < 5) diff --git a/Examples/Blink/Demo.hs b/Examples/Blink/Demo.hs new file mode 100644 --- /dev/null +++ b/Examples/Blink/Demo.hs @@ -0,0 +1,10 @@ +{-# LANGUAGE RebindableSyntax #-} + +module Examples.Blink.Demo where + +import Copilot.Zephyr.Board.Generic + +main :: IO () +main = zephyr $ do + led0 =: blinking + delay =: MilliSeconds (constant 100) diff --git a/Examples/Blink/README b/Examples/Blink/README new file mode 100644 --- /dev/null +++ b/Examples/Blink/README @@ -0,0 +1,25 @@ +This is a demo program using zephyr-copilot. + +To build the C code: + + stack build zephyr-copilot + stack runghc Demo.hs + +It simply flashes the board's User LED, so should work on many boards. + +The resulting `generated/` directory can be built and flashed to a board +using Zephyr. + +First, follow Zephyr's getting started guide to install it: +https://docs.zephyrproject.org/latest/getting_started/ + +Once Zephyr is working, to build the code generated by zephyr-copilot, +run west from within the zephyr git repository, pointing at the path +of the `generated/` directory. For example: + + west build -b adafruit_trinket_m0 -s \ + ~/zephyr-copilot/Examples/Blink/generated/ + +Then to flash it to the board: + + west flash diff --git a/Examples/Blink/stack.yaml b/Examples/Blink/stack.yaml new file mode 100644 --- /dev/null +++ b/Examples/Blink/stack.yaml @@ -0,0 +1,28 @@ +packages: +- '.' +- '../..' +resolver: lts-18.9 +extra-deps: +- sketch-frp-copilot-1.0.1 +- copilot-3.7 +- copilot-c99-3.7 +- copilot-core-3.7 +- copilot-language-3.7 +- copilot-libraries-3.7 +- copilot-theorem-3.7 +- ansi-terminal-0.9.1 +- bimap-0.3.3 +- language-c99-0.1.2 +- language-c99-simple-0.1.2 +- language-c99-util-0.1.1 +- optparse-applicative-0.15.1.0 +- panic-0.4.0.1 +- parameterized-utils-2.1.3.0 +- random-1.1 +- what4-1.1 +- bitwise-1.0.0.1 +- config-value-0.8.1 +- versions-4.0.3 +- zenc-0.1.2 +- bv-sized-1.0.2 + diff --git a/Examples/Button/Demo.cabal b/Examples/Button/Demo.cabal new file mode 100644 --- /dev/null +++ b/Examples/Button/Demo.cabal @@ -0,0 +1,10 @@ +Name: Demo +Cabal-Version: >= 1.10 +Build-Type: Simple +Version: 0.0 + +Library + GHC-Options: -Wall -fno-warn-tabs + Default-Language: Haskell2010 + Exposed-Modules: Demo + Build-Depends: zephyr-copilot, base (>= 4.5 && < 5) diff --git a/Examples/Button/Demo.hs b/Examples/Button/Demo.hs new file mode 100644 --- /dev/null +++ b/Examples/Button/Demo.hs @@ -0,0 +1,21 @@ +{-# LANGUAGE RebindableSyntax #-} + +module Examples.Button.Demo where + +import Copilot.Zephyr.Board.Generic + +main :: IO () +main = zephyr $ do + buttonpressed <- input' sw0 [False, False, False, True, True] + led0 =: buttonpressed || blinking + delay =: MilliSeconds (longer_and_longer * 2) + +longer_and_longer :: Stream Word32 +longer_and_longer = counter $ counter false `mod` 64 == 0 + +counter :: Stream Bool -> Stream Word32 +counter reset = s + where + s = if reset then 0 else z + 1 + z = [0] ++ s + diff --git a/Examples/Button/README b/Examples/Button/README new file mode 100644 --- /dev/null +++ b/Examples/Button/README @@ -0,0 +1,26 @@ +This is a demo program using zephyr-copilot. + +To build the C code: + + stack build zephyr-copilot + stack runghc Demo.hs + +It lights up the board's User LED when the User Button is pressed, +and blinks it otherwise, so should work on many boards. + +The resulting `generated/` directory can be built and flashed to a board +using Zephyr. + +First, follow Zephyr's getting started guide to install it: +https://docs.zephyrproject.org/latest/getting_started/ + +Once Zephyr is working, to build the code generated by zephyr-copilot, +run west from within the zephyr git repository, pointing at the path +of the `generated/` directory. For example: + + west build -b adafruit_feather_nrf52840 -s \ + ~/zephyr-copilot/Examples/Button/generated/ + +Then to flash it to the board: + + west flash diff --git a/Examples/Button/stack.yaml b/Examples/Button/stack.yaml new file mode 100644 --- /dev/null +++ b/Examples/Button/stack.yaml @@ -0,0 +1,28 @@ +packages: +- '.' +- '../..' +resolver: lts-18.9 +extra-deps: +- sketch-frp-copilot-1.0.1 +- copilot-3.7 +- copilot-c99-3.7 +- copilot-core-3.7 +- copilot-language-3.7 +- copilot-libraries-3.7 +- copilot-theorem-3.7 +- ansi-terminal-0.9.1 +- bimap-0.3.3 +- language-c99-0.1.2 +- language-c99-simple-0.1.2 +- language-c99-util-0.1.1 +- optparse-applicative-0.15.1.0 +- panic-0.4.0.1 +- parameterized-utils-2.1.3.0 +- random-1.1 +- what4-1.1 +- bitwise-1.0.0.1 +- config-value-0.8.1 +- versions-4.0.3 +- zenc-0.1.2 +- bv-sized-1.0.2 + diff --git a/Examples/Feather/Demo.cabal b/Examples/Feather/Demo.cabal new file mode 100644 --- /dev/null +++ b/Examples/Feather/Demo.cabal @@ -0,0 +1,10 @@ +Name: Demo +Cabal-Version: >= 1.10 +Build-Type: Simple +Version: 0.0 + +Library + GHC-Options: -Wall -fno-warn-tabs + Default-Language: Haskell2010 + Exposed-Modules: Demo + Build-Depends: zephyr-copilot, base (>= 4.5 && < 5) diff --git a/Examples/Feather/Demo.hs b/Examples/Feather/Demo.hs new file mode 100644 --- /dev/null +++ b/Examples/Feather/Demo.hs @@ -0,0 +1,18 @@ +{-# LANGUAGE RebindableSyntax #-} + +module Examples.Feather.Demo where + +import Copilot.Zephyr.Board.Adafruit_feather_m0_basic_proto + +main :: IO () +main = zephyr $ do + x <- input' pin9 [False, False, False, True, True] + led0 =: not x + + pin12 =: true + pin11 =: false + pin10 =: blinking + pin6 =: frequency 4 + pin5 =: frequency 8 + + delay =: MilliSeconds (constant 100) diff --git a/Examples/Feather/README b/Examples/Feather/README new file mode 100644 --- /dev/null +++ b/Examples/Feather/README @@ -0,0 +1,25 @@ +This is a demo program using zephyr-copilot. +It is an example of using GPIO ports specific to a particular board, +in this case the adafruit_feather_m0_basic_proto. + +To build the C code: + + stack build zephyr-copilot + stack runghc Demo.hs + +The resulting `generated/` directory can be built and flashed to a board +using Zephyr. + +First, follow Zephyr's getting started guide to install it: +https://docs.zephyrproject.org/latest/getting_started/ + +Once Zephyr is working, to build the code generated by zephyr-copilot, +run west from within the zephyr git repository, pointing at the path +of the `generated/` directory. For example: + + west build -b adafruit_feather_m0_basic_proto -s \ + ~/zephyr-copilot/Examples/Feather/generated/ + +Then to flash it to the board: + + west flash diff --git a/Examples/Feather/stack.yaml b/Examples/Feather/stack.yaml new file mode 100644 --- /dev/null +++ b/Examples/Feather/stack.yaml @@ -0,0 +1,28 @@ +packages: +- '.' +- '../..' +resolver: lts-18.9 +extra-deps: +- sketch-frp-copilot-1.0.1 +- copilot-3.7 +- copilot-c99-3.7 +- copilot-core-3.7 +- copilot-language-3.7 +- copilot-libraries-3.7 +- copilot-theorem-3.7 +- ansi-terminal-0.9.1 +- bimap-0.3.3 +- language-c99-0.1.2 +- language-c99-simple-0.1.2 +- language-c99-util-0.1.1 +- optparse-applicative-0.15.1.0 +- panic-0.4.0.1 +- parameterized-utils-2.1.3.0 +- random-1.1 +- what4-1.1 +- bitwise-1.0.0.1 +- config-value-0.8.1 +- versions-4.0.3 +- zenc-0.1.2 +- bv-sized-1.0.2 + 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/README b/README new file mode 100644 --- /dev/null +++ b/README @@ -0,0 +1,35 @@ +Embedded programming in haskell using the Copilot stream DSL and Zephyr +zephyr-copilot contains allows using Haskell to program many boards +supported by the Zephyr project. + +zephyr-copilot uses the Copilot stream DSL (domain-specific language) +and Functional Reactive Programming (FRP) to generate a program which +can be compiled in Zephyr and flashed to the board. + +See Copilot.Zephyr for details on how to use write a program using this +library. + +For example, to make a board blink its LED: + + import Copilot.Zephyr.Board.Generic + main = zephyr $ do + led0 =: blinking + delay =: MilliSeconds (constant 100) + +This and other examples are included in the Examples/ directory, each +with their own README explaining how to build and use them. + +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. + + +Zephyr is a real time embedded operating system (RTOS) supporting +hundreds of boards. + +## Contributing + +Contributions are welcome, including adding support for more parts of +Zephyr and more boards that are supported by Zephyr. + +Any contribution should have well documented functions and types. diff --git a/TODO b/TODO new file mode 100644 --- /dev/null +++ b/TODO @@ -0,0 +1,18 @@ +for first release: + USB serial interface + + PWM (or remove unported code) + ADC (or remove unported code) + +later: + Write more board modules for Zerphyr's many boards. + + Generate board definition files from zephy's metadata (devicetree + etc). Unfortunately does not include GPIO pins beyond the user led + and switch for most boards. + + Also see arduino-copilot's TODO list for some generic ideas that + are also applicable here. + + Zephyr has many libraries and capabilities, that could all be + supported. diff --git a/src/Copilot/Zephyr.hs b/src/Copilot/Zephyr.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Zephyr.hs @@ -0,0 +1,92 @@ +-- | Programming embedded systems with Copilot, in functional reactive style. +-- +-- This module should work with any board supported by the Zephyr project. +-- +-- +-- See Copilot.Zephyr.Board.* for board specific modules. + +{-# LANGUAGE RebindableSyntax #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# OPTIONS_GHC -fno-warn-orphans #-} + +module Copilot.Zephyr ( + -- * Sketch generation + zephyr, + Sketch, + Pin, + Zephyr, + -- * Functional reactive programming + Behavior, + TypedBehavior(..), + Event, + (@:), + -- * Inputs + Input, + input, + input', + pullup, + -- * Outputs + Output, + (=:), + delay, + -- * Other types + MilliSeconds(..), + MicroSeconds(..), + IsDigitalIOPin, + IsAnalogInputPin, + IsPWMPin, + -- * Utilities + blinking, + firstIteration, + frequency, + sketchSpec, + -- * Combinators + liftB, + liftB2, + whenB, + scheduleB, + ifThenElse, + IfThenElse, + -- * Copilot DSL + -- + -- | Most of 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 + -- + Stream, + module X, +) where + +import Language.Copilot as X hiding (Stream, ifThenElse) +import Language.Copilot (Stream) +import Sketch.FRP.Copilot +import Copilot.Zephyr.Internals +import Copilot.Zephyr.Main +import Control.Monad.Writer +import qualified Data.Map as M +import qualified Data.Set as S + +-- | Normally when a digital value is read from a `Pin`, it is configured +-- without the internal pullup resistor being enabled. Use this to enable +-- the pullup register for all reads from the `Pin`. When the board does not +-- have an internal pullup resistor, this will have no effect. +-- +-- Bear in mind that enabling the pullup resistor inverts the value that +-- will be read from the pin. +-- +-- > pullup pin12 +pullup :: IsDigitalIOPin t => Pin t -> Sketch () +pullup (Pin p) = tell [(\_ -> return (), \_ -> f)] + where + f = (emptyFramework @Zephyr) + { pinmodes = M.singleton p (S.singleton InputPullupMode) + } diff --git a/src/Copilot/Zephyr/Board/Adafruit_feather_m0_basic_proto.hs b/src/Copilot/Zephyr/Board/Adafruit_feather_m0_basic_proto.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Zephyr/Board/Adafruit_feather_m0_basic_proto.hs @@ -0,0 +1,54 @@ +-- | Programming the adafruit_feather_m0_basic_proto board with Copilot. + +{-# LANGUAGE DataKinds #-} + +module Copilot.Zephyr.Board.Adafruit_feather_m0_basic_proto ( + module Copilot.Zephyr + , sw0 + , led0 + -- * Pins + , pin0 + , pin1 + , pin5 + , pin6 + , pin9 + , pin10 + , pin11 + , pin12 + , pin13 + , pin20 + , pin21 +) where + +import Copilot.Zephyr +import Copilot.Zephyr.Internals +import Copilot.Zephyr.Board.Generic (sw0, led0) + +-- TODO: a0, a1-a5 +-- TODO: several other pins can be analog input +-- TODO: several pins support pwm + +-- The GPIO addresses were found by reading the schematic at +-- https://learn.adafruit.com/adafruit-feather-m0-basic-proto/downloads +-- eg, pin13 is labeled as "D13" and connects to "PA17". + +pin0, pin1, pin5, pin6, pin9, pin10, pin11 :: Pin '[ 'DigitalIO ] +pin12, pin13, pin20, pin21 :: Pin '[ 'DigitalIO ] + +pin0 = Pin (Zephyr (GPIOAlias "gpio_pin_0") (porta 11)) +pin1 = Pin (Zephyr (GPIOAlias "gpio_pin_1") (porta 10)) +pin5 = Pin (Zephyr (GPIOAlias "gpio_pin_5") (porta 15)) +pin6 = Pin (Zephyr (GPIOAlias "gpio_pin_6") (porta 20)) +pin9 = Pin (Zephyr (GPIOAlias "gpio_pin_9") (porta 7)) +pin10 = Pin (Zephyr (GPIOAlias "gpio_pin_10") (porta 18)) +pin11 = Pin (Zephyr (GPIOAlias "gpio_pin_11") (porta 16)) +pin12 = Pin (Zephyr (GPIOAlias "gpio_pin_12") (porta 19)) +-- | same as led0 +pin13 = led0 +-- | SDA +pin20 = Pin (Zephyr (GPIOAlias "gpio_pin_20") (porta 22)) +-- | SCL +pin21 = Pin (Zephyr (GPIOAlias "gpio_pin_21") (porta 23)) + +porta :: Int -> GPIOAddress +porta n = GPIOAddress ("porta " <> show n) diff --git a/src/Copilot/Zephyr/Board/Adafruit_itsybitsy_m4_express.hs b/src/Copilot/Zephyr/Board/Adafruit_itsybitsy_m4_express.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Zephyr/Board/Adafruit_itsybitsy_m4_express.hs @@ -0,0 +1,69 @@ +-- | Programming the adafruit_itsybitsy_m4_express board with Copilot. + +{-# LANGUAGE DataKinds #-} + +module Copilot.Zephyr.Board.Adafruit_itsybitsy_m4_express ( + module Copilot.Zephyr + , sw0 + , led0 + -- * Pins + , pin0 + , pin1 + , pin2 + , pin3 + , pin4 + , pin7 + , pin9 + , pin10 + , pin11 + , pin12 + , pin13 + , sck + , mosi + , miso +) where + +import Copilot.Zephyr +import Copilot.Zephyr.Internals +import Copilot.Zephyr.Board.Generic (sw0, led0) + +-- TODO: a0, a1, a2-a5 +-- TODO: pin5 is output-only, not input, intended for PWM, but may be able +-- to do digital output too. Current types do not allow output-only. +-- TODO: several other pins can be analog input +-- TODO: many pins support pwm, including led0 +-- TODO: DotStar led (pin #6 and #8) + +-- The GPIO addresses were found by reading the schematic at +-- https://learn.adafruit.com/introducing-adafruit-itsybitsy-m4/downloads +-- eg, pin0 is labeled as "D0" and connects to "PA16". + +pin0, pin1, pin2, pin3, pin4, pin7, pin9, pin10 :: Pin '[ 'DigitalIO ] +pin11, pin12, pin13, sck, mosi, miso :: Pin '[ 'DigitalIO ] + +-- | RX +pin0 = Pin (Zephyr (GPIOAlias "gpio_pin_0") (porta 16)) +-- | TX +pin1 = Pin (Zephyr (GPIOAlias "gpio_pin_1") (porta 17)) +pin2 = Pin (Zephyr (GPIOAlias "gpio_pin_2") (porta 7)) +pin3 = Pin (Zephyr (GPIOAlias "gpio_pin_3") (portb 22)) +pin4 = Pin (Zephyr (GPIOAlias "gpio_pin_4") (porta 15)) +pin7 = Pin (Zephyr (GPIOAlias "gpio_pin_7") (porta 18)) +pin9 = Pin (Zephyr (GPIOAlias "gpio_pin_9") (porta 19)) +pin10 = Pin (Zephyr (GPIOAlias "gpio_pin_10") (porta 20)) +pin11 = Pin (Zephyr (GPIOAlias "gpio_pin_11") (porta 21)) +pin12 = Pin (Zephyr (GPIOAlias "gpio_pin_12") (porta 23)) +-- | same as led0 +pin13 = led0 +-- | SPI SCK +sck = Pin (Zephyr (GPIOAlias "gpio_pin_sck") (porta 1)) +-- | SPI MOSI +mosi = Pin (Zephyr (GPIOAlias "gpio_pin_mosi") (porta 0)) +-- | SPI MISO +miso = Pin (Zephyr (GPIOAlias "gpio_pin_miso") (portb 23)) + +porta :: Int -> GPIOAddress +porta n = GPIOAddress ("porta " <> show n) + +portb :: Int -> GPIOAddress +portb n = GPIOAddress ("portb " <> show n) diff --git a/src/Copilot/Zephyr/Board/Generic.hs b/src/Copilot/Zephyr/Board/Generic.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Zephyr/Board/Generic.hs @@ -0,0 +1,36 @@ +-- | This module exposes inputs and outputs that Zephyr provides +-- for many boards, such as led0 and sw0. +-- +-- When used with a board that does not support a particular input or +-- output, compilation of the generated C code will fail with an error. + +{-# LANGUAGE RebindableSyntax #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE ScopedTypeVariables #-} + +module Copilot.Zephyr.Board.Generic +( + led0, + sw0, + module X, +) where + +import Copilot.Zephyr as X +import Copilot.Zephyr.Internals + +-- | An on-board LED, connected to a GPIO pin. +-- +-- Many boards include such a LED, which is referred to as the "User LED" +-- in Zephyr's documentation. +led0 :: Pin '[ 'DigitalIO ] +led0 = Pin (Zephyr (GPIOAlias "led0") GPIOAddressBuiltIn) + +-- | A push button, connected to a GPIO pin. +-- +-- Many boards include such a button, which is referred to as the "User Button" +-- in Zephyr's documentation. +sw0 :: Pin '[ 'DigitalIO ] +sw0 = Pin (Zephyr (GPIOAlias "sw0") GPIOAddressBuiltIn) diff --git a/src/Copilot/Zephyr/Internals.hs b/src/Copilot/Zephyr/Internals.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Zephyr/Internals.hs @@ -0,0 +1,167 @@ +-- | You should not need to import this module unless you're adding support +-- for a specific board supported by Zephyr, or a Zephyr library. + +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE UndecidableInstances #-} + +module Copilot.Zephyr.Internals ( + module Copilot.Zephyr.Internals, + module X +) where + +import Sketch.FRP.Copilot as X +import Sketch.FRP.Copilot.Types as X +import Sketch.FRP.Copilot.Internals as X +import Language.Copilot +import Control.Monad.Writer +import qualified Data.Map as M +import qualified Data.Set as S +import Data.Char (toLower, toUpper) + +-- | 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. +type Sketch = GenSketch Zephyr + +-- | The framework of a sketch. +type Framework = GenFramework Zephyr + +-- | A pin on the board. +-- +-- For definitions of specific pins, load a module which provides the pins +-- of a particular board. +-- +-- A type-level list indicates how a Pin can be used, so the haskell +-- compiler will detect impossible uses of pins. +newtype Pin t = Pin Zephyr + deriving (Show, Eq, Ord) + +-- | Indicates that you're programming a board with Zephyr. +-- The similar library arduino-copilot allows programming +-- Arduinos in a very similar style to this one. +data Zephyr = Zephyr GPIOAlias GPIOAddress + deriving (Show, Eq, Ord) + +instance Context Zephyr + +newtype GPIOAlias = GPIOAlias String + deriving (Show, Eq, Ord) + +data GPIOAddress + = GPIOAddress String + -- ^ Eg "porta 17" + | GPIOAddressBuiltIn + -- ^ Use when Zephyr defines the GPIO address for a GPIOAlias. + deriving (Show, Eq, Ord) + +instance IsDigitalIOPin t => Output Zephyr (Pin t) (Event () (Stream Bool)) where + (Pin p@(Zephyr (GPIOAlias n) _)) =: (Event b c) = do + (f, triggername) <- defineTriggerAlias pinsetfunc basef + tell [(go triggername, const f)] + where + go triggername tl = + let c' = addTriggerLimit tl c + in trigger triggername c' [arg b] + basef = (emptyFramework @Zephyr) + { pinmodes = M.singleton p (S.singleton OutputMode) + , defines = (\v -> [CChunk v]) + [ CLine $ "static inline int " + <> pinsetfunc + <> "(int value) {" + , CLine $ " return gpio_pin_set" + <> "(" <> pinDevVar n + <> ", " <> pinDevDef n + <> ", value);" + , CLine "}" + ] + } + pinsetfunc = "gpio_pin_set_" <> map toLower n + +pinDevVar :: String -> String +pinDevVar n = "pin_dev_" <> map toLower n + +pinDevDef :: String -> String +pinDevDef n = "PIN_DEV_" <> map toUpper n + +pinDevNode :: String -> String +pinDevNode n = pinDevDef n <> "_NODE" + +-- FIXME for zephyr +instance IsPWMPin t => Output Zephyr (Pin t) (Event 'PWM (Stream Word8)) where + (Pin (Zephyr (GPIOAlias n) _)) =: (Event v c) = do + (f, triggername) <- defineTriggerAlias' ("pin_" <> n) "analogWrite" mempty + tell [(go triggername, const f)] + where + go triggername tl = + let c' = addTriggerLimit tl c + in trigger triggername c' [arg v] + -- analogWrite does not need any pinmodes set up + +instance IsDigitalIOPin t => Input Zephyr (Pin t) Bool where + input' (Pin p@(Zephyr (GPIOAlias n) _)) interpretvalues = mkInput $ InputSource + { defineVar = mkCChunk + [ CLine $ "bool " <> varname <> ";" + , CLine $ "static const struct gpio_dt_spec " <> specname + <> " = GPIO_DT_SPEC_GET_OR(" <> nodename <> ", gpios, {0});" + ] + , setupInput = mempty + , inputPinmode = M.singleton p InputMode + , readInput = mkCChunk + [CLine $ varname <> " = gpio_pin_get_dt(&" <> specname <> ");"] + , inputStream = extern varname interpretvalues' + } + where + varname = "zephyr_digital_pin_input_" <> n + specname = "zephyr_digital_pin_dt_spec_" <> n + nodename = pinDevNode n + interpretvalues' + | null interpretvalues = Nothing + | otherwise = Just interpretvalues + +-- | Value read from an ADC. Ranges from 0-1023. +type ADC = Int16 + +-- FIXME for zephyr +instance IsAnalogInputPin t => Input Zephyr (Pin t) ADC where + input' (Pin (Zephyr (GPIOAlias n) _)) interpretvalues = mkInput $ InputSource + { defineVar = mkCChunk [CLine $ "int " <> varname <> ";"] + , setupInput = mempty + , inputPinmode = mempty + , readInput = mkCChunk + [CLine $ varname <> " = analogRead(" <> show n <> ");"] + , inputStream = extern varname interpretvalues' + } + where + varname = "zephyr_analog_pin_input_" <> show n + interpretvalues' + | null interpretvalues = Nothing + | otherwise = Just interpretvalues + +instance Output Zephyr Delay MilliSeconds where + Delay =: (MilliSeconds n) = do + (f, triggername) <- defineTriggerAlias "k_msleep" mempty + tell [(go triggername, \_ -> f)] + where + go triggername tl = + let c = getTriggerLimit tl + in trigger triggername c [arg n] + +instance Output Zephyr Delay MicroSeconds where + Delay =: (MicroSeconds n) = do + (f, triggername) <- defineTriggerAlias "k_usleep" mempty + tell [(go triggername, \_ -> f)] + where + go triggername tl = + let c = getTriggerLimit tl + in trigger triggername c [arg n] diff --git a/src/Copilot/Zephyr/Main.hs b/src/Copilot/Zephyr/Main.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Zephyr/Main.hs @@ -0,0 +1,264 @@ +{-# LANGUAGE BangPatterns #-} + +module Copilot.Zephyr.Main (zephyr) where + +import Language.Copilot (Spec, interpret, reify) +import Copilot.Compile.C99 (compile) +import Copilot.Zephyr.Internals +import System.IO +import System.Directory +import System.IO.Temp (withSystemTempDirectory, createTempDirectory) +import System.FilePath +import System.Exit +import Data.List (isInfixOf, intercalate) +import Data.Maybe +import qualified Data.Map as M +import qualified Data.Set as S +import Options.Applicative + +-- | Typically your program's main will be implemented using this. +-- For example: +-- +-- > {-# LANGUAGE RebindableSyntax #-} +-- > +-- > import Copilot.Zephyr +-- > +-- > main = zephyr $ do +-- > led0 =: flashing +-- > delay =: MilliSeconds (constant 100) +-- +-- Running this program compiles the `Sketch` into C code using copilot +-- and writes it to a file. That can be built and uploaded to your board +-- using Zephyr. +-- +-- This also supports interpreting a `Sketch`, without loading it onto a +-- board. Run the program with parameters "-i 4" to display what it +-- would do on the first 4 iterations. The output will look something like +-- this: +-- +-- > delay: digitalWrite: +-- > (100) (13,false) +-- > (100) (13,true) +-- > (100) (13,false) +-- > (100) (13,true) +zephyr :: Sketch () -> IO () +zephyr s = go =<< execParser opts + where + opts = info (parseCmdLine <**> helper) + ( fullDesc + <> progDesc "Run this program with no options to generate an Zephyr program." + ) + + go o = case (mspec, interpretSteps o) of + (Nothing, _) -> do + hPutStrLn stderr "This Sketch does not do anything." + exitFailure + (Just spec, Just n) -> interpret n spec + (Just spec, Nothing) -> do + let name = "generated" + writeMain name spec f' + writePrjConf name kconfigs + writeAppOverlay name devicetree + writeCMakeLists name + + (mspec, f) = evalSketch s + + -- Strict evaluation because this may throw errors, + -- and we want to throw them before starting compilation. + !(f', kconfigs, devicetree) = finalizeFramework f + +data CmdLine = CmdLine + { interpretSteps :: Maybe Integer + } + + +parseCmdLine :: Parser CmdLine +parseCmdLine = CmdLine + <$> optional (option auto + ( long "interpret" + <> short 'i' + <> help "use copilot to interpret the program, displaying what it would do" + <> metavar "NUM" + )) + +writeMain :: String -> Spec -> Framework -> IO () +writeMain name spec framework = do + -- This could be a lot prettier, unfortunately copilot only exports + -- an interface that writes the generated code to a file. + -- And, the .c file includes a .h file that will make it fail to + -- build, so that include has to be filtered out. + withSystemTempDirectory "copilot" $ \toptmpdir -> do + mytmpdir <- createTempDirectory toptmpdir "copilot" + reify spec >>= compile (mytmpdir "copilot") + c <- lines <$> readFile (mytmpdir "copilot.c") + let c' = filter (Prelude.not . isInfixOf "#include \"") c + createDirectoryIfMissing False name + writeFile (name "main.c") $ + unlines $ map fromCLine $ + sketchFramework framework (map CLine c') + +writeCMakeLists :: String -> IO () +writeCMakeLists name = do + createDirectoryIfMissing False name + writeFile (name "CMakeLists.txt") $ unlines + [ "cmake_minimum_required(VERSION 3.20.0)" + , "find_package(Zephyr REQUIRED HINTS $ENV{ZEPHYR_BASE})" + , "project(" ++ name ++ ")" + , "" + , "target_sources(app PRIVATE main.c)" + ] + +data KConfig = KConfig String + +writePrjConf :: String -> [KConfig] -> IO () +writePrjConf name kconfigs = do + createDirectoryIfMissing False name + writeFile (name "prj.conf") $ unlines $ + map (\(KConfig s) -> s) kconfigs + +newtype DeviceTree = DeviceTree String + +writeAppOverlay :: String -> DeviceTree -> IO () +writeAppOverlay name (DeviceTree s) = do + createDirectoryIfMissing False name + writeFile (name "app.overlay") s + +-- Makes an Zephyr C program, using a Framework, and a list of lines of C +-- code generated by Copilot. +sketchFramework :: Framework -> [CLine] -> [CLine] +sketchFramework f ccode = map CLine $ concat + [ + [ "/* automatically generated, do not edit */" + , blank + , "#include " + , blank + ] + , map fromCLine (fromchunks (defines f)) + , [blank] + , map fromCLine ccode + , [blank] + , + [ "void main(void)" + ] + , codeblock $ concat + [ map fromCLine (fromchunks (earlySetups f)) + , map fromCLine (fromchunks (setups f)) + , ["while (1)"] + , codeblock $ concat + [ map fromCLine (fromchunks (loops f)) + , [ "step();" ] + ] + ] + ] + where + blank = "" + indent l = " " <> l + codeblock l = ["{"] <> map indent l <> ["}"] + -- If two CChunks are identical, only include it once. + -- This can happen when eg, the same setup code is generated + -- to use a resource that's accessed more than once in a program. + -- Note: Does not preserve order of chunks in the list. + fromchunks :: [CChunk] -> [CLine] + fromchunks cl = concatMap (\(CChunk l) -> l) $ + S.toList $ S.fromList cl + +finalizeFramework :: Framework -> (Framework, [KConfig], DeviceTree) +finalizeFramework f = + let (pindefines, pinsetups) = unzip $ mapMaybe setuppin + (M.toList (pinmodes f)) + includes = if not (null (concat pindefines)) + then mkCChunk + [ CLine "#include " + , CLine "#include " + , CLine "#include " + ] + else [] + f' = f + { defines = includes <> concat pindefines <> defines f + , setups = concat pinsetups <> setups f + } + kconfigs = if not (null (concat pindefines)) + then [KConfig "CONFIG_GPIO=y"] + else [] + devicetree = DeviceTree $ unlines $ + concatMap mkdevicetree (M.keys (pinmodes f)) + in (f', kconfigs, devicetree) + where + setuppin (Zephyr (GPIOAlias n) _, s) + | s == S.singleton OutputMode = Just $ + ( definepin n + , setmode n (ored ["GPIO_OUTPUT", gpioflags n]) + ) + | s == S.singleton InputMode = Just $ + ( definepin n + , setmode n (ored ["GPIO_INPUT", gpioflags n]) + ) + | s == S.singleton InputPullupMode = Just $ + ( definepin n + , setmode n (ored ["GPIO_PULL_UP", gpioflags n]) + ) + | s == S.fromList [InputMode, InputPullupMode] = Just $ + ( definepin n + , setmode n (ored ["GPIO_INPUT", "GPIO_PULL_UP", gpioflags n]) + ) + | S.null s = Nothing + | otherwise = error $ + "The program uses pin " ++ show n ++ + " in multiple ways in different places (" ++ + unwords (map show (S.toList s)) ++ "). " ++ + "This is not currently supported by zephyr-copilot." + + definepin n = mkCChunk + [ CLine $ "#define " <> gpionode n <> " DT_ALIAS(" <> n <> ")" + , CLine $ "#if DT_NODE_HAS_STATUS(" <> gpionode n <> ", okay)" + , CLine $ "#define " <> gpiolabel n + <> " DT_GPIO_LABEL(" <> gpionode n <> ", gpios)" + , CLine $ "#define " <> gpiopin n + <> " DT_GPIO_PIN(" <> gpionode n <> ", gpios)" + , CLine $ "#define " <> gpioflags n + <> " DT_GPIO_FLAGS(" <> gpionode n <> ", gpios)" + , CLine $ "#else" + , CLine $ "#error \"Unsupported board: devicetree alias is not" + <> " defined for " <> n <> "\"" + , CLine $ "#define " <> gpiolabel n <> "" + , CLine $ "#define " <> gpiopin n <> " 0" + , CLine $ "#define " <> gpioflags n <> " 0" + , CLine $ "#endif" + , CLine $ "const struct device *" <> pinDevVar n <> ";" + ] + + setmode n v = mkCChunk + [ CLine $ pinDevVar n <> " = device_get_binding(" + <> gpiolabel n <> ");" + , CLine $ "gpio_pin_configure(" + <> pinDevVar n <> ", " + <> gpiopin n <> ", " + <> v <> ");" + ] + + gpiopin n = pinDevDef n + gpiolabel n = pinDevDef (n <> "_LABEL") + gpioflags n = pinDevDef (n <> "_FLAGS") + gpionode n = pinDevNode n + + ored = intercalate " | " + + mkdevicetree (Zephyr _ GPIOAddressBuiltIn) = [] + mkdevicetree (Zephyr (GPIOAlias n) (GPIOAddress addr)) = + [ "/ {" + , "\tmypins {" + , "\t\tcompatible = \"gpio-keys\";" + , "\t\t" ++ n ++ ": " ++ n ++ "{" + , "\t\t\tgpios = <&" ++ addr ++ " 0>;" + , "\t\t\tlabel = \"" ++ n ++ "\";" + , "\t\t};" + , "\t};" + , "\taliases {" + , "\t\t" ++ map toalias n ++ " = &" ++ n ++ ";" + , "\t};" + , "};" + ] + where + toalias '_' = '-' + toalias c = c + diff --git a/stack.yaml b/stack.yaml new file mode 100644 --- /dev/null +++ b/stack.yaml @@ -0,0 +1,27 @@ +packages: +- '.' +resolver: lts-18.9 +extra-deps: +- sketch-frp-copilot-1.0.1 +- copilot-3.7 +- copilot-c99-3.7 +- copilot-core-3.7 +- copilot-language-3.7 +- copilot-libraries-3.7 +- copilot-theorem-3.7 +- ansi-terminal-0.9.1 +- bimap-0.3.3 +- language-c99-0.1.2 +- language-c99-simple-0.1.2 +- language-c99-util-0.1.1 +- optparse-applicative-0.15.1.0 +- panic-0.4.0.1 +- parameterized-utils-2.1.3.0 +- random-1.1 +- what4-1.1 +- bitwise-1.0.0.1 +- config-value-0.8.1 +- versions-4.0.3 +- zenc-0.1.2 +- bv-sized-1.0.2 +explicit-setup-deps: diff --git a/test.hs b/test.hs new file mode 100644 --- /dev/null +++ b/test.hs @@ -0,0 +1,54 @@ +-- The examples also constitute the test suite: Make sure they all compile. + +import Control.Monad +import Control.Exception +import System.Directory +import System.IO +import System.IO.Temp + +import qualified Examples.Blink.Demo +import qualified Examples.Button.Demo +import qualified Examples.Feather.Demo + +data TestCase = TestCase + { desc :: String + , builder :: IO () + , compileC :: Bool + } + +tests :: [TestCase] +tests = + [ TestCase "Blink" Examples.Blink.Demo.main True + , TestCase "Button" Examples.Button.Demo.main True + , TestCase "Feather" Examples.Feather.Demo.main True + ] + +main :: IO () +main = forM_ tests (runtest False) + +runtest :: Bool -> TestCase -> IO () +runtest canccompile t = withSystemTempDirectory "arduino-copilot-test" $ \tmpdir -> + bracket (setup tmpdir) cleanup (const copilottest) + where + setup tmpdir = do + setCurrentDirectory tmpdir + cleanup _ = return () + + copilottest = do + putStr (desc t ++ " copilot ") + hFlush stdout + r <- try' (builder t) + case r of + Right () -> do + putStrLn "OK" + hFlush stdout + ccompiletest + Left ex -> + putStrLn ("FAILED: " ++ show ex) + + ccompiletest = when (canccompile && compileC t) $ do + putStr (desc t ++ " C compilation ") + error "compilation not implemented" + + try' :: IO () -> IO (Either SomeException ()) + try' = try diff --git a/zephyr-copilot.cabal b/zephyr-copilot.cabal new file mode 100644 --- /dev/null +++ b/zephyr-copilot.cabal @@ -0,0 +1,88 @@ +Name: zephyr-copilot +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: Embedded programming in haskell using the Copilot stream DSL and Zephyr +Description: + zephyr-copilot contains allows using Haskell to program many boards + supported by the Zephyr project. + . + zephyr-copilot uses the Copilot stream DSL (domain-specific language) + and Functional Reactive Programming (FRP) to generate a program which + can be compiled in Zephyr and flashed to the board. + . + All the messy details are abstracted away, letting you focus on the + desired behavior of the board. + . + 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. + + . + Zephyr is a real time embedded operating system (RTOS) supporting + hundreds of boards. +Extra-Source-Files: + README + CHANGELOG + TODO + stack.yaml + Examples/Blink/README + Examples/Blink/Demo.cabal + Examples/Blink/stack.yaml + Examples/Button/README + Examples/Button/Demo.cabal + Examples/Button/stack.yaml + Examples/Feather/README + Examples/Feather/Demo.cabal + Examples/Feather/stack.yaml +test-suite test + Main-Is: test.hs + Type: exitcode-stdio-1.0 + GHC-Options: -Wall -fno-warn-tabs + Default-Language: Haskell2010 + Build-Depends: + base (>= 4.6 && < 5), + zephyr-copilot, + temporary, + directory, + process + Other-Modules: + Examples.Blink.Demo + Examples.Button.Demo + Examples.Feather.Demo + +Library + GHC-Options: -Wall -fno-warn-tabs + Default-Language: Haskell2010 + Hs-Source-Dirs: src + Exposed-Modules: + Copilot.Zephyr + Copilot.Zephyr.Internals + Copilot.Zephyr.Board.Generic + Copilot.Zephyr.Board.Adafruit_feather_m0_basic_proto + Copilot.Zephyr.Board.Adafruit_itsybitsy_m4_express + Other-Modules: + Copilot.Zephyr.Main + Build-Depends: + base (>= 4.5 && < 5), + sketch-frp-copilot (== 1.0.1), + 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/zephyr-copilot.git