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