Typically your Arduino program's main will be implemented using this. For example:

 {-# LANGUAGE RebindableSyntax #-}
 
 import Copilot.Arduino
 
 main = arduino $ do
	led =: flashing
 	delay =: MilliSeconds (constant 100)

Running this program compiles the Sketch into C code using copilot, and writes it to a .ino file. That can be built and uploaded to your Arduino using the Arduino IDE, or any other toolchain for Arduino sketches.

This also supports interpreting a Sketch, without loading it onto an Arduino. 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)     

An Arduino 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.

A pin on the Arduino board.

For definitions of pins like pin12, load a module such as Copilot.Arduino.Uno, 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.

Indicates that you're programming an arduino, and not some other kind of hardware. The similar library zephyr-copilot allows programming other embedded boards in a very similar style to this one.

A value that changes over time.

This is implemented as a Stream in the Copilot DSL. Copilot provides many operations on streams, for example && to combine two streams of Bools.

For documentation on using the Copilot DSL, see https://copilot-language.github.io/

A Behavior with an additional phantom type p.

The Compilot DSL only lets a Stream contain basic C types, a limitation that Behavior also has. When more type safely is needed, this can be used.

A discrete event, that occurs at particular points in time.

Generate an Event, from some type of behavior, that only occurs when the Behavior Bool is True.

Use this to read a value from a component of the board.

For example, to read a digital value from pin12 and turn on the led when the pin is high:

buttonpressed <- input pin12
led =: buttonpressed

Some pins support multiple types of reads, for example a pin may support a digital read (Bool), and an analog to digital converter read (ADC). In such cases you may need to specify the type of data to read:

v <- input a0 :: Sketch (Behavior ADC)

The list is input to use when simulating the Sketch.

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.

Bear in mind that enabling the pullup resistor inverts the value that will be read from the pin.

pullup pin12

Number of MillisSeconds since the Arduino booted.

n <- input millis

The value wraps back to zero after approximately 50 days.

Number of MicroSeconds since the Arduino booted.

n <- input micros

The value wraps back to zero after approximately 70 minutes.

Things that can have a Behavior or Event output to them.

The on-board LED.

Connect a Behavior or Event to an Output

led =: blinking

When a Behavior is used, its current value is written on each iteration of the Sketch.

For example, this constantly turns on the LED, even though it will already be on after the first iteration, because true is a Behavior (that is always True).

led =: true

To avoid unncessary work being done, you can use an Event instead. Then the write only happens at the points in time when the Event occurs. To turn a Behavior into an Event, use @:

So to make the LED only be turned on in the first iteration, and allow it to remain on thereafter without doing extra work:

led =: true @: firstIteration

Use this to do PWM output to a pin.

pin3 =: pwm (constant 128)

Each Word8 of the Behavior describes a PWM square wave. 0 is always off and 255 is always on.

Use this to add a delay between each iteration of the Sketch. A Sketch with no delay will run as fast as the hardware can run it.

delay := MilliSeconds (constant 100)

Value read from an Arduino's ADC. Ranges from 0-1023.

A stream of milliseconds.

A stream of microseconds.

Use this to make a LED blink on and off.

On each iteration of the Sketch, this changes to the opposite of its previous value.

This is implemented using Copilot's clk, so to get other blinking behaviors, just pick different numbers, or use Copilot Stream combinators.

blinking = clk (period 2) (phase 1)

True on the first iteration of the Sketch, and False thereafter.

Use this to make an event occur 1 time out of n.

This is implemented using Copilot's clk:

frequency = clk (period n) (phase 1)

Extracts a copilot Spec from a Sketch.

This can be useful to intergrate with other libraries such as copilot-theorem.

Apply a Copilot DSL function to a TypedBehavior.

Apply a Copilot DSL function to two TypedBehaviors.

Limit the effects of a Sketch to times when a Behavior Bool is True.

When applied to =:, this does the same thing as @: but without the FRP style conversion the input Behavior into an Event. So @: is generally better to use than this.

But, this can also be applied to input, to limit how often input gets read. Useful to avoid performing slow input operations on every iteration of a Sketch.

v <- whenB (frequency 10) $ input pin12

(It's best to think of the value returned by that as an Event, but it's currently represented as a Behavior, since the Copilot DSL cannot operate on Events.)

Schedule when to perform different Sketches.

This allows "if then else" expressions to be written that choose between two Streams, or Behaviors, or TypedBehaviors, or Sketches, when the RebindableSyntax language extension is enabled.

{-# LANGUAGE RebindableSyntax #-}
buttonpressed <- input pin3
if buttonpressed then ... else ...

A stream in Copilot is an infinite succession of values of the same type.

Streams can be built using simple primities (e.g., Const), by applying step-wise (e.g., Op1) or temporal transformations (e.g., Append, Drop) to streams, or by combining existing streams to form new streams (e.g., Op2, Op3).

The value of seq a b is bottom if a is bottom, and otherwise equal to b. In other words, it evaluates the first argument a to weak head normal form (WHNF). seq is usually introduced to improve performance by avoiding unneeded laziness.

A note on evaluation order: the expression seq a b does not guarantee that a will be evaluated before b. The only guarantee given by seq is that the both a and b will be evaluated before seq returns a value. In particular, this means that b may be evaluated before a. If you need to guarantee a specific order of evaluation, you must use the function pseq from the "parallel" package.

\(\mathcal{O}(n)\). filter, applied to a predicate and a list, returns the list of those elements that satisfy the predicate; i.e.,

filter p xs = [ x | x <- xs, p x]

>>> filter odd [1, 2, 3]
[1,3]

\(\mathcal{O}(\min(m,n))\). zip takes two lists and returns a list of corresponding pairs.

zip [1, 2] ['a', 'b'] = [(1, 'a'), (2, 'b')]

If one input list is short, excess elements of the longer list are discarded:

zip [1] ['a', 'b'] = [(1, 'a')]
zip [1, 2] ['a'] = [(1, 'a')]

zip is right-lazy:

zip [] _|_ = []
zip _|_ [] = _|_

zip is capable of list fusion, but it is restricted to its first list argument and its resulting list.

The print function outputs a value of any printable type to the standard output device. Printable types are those that are instances of class Show; print converts values to strings for output using the show operation and adds a newline.

For example, a program to print the first 20 integers and their powers of 2 could be written as:

main = print ([(n, 2^n) | n <- [0..19]])

Extract the first component of a pair.

Extract the second component of a pair.

otherwise is defined as the value True. It helps to make guards more readable. eg.

 f x | x < 0     = ...
     | otherwise = ...

\(\mathcal{O}(n)\). map f xs is the list obtained by applying f to each element of xs, i.e.,

map f [x1, x2, ..., xn] == [f x1, f x2, ..., f xn]
map f [x1, x2, ...] == [f x1, f x2, ...]

>>> map (+1) [1, 2, 3]

Application operator. This operator is redundant, since ordinary application (f x) means the same as (f $ x). However, $ has low, right-associative binding precedence, so it sometimes allows parentheses to be omitted; for example:

f $ g $ h x  =  f (g (h x))

It is also useful in higher-order situations, such as map ($ 0) xs, or zipWith ($) fs xs.

Note that ($) is levity-polymorphic in its result type, so that foo $ True where foo :: Bool -> Int# is well-typed.

general coercion from integral types

general coercion to fractional types

The Bounded class is used to name the upper and lower limits of a type. Ord is not a superclass of Bounded since types that are not totally ordered may also have upper and lower bounds.

The Bounded class may be derived for any enumeration type; minBound is the first constructor listed in the data declaration and maxBound is the last. Bounded may also be derived for single-constructor datatypes whose constituent types are in Bounded.

Class Enum defines operations on sequentially ordered types.

The enumFrom... methods are used in Haskell's translation of arithmetic sequences.

Instances of Enum may be derived for any enumeration type (types whose constructors have no fields). The nullary constructors are assumed to be numbered left-to-right by fromEnum from 0 through n-1. See Chapter 10 of the Haskell Report for more details.

For any type that is an instance of class Bounded as well as Enum, the following should hold:

• The calls succ maxBound and pred minBound should result in a runtime error.
• fromEnum and toEnum should give a runtime error if the result value is not representable in the result type. For example, toEnum 7 :: Bool is an error.
• enumFrom and enumFromThen should be defined with an implicit bound, thus:

   enumFrom     x   = enumFromTo     x maxBound
   enumFromThen x y = enumFromThenTo x y bound
     where
       bound | fromEnum y >= fromEnum x = maxBound
             | otherwise                = minBound