acknowledgements and parametric lenses

[msc-thesis1617.git] / methods.mtask.tex

diff --git a/methods.mtask.tex b/methods.mtask.tex
index 48f8844..df05035 100644 (file)
--- a/methods.mtask.tex
+++ b/methods.mtask.tex
@@ -2,7 +2,7 @@ The \gls{mTask}-\gls{EDSL} is the basis on which the system is built. The
 \gls{mTask}-\gls{EDSL} was created by Koopman et al.\ to support several views
 such as an \gls{iTasks} simulation and a \gls{C}-code generator. The \gls{EDSL}
 was designed to generate a ready to compile \gls{TOP}-like system for
 \gls{mTask}-\gls{EDSL} was created by Koopman et al.\ to support several views
 such as an \gls{iTasks} simulation and a \gls{C}-code generator. The \gls{EDSL}
 was designed to generate a ready to compile \gls{TOP}-like system for

-microcontrollers such as the Arduino\cite{koopman_type-safe_nodate}%
+microcontrollers such as the \gls{Arduino}\cite{koopman_type-safe_nodate}%

 \cite{plasmeijer_shallow_2016}.
 
 The \gls{mTask}-\gls{EDSL} is a shallowly embedded class based \gls{EDSL} and
 \cite{plasmeijer_shallow_2016}.
 
 The \gls{mTask}-\gls{EDSL} is a shallowly embedded class based \gls{EDSL} and


@@ -12,20 +12,21 @@ that are used in this extension. The parts of the \gls{EDSL} that are not used
 will not be discussed and the details of those parts can be found in the cited
 literature.
 
 will not be discussed and the details of those parts can be found in the cited
 literature.
 

-A view for the \gls{mTask}-\gls{EDSL} is a type of kind \CI{*->*->*} that
-implements some of the classes given. The types do not have to be present as
-fields in the higher kinded view and can, and will most often, solely be
-phantom types. A view is of the form \CI{v t r}. The first variable will be the
-type of the view, the second type variable will be the type of the
-\gls{EDSL}-expression and the third type variable represents the role of the
-expression. Currently the role of the expressions form a hierarchy. The three
-roles and their hierarchy are shown in Listing~\ref{lst:exprhier}. This implies
-that everything is a statement, only a \CI{Upd} and a \CI{Expr} are
-expressions. The \CI{Upd} restriction describes updatable expressions such as
-\gls{GPIO} pins and \gls{SDS}.
+A view for the \gls{mTask}-\gls{EDSL} is a type with kind \CI{*->*->*}%
+\footnote{A type with two free type variables.} that implements some of the
+classes given. The types do not have to be present as fields in the higher
+kinded view and can, and will most often, solely be phantom types. A view is of
+the form \CI{v t r}. The first type variable will be the type of the view, the
+second type variable will be the type of the \gls{EDSL}-expression and the
+third type variable represents the role of the expression. Currently the role
+of the expressions form a hierarchy. The three roles and their hierarchy are
+shown in Listing~\ref{lst:exprhier}. This implies that everything is a
+statement, only a \CI{Upd} and a \CI{Expr} are expressions. The \CI{Upd}
+restriction describes updatable expressions such as \gls{GPIO} pins and
+\glspl{SDS}.

 
 \begin{lstlisting}[%
 
 \begin{lstlisting}[%

-       language=Clean,label={lst:exprhier},caption={Expression role hierarchy}]
+       label={lst:exprhier},caption={Expression role hierarchy}]

 :: Upd   = Upd
 :: Expr  = Expr
 :: Stmt  = Stmt
 :: Upd   = Upd
 :: Expr  = Expr
 :: Stmt  = Stmt


@@ -35,47 +36,6 @@ instance isExpr Upd
 instance isExpr Expr
 \end{lstlisting}
 
 instance isExpr Expr
 \end{lstlisting}
 

-\section{Semantics}
-The \gls{C}-backend of the \gls{mTask}-system has an engine that is generated
-alongside the code for the \glspl{Task}. This engine will execute the
-\glspl{mTask} according to certain rules and semantics.
-\glspl{mTask} do not behave like functions but more like
-\gls{iTasks}-\glspl{Task}. An \gls{mTask} is queued when either his timer runs
-out or when it is started by another \gls{mTask}. When an \gls{mTask} is
-queued it does not block the execution but it will return immediately while
-the actual \gls{Task} will be executed some time in the future.
-
-The \gls{iTasks}-backend simulates the \gls{C}-backend and thus uses the same
-semantics. This engine expressed in pseudocode is listed as
-Algorithm~\ref{lst:engine}. All the \glspl{Task} are inspected on their waiting
-time. When the waiting time has not passed the delta is subtracted and they are
-pushed to the end of the queue. When the waiting has has surpassed they are
-executed. When a \gls{mTask} wants to queue another \gls{mTask} it can just
-append it to the queue.
-
-\begin{algorithm}[H]
-       \KwData{\textbf{queue} queue, \textbf{time} $t, t_p$}
-
-       $t\leftarrow\text{now}()$\;
-       \Begin{
-               \While{true}{
-                       $t_p\leftarrow t$\;
-                       $t\leftarrow\text{now}()$\;
-                       \If{notEmpty$($queue$)$}{
-                               $task\leftarrow \text{queue.pop}()$\;
-                               $task$.wait $\leftarrow task$.wait $-(t-t_p)$\;
-                               \eIf{$task.wait>t_0$}{
-                                       queue.append$(task)$\;
-                               }{
-                                       run\_task$(task)$\;
-                               }
-                       }
-               }
-       }
-       \caption{Engine pseudocode for the \gls{C}- and
-               \gls{iTasks}-backend}\label{lst:engine}
-\end{algorithm}
-

 \section{Expressions}
 Expressions in the \gls{mTask}-\gls{EDSL} are divided into two types, namely
 boolean expressions and arithmetic expressions. The class of arithmetic
 \section{Expressions}
 Expressions in the \gls{mTask}-\gls{EDSL} are divided into two types, namely
 boolean expressions and arithmetic expressions. The class of arithmetic


@@ -86,7 +46,7 @@ brevity. Moreover, the class restrictions are only shown in the first functions
 and omitted in subsequent funcitons. Both the boolean expression and arithmetic
 expression classes are shown in Listing~\ref{lst:arithbool}.
 
 and omitted in subsequent funcitons. Both the boolean expression and arithmetic
 expression classes are shown in Listing~\ref{lst:arithbool}.
 

-\begin{lstlisting}[language=Clean,label={lst:arithbool},
+\begin{lstlisting}[label={lst:arithbool},

        caption={Basic classes for expressions}]
 class arith v where
   lit           :: t -> v t Expr
        caption={Basic classes for expressions}]
 class arith v where
   lit           :: t -> v t Expr


@@ -104,32 +64,40 @@ class boolExpr v where
 Looping of \glspl{Task} happens because \glspl{Task} are executed after waiting
 a specified amount of time or when they are launched by another task or even
 themselves. Therefore there is no need for loop control flow functionality such
 Looping of \glspl{Task} happens because \glspl{Task} are executed after waiting
 a specified amount of time or when they are launched by another task or even
 themselves. Therefore there is no need for loop control flow functionality such

-as \emph{while} or \emph{for} constructions. The main control flow is the
-sequence operator and the \emph{if} statement. Both are shown in
-Listing~\ref{lst:control}. The first class of \emph{If} statements describe the
-regular \emph{if} statement. The expressions given can have any role. The
-functional dependency on \CI{s} determines the return type of the statement.
-The sequence operator is very straightforward and just ties the two expressions
-together in sequence.
+as \emph{while} or \emph{for} constructions. The main control flow operators
+are the sequence operator and the \emph{if} statement. Both are shown in
+Listing~\ref{lst:control}. The first class of \emph{If} statements describes
+the regular \emph{if} statement. The expressions given can have any role. The
+functional dependency on \CI{s} determines the return type of the
+statement. The listing includes examples of implementations that illustrate
+this dependency.
+
+The sequence operator is very straightforward and just ties
+the two expressions together in sequence.

 
 \begin{lstlisting}[%
 
 \begin{lstlisting}[%

-       language=Clean,label={lst:control},caption={Control flow operators}]
+       label={lst:control},caption={Control flow operators}]

 class If v q r ~s where
   If :: (v Bool p) (v t q) (v t r) -> v t s | ...
 
 class If v q r ~s where
   If :: (v Bool p) (v t q) (v t r) -> v t s | ...
 

+instance If Code Stmt Stmt Stmt
+instance If Code e    Stmt Stmt
+instance If Code Stmt e    Stmt
+instance If Code x    y    Expr
+

 class seq v where
   (:.) infixr 0 :: (v t p) (v u q) -> v u Stmt | ...
 \end{lstlisting}
 
 \section{Input/Output and class extensions}
 class seq v where
   (:.) infixr 0 :: (v t p) (v u q) -> v u Stmt | ...
 \end{lstlisting}
 
 \section{Input/Output and class extensions}

-All expressions that have an \CI{Upd} role can be assigned to. Examples of such
-expressions are \glspl{SDS} and \gls{GPIO}. Moreover, class extensions can be
-created for specific peripherals such as user LEDs. The classes facilitating
-this are shown in Listing~\ref{lst:sdsio}. In this way the assignment is the
-same for every assignable entity.
+Values can be assigned to all expressions that have an \CI{Upd} role. Examples
+of such expressions are \glspl{SDS} and \gls{GPIO} pins. Moreover, class
+extensions can be created for specific peripherals such as builtin \glspl{LED}.
+The classes facilitating this are shown in Listing~\ref{lst:sdsio}. In this way
+the assignment is the same for every assignable entity.

 
 \begin{lstlisting}[%
 
 \begin{lstlisting}[%

-       language=Clean,label={lst:sdsio},caption={Input/Output classes}]
+       label={lst:sdsio},caption={Input/Output classes}]

 :: DigitalPin = D0 | D1 | D2 | D3 | D4 | D5 |D6 | D7 | D8 | D9 | D10 | D11 | D12 | D13
 :: AnalogPin  = A0 | A1 | A2 | A3 | A4 | A5
 :: UserLED = LED1 | LED2 | LED3
 :: DigitalPin = D0 | D1 | D2 | D3 | D4 | D5 |D6 | D7 | D8 | D9 | D10 | D11 | D12 | D13
 :: AnalogPin  = A0 | A1 | A2 | A3 | A4 | A5
 :: UserLED = LED1 | LED2 | LED3


@@ -155,11 +123,11 @@ class assign v where
 A way of storing data in \glspl{mTask} is using \glspl{SDS}. \glspl{SDS} serve
 as variables in the \gls{mTask} and maintain their value across executions.
 The classes associated with \glspl{SDS} are listed in
 A way of storing data in \glspl{mTask} is using \glspl{SDS}. \glspl{SDS} serve
 as variables in the \gls{mTask} and maintain their value across executions.
 The classes associated with \glspl{SDS} are listed in

-Listing~\ref{lst:sdsclass}. The \CI{Main} class is introduced to box an
+Listing~\ref{lst:sdsclass}. The \CI{Main} type is introduced to box an

 \gls{mTask} and make it recognizable by the type system.
 
 \begin{lstlisting}[%
 \gls{mTask} and make it recognizable by the type system.
 
 \begin{lstlisting}[%

-       language=Clean,label={lst:sdsclass},caption={\glspl{SDS} in \gls{mTask}}]
+       label={lst:sdsclass},caption={\glspl{SDS} in \gls{mTask}}]

 :: In a b = In infix 0 a b
 :: Main a = {main :: a}
 
 :: In a b = In infix 0 a b
 :: Main a = {main :: a}
 


@@ -167,28 +135,83 @@ class sds v where
   sds :: ((v t Upd)->In t (Main (v c s))) -> (Main (v c s)) | ...
 \end{lstlisting}
 
   sds :: ((v t Upd)->In t (Main (v c s))) -> (Main (v c s)) | ...
 \end{lstlisting}
 

+\section{Semantics}
+The \gls{C}-backend of the \gls{mTask}-system has an engine that is generated
+alongside the code for the \glspl{Task}. This engine will execute the
+\glspl{mTask} according to certain rules and semantics.
+\glspl{mTask} do not behave like functions but more like
+\gls{iTasks}-\glspl{Task}. An \gls{mTask} is queued when either his timer runs
+out or when it is started by another \gls{mTask}. When an \gls{mTask} is
+queued it does not block the execution but it will return immediately while
+the actual \gls{Task} will be executed some time in the future.
+
+The \gls{iTasks}-backend simulates the \gls{C}-backend and thus uses the same
+semantics. This engine expressed in pseudocode is listed as
+Algorithm~\ref{lst:engine}. All the \glspl{Task} are inspected on their waiting
+time. When the waiting time has not passed; the delta is subtracted and the
+task gets pushed to the end of the queue. When the waiting has surpassed they are
+executed. When an \gls{mTask} wants to queue another \gls{mTask} it can just
+append it to the queue.
+
+\begin{algorithm}[H]
+       \KwData{\textbf{queue} queue, \textbf{time} $t, t_p$}
+
+       $t\leftarrow\text{now}()$\;
+       \Begin{
+               \While{true}{
+                       $t_p\leftarrow t$\;
+                       $t\leftarrow\text{now}()$\;
+                       \If{notEmpty$($queue$)$}{
+                               $task\leftarrow \text{queue.pop}()$\;
+                               $task$.wait $\leftarrow task$.wait $-(t-t_p)$\;
+                               \eIf{$task.wait>t_0$}{
+                                       queue.append$(task)$\;
+                               }{
+                                       run\_task$(task)$\;
+                               }
+                       }
+               }
+       }
+       \caption{Engine pseudocode for the \gls{C}- and
+               \gls{iTasks}-backend}\label{lst:engine}
+\end{algorithm}
+
+To achieve this in the \gls{EDSL} a \gls{Task} clas are added that work in a
+similar fashion as the \texttt{sds} class. This class is listed in
+Listing~\ref{lst:taskclass}. \glspl{Task} can have an argument and always have
+to specify a delay or waiting time. The type signature of the \CI{mtask} is
+complex and therefore an example is given. The aforementioned Listing
+shows a simple specification containing one task that increments a value
+indefinitely every one seconds.
+
+\begin{lstlisting}[label={lst:taskclass},%
+       caption={The classes for defining tasks}]
+class mtask v a where
+  task :: (((v delay r) a->v MTask Expr)->In (a->v u p) (Main (v t q))) -> Main (v t q) | ...
+
+count = task \count = (\n.count (lit 1000) (n +. One)) In {main = count (lit 1000) Zero}
+\end{lstlisting}
+

 \section{Example mTask}
 \section{Example mTask}

-\todo{Also explain semantics about running tasks}

 Some example \glspl{mTask} using almost all of the functionality are shown in
 Listing~\ref{lst:exmtask}. The \glspl{mTask} shown in the example do not belong
 to a particular view and therefore are of the type \CI{View t r}. The
 Some example \glspl{mTask} using almost all of the functionality are shown in
 Listing~\ref{lst:exmtask}. The \glspl{mTask} shown in the example do not belong
 to a particular view and therefore are of the type \CI{View t r}. The

-\CI{blink} \gls{mTask} show the classic \emph{Arduino} \emph{Hello World!}
-application that blinks a certain LED at each interval. The \CI{thermostat}
-\gls{mTask} will enable a digital pin powering a cooling fan when the analog
-pin representing a temperature sensor is too high. \CI{thermostat`} shows the
-same program but now using the assignment style \gls{GPIO}.
+\CI{blink} \gls{mTask} show the classic \gls{Arduino} \emph{Hello World!}
+application that blinks a certain \gls{LED} every second. The \CI{thermostat}
+expression will enable a digital pin powering a cooling fan when the analog pin
+representing a temperature sensor is too high. \CI{thermostat`} shows the same
+expression but now using the assignment style \gls{GPIO} technique.

 
 \begin{lstlisting}[%
 
 \begin{lstlisting}[%

-       language=Clean,label={lst:exmtask},caption={Some example \glspl{mTask}}]
-blink :: Main (View Int Stmt)
-blink = sds \x=1 In sds \led=LED1 In {main =
-  IF (x ==. lit 1) (ledOn led) (ledOff led) :.
-  x =. lit 1 -. x
-  }
+       label={lst:exmtask},caption={Some example \glspl{mTask}}]
+blink = task \blink=(\x.
+               IF (x ==. lit True) (ledOn led) (ledOff led) :.
+               blink (lit 1000) (Not x)
+       In {main=blink (lit 1000) True}

 
 thermostat :: Main (View () Stmt)
 thermostat = {main =
 
 thermostat :: Main (View () Stmt)
 thermostat = {main =

-  IF (analogRead A0 >. 50)
+  IF (analogRead A0 >. lit 50)

        ( digitalWrite D0 (lit True)  )
     ( digitalWrite D0 (lit False) )
   }
        ( digitalWrite D0 (lit True)  )
     ( digitalWrite D0 (lit False) )
   }


@@ -196,5 +219,5 @@ thermostat = {main =
 thermostat` :: Main (View () Stmt)
 thermostat` = let 
   a0 = aIO A0
 thermostat` :: Main (View () Stmt)
 thermostat` = let 
   a0 = aIO A0

-  d0 = dIO D0 in {main = IF (a0 >. 50) (d0 =. lit True) (d0 =. lit False) }
+  d0 = dIO D0 in {main = IF (a0 >. lit 50) (d0 =. lit True) (d0 =. lit False) }

 \end{lstlisting}
 \end{lstlisting}