From 61922d4f61677acca7e9b71295c055bc7e9618a9 Mon Sep 17 00:00:00 2001 From: Mart Lubbers Date: Wed, 21 Sep 2022 15:49:24 +0200 Subject: [PATCH] more updates, slight restructure --- appendix/bytecode.tex | 3 +- appendix/clean_for_haskell_programmers.tex | 3 +- backmatter/acknowledgements.tex | 5 +- backmatter/curriculum_vitae.tex | 3 +- backmatter/research_data_management.tex | 13 +- backmatter/samenvatting.tex | 3 +- backmatter/summary.tex | 3 +- conclusion/conclusion.tex | 3 +- .../class_deep_embedding.tex | 3 +- domain-specific_languages/dsl_techniques.tex | 3 +- .../first-class_datatypes.tex | 3 +- ...ed_multi-view_stack-based_computations.tex | 3 +- glossaries.tex | 51 ++++-- hyphenation.tex | 9 + introduction/introduction.tex | 3 +- mtask/.chktexrc | 1 + mtask/beyond_microprocessors.tex | 2 +- mtask/integration.tex | 2 +- mtask/interpreting.tex | 2 +- mtask/mtask.tex | 167 +++++++++++++++--- mtask/mtask_by_example.tex | 2 +- other.bib | 151 ++++++++++++---- preamble.tex | 86 +++++++-- subfilepostamble.tex | 1 + thesis.tex | 22 +-- .../smart_campus.tex | 2 +- 26 files changed, 412 insertions(+), 137 deletions(-) create mode 100644 hyphenation.tex create mode 120000 mtask/.chktexrc diff --git a/appendix/bytecode.tex b/appendix/bytecode.tex index 44ad97e..b46e53e 100644 --- a/appendix/bytecode.tex +++ b/appendix/bytecode.tex @@ -5,8 +5,7 @@ \pagenumbering{arabic} }{} -\chapter{Bytecode instruction set}% -\label{chp:bytecode_instruction_set} +\myappendix{chp:bytecode_instruction_set}{Bytecode instruction set}% \todo[inline]{formatting} \begin{tabular}{ll} diff --git a/appendix/clean_for_haskell_programmers.tex b/appendix/clean_for_haskell_programmers.tex index 65dfb87..56c39d3 100644 --- a/appendix/clean_for_haskell_programmers.tex +++ b/appendix/clean_for_haskell_programmers.tex @@ -7,8 +7,7 @@ }{ } -\chapter{\texorpdfstring{\glsentrytext{CLEAN}}{Clean} for \texorpdfstring{\glsentrytext{HASKELL}}{Haskell} Programmers}% -\label{chp:clean_for_haskell_programmers} +\myappendix{chp:clean_for_haskell_programmers}{\texorpdfstring{\glsentrytext{CLEAN}}{Clean} for \texorpdfstring{\glsentrytext{HASKELL}}{Haskell} Programmers}% This note is meant to give people who are familiar with the functional programming language \gls{HASKELL} a consise overview of \gls{CLEAN} language elements and how they differ from \gls{HASKELL}. The goal is to support the reader when reading \gls{CLEAN} code. diff --git a/backmatter/acknowledgements.tex b/backmatter/acknowledgements.tex index 61f46ab..b000c27 100644 --- a/backmatter/acknowledgements.tex +++ b/backmatter/acknowledgements.tex @@ -4,8 +4,7 @@ \ifSubfilesClassLoaded{ \pagenumbering{arabic} }{} -\chapter{Acknowledgements}% -\label{chp:acknowledgements} +\mybackmatter{chp:acknowledgements}{Acknowledgements}% \begin{center} \noindent Funding: Teun de Groot, Ton van Heusden @@ -22,7 +21,7 @@ Co-authors: Jeremy Singer, Phil Trinder, Adrian Ramsingh, Sustrainable group % %Mentors: Jos Baack, Francisco Torreira, Franc Grootjen, the late Louis Vuurpijl, Ralf Hinze % -%Friends: Pieter Wolfert (and Annerieke Wessels); Chris Kamphuis and Maudy Bijen; Koen Dercksen and Michelle Everard; George Gregoire; Larry Caruthers; Tim Hirschler; Emma Dahl; Truman Crandell; +%Friends: Pieter Wolfert (and Annerieke Wessels); Chris Kamphuis and Maudy Bijen; Koen Dercksen and Michelle Everard; George Gregoire; Larry Caruthers; Tim Hirschler; Emma Lindahl; Truman Crandell; %\selectlanguage{russian} %Александер Барков; %\selectlanguage{british} diff --git a/backmatter/curriculum_vitae.tex b/backmatter/curriculum_vitae.tex index 30524cd..9deaada 100644 --- a/backmatter/curriculum_vitae.tex +++ b/backmatter/curriculum_vitae.tex @@ -4,8 +4,7 @@ \ifSubfilesClassLoaded{ \pagenumbering{arabic} }{} -\chapter{Curriculum Vit\ae}% -\label{chp:curriculum_vitae} +\mybackmatter{chp:curriculum_vitae}{Curriculum Vit\ae}% Mart Lubbers \vspace{\baselineskip} diff --git a/backmatter/research_data_management.tex b/backmatter/research_data_management.tex index 430d5fb..bd48373 100644 --- a/backmatter/research_data_management.tex +++ b/backmatter/research_data_management.tex @@ -5,8 +5,7 @@ \pagenumbering{arabic} }{} -\chapter{Research Data Management}% -\label{chp:research_data_management} +\mybackmatter{chp:research_data_management}{Research Data Management}% This thesis research has been carried out under the research data management policy of the Institute for Computing and Information Science of Radboud University, the Netherlands\footnote{\url{https://www.ru.nl/icis/research-data-management/}, last accessed \formatdate{20}{1}{2020}.}. @@ -14,7 +13,7 @@ The following research datasets have been produced during this PhD research: \todo{reference correct chapters} \begin{itemize} \item \ldots - \item \rdmentry{Chapter 0} + \item \rdmentry{\Cref{chp:classy_deep_embedding}} {\mlubbers} {2022} {Literate Haskell/lhs2TeX source code for the paper ``Deep Embedding with Class'': TFP 2022} @@ -24,22 +23,22 @@ The following research datasets have been produced during this PhD research: {2021} {Source code for the interpreted mTask language} {DANS}{10.17026/dans-zrn-2wv3} %chktex 8 - \item \rdmentry{Chapter 0} + \item \rdmentry{\Cref{chp:smart_campus}} {\mlubbers; \pkoopman; Ramsingh, A.\ (University of Glasgow); Singer, dr.\ J.\ (University of Glasgow); Trinder, prof.~dr.\ P.\ (University of Glasgow)} {2021} {Source code of the PRSS and CWSS applications} {DANS}{10.17026/dans-zvf-4p9m} %chktex 8 - \item \rdmentry{Chapter 0} + \item \rdmentry{\Cref{prt:top}} {\mlubbers; \pkoopman; \rplasmeijer} {2020} {Source code for the multitasking mTask language integrated with the iTask system} {DANS}{10.17026/dans-x2y-rtxx} %chktex 8 - \item \rdmentry{Chapter 0} + \item \rdmentry{\Cref{prt:top}} {\mlubbers; \pkoopman; \rplasmeijer} {2020} {Source code for a simplified mTask language integrated with the iTask system} {DANS}{10.17026/dans-xv6-fvxd} %chktex 8 - \item \rdmentry{Chapter 0}% + \item \rdmentry{\Cref{prt:top}} {\mlubbers; \pkoopman; \rplasmeijer} {2020} {Source code for the mTask language} diff --git a/backmatter/samenvatting.tex b/backmatter/samenvatting.tex index 0c1ee31..d980132 100644 --- a/backmatter/samenvatting.tex +++ b/backmatter/samenvatting.tex @@ -5,8 +5,7 @@ \pagenumbering{arabic} }{} -\chapter{Samenvatting}% -\label{chp:samenvatting} +\mybackmatter{chp:samenvatting}{Samenvatting}% \selectlanguage{dutch} \begin{center} diff --git a/backmatter/summary.tex b/backmatter/summary.tex index 7e4f260..f96ac22 100644 --- a/backmatter/summary.tex +++ b/backmatter/summary.tex @@ -5,8 +5,7 @@ \pagenumbering{arabic} }{} -\chapter{Summary}% -\label{chp:summary} +\mybackmatter{chp:summary}{Summary}% \begin{center} \noindent% diff --git a/conclusion/conclusion.tex b/conclusion/conclusion.tex index ea20f10..0dd6005 100644 --- a/conclusion/conclusion.tex +++ b/conclusion/conclusion.tex @@ -5,8 +5,7 @@ \pagenumbering{arabic} }{} -\chapter{Coda}% -\label{chp:conclusion} +\mychapter{chp:conclusion}{Coda}% \input{subfilepostamble} \end{document} diff --git a/domain-specific_languages/class_deep_embedding.tex b/domain-specific_languages/class_deep_embedding.tex index 8c96393..cf9dc1d 100644 --- a/domain-specific_languages/class_deep_embedding.tex +++ b/domain-specific_languages/class_deep_embedding.tex @@ -5,8 +5,7 @@ \pagenumbering{arabic} }{} -\chapter{Deep embedding with class}% -\label{chp:classy_deep_embedding} +\mychapter{chp:classy_deep_embedding}{Deep embedding with class}% \begin{chapterabstract} The two flavours of DSL embedding are shallow and deep embedding. diff --git a/domain-specific_languages/dsl_techniques.tex b/domain-specific_languages/dsl_techniques.tex index e603d09..a843ccf 100644 --- a/domain-specific_languages/dsl_techniques.tex +++ b/domain-specific_languages/dsl_techniques.tex @@ -5,8 +5,7 @@ \pagenumbering{arabic} }{} -\chapter{DSL embedding techniques}% -\label{chp:dsl_embedding_techniques} +\mychapter{chp:dsl_embedding_techniques}{DSL embedding techniques}% An \gls{EDSL} is a language embedded in a host language created for a specific domain\todo{citation needed?}. \glspl{EDSL} can have one or more backends or views. Commonly used views are pretty printing, compiling, simulating, verifying and proving the program. diff --git a/domain-specific_languages/first-class_datatypes.tex b/domain-specific_languages/first-class_datatypes.tex index e897e00..7e277fb 100644 --- a/domain-specific_languages/first-class_datatypes.tex +++ b/domain-specific_languages/first-class_datatypes.tex @@ -5,8 +5,7 @@ \pagenumbering{arabic} }{} -\chapter{First-class datatypes \ldots}% -\label{chp:first-class_datatypes} +\mychapter{chp:first-class_datatypes}{First-class datatypes \ldots}% TFP22 \input{subfilepostamble} diff --git a/domain-specific_languages/strongly-typed_multi-view_stack-based_computations.tex b/domain-specific_languages/strongly-typed_multi-view_stack-based_computations.tex index 2e186dc..8ece8f8 100644 --- a/domain-specific_languages/strongly-typed_multi-view_stack-based_computations.tex +++ b/domain-specific_languages/strongly-typed_multi-view_stack-based_computations.tex @@ -5,8 +5,7 @@ \pagenumbering{arabic} }{} -\chapter{Strongly-Typed Multi-View Stack-Based Computations}% -\label{chp:strongly-typed_multi-view_stack-based_computations} +\mychapter{chp:strongly-typed_multi-view_stack-based_computations}{Strongly-Typed Multi-View Stack-Based Computations}% TFP22 \input{subfilepostamble} diff --git a/glossaries.tex b/glossaries.tex index 9922387..afe557e 100644 --- a/glossaries.tex +++ b/glossaries.tex @@ -1,37 +1,38 @@ % Acronyms \newacronym{ADT}{ADT}{algebraic data type} +\newacronym{API}{API}{application programming interface} +\newacronym{ARDSL}{ARDSL}{\gls{ARDUINO} \acrshort{DSL}} +\newacronym{BLE}{BLE}{Bluetooth low energy} +\newacronym{CRS}{PRS}{clean raspberry pi supersensor} +\newacronym{CWS}{PWS}{clean wemos supersensor} \newacronym{DSL}{DSL}{domain-specific language} \newacronym{EDSL}{eDSL}{embedded \acrshort{DSL}} +\newacronym{FP}{FP}{functional programming} \newacronym{GADT}{GADT}{generalised \acrshort{ADT}} \newacronym{GHC}{GHC}{Glasgow Haskell Compiler} +\newacronym{GPIO}{GPIO}{general-purpose \acrlong{IO}} \newacronym{GPL}{GPL}{general-purpose language} -\newacronym{PRS}{PRS}{python raspberry pi supersensor} -\newacronym{PWS}{PWS}{(micro)python wemos supersensor}%chktex 36 -\newacronym{CRS}{PRS}{clean raspberry pi supersensor} -\newacronym{CWS}{PWS}{clean wemos supersensor} -\newacronym{FP}{FP}{functional programming} \newacronym{GRS}{GRS}{graph rewriting system} -\newacronym{GPIO}{GPIO}{general-purpose \acrlong{IO}} \newacronym{GUI}{GUI}{graphical \acrlong{UI}} \newacronym{IOT}{IoT}{internet of things} +\newacronym{IO}{IO}{input/output} \newacronym{LEAN}{LEAN}{language of East-Anglia and Nijmegen} \newacronym{LED}{LED}{light-emitting diode} +\newacronym{MCU}{MCU}{microcontroller unit} +\newacronym{OS}{OS}{operating system} +\newacronym{OTA}{OTA}{over-the-air} +\newacronym{PRS}{PRS}{python raspberry pi supersensor} +\newacronym{PWS}{PWS}{(micro)python wemos supersensor}%chktex 36 +\newacronym{RAM}{RAM}{random-access memory} +\newacronym{RFID}{RFID}{radio-frequency identification} +\newacronym{RTOS}{RTOS}{real-time \acrshort{OS}} +\newacronym{SDS}{SDS}{shared data source} +\newacronym{SN}{SN}{sensor network} \newacronym{TOP}{TOP}{task-oriented programming} \newacronym{TOSD}{TOSD}{task-oriented software development} \newacronym{TRS}{TRS}{term rewriting system} -\newacronym{RFID}{RFID}{radio-frequency identification} -\newacronym{SN}{SN}{sensor network} -\newacronym{BLE}{BLE}{Bluetooth low energy} -\newacronym{API}{API}{application programming interface} -\newacronym{OS}{OS}{operating system} -\newacronym{IO}{IO}{input/output} -\newacronym{RTOS}{RTOS}{real-time \acrshort{OS}} -\newacronym{RAM}{RAM}{random-access memory} -\newacronym{OTA}{OTA}{over-the-air} -\newacronym{MCU}{MCU}{microcontroller unit} \newacronym{UI}{UI}{user interface} \newacronym{UOD}{UoD}{universe of discourse} -\newacronym{SDS}{SDS}{shared data source} % Glossaries \newglossaryentry{MTASK}{% @@ -70,3 +71,19 @@ name=I\textsuperscript{2}C, description={is a simple serial communication protocol often used to connect sensors to microprocessors} } +\newglossaryentry{TINYML}{ + name=TinyML, + description={is a deep learning framework for microprocessors} +} +\newglossaryentry{PYTHON}{ + name=Python, + description={is a multi-paradigm interpreted programming language} +} +\newglossaryentry{MICROPYTHON}{ + name=MicroPython, + description={is a \gls{PYTHON} implementation tailored for microprocessors} +} +\newglossaryentry{FREERTOS}{ + name=FreeRTOS, + description={is an open-source \gls{RTOS} for microprocessors} +} diff --git a/hyphenation.tex b/hyphenation.tex new file mode 100644 index 0000000..2c581e7 --- /dev/null +++ b/hyphenation.tex @@ -0,0 +1,9 @@ +\hyphenation{ + Has-kell + qua-si-quo-ter + qua-si-quo-ters + qua-si-quo-ta-tion + me-ta-pro-gram-ming + re-i-fi-ca-tion + pro-gram-mer +} diff --git a/introduction/introduction.tex b/introduction/introduction.tex index 384fe48..fd1c445 100644 --- a/introduction/introduction.tex +++ b/introduction/introduction.tex @@ -4,14 +4,13 @@ \ifSubfilesClassLoaded{ \pagenumbering{arabic} }{} -\chapter{Introduction}% +\mychapter{chp:introduction}{Introduction} %\setlength{\epigraphwidth}{.5\textwidth}% %\epigraphhead[30]{ % A \textbf{rhapsody} in music is a one-movement work that is episodic yet integrated, free-flowing in structure, featuring a range of highly contrasted moods, colour, and tonality. An air of spontaneous inspiration and a sense of improvisation make it freer in form than a set of variations. %}{% % Wikipedia~\cite{wikipedia_contributors_rhapsody_2022} %}% -\label{chp:introduction} The sheer number of connected devices around us is increasing exponentially. First and foremost, these devices are driven by software. This thesis is about \ldots diff --git a/mtask/.chktexrc b/mtask/.chktexrc new file mode 120000 index 0000000..98bff35 --- /dev/null +++ b/mtask/.chktexrc @@ -0,0 +1 @@ +../.chktexrc \ No newline at end of file diff --git a/mtask/beyond_microprocessors.tex b/mtask/beyond_microprocessors.tex index 467e1a0..4677fe9 100644 --- a/mtask/beyond_microprocessors.tex +++ b/mtask/beyond_microprocessors.tex @@ -5,7 +5,7 @@ \pagenumbering{arabic} }{} -\chapter{\texorpdfstring{\acrshort{TOP}}{TOP} for \texorpdfstring{\acrshort{IOT}}{IoT} beyond microprocessors} +\mychapter{chp:async_shares}{\texorpdfstring{\acrshort{TOP}}{TOP} for \texorpdfstring{\acrshort{IOT}}{IoT} beyond microprocessors} Async shares paper (parts of TIOT). \input{subfilepostamble} diff --git a/mtask/integration.tex b/mtask/integration.tex index 24b2818..547f38f 100644 --- a/mtask/integration.tex +++ b/mtask/integration.tex @@ -5,7 +5,7 @@ \pagenumbering{arabic} }{} -\chapter{Integrating mTask tasks with iTask} +\mychapter{chp:integrating_mtask}{Integrating mTask tasks with iTask} IFL18 paper \input{subfilepostamble} diff --git a/mtask/interpreting.tex b/mtask/interpreting.tex index 4836793..8011310 100644 --- a/mtask/interpreting.tex +++ b/mtask/interpreting.tex @@ -5,7 +5,7 @@ \pagenumbering{arabic} }{} -\chapter{Executing mTask tasks on microcontrollers} +\mychapter{chp:executing_mtask}{Executing mTask tasks on microcontrollers} IFL19 paper 4COWS paper diff --git a/mtask/mtask.tex b/mtask/mtask.tex index 7e54b3f..46aaeff 100644 --- a/mtask/mtask.tex +++ b/mtask/mtask.tex @@ -5,10 +5,12 @@ \pagenumbering{arabic} }{} -\chapter{\Gls{TOP} for the \gls{IOT}} +\mychapter{chp:top4iot}{Introduction to \gls{IOT} programming} +\todo{betere chapter naam} \begin{chapterabstract} This chapter introduces \gls{MTASK} and puts it into perspective compared to traditional microprocessor programming. \end{chapterabstract} + Traditionally, the first program that one writes when trying a new language is the so called \emph{Hello World!} program. This program has the single task of printing the text \emph{Hello World!} to the screen and exiting again, useful to become familiarised with the syntax and verify that the toolchain and runtime environment is working. On microprocessors, there often is no screen for displaying text. @@ -23,13 +25,13 @@ In between it waits for 500 milliseconds so that the blinking is actually visibl Compiling this results in a binary firmware that needs to be flashed onto the program memory. Translating the traditional blink program to \gls{MTASK} can almost be done by simply substituting some syntax as seen in \cref{lst:blinkImp}. -E.g.\ \cleaninline{digitalWrite} becomes \cleaninline{writeD}, literals are prefixed with \cleaninline{lit} and the pin to blink is changed to represent the actual pin for the builtin \gls{LED} of the device used in the exercises. +E.g.\ \arduinoinline{digitalWrite} becomes \cleaninline{writeD}, literals are prefixed with \cleaninline{lit} and the pin to blink is changed to represent the actual pin for the builtin \gls{LED} of the device used in the exercises. In contrast to the imperative \gls{CPP} dialect, \gls{MTASK} is a \gls{TOP} language and therefore there is no such thing as a loop, only task combinators to combine tasks. To simulate a loop, the \cleaninline{rpeat} task can be used, this task executes the argument task and, when stable, reinstates it. The body of the \cleaninline{rpeat} contains similarly named tasks to write to the pins and to wait in between. The tasks are connected using the sequential \cleaninline{>>|.} combinator that for all current intents and purposes executes the tasks after each other. -\begin{figure}[!ht] +\begin{figure}[ht] \begin{subfigure}[b]{.5\linewidth} \begin{lstArduino}[caption={Blink program.},label={lst:arduinoBlink}] void setup() { @@ -48,23 +50,100 @@ void loop() { blink :: Main (MTask v ()) | mtask v blink = - declarePin D4 PMOutput \d4-> + declarePin D2 PMOutput \d2-> {main = rpeat ( - writeD d4 true + writeD d2 true >>|. delay (lit 500) - >>|. writeD d4 false + >>|. writeD d2 false >>|. delay (lit 500) )}\end{lstClean} \end{subfigure} \end{figure} -\chapter{The \gls{MTASK} \gls{DSL}} +\section{Threaded blinking} +Now say that we want to blink multiple blinking patterns on different \glspl{LED} concurrently. +For example, blink three \glspl{LED} connected to \gls{GPIO} pins $1,2$ and $3$ at intervals of $500,300$ and $800$ milliseconds. +Intuitively you want to lift the blinking behaviour to a function and call this function three times with different parameters as done in \cref{lst:blinkthreadno} + +\begin{lstArduino}[caption={Naive approach to multiple blinking patterns.},label={lst:blinkthreadno}] +void setup () { ... } + +void blink (int pin, int wait) { + digitalWrite(pin, HIGH); + delay(wait); + digitalWrite(pin, LOW); + delay(wait); +} + +void loop() { + blink (1, 500); + blink (2, 300); + blink (3, 800); +}\end{lstArduino} + +Unfortunately, this does not work because the \arduinoinline{delay} function blocks all further execution. +The resulting program will blink the \glspl{LED} after each other instead of at the same time. +To overcome this, it is necessary to slice up the blinking behaviour in very small fragments so it can be manually interleaved~\cite{feijs_multi-tasking_2013}. +Listing~\ref{lst:blinkthread} shows how three different blinking patterns might be achieved in \gls{ARDUINO} using the slicing method. +If we want the blink function to be a separate parametrizable function we need to explicitly provide all references to the required state. +Furthermore, the \arduinoinline{delay} function can not be used and polling \arduinoinline{millis} is required. +The \arduinoinline{millis} function returns the number of milliseconds that have passed since the boot of the microprocessor. +Some devices use very little energy when in \arduinoinline{delay} or sleep state. +Resulting in \arduinoinline{millis} potentially affects power consumption since the processor is basically busy looping all the time. +In the simple case of blinking three \glspl{LED} on fixed intervals, it might be possible to calculate the delays in advance using static analysis and generate the appropriate \arduinoinline{delay} code. +Unfortunately, this is very hard when for example the blinking patterns are determined at runtime. + +\begin{lstArduino}[label={lst:blinkthread},caption={Threading three blinking patterns.}] +long led1 = 0, led2 = 0, led3 = 0; +bool st1 = false, st2 = false, st3 = false; + +void blink(int pin, int delay, long *lastrun, bool *st) { + if (millis() - *lastrun > delay) { + digitalWrite(pin, *st = !*st); + *lastrun += delay; + } +} + +void loop() { + blink(1, 500, &led1, &st1); + blink(2, 300, &led2, &st1); + blink(3, 800, &led3, &st1); +}\end{lstArduino} + +This method is very error prone, requires a lot of pointer juggling and generally results into spaghetti code. +Furthermore, it is very difficult to represent dependencies between threads, often state machines have to be explicitly programmed by hand to achieve this. + +\section{Blinking in \gls{MTASK}} +The \cleaninline{delay} \emph{task} does not block the execution but \emph{just} emits no value when the target waiting time has not yet passed and emits a stable value when the time is met. +In contrast, the \cleaninline{delay} \emph{function} on the \gls{ARDUINO} is blocking which prohibits interleaving. +To make code reuse possible and make the implementation more intuitive, the blinking behaviour is lifted to a recursive function instead of using the imperative \cleaninline{rpeat} construct. +The function is parametrized with the current state, the pin to blink and the waiting time. +Creating recursive functions like this is not possible in the \gls{ARDUINO} language because the program would run out of stack in an instant and nothing can be interleaved. +With a parallel combinator, tasks can be executed in an interleaved fashion. +Therefore, blinking three different blinking patterns is as simple as combining the three calls to the \cleaninline{blink} function with their arguments as seen in \cref{lst:blinkthreadmtask}. + +\begin{lstClean}[label={lst:blinkthreadmtask},caption={Threaded blinking.}] +blinktask :: MTask v () | mtask v +blinktask = + declarePin D1 PMOutput \d1-> + declarePin D2 PMOutput \d2-> + declarePin D3 PMOutput \d3-> + fun \blink=(\(st, pin, wait)-> + delay wait + >>|. writeD d13 st + >>|. blink (Not st, pin, wait)) In + {main = blink (true, d1, lit 500) + .||. blink (true, d2, lit 300) + .||. blink (true, d3, lit 800) + }\end{lstClean} + +\mychapter{chp:mtask_dsl}{The \gls{MTASK} \gls{DSL}} \begin{chapterabstract} This chapter serves as a complete guide to the \gls{MTASK} language, from an \gls{MTASK} programmer's perspective. \end{chapterabstract} The \gls{MTASK} system is a \gls{TOP} programming environment for programming microprocessors. -It is implemented as an \gls{EDSL} in \gls{CLEAN} using class-based---or tagless-final---embedding (See~\cref{ssec:tagless}). +It is implemented as an \gls{EDSL} in \gls{CLEAN} using class-based---or tagless-final---embedding (See \cref{ssec:tagless}). Due to the nature of the embedding technique, it is possible to have multiple interpretations of---or views on---programs written in the \gls{MTASK} language. \begin{itemize} @@ -101,7 +180,7 @@ The class constraints for values in \gls{MTASK} are omnipresent in all functions \cleaninline{Int} & \cinline{int16_t} & 16\\ \cleaninline{:: Long} & \cinline{int32_t} & 32\\ \cleaninline{Real} & \cinline{float} & 32\\ - \cleaninline{:: T = A | B | C} & \cinline{enum} & 16\\ + \cleaninline{:: T = A \| B \| C} & \cinline{enum} & 16\\ \bottomrule \end{tabular} \caption{Mapping from \gls{CLEAN}/\gls{MTASK} data types to \gls{CPP} datatypes.}% @@ -121,29 +200,31 @@ class basicType t | type t where ... class mtask v | expr, ..., int, real, long v someExpr :: v Int | mtask v -tempTask :: MTask v Bool | mtask, dht v +someExpr = ... + +someTask :: MTask v Int | mtask v +someTask = + sensor1 config1 \sns1-> + sensor2 config2 \sns2-> + fun \fun1= ( ... ) + In fun \fun2= ( ... ) + In {main=mainexpr} \end{lstClean} \section{Expressions} -\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}), to do basic arithmetics and conditional execution. +\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. For every common arithmetic operator in the host language, an \gls{MTASK} variant is present, suffixed by a period to not clash with \gls{CLEAN}'s builtin operators. \begin{lstClean}[caption={The \gls{MTASK} class for expressions},label={lst:expressions}] class expr v where lit :: t -> v t | type t (+.) infixl 6 :: (v t) (v t) -> v t | basicType, +, zero t - (-.) infixl 6 :: (v t) (v t) -> v t | basicType, -, zero t - (*.) infixl 7 :: (v t) (v t) -> v t | basicType, *, zero, one t - (/.) infixl 7 :: (v t) (v t) -> v t | basicType, /, zero t + ... (&.) infixr 3 :: (v Bool) (v Bool) -> v Bool (|.) infixr 2 :: (v Bool) (v Bool) -> v Bool Not :: (v Bool) -> v Bool (==.) infix 4 :: (v a) (v a) -> v Bool | Eq, basicType a - (!=.) infix 4 :: (v a) (v a) -> v Bool | Eq, basicType a - (<.) infix 4 :: (v a) (v a) -> v Bool | Ord, basicType a - (>.) infix 4 :: (v a) (v a) -> v Bool | Ord, basicType a - (<=.) infix 4 :: (v a) (v a) -> v Bool | Ord, basicType a - (>=.) infix 4 :: (v a) (v a) -> v Bool | Ord, basicType a + ... If :: (v Bool) (v t) (v t) -> v t | type t \end{lstClean} @@ -165,6 +246,7 @@ false :== lit False \end{lstClean} \subsection{Functions} +Functions in \gls{MTASK} are defined \section{Tasks} \subsection{Basic tasks} @@ -175,18 +257,59 @@ false :== lit False \subsubsection{Miscellaneous} \subsection{\glspl{SDS}} -\chapter{Green computing with \gls{MTASK}} +\mychapter{chp:green_computing_mtask}{Green computing with \gls{MTASK}} -\chapter{Integration with \gls{ITASK}} +\mychapter{chp:integration_with_itask}{Integration with \gls{ITASK}} \section{Devices} \section{Lift tasks} \section{Lift \glspl{SDS}} -\chapter{Implementation} +\mychapter{chp:implementation}{Implementation} IFL19 paper, bytecode instructieset~\cref{chp:bytecode_instruction_set} \section{Integration with \gls{ITASK}} IFL18 paper stukken +\chapter{\gls{MTASK} history} +\section{Generating \glsentrytext{C}/\glsentrytext{CPP} code} +A first throw at a class-based shallowly \gls{EDSL} for microprocessors was made by Pieter Koopman and Rinus Plasmijer in 2016~\cite{plasmeijer_shallow_2016}. +The language was called \gls{ARDSL} and offered a type safe interface to \gls{ARDUINO} \gls{CPP} dialect. +A \gls{CPP} code generation backend was available together with an \gls{ITASK} simulation backend. +There was no support for tasks or even functions. +Some time later in the 2015 CEFP summer school, an extended version was created that allowed the creation of imperative tasks, \glspl{SDS} and the usage of functions~\cite{koopman_type-safe_2019}. +The name then changed from \gls{ARDSL} to \gls{MTASK}. + +\section{Integration with \glsentrytext{ITASK}} +Mart Lubbers extended this in his Master's Thesis by adding integration with \gls{ITASK} and a bytecode compiler to the language~\cite{lubbers_task_2017}. +\Gls{SDS} in \gls{MTASK} could be accessed on the \gls{ITASK} server. +In this way, entire \gls{IOT} systems could be programmed from a single source. +However, this version used a simplified version of \gls{MTASK} without functions. +This was later improved upon by creating a simplified interface where \glspl{SDS} from \gls{ITASK} could be used in \gls{MTASK} and the other way around~\cite{lubbers_task_2018}. +It was shown by Matheus Amazonas Cabral de Andrade that it was possible to build real-life \gls{IOT} systems with this integration~\cite{amazonas_cabral_de_andrade_developing_2018}. +Moreover, a course on the \gls{MTASK} simulator was provided at the 2018 CEFP/3COWS winter school in Ko\v{s}ice, Slovakia~\cite{koopman_simulation_2018}. + +\section{Transition to \glsentrytext{TOP}} +The \gls{MTASK} language as it is now was introduced in 2018~\cite{koopman_task-based_2018}. +This paper updated the language to support functions, tasks and \glspl{SDS} but still compiled to \gls{CPP} \gls{ARDUINO} code. +Later the bytecode compiler and \gls{ITASK} integration was added to the language~\cite{lubbers_interpreting_2019}. +Moreover, it was shown that it is very intuitive to write \gls{MCU} applications in a \gls{TOP} language~\cite{lubbers_multitasking_2019}. +One reason for this is that a lot of design patterns that are difficult using standard means are for free in \gls{TOP} (e.g.\ multithreading). +In 2019, the CEFP summer school in Budapest, Hungary hosted a course on developing \gls{IOT} applications with \gls{MTASK} as well~\cite{lubbers_writing_2019}. + +\section{\glsentrytext{TOP}} +In 2022, the SusTrainable summer school in Rijeka, Croatia hosted a course on developing greener \gls{IOT} applications using \gls{MTASK} as well (the lecture notes are to be written). +Several students worked on extending \gls{MTASK} with many useful features: +Erin van der Veen did preliminary work on a green computer analysis, built a simulator and explored the possibilities for adding bounded datatypes~\cite{veen_van_der_mutable_2020}; Michel de Boer investigated the possibilities for secure communication channels~\cite{boer_de_secure_2020}; and Sjoerd Crooijmans added abstractions for low-power operation to \gls{MTASK} such as hardware interrupts and power efficient scheduling~\cite{crooijmans_reducing_2021}. +Elina Antonova defined a preliminary formal semantics for a subset of \gls{MTASK}~\cite{antonova_MTASK_2022}. +Moreover, plans for student projects and improvements include exploring integrating \gls{TINYML} into \gls{MTASK}; and adding intermittent computing support to \gls{MTASK}. + +In 2023, the SusTrainable summer school in Coimbra, Portugal will host a course on \gls{MTASK} as well. + +\section{\glsentrytext{MTASK} in practise} +Funded by the Radboud-Glasgow Collaboration Fund, collaborative work was executed with Phil Trinder, Jeremy Singer and Adrian Ravi Kishore Ramsingh. +An existing smart campus application was developed using \gls{MTASK} and quantitively and qualitatively compared to the original application that was developed using a traditional \gls{IOT} stack~\cite{lubbers_tiered_2020}. +The collaboration is still ongoing and a journal article is under review comparing four approaches for the edge layer: \gls{PYTHON}, \gls{MICROPYTHON}, \gls{ITASK} and \gls{MTASK}. +Furthermore, power efficiency behaviour of traditional versus \gls{TOP} \gls{IOT} stacks is being compared as well adding a \gls{FREERTOS} implementation to the mix as well + \input{subfilepostamble} \end{document} diff --git a/mtask/mtask_by_example.tex b/mtask/mtask_by_example.tex index 48d4590..c3d64ac 100644 --- a/mtask/mtask_by_example.tex +++ b/mtask/mtask_by_example.tex @@ -5,7 +5,7 @@ \pagenumbering{arabic} }{} -\chapter{mTask by example} +\mychapter{chp:mtask_by_example}{mTask by example} Hiermee beginnen, dan is het gelijk duidelijk hoe mTask werkt, dan zijn de volgende chapters implementatie dingen. CEFP19 lecture notes. Dit evt.\ ook gecombineerd met energy aware \gls{TOP} programming en CEFP22 lecture notes. diff --git a/other.bib b/other.bib index 4668fcb..46bff99 100644 --- a/other.bib +++ b/other.bib @@ -354,6 +354,30 @@ Publisher: Association for Computing Machinery}, file = {Gibbons - 2015 - Functional Programming for Domain-Specific Languag.pdf:/home/mrl/.local/share/zotero/storage/ARUBLFU6/Gibbons - 2015 - Functional Programming for Domain-Specific Languag.pdf:application/pdf}, } +@incollection{lubbers_writing_2019, + address = {Cham}, + title = {Writing {Internet} of {Things} applications with {Task} {Oriented} {Programming}}, + abstract = {The Internet of Things (IOT) is growing fast. In 2018, there was approximately one connected device per person on earth and the number has been growing ever since. The devices interact with the environment via different modalities at the same time using sensors and actuators making the programs parallel. Yet, writing this type of programs is difficult because the devices have little computation power and memory, the platforms are heterogeneous and the languages are low level. Task Oriented Programming (TOP) is a novel declarative programming language paradigm that is used to express coordination of work, collaboration of users and systems, the distribution of shared data and the human computer interaction. The mTask language is a specialized, yet full-fledged, multi-backend TOP language for IOT devices. With the bytecode interpretation backend and the integration with iTasks, tasks can be executed on the device dynamically. This means that —according to the current state of affairs— tasks can be tailor-made at run time, compiled to device-agnostic bytecode and shipped to the device for interpretation. Tasks sent to the device are fully integrated in iTasks to allow every form of interaction with the tasks such as observation of the task value and interaction with Shared Data Sources (SDSs). The application is —server and devices— are programmed in a single language, albeit using two embedded Domain Specific Languages (EDSLs).}, + language = {en}, + booktitle = {Central {European} {Functional} {Programming} {School}: 8th {Summer} {School}, {CEFP} 2019, {Budapest}, {Hungary}, {July} 17–21, 2019, {Revised} {Selected} {Papers}}, + publisher = {Springer International Publishing}, + author = {Lubbers, Mart and Koopman, Pieter and Plasmeijer, Rinus}, + year = {2019}, + pages = {51}, + file = {Lubbers - Writing Internet of Things applications with Task .pdf:/home/mrl/.local/share/zotero/storage/ILZIBYW5/Lubbers - Writing Internet of Things applications with Task .pdf:application/pdf}, +} + +@mastersthesis{veen_van_der_mutable_2020, + address = {Nijmegen}, + title = {Mutable {Collection} {Types} in {Shallow} {Embedded} {DSLs}}, + language = {en}, + school = {Radboud University}, + author = {Veen, van der, Erin}, + month = jun, + year = {2020}, + file = {thesis_final.pdf:/home/mrl/.local/share/zotero/storage/Y9QWGGB9/thesis_final.pdf:application/pdf}, +} + @phdthesis{alimarine_generic_2005, address = {Nijmegen}, type = {{PhD}}, @@ -365,6 +389,18 @@ Publisher: Association for Computing Machinery}, file = {Alimarine - Generic Functional Programming.pdf:/home/mrl/.local/share/zotero/storage/PDTS3SGX/Alimarine - Generic Functional Programming.pdf:application/pdf}, } +@phdthesis{boer_de_secure_2020, + address = {Nijmegen}, + type = {Bachelor's {Thesis}}, + title = {Secure {Communication} {Channels} for the {mTask} {System}.}, + language = {en}, + school = {Radboud University}, + author = {Boer, de, Michel}, + month = jun, + year = {2020}, + file = {Boer, de - 2020 - Secure Communication Channels for the mTask System.pdf:/home/mrl/.local/share/zotero/storage/C46E3FBF/Boer, de - 2020 - Secure Communication Channels for the mTask System.pdf:application/pdf}, +} + @inproceedings{barendregt_towards_1987, title = {Towards an intermediate language for graph rewriting}, volume = {1}, @@ -395,6 +431,17 @@ Publisher: Association for Computing Machinery}, file = {Stutterheim et al. - 2018 - Maintaining Separation of Concerns Through Task Or.pdf:/home/mrl/.local/share/zotero/storage/4GXJEM2U/Stutterheim et al. - 2018 - Maintaining Separation of Concerns Through Task Or.pdf:application/pdf}, } +@article{barendsen_uniqueness_1996, + title = {Uniqueness typing for functional languages with graph rewriting semantics}, + volume = {6}, + number = {6}, + journal = {Mathematical structures in computer science}, + author = {Barendsen, Erik and Smetsers, Sjaak}, + year = {1996}, + pages = {579--612}, + file = {Barendsen and Smetsers - 1996 - Uniqueness typing for functional languages with gr.pdf:/home/mrl/.local/share/zotero/storage/BPRC6KJK/Barendsen and Smetsers - 1996 - Uniqueness typing for functional languages with gr.pdf:application/pdf}, +} + @mastersthesis{bohm_asynchronous_2019, address = {Nijmegen}, title = {Asynchronous {Actions} in a {Synchronous} {World}}, @@ -442,6 +489,20 @@ few changes in existing programs.}, file = {Hentschel et al. - 2016 - Supersensors Raspberry Pi Devices for Smart Campu.pdf:/home/mrl/.local/share/zotero/storage/ATK53FN2/Hentschel et al. - 2016 - Supersensors Raspberry Pi Devices for Smart Campu.pdf:application/pdf}, } +@inproceedings{feijs_multi-tasking_2013, + address = {Wuxi, China}, + title = {Multi-tasking and {Arduino} : why and how?}, + isbn = {978-90-386-3462-3}, + abstract = {In this article I argue that it is important to develop experiential prototypes which have multi-tasking capabilities. At the same time I show that for embedded prototype software based on the popular Arduino platform this is not too difficult. The approach is explained and illustrated using technical examples – practical and hands-on, down to the code level. At the same time a few helpful notations for designing and documenting the software are introduced and illustrated by the same examples. Finally a few case studies of the technical approach are listed.}, + language = {English}, + booktitle = {Design and semantics of form and movement. 8th {International} {Conference} on {Design} and {Semantics} of {Form} and {Movement} ({DeSForM} 2013)}, + author = {Feijs, Loe}, + editor = {Chen, L. L. and Djajadiningrat, T. and Feijs, L. M. G. and Fraser, S. and Hu, J. and Kyffin, S. and Steffen, D.}, + year = {2013}, + pages = {119--127}, + file = {Feijs - 2013 - Multi-tasking and Arduino why and how.pdf:/home/mrl/.local/share/zotero/storage/8A3Q8LHA/Feijs - 2013 - Multi-tasking and Arduino why and how.pdf:application/pdf}, +} + @misc{achten_clean_2007, title = {Clean for {Haskell98} {Programmers}}, url = {https://www.mbsd.cs.ru.nl/publications/papers/2007/achp2007-CleanHaskellQuickGuide.pdf}, @@ -505,6 +566,22 @@ few changes in existing programs.}, file = {groj10-Haskell_front_end_Clean.pdf:/home/mrl/.local/share/zotero/storage/WVZWX8WT/groj10-Haskell_front_end_Clean.pdf:application/pdf}, } +@incollection{plasmeijer_shallow_2016, + address = {Cham}, + series = {Lecture {Notes} in {Computer} {Science}}, + title = {A {Shallow} {Embedded} {Type} {Safe} {Extendable} {DSL} for the {Arduino}}, + volume = {9547}, + isbn = {978-3-319-39109-0 978-3-319-39110-6}, + url = {http://link.springer.com/10.1007/978-3-319-39110-6}, + urldate = {2017-02-22}, + booktitle = {Trends in {Functional} {Programming}}, + publisher = {Springer International Publishing}, + author = {Plasmeijer, Rinus and Koopman, Pieter}, + year = {2016}, + doi = {10.1007/978-3-319-39110-6}, + file = {chp%3A10.1007%2F978-3-319-39110-6_6.pdf:/home/mrl/.local/share/zotero/storage/TJVP6FHF/chp%3A10.1007%2F978-3-319-39110-6_6.pdf:application/pdf}, +} + @inproceedings{cheney_lightweight_2002, title = {A lightweight implementation of generics and dynamics}, url = {http://dl.acm.org/citation.cfm?id=581698}, @@ -701,6 +778,17 @@ Publisher: Association for Computing Machinery}, file = {CARETTE et al. - 2009 - Finally tagless, partially evaluated Tagless stag.pdf:/home/mrl/.local/share/zotero/storage/T8C8VMHP/CARETTE et al. - 2009 - Finally tagless, partially evaluated Tagless stag.pdf:application/pdf}, } +@incollection{koopman_simulation_2018, + address = {Cham}, + title = {Simulation of a {Task}-{Based} {Embedded} {Domain} {Specific} {Language} for the {Internet} of {Things}}, + language = {en}, + booktitle = {Central {European} {Functional} {Programming} {School}: 7th {Summer} {School}, {CEFP} 2018, {Košice}, {Slovakia}, {January} 22–26, 2018, {Revised} {Selected} {Papers}}, + publisher = {Springer International Publishing}, + author = {Koopman, Pieter and Lubbers, Mart and Plasmeijer, Rinus}, + year = {2018}, + pages = {51}, +} + @techreport{plasmeijer_clean_2021, address = {Nijmegen}, title = {Clean {Language} {Report} version 3.1}, @@ -809,6 +897,22 @@ Publisher: Association for Computing Machinery}, pages = {36--43}, } +@incollection{koopman_type-safe_2019, + address = {Cham}, + title = {Type-{Safe} {Functions} and {Tasks} in a {Shallow} {Embedded} {DSL} for {Microprocessors}}, + isbn = {978-3-030-28346-9}, + url = {https://doi.org/10.1007/978-3-030-28346-9_8}, + abstract = {The Internet of Things, IoT, brings us large amounts of connected computing devices that are equipped with dedicated sensors and actuators. These computing devices are typically driven by a cheap microprocessor system with a relatively slow processor and a very limited amount of memory. Due to the special input-output capabilities of IoT devices and their connections it is very attractive to execute (parts of) programs on these microcomputers.}, + booktitle = {Central {European} {Functional} {Programming} {School}: 6th {Summer} {School}, {CEFP} 2015, {Budapest}, {Hungary}, {July} 6–10, 2015, {Revised} {Selected} {Papers}}, + publisher = {Springer International Publishing}, + author = {Koopman, Pieter and Plasmeijer, Rinus}, + editor = {Zsók, Viktória and Porkoláb, Zoltán and Horváth, Zoltán}, + year = {2019}, + doi = {10.1007/978-3-030-28346-9_8}, + pages = {283--340}, + file = {Koopman and Plasmeijer - 2019 - Type-Safe Functions and Tasks in a Shallow Embedde.pdf:/home/mrl/.local/share/zotero/storage/UY2DY4EJ/Koopman and Plasmeijer - 2019 - Type-Safe Functions and Tasks in a Shallow Embedde.pdf:application/pdf}, +} + @techreport{cheney_first-class_2003, title = {First-class phantom types}, url = {https://ecommons.cornell.edu/handle/1813/5614}, @@ -854,6 +958,17 @@ Publisher: Association for Computing Machinery}, file = {Hinze and Jeuring - Generic Haskell practice and theory.pdf:/home/mrl/.local/share/zotero/storage/QDRNI5VB/Hinze and Jeuring - Generic Haskell practice and theory.pdf:application/pdf}, } +@phdthesis{antonova_mtask_2022, + address = {Nijmegen}, + type = {Bachelor's {Thesis}}, + title = {{mTask} {Semantics} and its {Comparison} to {TopHat}}, + language = {en}, + school = {Radboud University}, + author = {Antonova, Elina}, + year = {2022}, + file = {Crooijmans - 2021 - Reducing the Power Consumption of IoT Devices in T.pdf:/home/mrl/.local/share/zotero/storage/YIEQ97KK/Crooijmans - 2021 - Reducing the Power Consumption of IoT Devices in T.pdf:application/pdf}, +} + @misc{wadler_expression_1998, title = {The expression problem}, url = {https://homepages.inf.ed.ac.uk/wadler/papers/expression/expression.txt}, @@ -885,16 +1000,6 @@ Publisher: Association for Computing Machinery}, year = {2022}, note = {accessed on: 2022-09-06}, } -@article{barendsen_uniqueness_1996, - title = {Uniqueness typing for functional languages with graph rewriting semantics}, - volume = {6}, - number = {6}, - journal = {Mathematical structures in computer science}, - author = {Barendsen, Erik and Smetsers, Sjaak}, - year = {1996}, - pages = {579--612}, - file = {Barendsen and Smetsers - 1996 - Uniqueness typing for functional languages with gr.pdf:/home/mrl/.local/share/zotero/storage/BPRC6KJK/Barendsen and Smetsers - 1996 - Uniqueness typing for functional languages with gr.pdf:application/pdf}, -} @incollection{backus_introduction_1990, address = {USA}, @@ -907,18 +1012,6 @@ Publisher: Association for Computing Machinery}, pages = {219--247}, } -@article{achten_ins_1995, - title = {The ins and outs of {Clean} {I}/{O}}, - volume = {5}, - doi = {10.1017/S0956796800001258}, - number = {1}, - journal = {Journal of Functional Programming}, - author = {Achten, Peter and Plasmeijer, Rinus}, - year = {1995}, - note = {Publisher: Cambridge University Press}, - pages = {81--110}, -} - @inproceedings{peyton_jones_imperative_1993, address = {New York, NY, USA}, series = {{POPL} '93}, @@ -935,17 +1028,3 @@ Publisher: Association for Computing Machinery}, pages = {71--84}, file = {Peyton Jones and Wadler - 1993 - Imperative Functional Programming.pdf:/home/mrl/.local/share/zotero/storage/9DQ5V3N3/Peyton Jones and Wadler - 1993 - Imperative Functional Programming.pdf:application/pdf}, } - -@inproceedings{achten_high_1993, - address = {London}, - title = {High {Level} {Specification} of {I}/{O} in {Functional} {Languages}}, - isbn = {978-1-4471-3215-8}, - abstract = {The interface with the outside world has always been one of the weakest points of functional languages. It is not easy to incorporate I/O without being allowed to do side-effects. Furthermore, functional languages allow redexes to be evaluated in any order while I/O generally has to be performed in a very specific order. In this paper we present a new solution for the I/O problem which we have incorporated in the language Concurrent Clean. Concurrent Clean offers a linear type system called Unique Types. It makes it possible to define functions with side-effects without violating the functional semantics. Now it is possible to change any object in the world in the way we wanted: e.g. arrays can be updated in-situ, arbitrary file manipulation is possible. We have used this powerful tool among others to create a library for window based I/O. Using an explicit environment passing scheme provides a high-level and elegant functional specification method for I/O, called Event I/O. Now the specification of I/O has become one of the strengths of functional languages: interactive programs written in Concurrent Clean are concise, easy to write and comprehend as well as efficient. The presented solution can in principle be applied for any other functional language as well provided that it actually uses graph rewriting semantics in the implementation.}, - booktitle = {Functional {Programming}, {Glasgow} 1992}, - publisher = {Springer London}, - author = {Achten, Peter and van Groningen, John and Plasmeijer, Rinus}, - editor = {Launchbury, John and Sansom, Patrick}, - year = {1993}, - pages = {1--17}, - file = {Achten et al. - 1993 - High Level Specification of IO in Functional Lang.pdf:/home/mrl/.local/share/zotero/storage/4QVH7AYC/Achten et al. - 1993 - High Level Specification of IO in Functional Lang.pdf:application/pdf}, -} diff --git a/preamble.tex b/preamble.tex index 6c3ec94..9efb9df 100644 --- a/preamble.tex +++ b/preamble.tex @@ -9,11 +9,14 @@ \usepackage{titlecaps} % titlecase commands \usepackage{amsmath} % extra math \usepackage{amssymb} % extra math symbols +\usepackage{relsize} % \smaller command +\usepackage{atveryend} % \smaller command \everymath{\it\/} \DeclareMathSymbol{\shortminus}{\mathbin}{AMSa}{"39} %chktex 18 % Internationalisation \usepackage[dutch,russian,british]{babel} +\input{hyphenation} %\babelfont[russian]{rm}{Liberation Serif} % Papersize and layout @@ -28,22 +31,67 @@ paperwidth=17cm, paperheight=24cm, } -\usepackage[ - height={1.5cm}, - width={12mm}, - distance={1.55cm}, - topthumbmargin={auto}, - bottomthumbmargin={auto}, - eventxtindent={.5cm}, - oddtxtexdent={.3cm}]{thumbs} % thumb marks +\usepackage{float} \usepackage{fancyhdr} % Custom headers and footers -%\pagestyle{fancy} -\pagestyle{headings} +%\pagestyle{headings} +\pagestyle{fancy} +\fancyhead{} +\fancyfoot{} +\setlength{\unitlength}{18mm} +\newcommand{\blob}{\rule[-.2\unitlength]{2\unitlength}{.5\unitlength}} +\fancyhead[RE]{\rightmark} +\fancyhead[LO]{\leftmark} +\newcommand{\frontmatterfancy}[0]{ + \fancyhead[RO]{\thepage} + \fancyhead[LE]{\thepage} +} +\newcommand{\mainmatterfancy}[0]{ + \fancyhead[RO]{ + \thepage% + \begin{picture}(0,0) + \put(1,-\value{chapter}){\blob} + \end{picture} + } + \fancyhead[LE]{ + \begin{picture}(0,0) + \put(-3,-\value{chapter}){\blob} + \end{picture}% + \thepage% + } +} +\newcommand{\backmatterfancy}[0]{ + \fancyhead[RO]{ + \thepage% + \begin{picture}(0,0) + \put(1,-1){\blob} + \end{picture} + } + \fancyhead[LE]{ + \begin{picture}(0,0) + \put(-3,-1){\blob} + \end{picture}% + \thepage% + } +} +\renewcommand{\chaptermark}[1]{\markboth{\chaptername\ \thechapter.\ #1}{}} +\renewcommand{\sectionmark}[1]{\markright{\thesection.\ #1}} +%\renewcommand{\chaptermark}[1]{\markboth{\MakeUppercase{\chaptername}\ \thechapter.\ #1}{}} +%\renewcommand{\headrulewidth}{0pt} +\renewcommand{\footrulewidth}{0pt} \usepackage{etoolbox} % To patch the chapter command % Have better page numbering in chapters \patchcmd{\chapter}{plain}{headings}{}{} \usepackage{epigraph} % Epigraph \renewcommand\partname{Movement} % Rename parts to movements (rhapsody uhu) +\addto\captionsbritish{\renewcommand{\partname}{Movement}} +\usepackage{titlesec} +\makeatletter +\titleformat{\part}[block] + {\Huge} + {\partname~\thepart:} + {20pt} + {} + \newenvironment{chapterabstract} {\begin{quote}} {\end{quote}} @@ -196,8 +244,8 @@ } % Index -\usepackage{makeidx} -\makeindex% Enable the index +%\usepackage{makeidx} +%\makeindex% Enable the index % Custom enumerations \usepackage[inline,shortlabels]{enumitem} @@ -223,3 +271,17 @@ \newcommand{\mlubbers}{Lubbers, M.\ (Radboud University)} \newcommand{\pkoopman}{Koopman, dr.\ P.\ (Radboud University)} \newcommand{\rplasmeijer}{Plasmeijer, prof.\ dr.\ ir.\ R.\ (Radboud University)} + +\newcommand{\mychapter}[2]{ + \chapter{#2}% + \label{#1}% +} +\newcommand{\myappendix}[2]{ + \chapter{#2}% + \label{#1}% +} +\newcommand{\mybackmatter}[2]{ + \chapter{#2}% + \label{#1}% +} +\newcommand{\mypart}[3]{\part[#2: #3]{#2\\[2ex]\smaller{}#3}\label{#1}} diff --git a/subfilepostamble.tex b/subfilepostamble.tex index e44f9e6..e944d9e 100644 --- a/subfilepostamble.tex +++ b/subfilepostamble.tex @@ -1,5 +1,6 @@ \ifSubfilesClassLoaded{% \bibliography{../other,../self} + \printglossaries% }{ } diff --git a/thesis.tex b/thesis.tex index 4949745..8ddbe1f 100644 --- a/thesis.tex +++ b/thesis.tex @@ -28,7 +28,7 @@ \selectlanguage{british} \frontmatter% -%\addtitlethumb{Frontmatter}{}{white}{gray}{pagesLTS.0} +\frontmatterfancy% %Titlepage \subfile{frontmatter/titlepage} @@ -53,15 +53,14 @@ % The actual document \mainmatter% -\addthumb{Chapters}{\arabic{chapter}}{white}{gray} % Arabic chapter thumbs +\mainmatterfancy% \setcounter{chapter}{-1} % Introduction \subfile{introduction/introduction} % DSL -\part[Prelude: Domain-Specific Languages]{Prelude\\Domain-Specific Languages}% -\label{prt:dsl} +\mypart{prt:dsl}{Prelude}{Domain-Specific Languages}% % DSL Techniques \subfile{domain-specific_languages/dsl_techniques} @@ -75,13 +74,11 @@ % Stack computations? \subfile{domain-specific_languages/strongly-typed_multi-view_stack-based_computations} -\part[Exposition: Task-Oriented Internet of Things Programming]{Exposition\\Task-Oriented Internet of Things Programming}% -\label{prt:top} +\mypart{prt:top}{Exposition}{Task-Oriented Programming for the Internet of Things}% \subfile{mtask/mtask} -\part[Transformation: Tiered vs.\ tierless programming]{Transformation\\Tiered vs.\ tierless programming}% -\label{prt:tvt} +\mypart{prt:tvt}{Transformation}{Tiered vs.\ tierless programming}% \subfile{tiered_vs._tierless_programming/smart_campus} @@ -93,14 +90,13 @@ \appendix% \label{chp:appendix} \addcontentsline{toc}{part}{Appendix} -\addthumb{Appendices}{\Alph{chapter}}{white}{gray} % Alpha appendix thumbs \subfile{appendix/clean_for_haskell_programmers} \subfile{appendix/bytecode} \backmatter% +\backmatterfancy% \bookmarksetup{startatroot} % descend back out of the appendix -\addtitlethumb{Backmatter}{}{white}{gray}{pagesLTS.0} % Empty backmatter thumbs % Bibliography \phantomsection{}% @@ -143,8 +139,8 @@ \endgroup % Index -\addcontentsline{toc}{chapter}{Index}% -\label{chp:index} -\printindex +%\addcontentsline{toc}{chapter}{Index}% +%\label{chp:index} +%\printindex \end{document} diff --git a/tiered_vs._tierless_programming/smart_campus.tex b/tiered_vs._tierless_programming/smart_campus.tex index ce6405e..e422e1e 100644 --- a/tiered_vs._tierless_programming/smart_campus.tex +++ b/tiered_vs._tierless_programming/smart_campus.tex @@ -5,7 +5,7 @@ \pagenumbering{arabic} }{} -\chapter{Smart campus application} +\mychapter{chp:smart_campus}{Smart campus application} IOT2020/TIOT papers \input{subfilepostamble} -- 2.20.1