The \gls{mTask}-\gls{EDSL} is the language used for the proposed system. The
\gls{mTask}-\gls{EDSL} was created by Koopman et al.\ and supports several
views such as an \gls{iTasks} simulation and a \gls{C}-code generator. The
\gls{EDSL} was designed to generate a ready-to-compile \gls{TOP}-like program
for microcontrollers such as the \gls{Arduino}~\cite{koopman_type-safe_nodate}%
\cite{plasmeijer_shallow_2016}.

The \gls{mTask}-\gls{EDSL} is a shallowly embedded class based \gls{EDSL} and
therefore it is very suitable to have a new backend that partly implements the
classes given. The following sections show the details of the \gls{EDSL} that
is used in this extension. The parts of the \gls{EDSL} that are not used will
not be discussed and the details of those parts can be found in the cited
literature.

A view for the \gls{mTask}-\gls{EDSL} is a type with two free type
variables\footnote{kind \CI{*->*->*}.} that implements some of the classes
given. The types do not have to be present as fields in the higher kinded view
and can, and will most often, be exclusively phantom types. Thus, views are of
the form:\\\CI{:: v t r = ...}.  The first type variable will be the type of the
view. The second type variable will be the type of the \gls{EDSL}-expression
and the third type variable represents the role of the expression. Currently
the role of the expressions form a hierarchy. The three roles and their
hierarchy are shown in Listing~\ref{lst:exprhier}. This implies that everything
is a statement, only a \CI{Upd} and a \CI{Expr} are expressions. The \CI{Upd}
restriction describes updatable expressions such as \gls{GPIO} pins and
\glspl{SDS}.

\begin{lstlisting}[%
	label={lst:exprhier},caption={Expression role hierarchy}]
:: Upd   = Upd
:: Expr  = Expr
:: Stmt  = Stmt

class isExpr a :: a -> Int
instance isExpr Upd
instance isExpr Expr
\end{lstlisting}

\section{Expressions}
Expressions in the \gls{mTask}-\gls{EDSL} are divided into two types, namely
boolean expressions and arithmetic expressions. The class of arithmetic
language constructs also contains the function \CI{lit} that lifts a
host-language value into the \gls{EDSL} domain. All standard arithmetic
functions are included in the \gls{EDSL} but are omitted in the example for
brevity. Moreover, the class restrictions are only shown in the first functions
and are omitted in subsequent functions. Both the boolean expression and
arithmetic expression classes are shown in Listing~\ref{lst:arithbool}.

\begin{lstlisting}[label={lst:arithbool},
	caption={Basic classes for expressions}]
class arith v where
  lit           :: t -> v t Expr
  (+.) infixl 6 :: (v t p) (v t q) -> v t Expr          | +, zero t    & isExpr p & isExpr q
  (-.) infixl 6 :: (v t p) (v t q) -> v t Expr          | -, zero t    & ...
  ...
class boolExpr v where
  Not           :: (v Bool p) -> v Bool Expr            | ...
  (&.) infixr 3 :: (v Bool p) (v Bool q) -> v Bool Expr | ...
  ...
  (==.) infix 4 :: (v a p) (v a q) -> v Bool Expr       | ==, toCode a & ...
\end{lstlisting}

\section{Control flow}
Looping of \glspl{Task} happens because \glspl{Task} are executed after waiting
a specified amount of time or when they are launched by another \gls{Task} or
even themselves. Therefore there is no need for loop control flow functionality
such as \emph{while} or \emph{for} constructions. The main control flow
operators are the sequence operator and the \emph{if} statement. Both are shown
in Listing~\ref{lst:control}. The first class of \emph{If} statements describes
the regular \emph{if} statement. The expressions given can have any role. The
functional dependency on \CI{s} determines the return type of the statement.
The listing includes examples of implementations that illustrate this
dependency.

The sequence operator is straightforward and its only function is to tie
two expressions together. The left expression is executed first, followed by
the right expression.

\begin{lstlisting}[%
	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 | ...

instance If Code Stmt Stmt Stmt
instance If Code e    Stmt Stmt
instance If Code Stmt e    Stmt
instance If Code x    y    Expr

class seq v where
  (:.) infixr 0 :: (v t p) (v u q) -> v u Stmt | ...
\end{lstlisting}

\section{Input/Output and class extensions}
Values can be assigned to all expressions that have an \CI{Upd} role. Examples
of such expressions are \glspl{SDS} and \gls{GPIO} pins. Moreover, class
extensions can be created for specific peripherals such as built-in
\glspl{LED}. The classes facilitating this are shown in
Listing~\ref{lst:sdsio}. In this way the assignment is the same for every
assignable entity.

\begin{lstlisting}[%
	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

class dIO v where dIO :: DigitalPin -> v Bool Upd
class aIO v where aIO :: AnalogPin -> v Int Upd
class analogRead v where
  analogRead :: AnalogPin -> v Int Expr
  analogWrite :: AnalogPin (v Int p) -> v Int Expr
class digitalRead v where
  digitalRead :: DigitalPin -> v Bin Expr
  digitalWrite :: DigitalPin (v Bool p) -> v Int Expr

:: UserLED = LED1 | LED2 | LED3
class userLed v where
  ledOn  :: (v UserLED q) -> (v () Stmt)
  ledOff :: (v UserLED q) -> (v () Stmt)

class assign v where
  (=.) infixr 2 :: (v t Upd) (v t p) -> v t Expr | ...
\end{lstlisting}

One way of storing data in \glspl{mTask} is using \glspl{SDS}. \glspl{SDS}
serve as variables in \gls{mTask} and maintain their value across executions.
\glspl{SDS} can be used by multiple \glspl{Task} and can be used to share data.
The classes associated with \glspl{SDS} are listed in
Listing~\ref{lst:sdsclass}. The \CI{Main} type is introduced to box an
\gls{mTask} and make it recognizable by the type system by separating programs
and decorations such as \glspl{SDS}.

\begin{lstlisting}[%
	label={lst:sdsclass},caption={\glspl{SDS} in \gls{mTask}}]
:: In a b = In infix 0 a b
:: Main a = {main :: a}

class sds v where
  sds :: ((v t Upd)->In t (Main (v c s))) -> (Main (v c s)) | ...
\end{lstlisting}

\section{Semantics}
The \gls{C}-backend of the \gls{mTask}-system has an engine that is generated
alongside the code for the \glspl{Task}. This engine will execute the
\glspl{mTask} according to certain rules and semantics.
\gls{mTask}-\glspl{Task} do not behave like functions but more like
\gls{iTasks}-\glspl{Task}. An \gls{mTask} is queued when either its timer runs
out or when it is launched by another \gls{mTask}. When an \gls{mTask} is
queued it does not block the execution and it will return immediately while the
actual \gls{Task} will be executed anytime in the future.

The \gls{iTasks}-backend simulates the \gls{C}-backend and thus uses the same
semantics. This engine expressed in pseudocode is listed as
Algorithm~\ref{lst:engine}. All the \glspl{Task} are inspected on their waiting
time. When the waiting time has not passed; the delta is subtracted and the
\gls{Task} gets pushed to the end of the queue. When the waiting has surpassed
they are executed. When an \gls{mTask} opts to queue another \gls{mTask} it
can just append it to the queue.

~\\
\begin{algorithm}[H]
	\KwData{\textbf{queue} queue, \textbf{time} $t, t_p$}

	$t\leftarrow\text{now}()$\;
	\Begin{
		\While{true}{
			$t_p\leftarrow t$\;
			$t\leftarrow\text{now}()$\;
			\If{notEmpty$($queue$)$}{
				$task\leftarrow \text{queue.pop}()$\;
				$task$.wait $\leftarrow task$.wait $-(t-t_p)$\;
				\eIf{$task.wait>t_0$}{
					queue.append$(task)$\;
				}{
					run\_task$(task)$\;
				}
			}
		}
	}
	\caption{Engine pseudocode for the \gls{C}- and
		\gls{iTasks}-view}\label{lst:engine}
\end{algorithm}
~\\

To achieve this in the \gls{EDSL} a \gls{Task} class is added that work in a
similar fashion as the \texttt{sds} class. This class is listed in
Listing~\ref{lst:taskclass}. \glspl{Task} can have an argument and always have
to specify a delay or waiting time. The type signature of the \CI{mtask} is
complex and therefore an example is given. The aforementioned Listing
shows a simple specification containing one \gls{Task} that increments a value
indefinitely every one seconds.

\begin{lstlisting}[label={lst:taskclass},%
	caption={The classes for defining \glspl{Task}}]
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) | ...

count = task \count = (\n.count (lit 1000) (n +. One)) In {main = count (lit 1000) Zero}
\end{lstlisting}

\section{Example mTask}
Some example \glspl{mTask} using almost all of their functionality are shown in
Listing~\ref{lst:exmtask}. The \glspl{mTask} shown in the example do not belong
to a particular view and therefore are of the type \CI{View t r}. The
\CI{blink} \gls{mTask} show the classic \gls{Arduino} blinking led application
that blinks a certain \gls{LED} every second. The \CI{thermostat} expression
will enable a digital pin powering a cooling fan when the analog pin
representing a temperature sensor is too high. \CI{thermostat`} shows the same
expression but now using the assignment style \gls{GPIO} technique. The
\CI{thermostat} example also shows that it is not necessary to run everything
as a \CI{task}. The main program code can also just consist of the contents of
the root \CI{main} itself.

\begin{lstlisting}[%
	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)
	In {main=blink (lit 1000) True}

thermostat :: Main (View () Stmt)
thermostat = {main =
  IF (analogRead A0 >. lit 50)
	( digitalWrite D0 (lit True)  )
    ( digitalWrite D0 (lit False) )
  }

thermostat` :: Main (View () Stmt)
thermostat` = let 
  a0 = aIO A0
  d0 = dIO D0 in {main = IF (a0 >. lit 50) (d0 =. lit True) (d0 =. lit False) }
\end{lstlisting}
