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 \gls{mTask} do not behave like functions but more like
  40 \gls{iTasks}-\glspl{Task}. When an \gls{mTask} is created it returns immediatly
  41 and the \gls{Task} will be executed sometime in the future. \glspl{Task} can
  42 run at an interval and they can start other tasks.
  43 \todo{Meer uitwijden over de mTask semantiek}
  44
  45 \section{Expressions}
  46 Expressions in the \gls{mTask}-\gls{EDSL} are divided into two types, namely
  47 boolean expressions and arithmetic expressions. The class of arithmetic
  48 language constructs also contains the function \CI{lit} that lifts a
  49 host-language value in to the \gls{EDSL} domain. All standard arithmetic
  50 functions are included but are omitted for brevity. Moreover the class
  51 restrictions are only shown in the first functions and are later omitted. Both
  52 the boolean expression and arithmetic expression classes are shown in
  53 Listing~\ref{lst:arithbool}.
  54
  55 \begin{lstlisting}[language=Clean,label={lst:arithbool},
  56         caption={Basic classes for expressions}]
  57 class arith v where
  58   lit           :: t -> v t Expr
  59   (+.) infixl 6 :: (v t p) (v t q) -> v t Expr          | +, zero t    & isExpr p & isExpr q
  60   (-.) infixl 6 :: (v t p) (v t q) -> v t Expr          | -, zero t    & ...
  61   ...
  62 class boolExpr v where
  63   Not           :: (v Bool p) -> v Bool Expr            | ...
  64   (&.) infixr 3 :: (v Bool p) (v Bool q) -> v Bool Expr | ...
  65   ...
  66   (==.) infix 4 :: (v a p) (v a q) -> v Bool Expr       | ==, toCode a & ...
  67 \end{lstlisting}
  68
  69 \section{Control flow}
  70 Looping of \glspl{Task} happens because \glspl{Task} are launched at regular
  71 intervals or relaunch themselves. Therefore there is no need for loop control
  72 flow functionality such as \CI{While} or \CI{For} constructions. The main
  73 control flow is the sequence operator and the \CI{If} statement. Both are shown
  74 in Listing~\ref{lst:control}. The first class of \CI{If} statements describe
  75 the regular if statement. The expressions given can have any role. The
  76 functional dependency on \CI{s} determines the return type of the statement.
  77 The sequence operator is very straightforward and just ties the two expressions
  78 together in sequence.
  79
  80 \begin{lstlisting}[%
  81         language=Clean,label={lst:control},caption={Control flow operators}]
  82 class If v q r ~s where
  83   If :: (v Bool p) (v t q) (v t r) -> v t s | ...
  84
  85 class seq v where
  86   (:.) infixr 0 :: (v t p) (v u q) -> v u Stmt | ...
  87 \end{lstlisting}
  88
  89 \section{Input/Output and class extensions}
  90 All expressions that have an \CI{Upd} role can be assigned to. Examples of such
  91 expressions are \glspl{SDS} and \gls{GPIO}. Moreover, class extensions can be
  92 created for specific peripherals such as user LEDs. The classes facilitating
  93 this are shown in Listing~\ref{lst:sdsio}. In this way the assignment is the
  94 same for every assignable entity.
  95
  96 \begin{lstlisting}[%
  97         language=Clean,label={lst:sdsio},caption={Input/Output classes}]
  98 :: DigitalPin = D0 | D1 | D2 | D3 | D4 | D5 |D6 | D7 | D8 | D9 | D10 | D11 | D12 | D13
  99 :: AnalogPin  = A0 | A1 | A2 | A3 | A4 | A5
 100 :: UserLED = LED1 | LED2 | LED3
 101
 102 class dIO v where dIO :: DigitalPin -> v Bool Upd
 103 class aIO v where aIO :: AnalogPin -> v Int Upd
 104 class analogRead v where
 105   analogRead :: AnalogPin -> v Int Expr
 106   analogWrite :: AnalogPin (v Int p) -> v Int Expr
 107 class digitalRead v where
 108   digitalRead :: DigitalPin -> v Bin Expr
 109   digitalWrite :: DigitalPin (v Bool p) -> v Int Expr
 110
 111 :: UserLED = LED1 | LED2 | LED3
 112 class userLed v where
 113   ledOn  :: (v UserLED q) -> (v () Stmt)
 114   ledOff :: (v UserLED q) -> (v () Stmt)
 115
 116 class assign v where
 117   (=.) infixr 2 :: (v t Upd) (v t p) -> v t Expr | ...
 118 \end{lstlisting}
 119
 120 A way of storing data in \glspl{mTask} is using \glspl{SDS}. \glspl{SDS} serve
 121 as variables in the \gls{mTask} and will keep their value across executions.
 122 The classes associated with \glspl{SDS} are listed in
 123 Listing~\ref{lst:sdsclass}. The \CI{Main} class is introduced to box an
 124 \gls{mTask} and make it recognizable by the type system.
 125
 126 \begin{lstlisting}[%
 127         language=Clean,label={lst:sdsclass},caption={\glspl{SDS} in \gls{mTask}}]
 128 :: In a b = In infix 0 a b
 129 :: Main a = {main :: a}
 130
 131 class sds v where
 132   sds :: ((v t Upd)->In t (Main (v c s))) -> (Main (v c s)) | ...
 133 \end{lstlisting}
 134
 135 \section{Example mTask}
 136 \todo{Also explain semantics about running tasks}
 137 Some example \glspl{mTask} using almost all of the functionality are show in
 138 Listing~\ref{lst:exmtask}. The \glspl{mTask} shown in the example do not belong
 139 to a particular view and therefore are of the type \CI{View t r}. The
 140 \CI{blink} \gls{mTask} show the classic \emph{Arduino} \emph{Hello World!}
 141 application that blinks a certain LED every interval. The \CI{thermostat}
 142 \gls{mTask} will enable a digital pin powering a cooling fan when the analog
 143 pin representing a temperature sensor is too high. \CI{thermostat`} shows the
 144 same program but now using the assignment style \gls{GPIO}.
 145
 146 \begin{lstlisting}[%
 147         language=Clean,label={lst:exmtask},caption={Some example \glspl{mTask}}]
 148 blink :: Main (View Int Stmt)
 149 blink = sds \x=1 In sds \led=LED1 In {main =
 150   IF (x ==. lit 1) (ledOn led) (ledOff led) :.
 151   x =. lit 1 -. x
 152   }
 153
 154 thermostat :: Main (View () Stmt)
 155 thermostat = {main =
 156   IF (analogRead A0 >. 50)
 157         ( digitalWrite D0 (lit True)  )
 158     ( digitalWrite D0 (lit False) )
 159   }
 160
 161 thermostat` :: Main (View () Stmt)
 162 thermostat` = let
 163   a0 = aIO A0
 164   d0 = dIO D0 in {main = IF (a0 >. 50) (d0 =. lit True) (d0 =. lit False) }
 165 \end{lstlisting}