diff --git a/CHANGELOG b/CHANGELOG new file mode 100644 --- /dev/null +++ b/CHANGELOG @@ -0,0 +1,5 @@ +arduino-copilot (0.0.1) unstable; urgency=medium + + * First release. + + -- Joey Hess Sat, 25 Jan 2020 10:33:09 -0400 diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,22 @@ +Copyright 2020 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/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/TODO b/TODO new file mode 100644 --- /dev/null +++ b/TODO diff --git a/arduino-copilot.cabal b/arduino-copilot.cabal new file mode 100644 --- /dev/null +++ b/arduino-copilot.cabal @@ -0,0 +1,63 @@ +Name: arduino-copilot +Version: 0.0.1 +Cabal-Version: >= 1.8 +License: BSD3 +Maintainer: Joey Hess +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 + . +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 diff --git a/demo/Makefile b/demo/Makefile new file mode 100644 --- /dev/null +++ b/demo/Makefile @@ -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 diff --git a/demo/README b/demo/README new file mode 100644 --- /dev/null +++ b/demo/README @@ -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 . 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. diff --git a/demo/demo.hs b/demo/demo.hs new file mode 100644 --- /dev/null +++ b/demo/demo.hs @@ -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 diff --git a/demo/pre-build-hook.sh b/demo/pre-build-hook.sh new file mode 100644 --- /dev/null +++ b/demo/pre-build-hook.sh @@ -0,0 +1,2 @@ +#!/bin/sh +exec stack run demo -Wall -fno-warn-tabs diff --git a/src/Arduino.hs b/src/Arduino.hs new file mode 100644 --- /dev/null +++ b/src/Arduino.hs @@ -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 " + , "#include " + , 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 <> ["}"] diff --git a/stack.yaml b/stack.yaml new file mode 100644 --- /dev/null +++ b/stack.yaml @@ -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: