zephyr-copilot (empty) → 1.0.0

raw patch · 25 files changed

+1170/−0 lines, 25 filesdep +basedep +containersdep +copilot

Dependencies added: base, containers, copilot, copilot-c99, copilot-language, directory, filepath, mtl, optparse-applicative, process, sketch-frp-copilot, temporary, zephyr-copilot

Files

• CHANGELOG +5/−0
• Examples/Blink/Demo.cabal +10/−0
• Examples/Blink/Demo.hs +10/−0
• Examples/Blink/README +25/−0
• Examples/Blink/stack.yaml +28/−0
• Examples/Button/Demo.cabal +10/−0
• Examples/Button/Demo.hs +21/−0
• Examples/Button/README +26/−0
• Examples/Button/stack.yaml +28/−0
• Examples/Feather/Demo.cabal +10/−0
• Examples/Feather/Demo.hs +18/−0
• Examples/Feather/README +25/−0
• Examples/Feather/stack.yaml +28/−0
• LICENSE +22/−0
• README +35/−0
• TODO +18/−0
• src/Copilot/Zephyr.hs +92/−0
• src/Copilot/Zephyr/Board/Adafruit_feather_m0_basic_proto.hs +54/−0
• src/Copilot/Zephyr/Board/Adafruit_itsybitsy_m4_express.hs +69/−0
• src/Copilot/Zephyr/Board/Generic.hs +36/−0
• src/Copilot/Zephyr/Internals.hs +167/−0
• src/Copilot/Zephyr/Main.hs +264/−0
• stack.yaml +27/−0
• test.hs +54/−0
• zephyr-copilot.cabal +88/−0

@@ -0,0 +1,5 @@+zephyr-copilot (1.0.0) unstable; urgency=medium++  * First release.++ -- Joey Hess <id@joeyh.name>  Fri, 11 Feb 2022 14:07:02 -0400

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

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

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

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

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

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

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

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

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

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

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

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

@@ -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,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.+<https://copilot-language.github.io/>++Zephyr is a real time embedded operating system (RTOS) supporting+hundreds of boards. <https://zephyrproject.org/>++## 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.

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

@@ -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.+-- <https://zephyrproject.org/>+--+-- 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+	-- <https://copilot-language.github.io/>+	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)+		}

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

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

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

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

@@ -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 <zephyr.h>"+		, 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 <device.h>"+			, CLine "#include <devicetree.h>"+			, CLine "#include <drivers/gpio.h>"+			]+		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+

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

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

@@ -0,0 +1,88 @@+Name: zephyr-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: 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.+ <https://copilot-language.github.io/>+ .+ Zephyr is a real time embedded operating system (RTOS) supporting+ hundreds of boards. <https://zephyrproject.org/>+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