arduino-copilot (empty) → 0.0.1

raw patch · 11 files changed

+550/−0 lines, 11 filesdep +basedep +copilotdep +copilot-c99setup-changed

Dependencies added: base, copilot, copilot-c99, directory, filepath, mtl, unix

Files

• CHANGELOG +5/−0
• LICENSE +22/−0
• Setup.hs +2/−0
• TODO +0/−0
• arduino-copilot.cabal +63/−0
• demo/Makefile +127/−0
• demo/README +28/−0
• demo/demo.hs +25/−0
• demo/pre-build-hook.sh +2/−0
• src/Arduino.hs +262/−0
• stack.yaml +14/−0

@@ -0,0 +1,5 @@+arduino-copilot (0.0.1) unstable; urgency=medium++  * First release.++ -- Joey Hess <id@joeyh.name>  Sat, 25 Jan 2020 10:33:09 -0400

@@ -0,0 +1,22 @@+Copyright 2020 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,2 @@+import Distribution.Simple+main = defaultMain

@@ -0,0 +1,63 @@+Name: arduino-copilot+Version: 0.0.1+Cabal-Version: >= 1.8+License: BSD3+Maintainer: Joey Hess <id@joeyh.name>+Author: Joey Hess+Stability: Experimental+Copyright: 2020 Joey Hess+License-File: LICENSE+Build-Type: Simple+Category: Embedded, Language+Synopsis: Arduino programming in haskell using the stream DSL+Description:+ arduino-copilot contains the basic building blocks to program your+ Arduino Nano, Arduino Uno or compatible hardware using Haskell+ and Functional Reactive Programming (FRP).+ .+ arduino-copilot uses the Copilot stream domain-specific language (DSL)+ to generate an Arduino sketch, which can be loaded in the Arduino IDE+ and uploaded to the board. Other methods of deploying sketches to the+ Arduino, such as the Arduino-Makefile, can also be used with a sketch+ generated by arduino-copilot.+ .+ All the messy details are abstracted away, letting you focus on the+ desired behavior of the Arduino. This is all the code needed to make+ it blink its LED:+ .+ -- > import Arduino+ -- > main = arduino $ do+ -- >    led =: clk (period 2) (phase 1)+ -- >    delay =: const16 100+ .+ 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.+ A tutorial, bug reports, and todos are available at+ <https://github.com/Copilot-Language/copilot-discussion>.+Extra-Source-Files:+  CHANGELOG+  TODO+  stack.yaml+  demo/Makefile+  demo/README+  demo/demo.hs+  demo/pre-build-hook.sh++Library+  GHC-Options: -Wall -fno-warn-tabs+  Hs-Source-Dirs: src+  Exposed-Modules:+    Arduino+  Build-Depends:+    base (>= 4.5 && < 5),+    copilot (== 3.1.*),+    copilot-c99 (== 3.1.*),+    filepath,+    directory,+    mtl,+    unix++source-repository head+  type: git+  location: git://git.joeyh.name/haskell-arduino-copilot.git

@@ -0,0 +1,127 @@+# Arduino Make file. Refer to https://github.com/sudar/Arduino-Makefile+BOARD_TAG    = uno+include /usr/share/arduino/Arduino.mk++# --- leonardo (or pro micro w/leo bootloader)+#BOARD_TAG    = leonardo+#MONITOR_PORT = /dev/ttyACM0+#include /usr/share/arduino/Arduino.mk++# --- mega2560 ide 1.0+#BOARD_TAG    = mega2560+#ARDUINO_PORT = /dev/ttyACM0+#include /usr/share/arduino/Arduino.mk++# --- mega2560 ide 1.6+#BOARD_TAG    = mega+#BOARD_SUB    = atmega2560+#MONITOR_PORT = /dev/ttyACM0+#ARDUINO_DIR  = /where/you/installed/arduino-1.6.5+#include /usr/share/arduino/Arduino.mk++# --- nano ide 1.0+#BOARD_TAG    = nano328+#MONITOR_PORT = /dev/ttyUSB0+#include /usr/share/arduino/Arduino.mk++# --- nano ide 1.6+#BOARD_TAG   = nano+#BOARD_SUB   = atmega328+#ARDUINO_DIR = /where/you/installed/arduino-1.6.5+#include /usr/share/arduino/Arduino.mk++# --- pro mini+#BOARD_TAG    = pro5v328+#MONITOR_PORT = /dev/ttyUSB0+#include /usr/share/arduino/Arduino.mk++# --- sparkfun pro micro+#BOARD_TAG         = promicro16+#ALTERNATE_CORE    = promicro+#BOARDS_TXT        = $(HOME)/arduino/hardware/promicro/boards.txt+#BOOTLOADER_PARENT = $(HOME)/arduino/hardware/promicro/bootloaders+#BOOTLOADER_PATH   = caterina+#BOOTLOADER_FILE   = Caterina-promicro16.hex+#ISP_PROG     	   = usbasp+#AVRDUDE_OPTS 	   = -v+#include /usr/share/arduino/Arduino.mk++# --- chipkit+#BOARD_TAG = mega_pic32+#MPIDE_DIR = /where/you/installed/mpide-0023-linux64-20130817-test+#include /usr/share/arduino/chipKIT.mk++# --- pinoccio+#BOARD_TAG         = pinoccio256+#ALTERNATE_CORE    = pinoccio+#BOOTLOADER_PARENT = $(HOME)/arduino/hardware/pinoccio/bootloaders+#BOOTLOADER_PATH   = STK500RFR2/release_0.51+#BOOTLOADER_FILE   = boot_pinoccio.hex+#CFLAGS_STD        = -std=gnu99+#CXXFLAGS_STD      = -std=gnu++11+#include /usr/share/arduino/Arduino.mk++# --- fio+#BOARD_TAG = fio+#include /usr/share/arduino/Arduino.mk++# --- atmega-ng ide 1.6+#BOARD_TAG    = atmegang+#BOARD_SUB    = atmega168+#MONITOR_PORT = /dev/ttyACM0+#ARDUINO_DIR  = /where/you/installed/arduino-1.6.5+#include /usr/share/arduino/Arduino.mk++# --- arduino-tiny ide 1.0+#ISP_PROG     	    = usbasp+#BOARD_TAG          = attiny85at8+#ALTERNATE_CORE     = tiny+#ARDUINO_VAR_PATH   = $(HOME)/arduino/hardware/tiny/cores/tiny+#ARDUINO_CORE_PATH  = $(HOME)/arduino/hardware/tiny/cores/tiny+#AVRDUDE_OPTS 	    = -v+#include /usr/share/arduino/Arduino.mk++# --- arduino-tiny ide 1.6+#ISP_PROG       = usbasp+#BOARD_TAG      = attiny85at8+#ALTERNATE_CORE = tiny+#ARDUINO_DIR    = /where/you/installed/arduino-1.6.5+#include /usr/share/arduino/Arduino.mk++# --- damellis attiny ide 1.0+#ISP_PROG       = usbasp+#BOARD_TAG      = attiny85+#ALTERNATE_CORE = attiny-master+#AVRDUDE_OPTS   = -v+#include /usr/share/arduino/Arduino.mk++# --- damellis attiny ide 1.6+#ISP_PROG       = usbasp+#BOARD_TAG      = attiny+#BOARD_SUB      = attiny85+#ALTERNATE_CORE = attiny+#F_CPU          = 16000000L+#ARDUINO_DIR    = /where/you/installed/arduino-1.6.5+#include /usr/share/arduino/Arduino.mk++# --- teensy3+#BOARD_TAG 	 = teensy31+#ARDUINO_DIR = /where/you/installed/the/patched/teensy/arduino-1.0.6+#include /usr/share/arduino/Teensy.mk++# --- mighty 1284p+#BOARD_TAG         = mighty_opt+#BOARDS_TXT        = $(HOME)/arduino/hardware/mighty-1284p/boards.txt+#BOOTLOADER_PARENT = $(HOME)/arduino/hardware/mighty-1284p/bootloaders+#BOOTLOADER_PATH   = optiboot+#BOOTLOADER_FILE   = optiboot_atmega1284p.hex+#ISP_PROG     	   = usbasp+#AVRDUDE_OPTS 	   = -v+#include /usr/share/arduino/Arduino.mk++# --- atmega328p on breadboard+#BOARD_TAG    = atmega328bb+#ISP_PROG     = usbasp+#AVRDUDE_OPTS = -v+#BOARDS_TXT   = $(HOME)/arduino/hardware/breadboard/boards.txt+#include /usr/share/arduino/Arduino.mk

@@ -0,0 +1,28 @@+This is a demo program using arduino-copilot. ++To build the C code:++	stack run demo++The resulting `.ino` sketch can be loaded into the Arduino IDE and flashed+to an Arduino board using the IDE.++It simply flashes the Arduino's on board LED, so should work on most or all+Arduino boards.++## Arduino-Makefile integration++The `Makefile` and `pre-build-hook.sh` show how to integrate arduino-copilot+with <https://github.com/sudar/Arduino-Makefile>. This automates generating+the C code, compiling that, and flashing it onto an Arduino Uno board,+with a single command++	make flash++Note that you will need to manually build the C code once, as shown above+, since the Arduino-Makefile expects to find a `.ino` file.++The path in the `Makefile` to `Arduino.mk` may need to be adjusted (the+default is the location where on a Debian system, `apt-get install+arduino-mk` will install it). You may also adjust the `Makefile` to target+a different board than the Arduino Uno.

@@ -0,0 +1,25 @@+{-# LANGUAGE RebindableSyntax #-}++import Arduino++flashing :: Stream Bool+flashing = clk (period (2 :: Int16)) (phase 1)++longer_and_longer :: Stream Int16+longer_and_longer = counter true $ counter true false `mod` 64 == 0++counter :: Stream Bool -> Stream Bool -> Stream Int16+counter inc reset = cnt+   where+	cnt = if reset+		then 0+		else if inc+			then z + 1+			else z+	z = [0] ++ cnt++main :: IO ()+main = arduino $ do+	buttonpressed <- boolInput (Pin 14)+	led =: buttonpressed || flashing+	delay =: longer_and_longer

@@ -0,0 +1,2 @@+#!/bin/sh+exec stack run demo -Wall -fno-warn-tabs

@@ -0,0 +1,262 @@+{-# LANGUAGE RebindableSyntax #-}++module Arduino (+	module X,+	-- * Arduino sketch generation+	Sketch,+	Input,+	Output,+	arduino,+	-- * Combinators+	(=:),+	(@:),+	-- * Inputs+	boolInput,+	boolInput',+	-- TODO enumerate all avail pins, don't export constructor+	Pin(..),+	-- * Outputs+	led,+	MicroSeconds,+	delay,+	-- * Utilities+	firstIteration,+	sketchSpec,+) where++import Language.Copilot as X+import Copilot.Compile.C99+import System.Environment+import System.Directory+import System.Posix.Temp (mkdtemp)+import System.FilePath+import Text.Read+import Control.Monad.Writer+import Data.List (isInfixOf)+import qualified Prelude++-- | An Arduino sketch, implemented using copilot.+--+-- On each iteration of a Sketch, all inputs used by it are first+-- collected, before any outputs are performed.+--+-- Like a copilot `Spec`, a Sketch's outputs are not run in any+-- particular order.+type Sketch = Sketch' ()++type Sketch' t = Writer [(Spec, Framework)] t++data Framework = Framework+	{ defines :: [CFragment]+	, setups :: [CFragment]+	, loops :: [CFragment]+	}++type CFragment = String++instance Semigroup Framework where+	a <> b = Framework+		{ defines = defines a <> defines b+		, setups = setups a <> setups b+		, loops = loops a  <> loops b+		}++instance Monoid Framework where+	mempty = Framework mempty mempty mempty++class ToFramework t where+	toFramework :: t -> Framework++type Behavior t = Stream t -> Spec++-- | Somewhere that a Stream can be directed to, in order to control the+-- Arduino.+data Output t = Output+	{ setupOutput :: [CFragment]+	, outputCond :: Stream Bool+	, outputBehavior :: Stream Bool -> Behavior t+	}++instance ToFramework (Output t) where+	toFramework o = Framework+		{ defines = mempty+		, setups = setupOutput o+		, loops = mempty+		}++-- | A source of a `Stream` of values input from the Arduino.+type Input t = Sketch' (Stream t)++data Input' t = Input'+	{ defineVar :: [CFragment]+	, setupInput :: [CFragment]+	, readInput :: [CFragment]+	, inputStream :: Stream t+	}++instance ToFramework (Input' t) where+	toFramework i = Framework+		{ defines = defineVar i+		, setups = setupInput i+		, loops = readInput i+		}++-- | A GPIO pin+newtype Pin = Pin Int++mkInput :: Input' t -> Input t+mkInput i = do+	tell [(return (), toFramework i)]+	return (inputStream i)++-- | Connect a `Stream` to an `Output`.+(=:) :: Output t -> Stream t -> Sketch+o =: s = tell [(go, toFramework o)]+  where+	go = (outputBehavior o) (outputCond o) s++-- Same fixity as =<<+infixr 1 =:++-- | By default, an `Output` is written to 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.+--+-- > led =: true+--+-- To avoid unnecessary work being done, this combinator can make an+-- `Output` only be written to when the current value of the provided+-- `Stream` is True.+--+-- 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 @: firstIteration =: true+(@:) :: Output t -> Stream Bool -> Output t+(@:) o c = o { outputCond = c }++-- | True on the first iteration of the Sketch, and False thereafter.+firstIteration :: Stream Bool+firstIteration = [True]++false++-- FIXME should be a newtype, but how to make a stream of a newtype?+type MicroSeconds = Int16++-- | The on-board LED.+led :: Output Bool+led = Output+	{ setupOutput = ["pinMode(13, OUTPUT)"]+	, outputBehavior = +		\c v -> trigger "digitalWrite" c [arg (constI16 13), arg v]+	, outputCond = true+	}++-- | Use this to add a delay between each iteration of the Sketch.+delay :: Output MicroSeconds+delay = Output+	{ setupOutput = []+	, outputBehavior = \c n -> trigger "delay" c [arg n]+	, outputCond = true+	}++-- | Reading from a GPIO pin.+boolInput :: Pin -> Input Bool+boolInput n = boolInput' n []++-- | The optional list is used as simulated input+-- when interpreting the program.+boolInput' :: Pin -> [Bool] -> Input Bool+boolInput' (Pin n) interpretvalues = mkInput $ Input'+	{ defineVar = ["bool " <> varname]+	, setupInput = ["pinMode(" <> show n <> ", INPUT)"]+	, readInput = [varname <> " = digitalRead(" <> show n <> ")"]+	, inputStream = extern varname interpretvalues'+	}+  where+	varname = "arduino_boolinput" <> show n+	interpretvalues'+		| null interpretvalues = Nothing+		| otherwise = Just interpretvalues++-- | Typically your Arduino program's main will use this. For example:+--+-- > main = arduino $ do+-- >	led =: clk (period 2) (phase 1)+-- > 	delay =: const16 100+--+-- The `Sketch` is compiled into C code using copilot, and written+-- to a .ino file. That can be built and uploaded to your Arduino+-- using the Arduino IDE, or any other toolchain for Arduino sketches.+arduino :: Sketch -> IO ()+arduino s = do+	let (is, fs) = unzip (execWriter s)+	let spec = sequence_ is+	-- TODO optparse-applicative+	ps <- getArgs+	case ps of+		[] -> writeIno spec (mconcat fs)+		["-i", n] -> case readMaybe n of+			Just n' -> interpret n' spec+			Nothing -> error "expected a number after -i"+		_ -> error "bad parameters"++-- | Extracts a copilot `Spec` from a `Sketch`.+--+-- This can be useful to intergrate with other libraries +-- such as copilot-theorem.+sketchSpec :: Sketch -> Spec+sketchSpec s = sequence_ is+  where+	(is, _fs) = unzip (execWriter s)++writeIno :: Spec -> Framework -> IO ()+writeIno 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 when used in the .ino file, so that include has to be+	-- filtered out.+	toptmpdir <- getTemporaryDirectory+	mytmpdir <- mkdtemp (toptmpdir </> "copilot")+	reify spec >>= compile (mytmpdir </> "copilot")+	c <- lines <$> readFile (mytmpdir </> "copilot.c")+	let c' = filter (Prelude.not . isInfixOf "#include \"") c+	-- Use a name for the ino file that will let the Arduino IDE find it.+	d <- getCurrentDirectory+	let dirbase = takeFileName d+	writeFile (addExtension dirbase "ino") $ +		sketchFramework framework c'+	removeDirectoryRecursive mytmpdir+	++sketchFramework :: Framework -> [String] -> String+sketchFramework f ccode = unlines $ concat+	[+		[ "/* automatically generated, do not edit */"+		, blank+		, "#include <stdbool.h>"+		, "#include <stdint.h>"+		, blank+		]+	, map statement (defines f)+	, [blank]+	, ccode+	, [blank]+	,+		[ "void setup()"+		]+	, codeblock $ map statement (setups f)+	, [blank]+	,+		[ "void loop()"+		]+	, codeblock $ map statement $ (loops f) <>+		[ "step()"+		]+	]+  where+	blank = ""+	indent l = "  " <> l+	statement d = d <> ";"+	codeblock l = ["{"] <> map indent l <> ["}"]

@@ -0,0 +1,14 @@+packages:+- '.'+resolver: lts-13.29+extra-deps:+- copilot-3.1+- copilot-c99-3.1+- copilot-core-3.1+- copilot-language-3.1+- copilot-libraries-3.1+- copilot-theorem-3.1+- language-c99-0.1.2+- language-c99-simple-0.1.2+- language-c99-util-0.1.1+explicit-setup-deps: