X-Git-Url: https://git.martlubbers.net/?a=blobdiff_plain;f=top%2Flang.tex;h=8c9e3f7685635268e9e894dcf3c9c1617692a1c1;hb=ed3041263afe2ea88dc234a46f3b00d63493b8a8;hp=1e1b02c9cd4f9e0eb81d04220d4cc0789f350071;hpb=d37f1f0d625c081afa66e43d43df55c3741001ae;p=phd-thesis.git diff --git a/top/lang.tex b/top/lang.tex index 1e1b02c..8c9e3f7 100644 --- a/top/lang.tex +++ b/top/lang.tex @@ -4,38 +4,137 @@ \begin{document} \input{subfileprefix} - \chapter{The \texorpdfstring{\gls{MTASK}}{mTask} language}%\texorpdfstring{\glsxtrshort{DSL}}{DSL}}% \label{chp:mtask_dsl} \begin{chapterabstract} \noindent This chapter introduces the \gls{TOP} language \gls{MTASK} language by: \begin{itemize} \item introducing the setup of the \gls{EDSL}; - \item and showing the language interface and examples for the type system, data types, expressions, tasks and their combinators. + \item describing briefly the various interpretations; + \item and showing the language interface for: + \begin{itemize} + \item the types; + \item expressions, datatypes, and functions; + \item tasks and task combinators; + \item and \glspl{SDS}. + \end{itemize} \end{itemize} \end{chapterabstract} -The \gls{MTASK} system is a complete \gls{TOP} programming environment for programming microcontrollers, i.e.\ it contains a \gls{TOP} language and a \gls{TOP} engine. -It is implemented as an \gls{EDSL} in \gls{CLEAN} using class-based---or tagless-final---embedding (see \cref{sec:tagless-final_embedding}). +The \gls{MTASK} system is a complete \gls{TOP} programming environment for programming microcontrollers. +This means that it not only contains a \gls{TOP} language but also a \gls{TOP} engine. Due to the nature of the embedding technique, it is possible to have multiple interpretations for programs written in the \gls{MTASK} language. -The following interpretations are available for \gls{MTASK}. +As the language is implemented as an \gls{EDSL} in \gls{CLEAN} using class-based---or tagless-final---embedding (see \cref{sec:tagless-final_embedding}). +This means that the language is a collection of type classes and interpretations are data types implementing these classes. +Consequently, the language is extensible both in language constructs and in intepretations. +Adding a language construct is as simple as adding a type class and adding an interpretation is done by creating a new data type and providing implementations for the various type classes. +Let us illustrate this by taking the very simple language of literal values. +This language interface can be described using a single type constructor class with a single function \cleaninline{lit}. +This function is for lifting a values, as long as it has a \cleaninline{toString} instance, from the host language to our new \gls{DSL}. + +\begin{lstClean} +class literals v where + lit :: a -> v a | toString a +\end{lstClean} + +Providing an evaluator is straightforward as can be seen in the following listing. +The evaluator is just a box holding a value of the computation but could also be some monadic computation. + +\begin{lstClean} +:: Eval a = Eval a + +runEval :: (Eval a) -> a +runEval (Eval a) = a + +instance literals Eval where + lit a = Eval a +\end{lstClean} + +Extending our language with a printer happens by defining a new data type and providing instances for the type constructor classes. +The printer stores a printed representation and hence the type is just a phantom type. + +\begin{lstClean} +:: Printer a = Printer String + +runPrinter :: (Printer a) -> String +runPrinter (Printer a) = a + +instance literals Printer where + lit a = Printer (toString a) +\end{lstClean} -\begin{description} - \item[Pretty printer] +Finally, adding language constructs happens by defining new type classes and giving implementations for some of the interpretations. +The following listing adds an addition construct to the language and shows implementations for the evaluator and printer. - This interpretation converts the expression to a string representation. - \item[Simulator] +\begin{lstClean} +class addition v where + add :: v a -> v a -> v a | + a + +instance addition Eval where + add (Eval l) (Eval r) = Eval (l + r) + +instance addition Printer where + add (Printer l) (Printer r) = Printer ("(" +++ l +++ "+" +++ r +++ ")") +\end{lstClean} + +Terms in our little toy language can be overloaded in their interpretation, they are just an interface. +For example, $1+5$ is written as \cleaninline{add (lit 1) (lit 5)} and has the type \cleaninline{v Int \| literals, addition v}. +However, due to the way polymorphism is implemented in most functional languages, it is not always straightforward to use multiple interpretations in one function. +Creating such a function, e.g.\ one that both prints and evaluates an expression, requires rank-2 polymorphism (see \cref{lst:rank2_mtask}). + +\section{Interpretations} +This section describes all \gls{MTASK}'s interpretations. +Not all of these interpretations are necessarily \gls{TOP} engines, i.e.\ not all of the interpretations execute the terms/tasks. +Some may perform an analysis over the program or typeset the program so that a textual representation can be shown. + +\subsection{Pretty printer} +This interpretation converts the expression to a string representation. +As the host language \gls{CLEAN} constructs the \gls{MTASK} expressions at run time, it can be useful to show the constructed expression. +The only function exposed for this interpretation is the \cleaninline{showMain} (\cref{lst:showmain}) function. +It runs the pretty printer and returns a list of strings containing the pretty printed result as shown in \cref{lst:showexample}. +The pretty printing function does the best it can but obviously cannot reproduce the layout, curried functions and variable names. +This shortcoming is illustrated by the example application for blinking a single \gls{LED} using a function and currying in \cref{lst:showexample}. + +\begin{lstClean}[caption={The entrypoint for the pretty printing interpretation.},label={lst:showmain}] +:: Show a // from the mTask Show library +showMain :: (Main (Show a)) -> [String] | type a +\end{lstClean} + +\begin{lstClean}[caption={Pretty printing interpretation example.},label={lst:showexample}] +blinkTask :: Main (MTask v Bool) | mtask v +blinkTask = + fun \blink=(\state-> + writeD d13 state >>|. delay (lit 500) >>=. blink o Not + ) In {main = blink true} + +// output: +// fun f0 a1 = writeD(D13, a1) >>= \a2.(delay 1000) >>| (f0 (Not a1)) in (f0 True) +\end{lstClean} + +\subsection{Simulator} +The simulator converts the expression to a ready-for-work \gls{ITASK} simulation in which the user can inspect and control the simulated peripherals and see the internal state of the tasks. +The task resulting from the \cleaninline{simulate} function presents the user with an interactive simulation environment (see \cref{lst:simulatemain,fig:sim}). +From within the interactive application, tasks can be (partly) executed, peripheral states changed and \glspl{SDS} interacted with. + +\begin{lstClean}[caption={The entrypoint for the simulation interpretation.},label={lst:simulatemain}] +:: TraceTask a // from the mTask Show library +simulate :: (Main (TraceTask a)) -> [String] | type a +\end{lstClean} - The simulator converts the expression to a ready-for-work \gls{ITASK} simulation in which the user can inspect and control the simulated peripherals and see the internal state of the tasks. - \item[Byte code compiler] +\begin{figure} + \centering + \includegraphics[width=\linewidth]{simg} + \caption{Simulator interface for the blink program.}\label{fig:sim} +\end{figure} - The compiler compiles the \gls{MTASK} program to a specialised byte code. - Using a handful of integration functions and tasks (see \cref{chp:integration_with_itask}), \gls{MTASK} tasks can be executed on microcontrollers and integrated in \gls{ITASK} as if they were regular \gls{ITASK} tasks. - Furthermore, with special language constructs, \glspl{SDS} can be shared between \gls{MTASK} and \gls{ITASK} programs. -\end{description} +\subsection{Byte code compiler} +The main interpretation of the \gls{MTASK} system is the byte code compiler. +With it, and a handful of integration functions and tasks, \gls{MTASK} tasks can be executed on microcontrollers and integrated in \gls{ITASK} as if they were regular \gls{ITASK} tasks. +Furthermore, with a special language construct, \glspl{SDS} can be shared between \gls{MTASK} and \gls{ITASK} programs as well. +This interface is explained thoroughly in \cref{chp:integration_with_itask}. -When using the compiler interpretation in conjunction with the \gls{ITASK} integration, \gls{MTASK} is a heterogeneous \gls{DSL}. -I.e.\ some components---e.g.\ the \gls{RTS} on the microcontroller---is largely unaware of the other components in the system, and it is executed on a completely different architecture. +When using the byte code compiler interpretation in conjunction with the \gls{ITASK} integration, \gls{MTASK} is a heterogeneous \gls{DSL}. +I.e.\ some components---for example the \gls{RTS} on the microcontroller---is largely unaware of the other components in the system, and it is executed on a completely different architecture. The \gls{MTASK} language is an enriched simply-typed $\lambda$-calculus with support for some basic types, arithmetic operations, and function definition; and a task language (see \cref{sec:top}). \section{Types} @@ -49,23 +148,23 @@ The class constraints for values in \gls{MTASK} are omnipresent in all functions \begin{table}[ht] \centering - \caption{Mapping from \gls{CLEAN}/\gls{MTASK} data types to \gls{CPP} datatypes.}% + \caption{Translation from \gls{CLEAN}\slash\gls{MTASK} data types to \ccpp{} datatypes.}% \label{tbl:mtask-c-datatypes} \begin{tabular}{lll} \toprule - \gls{CLEAN}/\gls{MTASK} & \gls{CPP} type & \textnumero{}bits\\ + \gls{CLEAN}\slash\gls{MTASK} & \ccpp{} type & \textnumero{}bits\\ \midrule \cleaninline{Bool} & \cinline{bool} & 16\\ \cleaninline{Char} & \cinline{char} & 16\\ \cleaninline{Int} & \cinline{int16_t} & 16\\ - \cleaninline{:: Long} & \cinline{int32_t} & 32\\ \cleaninline{Real} & \cinline{float} & 32\\ + \cleaninline{:: Long} & \cinline{int32_t} & 32\\ \cleaninline{:: T = A \| B \| C} & \cinline{enum} & 16\\ \bottomrule \end{tabular} \end{table} -\Cref{lst:constraints} contains the definitions for the auxiliary types and type constraints (such as \cleaninline{type} an \cleaninline{basicType}) that are used to construct \gls{MTASK} expressions. +\Cref{lst:constraints} contains the definitions for the auxiliary types and type constraints (such as \cleaninline{type} and \cleaninline{basicType}) that are used to construct \gls{MTASK} expressions. The \gls{MTASK} language interface consists of a core collection of type classes bundled in the type class \cleaninline{class mtask}. Every interpretation implements the type classes in the \cleaninline{mtask} class There are also \gls{MTASK} extensions that not every interpretation implements such as peripherals and \gls{ITASK} integration. @@ -96,6 +195,22 @@ someTask = In { main = mainexpr } \end{lstClean} +\Gls{MTASK} expressions are usually overloaded in their interpretation (\cleaninline{v}). +In \gls{CLEAN}, all free variables in a type are implicitly universally quantified. +In order to use the \gls{MTASK} expressions with multiple interpretations, rank-2 polymorphism is required \citep{odersky_putting_1996}\citep[\citesection{3.7.4}]{plasmeijer_clean_2021}. +\Cref{lst:rank2_mtask} shows an example of a function that simulates an \gls{MTASK} expression while showing the pretty printed representation in parallel. +Providing a type for the \cleaninline{simulateAndPrint} function is mandatory as the compiler cannot infer the type of rank-2 polymorphic functions. + +\begin{lstClean}[label={lst:rank2_mtask},caption={Rank-2 polymorphism to allow multiple interpretations}] +prettyPrint :: Main (MTask PrettyPrint a) -> String +simulate :: Main (MTask Simulate a) -> Task a + +simulateAndPrint :: (A.v: Main (MTask v a) | mtask v) -> Task a | type a +simulateAndPrint mt = + simulate mt + -|| Hint "Current task:" @>> viewInformation [] (prettyPrint mt) +\end{lstClean} + \section{Expressions}\label{sec:expressions} This section shows all \gls{MTASK} constructs for exppressions. \Cref{lst:expressions} shows the \cleaninline{expr} class containing the functionality to lift values from the host language to the \gls{MTASK} language (\cleaninline{lit}); perform number and boolean arithmetics; do comparisons; and conditional execution. @@ -115,6 +230,7 @@ class expr v where \end{lstClean} Conversion to-and-fro data types is available through the overloaded functions \cleaninline{int}, \cleaninline{long} and \cleaninline{real} that will convert the argument to the respective type similar to casting in \gls{C}. +For most interpretations, there are instances of these classes for all numeric types. \begin{lstClean}[caption={Type conversion functions in \gls{MTASK}.}] class int v a :: (v a) -> v Int @@ -280,7 +396,7 @@ For the \gls{DHT} sensor there are two basic tasks, \cleaninline{temperature} an Currently, two different types of \gls{DHT} sensors are supported, the \emph{DHT} family of sensors connect through $1$-wire protocol and the \emph{SHT} family of sensors connected using \gls{I2C} protocol. Creating such a \cleaninline{DHT} object is very similar to creating functions in \gls{MTASK} and uses \gls{HOAS} to make it type safe. -\begin{lstClean}[label={lst:dht},caption{The \gls{MTASK} interface for \glspl{DHT} sensors.}] +\begin{lstClean}[label={lst:dht},caption={The \gls{MTASK} interface for \glspl{DHT} sensors.}] :: DHT //abstract :: DHTInfo = DHT_DHT Pin DHTtype @@ -296,13 +412,16 @@ measureTemp = DHT (DHT_SHT (i2c 0x36)) \dht-> {main=temperature dht} \end{lstClean} -\Gls{GPIO} access is divided into three classes: analog, digital and pin modes. +\Gls{GPIO} access is divided into three classes: analog, digital and pin modes (see \cref{lst:gpio}). For all pins and pin modes an \gls{ADT} is available that enumerates the pins. The analog \gls{GPIO} pins of a microcontroller are connected to an \gls{ADC} that translates the voltage to an integer. Analog \gls{GPIO} pins can be either read or written to. Digital \gls{GPIO} pins only report a high or a low value. -The type class definition is a bit more complex since analog \gls{GPIO} pins can be used as digital \gls{GPIO} pins as well. -Therefore, if the \cleaninline{p} type implements the \cleaninline{pin} class---i.e.\ either \cleaninline{APin} or \cleaninline{DPin}---the \cleaninline{dio} class can be used. +The \cleaninline{pin} type class allows functions to be overloaded in either the analog or digital pins, e.g.\ analog pins can be considered as digital pins as well. + +For digital \gls{GPIO} interaction, the \cleaninline{dio} type class is used. +The first argument of the functions in this class is overloaded, i.e.\ it accepts either an \cleaninline{APin} or a \cleaninline{DPin}. +Analog \gls{GPIO} tasks are bundled in the \cleaninline{aio} type class. \Gls{GPIO} pins usually operate according to a certain pin mode that states whether the pin acts as an input pin, an input with an internal pull-up resistor or an output pin. This setting can be applied using the \cleaninline{pinMode} class by hand or by using the \cleaninline{declarePin} \gls{GPIO} pin constructor. Setting the pin mode is a task that immediately finisheds and fields a stable unit value. @@ -311,10 +430,12 @@ Reading a pin is a task that yields an unstable value---i.e.\ the value read fro \begin{lstClean}[label={lst:gpio},caption={The \gls{MTASK} interface for \gls{GPIO} access.}] :: APin = A0 | A1 | A2 | A3 | A4 | A5 -:: DPin = D0 | D1 | D2 | D3 | D4 | D5 | D6 | D7 | D8 | D9 | D10 | D11 | D12 | D13 +:: DPin = D0 | D1 | D2 | D3 | D4 | D5 | D6 | D7 | D8 | D9 | D10 | ... :: PinMode = PMInput | PMOutput | PMInputPullup :: Pin = AnalogPin APin | DigitalPin DPin + class pin p :: p -> Pin +instance pin APin, DPin class aio v where writeA :: (v APin) (v Int) -> MTask v Int @@ -329,6 +450,12 @@ class pinMode v where declarePin :: p PinMode ((v p) -> Main (v a)) -> Main (v a) | pin p \end{lstClean} +\Cref{lst:gpio_examples} shows two examples of \gls{MTASK} tasks using \gls{GPIO} pins. +\cleaninline{task1} reads analog \gls{GPIO} pin 3. +This is a task that never terminates. +\cleaninline{task2} writes the \cleaninline{true} (\gls{ARDUINO} \arduinoinline{HIGH}) value to digital \gls{GPIO} pin 3. +This task finishes immediately after writing to the pin. + \begin{lstClean}[label={lst:gpio_examples},caption={\Gls{GPIO} example in \gls{MTASK}.}] task1 :: MTask v Int | mtask v task1 = declarePin A3 PMInput \a3->{main=readA a3} @@ -339,6 +466,7 @@ task2 = declarePin D3 PMOutput \d3->{main=writeD d3 true} \subsection{Task combinators} Task combinators are used to combine multiple tasks to describe workflows. +In contrast to \gls{ITASK}, that uses super combinators to derive the simpler ones, \gls{MTASK} has a set of simpler combinators from which more complicated workflow can be derived. There are three main types of task combinators, namely: \begin{enumerate*} \item Sequential combinators that execute tasks one after the other, possibly using the result of the left hand side. @@ -352,7 +480,7 @@ All seqential task combinators are expressed in the \cleaninline{expr} class and This combinator has a single task on the left-hand side and a list of \emph{task continuations} on the right-hand side. The list of task continuations is checked every rewrite step and if one of the predicates matches, the task continues with the result of this combination. \cleaninline{>>=.} is a shorthand for the bind operation, if the left-hand side is stable, the right-hand side function is called to produce a new task. -\cleaninline{>>|.} is a shorthand for the sequence operation, if the left-hand side is stable, it continues with the right-hand side task. +\cleaninline{>>\|.} is a shorthand for the sequence operation, if the left-hand side is stable, it continues with the right-hand side task. The \cleaninline{>>~.} and \cleaninline{>>..} combinators are variants of the ones above that ignore the stability and continue on an unstable value as well. \begin{lstClean}[label={lst:mtask_sequential},caption={Sequential task combinators in \gls{MTASK}.}] @@ -386,13 +514,18 @@ readPinBin lim = declarePin PMInput A2 \a2-> \subsubsection{Parallel}\label{sssec:combinators_parallel} The result of a parallel task combination is a compound that actually executes the tasks at the same time. - There are two types of parallel task combinators (see \cref{lst:mtask_parallel}). + +\begin{lstClean}[label={lst:mtask_parallel},caption={Parallel task combinators in \gls{MTASK}.}] +class (.&&.) infixr 4 v :: (MTask v a) (MTask v b) -> MTask v (a, b) +class (.||.) infixr 3 v :: (MTask v a) (MTask v a) -> MTask v a +\end{lstClean} + The conjunction combinator (\cleaninline{.&&.}) combines the result by putting the values from both sides in a tuple. The stability of the task depends on the stability of both children. If both children are stable, the result is stable, otherwise the result is unstable. The disjunction combinator (\cleaninline{.\|\|.}) combines the results by picking the leftmost, most stable task. -The semantics are easily described using \gls{CLEAN} functions shown in \cref{lst:semantics_con,lst:semantics_dis}. +The semantics are most easily described using the \gls{CLEAN} functions shown in \cref{lst:semantics_con,lst:semantics_dis}. \begin{figure}[ht] \centering @@ -420,12 +553,7 @@ dis (Value l ls) (Value r rs) \end{subfigure} \end{figure} -\begin{lstClean}[label={lst:mtask_parallel},caption={Parallel task combinators in \gls{MTASK}.}] -class (.&&.) infixr 4 v :: (MTask v a) (MTask v b) -> MTask v (a, b) -class (.||.) infixr 3 v :: (MTask v a) (MTask v a) -> MTask v a -\end{lstClean} - -\Cref{lst:mtask_parallel_example} gives an example of the parallel task combinator. +\Cref{lst:mtask_parallel_example} gives an example program using the parallel task combinator. This program will read two pins at the same time, returning when one of the pins becomes \arduinoinline{HIGH}. If the combinator was the \cleaninline{.&&.} instead, the type would be \cleaninline{MTask v (Bool, Bool)} and the task would only return when both pins have been \arduinoinline{HIGH} but not necessarily at the same time. @@ -451,7 +579,7 @@ class rpeat v where To demonstrate the combinator, \cref{lst:mtask_repeat_example} show \cleaninline{rpeat} in use. This task will mirror the value read from analog \gls{GPIO} pin \cleaninline{A1} to pin \cleaninline{A2} by constantly reading the pin and writing the result. -\begin{lstClean}[label={lst:mtask_repeat_example},caption={Exemplatory repeat task in \gls{MTASK}.}] +\begin{lstClean}[label={lst:mtask_repeat_example},caption={Exemplary repeat task in \gls{MTASK}.}] task :: MTask v Int | mtask v task = declarePin A1 PMInput \a1-> @@ -481,7 +609,7 @@ class sds v where \Cref{lst:mtask_sds_examples} shows an example using \glspl{SDS}. The \cleaninline{count} function takes a pin and returns a task that counts the number of times the pin is observed as high by incrementing the \cleaninline{share} \gls{SDS}. -In the \cleaninline{main} expression, this function is called twice and the results are combined using the parallel or combinator (\cleaninline{.||.}). +In the \cleaninline{main} expression, this function is called twice and the results are combined using the parallel or combinator (\cleaninline{.\|\|.}). Using a sequence of \cleaninline{getSds} and \cleaninline{setSds} would be unsafe here because the other branch might write their old increment value immediately after writing, effectively missing a count.\todo{beter opschrijven} \begin{lstClean}[label={lst:mtask_sds_examples},caption={Examples with \glspl{SDS} in \gls{MTASK}.}]