an example we have the simple arithmetic \gls{EDSL} shown in
Listing~\ref{lst:exdeep}.
-\begin{lstlisting}[language=Clean,label={lst:exdeep},%
+\begin{lstlisting}[label={lst:exdeep},%
caption={A minimal deep \gls{EDSL}}]
:: DSL
= LitI Int
the lack of extendability remains a problem. If a language construct is added,
no compile time guarantee is given that all views support it.
-\begin{lstlisting}[language=Clean,label={lst:exdeepgadt},%
+\begin{lstlisting}[label={lst:exdeepgadt},%
caption={A minimal deep \gls{EDSL} using \glspl{GADT}}]
:: DSL a
= LitI Int -> DSL Int
something like the code shown in Listing~\ref{lst:exshallow}. Note that much of
the internals of the language can be hidden using monads.
-\begin{lstlisting}[language=Clean,label={lst:exshallow},%
+\begin{lstlisting}[label={lst:exshallow},%
caption={A minimal shallow \gls{EDSL}}]
:: Env = ... // Some environment
:: DSL a = DSL (Env -> a)
extension is added in a new class, this problem does not arise and views can
choose to implement only parts of the collection of classes.
-\begin{lstlisting}[language=Clean,label={lst:exclassshallow},%
+\begin{lstlisting}[label={lst:exclassshallow},%
caption={A minimal class based shallow \gls{EDSL}}]
:: Env = ... // Some environment
:: Evaluator a = Evaluator (Env -> a)
\glspl{SDS}.
\begin{lstlisting}[%
- language=Clean,label={lst:exprhier},caption={Expression role hierarchy}]
+ label={lst:exprhier},caption={Expression role hierarchy}]
:: Upd = Upd
:: Expr = Expr
:: Stmt = Stmt
and omitted in subsequent funcitons. Both the boolean expression and arithmetic
expression classes are shown in Listing~\ref{lst:arithbool}.
-\begin{lstlisting}[language=Clean,label={lst:arithbool},
+\begin{lstlisting}[label={lst:arithbool},
caption={Basic classes for expressions}]
class arith v where
lit :: t -> v t Expr
the two expressions together in sequence.
\begin{lstlisting}[%
- language=Clean,label={lst:control},caption={Control flow operators}]
+ label={lst:control},caption={Control flow operators}]
class If v q r ~s where
If :: (v Bool p) (v t q) (v t r) -> v t s | ...
the assignment is the same for every assignable entity.
\begin{lstlisting}[%
- language=Clean,label={lst:sdsio},caption={Input/Output classes}]
+ label={lst:sdsio},caption={Input/Output classes}]
:: DigitalPin = D0 | D1 | D2 | D3 | D4 | D5 |D6 | D7 | D8 | D9 | D10 | D11 | D12 | D13
:: AnalogPin = A0 | A1 | A2 | A3 | A4 | A5
:: UserLED = LED1 | LED2 | LED3
\gls{mTask} and make it recognizable by the type system.
\begin{lstlisting}[%
- language=Clean,label={lst:sdsclass},caption={\glspl{SDS} in \gls{mTask}}]
+ label={lst:sdsclass},caption={\glspl{SDS} in \gls{mTask}}]
:: In a b = In infix 0 a b
:: Main a = {main :: a}
shows a simple specification containing one task that increments a value
indefinitely every one seconds.
-\begin{lstlisting}[language=Clean,label={lst:taskclass},%
+\begin{lstlisting}[label={lst:taskclass},%
caption={The classes for defining tasks}]
class mtask v a where
task :: (((v delay r) a->v MTask Expr)->In (a->v u p) (Main (v t q))) -> Main (v t q) | ...
expression but now using the assignment style \gls{GPIO} technique.
\begin{lstlisting}[%
- language=Clean,label={lst:exmtask},caption={Some example \glspl{mTask}}]
+ label={lst:exmtask},caption={Some example \glspl{mTask}}]
blink = task \blink=(\x.
IF (x ==. lit True) (ledOn led) (ledOff led) :.
blink (lit 1000) (Not x)
\caption{The states of a \CI{TaskValue}}\label{fig:taskvalue}
\end{figure}
-\begin{lstlisting}[language=Clean,label={lst:taskex},%
+\begin{lstlisting}[label={lst:taskex},%
caption={An example \gls{Task} for entering a name}]
:: Name = { firstname :: String
, lastname :: String
dictates.
\end{itemize}
-\begin{lstlisting}[language=Clean,%
+\begin{lstlisting}[%
caption={\Gls{Task}-combinators},label={lst:combinators}]
//Step combinator
(>>*) infixl 1 :: (Task a) [TaskCont a (Task b)] -> Task b | iTask a & iTask b
executed.
\begin{lstlisting}[%
- language=Clean,label={lst:shares},caption={\Gls{SDS} functions}]
+ label={lst:shares},caption={\Gls{SDS} functions}]
get :: (ReadWriteShared r w) -> Task r | iTask r
set :: w (ReadWriteShared r w) -> Task w | iTask w
upd :: (r -> w) (ReadWriteShared r w) -> Task w | iTask r & iTask w
and send it to the server so that the server knows what the client is capable
of. The exact specification is listed in Listing~\ref{lst:devicespec}
-\begin{lstlisting}[language=Clean,label={lst:devicespec},
+\begin{lstlisting}[label={lst:devicespec},
caption={Device specification for \glspl{mTask}}]
:: MTaskDeviceSpec =
{haveLed :: Bool
All of this is listed in Listing~\ref{lst:mtaskdevice}. The definitions of the
message format are explained in the following section.
-\begin{lstlisting}[language=Clean,caption={Device type},label={lst:mtaskdevice}]
+\begin{lstlisting}[caption={Device type},label={lst:mtaskdevice}]
deviceStore :: Shared [MTaskDevice]
:: Channels :== ([MTaskMSGRecv], [MTaskMSGSend], Bool)
\section{Communication}
All \gls{mTask} messages are encoded following the specification given in
Appendix~\ref{app:communication-protocol}. Available messages are:
-\begin{lstlisting}[language=Clean,caption={Available messages}]
+\begin{lstlisting}[caption={Available messages}]
:: MTaskMSGRecv
= MTTaskAck Int Int | MTTaskDelAck Int
| MTSDSAck Int | MTSDSDelAck Int
and still update the latest instance. Listing~\ref{lst:connectDevice} shows the
connection function.
-\begin{lstlisting}[language=Clean,label={lst:connectDevice},%
+\begin{lstlisting}[label={lst:connectDevice},%
caption={Connect a device}]
withDevices :: MTaskDevice (MTaskDevice -> MTaskDevice) -> Task [MTaskDevice]
does not have to implement all the available classes. Moreover, classes can be
added at will without interfering with the existing views.
+\section{Semantics}
+\todo{semantics}
+
\section{Bytecode compilation}
The \glspl{mTask} are sent to the device in bytecode and are saved in the
memory of the device. To compile the \gls{EDSL} code to bytecode, a view is
detect which type the value is. The devices know of these prefixes and act
accordingly.
-\begin{lstlisting}[language=Clean,label={lst:bcview},caption={Bytecode view}]
+\begin{lstlisting}[label={lst:bcview},caption={Bytecode view}]
:: ByteCode a p = BC (RWS () [BC] BCState ())
:: BCValue = E.e: BCValue e & mTaskType, TC e
:: BCShare = {
\end{lstlisting}
\section{Implementation}
+\subsection{Instruction Set}
+The instruction set is given in Listing~\ref{bc:instr}. The instruction set is
+kept large, but under $255$, to get the highest expressivity for the lowest
+program size.
+
+The interpreter is a
+stack machine. Therefore the it needs instructions like \emph{Push} and
+\emph{Pop}. The virtual instruction \CI{BCLab} is added to allow for an easy
+implementation. However, this is not a real instruction and the labels are
+resolved to actual addresses in the final step of compilation to save
+instructions.
+
+\begin{lstlisting}[label={bc:instr},%
+ caption={Bytecode instruction set}]
+:: BC = BCNop
+ | BCLab Int | BCPush BCValue | BCPop
+ //SDS functions
+ | BCSdsStore BCShare | BCSdsFetch BCShare | BCSdsPublish BCShare
+ //Unary ops
+ | BCNot
+ //Binary Int ops
+ | BCAdd | BCSub | BCMul
+ | BCDiv
+ //Binary Bool ops
+ | BCAnd | BCOr
+ //Binary ops
+ | BCEq | BCNeq | BCLes | BCGre
+ | BCLeq | BCGeq
+ //Conditionals and jumping
+ | BCJmp Int | BCJmpT Int | BCJmpF Int
+ //UserLED
+ | BCLedOn | BCLedOff
+ //Pins
+ | BCAnalogRead Pin | BCAnalogWrite Pin | BCDigitalRead Pin | BCDigitalWrite Pin
+ //Return
+ | BCReturn
+\end{lstlisting}
+
+All instructions are can be converted semi-automatically using the generic
+function \CI{consIndex\{*\}} that gives the index of the constructor. This
+constructor index is the actual byte value for the instruction. The
+\CI{BCValue} type contains existentially quantified types and therefore must
+have a given implementation for all generic functions.
+
\subsection{Helper functions}
+The \CI{ByteCode} type is just a boxed \gls{RWST} and that gives us access to
+the whole range of \gls{RWST} functions. However, to apply a function the type
+must be unboxed. After application the type must be boxed again. To achieve
+this some helper functions have been created. They are listed in
+Listing~\ref{lst:helpers}. The \CI{op} and \CI{op2} function is crafted to make
+operators that pop one or two values off the stack respectively. The \CI{tell`}
+is a wrapper around the \gls{RWST} function \CI{tell} that appends the argument
+to the \emph{Writer} value.
+
+\begin{lstlisting}[label={lst:helpers},caption={Some helper functions}]
+op2 :: (ByteCode a p1) (ByteCode a p2) BC -> ByteCode b Expr
+op2 (BC x) (BC y) bc = BC (x >>| y >>| tell [bc])
+
+op :: (ByteCode a p) BC -> ByteCode a Expr
+op (BC x) bc = BC (x >>| tell [bc])
+
+tell` :: [BC] -> (ByteCode a p)
+tell` x = BC (tell x)
+
+unBC :: (ByteCode a p) -> RWS () [BC] BCState ()
+unBC (BC x) = x
+\end{lstlisting}
+
+\subsection{Arithmetics \& Peripherals}
+Almost all of the code from the simple classes use exclusively helper
+functions. Listing~\ref{lst:arithview} shows some implementations. The classes
+\CI{boolExpr} and the classes for the peripherals are implemented in the same
+fashion.
+
+\begin{lstlisting}[label={lst:arithview},caption={%
+ Bytecode view implementation for arithmetic and peripheral classes}]
+instance arith ByteCode where
+ lit x = tell` [BCPush (BCValue x)]
+ (+.) x y = op2 x y BCDiv
+ ...
-\subsection{Arithmetics}
+instance userLed ByteCode where
+ ledOn l = op l BCLedOn
+ ledOff l = op l BCLedOff
+\end{lstlisting}
\subsection{Control Flow}
+\begin{lstlisting}[label={lst:controlflow},%
+ caption={Bytecode view for \texttt{arith}}]
+instance noOp ByteCode where
+ noOp = tell` [BCNop]
+\end{lstlisting}
-\subsection{Shared Data Sources}
+\subsection{Shared Data Sources \& Assignment}
+Shared data sources must be acquired from the state and constructing one
+happens via multiple steps. First a fresh identifier is grabbed from the state.
+Then a \CI{BCShare} record is created with that identifier. A \CI{BCSdsFetch}
+instruction is written and the body is generated to finally add the share to
+the actual state. The exact implementation is shown in
+Listing~\ref{lst:shareview}.
-\section{Semantics}
+\begin{lstlisting}[label={lst:shareview},%
+ caption={Bytecode view for \texttt{arith}}]
+instance sds ByteCode where
+ sds f = {main = BC (freshs
+ >>= \sdsi->pure {BCShare | sdsi=sdsi,sdsval=BCValue 0}
+ >>= \sds->pure (f (tell` [BCSdsFetch sds]))
+ >>= \(v In bdy)->modify (addSDS sds v)
+ >>| unBC (unMain bdy))}
+ pub (BC x) = BC (censor (\[BCSdsFetch s]->[BCSdsPublish s]) x)
-\todo{Uitleggen wat het systeem precies doet}
+addSDS sds v s = {s & sdss=[{sds & sdsval=BCValue v}:s.sdss]}
+\end{lstlisting}
+
+All assignable types compile to an \gls{RWST} that writes one instruction. For
+example, using an \gls{SDS} always results in an expression of the form
+\CI{sds \x=4 In ...}. The actual \CI{x} is the \gls{RWST} that always writes
+one \CI{BCSdsFetch} instruction with the correct \gls{SDS} embedded. When the
+call of the \CI{x} is not a read but an assignment, the instruction will be
+rewritten as a \CI{BCSdsStore}. The implementation for this is given in
+Listing~\ref{lst:assignmentview}.
+
+\begin{lstlisting}[label={lst:assignmentview},%
+ caption={Bytecode view implementation for assignment.}]
+instance assign ByteCode where
+ (=.) (BC v) (BC e) = BC (e >>| censor makeStore v)
+
+makeStore [BCSdsFetch i] = [BCSdsStore i]
+makeStore [BCDigitalRead i] = [BCDigitalWrite i]
+makeStore [...] = [...]
+\end{lstlisting}
+\section{Actual Compilation}
+\todo{hulp functies voor compileren}
{\\}{{$\lambda\:$}}1
{A.}{{$\forall\;\,$}}1
{E.}{{$\exists\;\,$}}1
+ {*}{{$^*$}}1
% {>}{{$>$}}1
% {<}{{$<$}}1
% {<=}{{$\leq$}}1
\newcommand{\CI}[1]{\lstinline[language=Clean,basicstyle=\ttfamily\fontseries{l}\normalsize]|#1|}
\lstset{%
- breakatwhitespace=false, % sets if automatic breaks should only happen at whitespace
- breaklines=true, % sets automatic line breaking
- captionpos=b, % sets the caption-position to bottom
- keepspaces=true, % keeps spaces in text, useful for keeping indentation of code (possibly needs columns=flexible)
- basicstyle=\ttfamily\fontseries{l}\footnotesize,% the size of the fonts that are used for the code
- commentstyle=\itshape\fontseries{m}, % comment style
- keywordstyle=\bfseries\fontseries{b}, % keyword style
- stringstyle=\ttfamily, % string literal style
- showspaces=false, % show spaces everywhere adding particular underscores; it overrides 'showstringspaces'
- showstringspaces=false, % underline spaces within strings only
- showtabs=false, % show tabs within strings adding particular underscores
- tabsize=4, % sets default tabsize to 2 spaces
- frame=L
+ breakatwhitespace=false,
+ breaklines=true,
+ captionpos=b,
+ keepspaces=true,
+ basicstyle=\ttfamily\fontseries{l}\footnotesize,
+ commentstyle=\itshape\fontseries{m},
+ keywordstyle=\bfseries\fontseries{b},
+ stringstyle=\ttfamily,
+ showspaces=false,
+ showstringspaces=false,
+ showtabs=false,
+ tabsize=4,
+ frame=L,
+ language=Clean
}
\title{iTasks and the Internet of Things}
repositories / msc-thesis1617.git / commitdiff