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