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 $-= 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}-backends}\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 launched at regular
 105 intervals or relaunch themselves. Therefore there is no need for loop control
 106 flow functionality such as \emph{while} or \emph{for} constructions. The main
 107 control flow is the sequence operator and the \emph{if} statement. Both are
 108 shown in Listing~\ref{lst:control}. The first class of \emph{If} statements
 109 describe the regular \emph{if} statement. The expressions given can have any
 110 role. The functional dependency on \CI{s} determines the return type of the
 111 statement.  The sequence operator is very straightforward and just ties the two
 112 expressions together in sequence.
 113
 114 \begin{lstlisting}[%
 115         language=Clean,label={lst:control},caption={Control flow operators}]
 116 class If v q r ~s where
 117   If :: (v Bool p) (v t q) (v t r) -> v t s | ...
 118
 119 class seq v where
 120   (:.) infixr 0 :: (v t p) (v u q) -> v u Stmt | ...
 121 \end{lstlisting}
 122
 123 \section{Input/Output and class extensions}
 124 All expressions that have an \CI{Upd} role can be assigned to. Examples of such
 125 expressions are \glspl{SDS} and \gls{GPIO}. Moreover, class extensions can be
 126 created for specific peripherals such as user LEDs. The classes facilitating
 127 this are shown in Listing~\ref{lst:sdsio}. In this way the assignment is the
 128 same for every assignable entity.
 129
 130 \begin{lstlisting}[%
 131         language=Clean,label={lst:sdsio},caption={Input/Output classes}]
 132 :: DigitalPin = D0 | D1 | D2 | D3 | D4 | D5 |D6 | D7 | D8 | D9 | D10 | D11 | D12 | D13
 133 :: AnalogPin  = A0 | A1 | A2 | A3 | A4 | A5
 134 :: UserLED = LED1 | LED2 | LED3
 135
 136 class dIO v where dIO :: DigitalPin -> v Bool Upd
 137 class aIO v where aIO :: AnalogPin -> v Int Upd
 138 class analogRead v where
 139   analogRead :: AnalogPin -> v Int Expr
 140   analogWrite :: AnalogPin (v Int p) -> v Int Expr
 141 class digitalRead v where
 142   digitalRead :: DigitalPin -> v Bin Expr
 143   digitalWrite :: DigitalPin (v Bool p) -> v Int Expr
 144
 145 :: UserLED = LED1 | LED2 | LED3
 146 class userLed v where
 147   ledOn  :: (v UserLED q) -> (v () Stmt)
 148   ledOff :: (v UserLED q) -> (v () Stmt)
 149
 150 class assign v where
 151   (=.) infixr 2 :: (v t Upd) (v t p) -> v t Expr | ...
 152 \end{lstlisting}
 153
 154 A way of storing data in \glspl{mTask} is using \glspl{SDS}. \glspl{SDS} serve
 155 as variables in the \gls{mTask} and maintain their value across executions.
 156 The classes associated with \glspl{SDS} are listed in
 157 Listing~\ref{lst:sdsclass}. The \CI{Main} class is introduced to box an
 158 \gls{mTask} and make it recognizable by the type system.
 159
 160 \begin{lstlisting}[%
 161         language=Clean,label={lst:sdsclass},caption={\glspl{SDS} in \gls{mTask}}]
 162 :: In a b = In infix 0 a b
 163 :: Main a = {main :: a}
 164
 165 class sds v where
 166   sds :: ((v t Upd)->In t (Main (v c s))) -> (Main (v c s)) | ...
 167 \end{lstlisting}
 168
 169 \section{Example mTask}
 170 \todo{Also explain semantics about running tasks}
 171 Some example \glspl{mTask} using almost all of the functionality are shown in
 172 Listing~\ref{lst:exmtask}. The \glspl{mTask} shown in the example do not belong
 173 to a particular view and therefore are of the type \CI{View t r}. The
 174 \CI{blink} \gls{mTask} show the classic \emph{Arduino} \emph{Hello World!}
 175 application that blinks a certain LED at each interval. The \CI{thermostat}
 176 \gls{mTask} will enable a digital pin powering a cooling fan when the analog
 177 pin representing a temperature sensor is too high. \CI{thermostat`} shows the
 178 same program but now using the assignment style \gls{GPIO}.
 179
 180 \begin{lstlisting}[%
 181         language=Clean,label={lst:exmtask},caption={Some example \glspl{mTask}}]
 182 blink :: Main (View Int Stmt)
 183 blink = sds \x=1 In sds \led=LED1 In {main =
 184   IF (x ==. lit 1) (ledOn led) (ledOff led) :.
 185   x =. lit 1 -. x
 186   }
 187
 188 thermostat :: Main (View () Stmt)
 189 thermostat = {main =
 190   IF (analogRead A0 >. 50)
 191         ( digitalWrite D0 (lit True)  )
 192     ( digitalWrite D0 (lit False) )
 193   }
 194
 195 thermostat` :: Main (View () Stmt)
 196 thermostat` = let
 197   a0 = aIO A0
 198   d0 = dIO D0 in {main = IF (a0 >. 50) (d0 =. lit True) (d0 =. lit False) }
 199 \end{lstlisting}