summaryrefslogtreecommitdiff
path: root/assignment-13/ufpl.tex
blob: 462180a1d4d365357c60b224ce197e65f45844b1 (plain) (blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
\documentclass[a4paper,twocolumn,english]{article}

\title{$\mu$FPL\\[.4em]
	\large{A small functional programming language for the Arduino}}
\author{Camil Staps}

\usepackage[margin=25mm,bottom=35mm]{geometry}
\usepackage{graphicx}
\usepackage{subcaption}
\usepackage[hidelinks]{hyperref}
\usepackage{cleveref}
\usepackage{csquotes}
\usepackage{minted}
\setminted{fontsize=\small,tabsize=4,style=bw}

\def\uFPL{$\mu$FPL}
\def\module#1{\texttt{\small#1}}
\def\clean#1{\texttt{\small#1}}

\begin{document}

\maketitle

\section{Introduction}
\uFPL\ is a small functional programming language that compiles to Arduino C++.
It is implemented as a deeply embedded DSL in the programming language Clean.%
	\footnote{I chose against a shallowly embedded DSL,
		because the iTasks simulator is easier to make when there are concrete types to manipulate.}
Programs in \uFPL\ are lists of rewrite rules on shared data sources.
Rewrite rules can be set to trigger only when a share changes.
There are specialised instructions to deal with an LCD shield.
Buttons and timing are provided by way of predefined read-only shares.
Type safety is guaranteed using poor man's GADTs by John van Groningen.
An iTasks simulator can be used to interactively design programs.%
	\footnote{\uFPL\ is tested on the nightly of January 7, 2018.}

An example of a program in \uFPL\ is given in \cref{lst:score}.
It keeps scores of two players and displays it on the LCD.
There are four named rules (\texttt{a}, \texttt{b}, \texttt{r} and \texttt{print})
	that are executed in parallel using the \texttt{|||} operator.
The first two rules increment the scores when a button is pressed.
The third rule resets the scores when button 2 is pressed.
The fourth rule is triggered whenever either score changes,
	and prints the score on the screen.

\begin{listing*}[p]
	\inputminted[firstline=13,lastline=32]{clean}{uFPL/Examples.icl}
	\caption{An example \uFPL\ program to keep scores of two players.\label{lst:score}}
\end{listing*}

\section{Implementation}

\subsection{DSL}
The DSL types are provided in \module{uFPL}.
Expressions in our DSL are provided for literals, common operators for integers and booleans
	and an \clean{EIf} constructor similar to Clean's \clean{if} (\cref{lst:exprs}).
Shorthands are provided for some constructors, especially those that require a bimap for type safety
	(such as \clean{==.} for \clean{Expr}).
Expressions have a type \clean{t} and a phantom type \clean{rw} which is either \clean{RW} or \clean{RO},
	indicating whether an expression can be written or is read-only.
The only expression that can be written is an \clean{EShared},
	which is a shared data source (although there are read-only shares, such as buttons).

\begin{listing*}[p]
	\inputminted[firstline=53,lastline=74]{clean}{uFPL.dcl}
	\caption{Expressions in our DSL.\label{lst:exprs}}
\end{listing*}

A program consists of a collection of \clean{NamedRule}s,
	a simple wrapper around the \clean{Rule} type (\cref{lst:rules}).
The last three constructors are only for the LCD shield.
The \clean{<\#} operator assigns a value to a shared data source.
With \clean{When} and \clean{>>>}, rules can be made conditional.
The first checks whether some condition holds,
	while the second uses triggers that only fire when a share has changed value.
Rules can be chained with \clean{:.} and named rules with \clean{|||}.

\begin{listing*}[p]
	\inputminted[firstline=76,lastline=93]{clean}{uFPL.dcl}
	\caption{Rules in our DSL.\label{lst:rules}}
\end{listing*}

The simplest trigger is \clean{Change}, which fires when a share has changed value.
The \clean{?=} trigger furthermore checks the new value.
Triggers can be composed with \clean{?\&} and \clean{?|}.

Shares (\cref{lst:shares}) have a name, type, initial value and a function to represent values in C.
Like expressions, they have type variables for their type and whether they can be written or not.
The \clean{srw} field is discussed in \cref{sec:impl:sim}.
Normally, it should not be needed to define shares yourself.
Wrapper functions as \clean{rwInt :: String Int -> Expr Int RW} from \module{uFPL.Bootstrap} can be used for that,
	similar to \clean{sharedStore} in iTasks.

\begin{listing*}[p]
	\inputminted[firstline=14,lastline=20]{clean}{uFPL.dcl}
	\caption{Shares in our DSL.\label{lst:shares}}
\end{listing*}

\subsection{Code generation}
A separate module, \module{uFPL.C}, provides types to represent simple C programs.
In \module{uFPL}, the \clean{gen} class takes care of generation to this C representation.

Every named rule becomes a separate C function.
Every rule becomes a statement in a function.
The \clean{loop} function loops through all tasks and a special \clean{system} task,
	which updates internal shares for buttons and timing.

Shares are represented by structs and only accessed through specialised functions (\cref{lst:share-repr})
	holding their value (\clean{val}) and the number of tasks that has triggers for the share (\clean{subscriptions}).
There exists different structs for different types.
When the value is set, the member \clean{dirty} is set to the number of \clean{subscriptions}.
When a trigger on the share is checked, the \clean{dirty} number is decreased.
The trigger only fires when \clean{dirty} is positive.
Tasks are executed in a queue,
	which guarantees that a task is always notified exactly once of a share change.

\begin{listing*}[p]
	\begin{minted}[gobble=2]{c}
		struct bshare {
			bool val;
			unsigned char dirty;
			unsigned char subscriptions;
		};
		void bsubscribe(struct bshare *share) {
			share->subscriptions++;
		}
		void bset(struct bshare *share, bool val) {
			share->val = val;
			share->dirty = share->subscriptions;
		}
		bool bdirty(struct bshare *share) {
			if (share->dirty) {
				share->dirty--;
				return true;
			}
			return false;
		}
	\end{minted}
	\caption{Representation of shares (here for booleans).\label{lst:share-repr}}
\end{listing*}

The predefined shares for buttons and timing are always included in the generated code.
It would be possible to only include them when they are used,
	but that would make generation of the \clean{system} function more complicated.
We rely on the C compiler to optimise unused shares.

\subsection{Simulation}
\label{sec:impl:sim}
The \module{uFPL} module provides a view for running rules on some state, independently of iTasks.
An iTasks simulator is provided to interactively write programs in \uFPL.
The \module{uFPL.Sim} module provides shadow types similar to those in \module{uFPL},
	but with less type safety guarantees.
This is needed because we cannot build generic representations of types with existential quantifiers.

We use a class \clean{lift :: t -> Task Dynamic} to lift shadow types to our DSL.
An example is given for addition in \cref{lst:lift}.
We have to explicitly test on all types (here \clean{Int} and \clean{Char})
	because type contexts in dynamic pattern matches are not supported yet.
In the iTask representation of the DSL, shares are identified with their name.
In a separate SDS these shares are defined.
The lift functionality looks up the right share in that SDS.
Whenever lifting fails (which is possible because the DSL is more restrictive),
	an exception is thrown.

\begin{listing*}[p]
	\inputminted[gobble=1,firstline=101,lastline=104]{clean}{uFPL/Sim.icl}
	\caption{Lifting shadow types to the DSL.\label{lst:lift}}
\end{listing*}

Unlifting from the DSL to the iTasks domain is simpler and does not require dynamics or tasks (\clean{unlift :: t -> u}).
In the case of shares, we would want to define multiple instances of unlift, with the types
	\clean{(UShared Int RW) -> IShared}, \clean{(UShared Int RO) -> IShared}, etc.,
	because the iTasks representation holds information about type and writability.
This yields a compiler error about multiply defined instances (which I think is a compiler bug).
To solve this, we use a dynamic representation of the value to check the type
	and a small piece of ABC code to check whether the share is read-only or not (\cref{lst:unlift-shares}).
The latter was only possible by adding an extra field to the DSL shares that holds a value of the \clean{rw} type.

\begin{listing*}[p]
	\inputminted[firstline=167,lastline=196]{clean}{uFPL/Sim.icl}
	\caption{Unlifting shares requires dynamics and ABC-code, due to a presumed compiler bug.\label{lst:unlift-shares}}
\end{listing*}

The iTasks simulator allows the user to update a set of named rules and shares on the right.
Because rules are supposed to be independent, it is not possible to change the order of the list.
On the left, the state is shown: either \enquote{OK} or an exception when lifting to the DSL fails.
This provides the user with the same amount of type safety as provided by the compiler.
Example errors are shown in \cref{fig:itasks-errors}.

\begin{figure*}[p]
	\centering
	\begin{subfigure}{.8\textwidth}
		\centering
		\includegraphics[width=\textwidth]{error-no-such-share}
		\caption{Using a non-existent share.}
	\end{subfigure}

	\begin{subfigure}{.8\textwidth}
		\centering
		\includegraphics[width=\textwidth]{error-share-type}
		\caption{Assigning a value with other type to a share.}
	\end{subfigure}

	\begin{subfigure}{.8\textwidth}
		\centering
		\includegraphics[width=\textwidth]{error-ro-share}
		\caption{Assigning a value to a read-only share.}
	\end{subfigure}
	\caption{Errors thrown in the iTasks simulator.\label{fig:itasks-errors}}
\end{figure*}

A number of actions is available to simulate the program.
The most basic action is \enquote{Step},
	which executes every named rule once.
It is not possible to update arbitrary shares, but for buttons and timing specialised actions are available (\cref{fig:itasks-score:simulation}).
Buttons can be toggled, which changes their value without executing any code.
Pressing a button means setting it to \clean{true}, doing a step and resetting it to \clean{false}.%
	\footnote{The system does not take into account that only one button can be pressed at the same time due to the resistor ladder on the LCD shield.}
When a program uses timing,
	actions exist for incrementing the value of \clean{millis} with \clean{100} or \clean{1000} (without stepping).
There also exists a fully automatic simulator
	which increments the value of \clean{millis} by \clean{1000} and performs a step every second.
However, due to (presumed) limitations of the iTasks framework,
	this is CPU-intensive and the state share sometimes misses an iteration.

In the left bottom view, the states of the shares and the display ($16\times2$ is assumed) are shown.

Finally, it is possible to generate code from within iTasks and save it to disk (\cref{fig:itasks-score:code-generation}).

\begin{figure*}[p]
	\begin{subfigure}{\textwidth}
		\includegraphics[width=\textwidth]{scores}
		\caption{Simulation.\label{fig:itasks-score:simulation}}
	\end{subfigure}
	\begin{subfigure}{\textwidth}
		\includegraphics[width=\textwidth]{scores-generate}
		\caption{Code generation.\label{fig:itasks-score:code-generation}}
	\end{subfigure}
	\caption{The scoring example program (\cref{lst:score}) in the iTasks simulator.\label{fig:itasks-scores}}
\end{figure*}

\section{Discussion}
\uFPL\ is strongly typed.
Variables are type-checked,
	but because \uFPL\ is a functional language the only variables are shares.
For type checking in the iTasks simulator we use tasks that lift shadow types to the DSL or throw exceptions.
The DSL has a straightforward syntax with shorthands whenever bimaps or other technicalities could be avoided.
It provides rudimentary task-oriented programming support using shared data sources
	and a theoretically arbitrary number of tasks in parallel,
	although sequencing, parameterised tasks and task control have not been implemented.

\uFPL\ does not allow for control over pins,
	but it would be straightforward to add this using more predefined shares.

I chose for the subscription model of shares because it allows to suspend and start tasks.
However, this has not been implemented yet.
Therefore, the number of subscriptions to a share is currently only a constant value.

Using a \clean{dirty} counter for shares requires that every task is executed equally often.
It would be possible to handle triggers with a bitmask where each bit indicates whether a task has seen the change.
This would allow for tasks starting other tasks.

Currently, tasks cannot return a value; all generated functions have type \clean{void} and arity 0.
It would be very easy to implement this as a syntactic sugar where a new share would be introduced to handle the inter-task communication.
However, I did not do that because adding these changes to the iTasks simulator would be tedious,
	and the proper way would be to generate functions with parameters and return types.

\end{document}