methods.mtask.tex

   1 The \gls{mTask}-\gls{EDSL} is the basis on which the system is built. The
   2 \gls{mTask}-\gls{EDSL} was created by Koopman et al.\ to support several views
   3 such as an \gls{iTasks} simulation and a \gls{C}-code generator. The \gls{EDSL}
   4 was designed to generate a ready to compile \gls{TOP}-like system for
   5 microcontrollers such as the Arduino\cite{koopman_type-safe_nodate}%
   6 \cite{plasmeijer_shallow_2016}.
   7
   8 The \gls{mTask}-\gls{EDSL} is a shallowly embedded class based \gls{EDSL} and
   9 therefore it is very suitable to have a new backend that partly implements the
  10 given classes. The following sections show the details of the \gls{EDSL}
  11 that are used in this extension. The parts of the \gls{EDSL} that are not used
  12 will not be discussed and the details of those parts can be found in the cited
  13 literature.
  14
  15 A view for the \gls{mTask}-\gls{EDSL} is a type of kind \CI{*->*->*} that
  16 implements some of the classes given. The types do not have to be present as
  17 fields in the higher kinded view and can, and will most often, solely be
  18 phantom types. A view is of the form \CI{v t r}. The first variable will be the
  19 type of the view, the second type variable will be the type of the
  20 \gls{EDSL}-expression and the third type variable represents the role of the
  21 expression. Currently the role of the expressions form a hierarchy. The three
  22 roles and their hierarchy are shown in Listing~\ref{lst:exprhier}. This implies
  23 that everything is a statement, only a \CI{Upd} and a \CI{Expr} are
  24 expressions. The \CI{Upd} restriction describes updatable expressions such as
  25 \gls{GPIO} pins and \gls{SDS}.
  26
  27 \begin{lstlisting}[%
  28         language=Clean,label={lst:exprhier},caption={Expression role hierarchy}]
  29 :: Upd   = Upd
  30 :: Expr  = Expr
  31 :: Stmt  = Stmt
  32
  33 class isExpr a :: a -> Int
  34 instance isExpr Upd
  35 instance isExpr Expr
  36 \end{lstlisting}
  37
  38 \section{Expressions}
  39 Expressions in the \gls{mTask}-\gls{EDSL} are divided into two types, namely
  40 boolean expressions and arithmetic expressions. The class of arithmetic
  41 language constructs also contains the function \CI{lit} that lifts a
  42 host-language value in to the \gls{EDSL} domain. All standard arithmetic
  43 functions are included in the \gls{EDSL} but are omitted in the example for
  44 brevity. Moreover, the class restrictions are only shown in the first functions
  45 and omitted in subsequent funcitons. Both the boolean expression and arithmetic
  46 expression classes are shown in Listing~\ref{lst:arithbool}.
  47
  48 \begin{lstlisting}[language=Clean,label={lst:arithbool},
  49         caption={Basic classes for expressions}]
  50 class arith v where
  51   lit           :: t -> v t Expr
  52   (+.) infixl 6 :: (v t p) (v t q) -> v t Expr          | +, zero t    & isExpr p & isExpr q
  53   (-.) infixl 6 :: (v t p) (v t q) -> v t Expr          | -, zero t    & ...
  54   ...
  55 class boolExpr v where
  56   Not           :: (v Bool p) -> v Bool Expr            | ...
  57   (&.) infixr 3 :: (v Bool p) (v Bool q) -> v Bool Expr | ...
  58   ...
  59   (==.) infix 4 :: (v a p) (v a q) -> v Bool Expr       | ==, toCode a & ...
  60 \end{lstlisting}
  61
  62 \section{Control flow}
  63 Looping of \glspl{Task} happens because \glspl{Task} are executed after waiting
  64 a specified amount of time or when they are launched by another task or even
  65 themselves. Therefore there is no need for loop control flow functionality such
  66 as \emph{while} or \emph{for} constructions. The main control flow is the
  67 sequence operator and the \emph{if} statement. Both are shown in
  68 Listing~\ref{lst:control}. The first class of \emph{If} statements describe the
  69 regular \emph{if} statement. The expressions given can have any role. The
  70 functional dependency on \CI{s} determines the return type of the statement.
  71 The sequence operator is very straightforward and just ties the two expressions
  72 together in sequence.
  73
  74 \begin{lstlisting}[%
  75         language=Clean,label={lst:control},caption={Control flow operators}]
  76 class If v q r ~s where
  77   If :: (v Bool p) (v t q) (v t r) -> v t s | ...
  78
  79 class seq v where
  80   (:.) infixr 0 :: (v t p) (v u q) -> v u Stmt | ...
  81 \end{lstlisting}
  82
  83 \section{Input/Output and class extensions}
  84 All expressions that have an \CI{Upd} role can be assigned to. Examples of such
  85 expressions are \glspl{SDS} and \gls{GPIO}. Moreover, class extensions can be
  86 created for specific peripherals such as user LEDs. The classes facilitating
  87 this are shown in Listing~\ref{lst:sdsio}. In this way the assignment is the
  88 same for every assignable entity.
  89
  90 \begin{lstlisting}[%
  91         language=Clean,label={lst:sdsio},caption={Input/Output classes}]
  92 :: DigitalPin = D0 | D1 | D2 | D3 | D4 | D5 |D6 | D7 | D8 | D9 | D10 | D11 | D12 | D13
  93 :: AnalogPin  = A0 | A1 | A2 | A3 | A4 | A5
  94 :: UserLED = LED1 | LED2 | LED3
  95
  96 class dIO v where dIO :: DigitalPin -> v Bool Upd
  97 class aIO v where aIO :: AnalogPin -> v Int Upd
  98 class analogRead v where
  99   analogRead :: AnalogPin -> v Int Expr
 100   analogWrite :: AnalogPin (v Int p) -> v Int Expr
 101 class digitalRead v where
 102   digitalRead :: DigitalPin -> v Bin Expr
 103   digitalWrite :: DigitalPin (v Bool p) -> v Int Expr
 104
 105 :: UserLED = LED1 | LED2 | LED3
 106 class userLed v where
 107   ledOn  :: (v UserLED q) -> (v () Stmt)
 108   ledOff :: (v UserLED q) -> (v () Stmt)
 109
 110 class assign v where
 111   (=.) infixr 2 :: (v t Upd) (v t p) -> v t Expr | ...
 112 \end{lstlisting}
 113
 114 A way of storing data in \glspl{mTask} is using \glspl{SDS}. \glspl{SDS} serve
 115 as variables in the \gls{mTask} and maintain their value across executions.
 116 The classes associated with \glspl{SDS} are listed in
 117 Listing~\ref{lst:sdsclass}. The \CI{Main} class is introduced to box an
 118 \gls{mTask} and make it recognizable by the type system.
 119
 120 \begin{lstlisting}[%
 121         language=Clean,label={lst:sdsclass},caption={\glspl{SDS} in \gls{mTask}}]
 122 :: In a b = In infix 0 a b
 123 :: Main a = {main :: a}
 124
 125 class sds v where
 126   sds :: ((v t Upd)->In t (Main (v c s))) -> (Main (v c s)) | ...
 127 \end{lstlisting}
 128
 129 \section{Semantics}
 130 The \gls{C}-backend of the \gls{mTask}-system has an engine that is generated
 131 alongside the code for the \glspl{Task}. This engine will execute the
 132 \glspl{mTask} according to certain rules and semantics.
 133 \glspl{mTask} do not behave like functions but more like
 134 \gls{iTasks}-\glspl{Task}. An \gls{mTask} is queued when either his timer runs
 135 out or when it is started by another \gls{mTask}. When an \gls{mTask} is
 136 queued it does not block the execution but it will return immediately while
 137 the actual \gls{Task} will be executed some time in the future.
 138
 139 The \gls{iTasks}-backend simulates the \gls{C}-backend and thus uses the same
 140 semantics. This engine expressed in pseudocode is listed as
 141 Algorithm~\ref{lst:engine}. All the \glspl{Task} are inspected on their waiting
 142 time. When the waiting time has not passed the delta is subtracted and they are
 143 pushed to the end of the queue. When the waiting has has surpassed they are
 144 executed. When a \gls{mTask} wants to queue another \gls{mTask} it can just
 145 append it to the queue.
 146
 147 \begin{algorithm}[H]
 148         \KwData{\textbf{queue} queue, \textbf{time} $t, t_p$}
 149
 150         $t\leftarrow\text{now}()$\;
 151         \Begin{
 152                 \While{true}{
 153                         $t_p\leftarrow t$\;
 154                         $t\leftarrow\text{now}()$\;
 155                         \If{notEmpty$($queue$)$}{
 156                                 $task\leftarrow \text{queue.pop}()$\;
 157                                 $task$.wait $\leftarrow task$.wait $-(t-t_p)$\;
 158                                 \eIf{$task.wait>t_0$}{
 159                                         queue.append$(task)$\;
 160                                 }{
 161                                         run\_task$(task)$\;
 162                                 }
 163                         }
 164                 }
 165         }
 166         \caption{Engine pseudocode for the \gls{C}- and
 167                 \gls{iTasks}-backend}\label{lst:engine}
 168 \end{algorithm}
 169
 170 To achieve this in the \gls{EDSL} a \gls{Task} clas are added that work in a
 171 similar fashion as the \texttt{sds} class. This class is listed in
 172 Listing~\ref{lst:taskclass}. \glspl{Task} can have an argument and always have
 173 to specify a delay or waiting time. The type signature of the \CI{mtask} is
 174 rather arcane and therefore an example is given. The aforementioned Listing
 175 shows a simple specification containing one task that increments a value
 176 indefinitely every one seconds.
 177
 178 \begin{lstlisting}[language=Clean,label={lst:taskclass},%
 179         caption={The classes for defining tasks}]
 180 class mtask v a where
 181   task :: (((v delay r) a->v MTask Expr)->In (a->v u p) (Main (v t q))) -> Main (v t q) | ...
 182
 183 count = task \count = (\n.count (lit 1000) (n +. One)) In {main = count (lit 1000) Zero}
 184 \end{lstlisting}
 185
 186 \section{Example mTask}
 187 Some example \glspl{mTask} using almost all of the functionality are shown in
 188 Listing~\ref{lst:exmtask}. The \glspl{mTask} shown in the example do not belong
 189 to a particular view and therefore are of the type \CI{View t r}. The
 190 \CI{blink} \gls{mTask} show the classic \gls{Arduino} \emph{Hello World!}
 191 application that blinks a certain LED every second. The \CI{thermostat}
 192 expression will enable a digital pin powering a cooling fan when the analog
 193 pin representing a temperature sensor is too high. \CI{thermostat`} shows the
 194 same expression but now using the assignment style \gls{GPIO} technique.
 195
 196 \begin{lstlisting}[%
 197         language=Clean,label={lst:exmtask},caption={Some example \glspl{mTask}}]
 198 blink = task \blink=(\x.
 199                 IF (x ==. lit True) (ledOn led) (ledOff led) :.
 200                 blink (lit 1000) (Not x)
 201         In {main=blink (lit 1000) True}
 202
 203 thermostat :: Main (View () Stmt)
 204 thermostat = {main =
 205   IF (analogRead A0 >. 50)
 206         ( digitalWrite D0 (lit True)  )
 207     ( digitalWrite D0 (lit False) )
 208   }
 209
 210 thermostat` :: Main (View () Stmt)
 211 thermostat` = let
 212   a0 = aIO A0
 213   d0 = dIO D0 in {main = IF (a0 >. 50) (d0 =. lit True) (d0 =. lit False) }
 214 \end{lstlisting}