updates
authorMart Lubbers <mart@martlubbers.net>
Wed, 15 Feb 2023 18:57:21 +0000 (19:57 +0100)
committerMart Lubbers <mart@martlubbers.net>
Wed, 15 Feb 2023 18:57:21 +0000 (19:57 +0100)
21 files changed:
appx/bytecode.tex
asbook.tex
back/acknowledgements.tex
back/curriculum_vitae.tex
back/research_data_management.tex
back/samenvatting.tex
back/summary.tex
bib/self.bib
check.txt [new file with mode: 0644]
dsl/class.tex
dsl/first.tex
latexmkrc
preamble/commands.tex
preamble/glossaries.tex
top/4iot.tex
top/blinktree.tex
top/contexttree1.tex [new file with mode: 0644]
top/contexttree2.tex [new file with mode: 0644]
top/finale.tex
top/imp.tex
tvt/tvt.tex

index 12e1c82..532f44b 100644 (file)
@@ -2,7 +2,6 @@
 
 \input{subfilepreamble}
 
-
 \begin{document}
 \input{subfileprefix}
 \ifSubfilesClassLoaded{\appendix\setcounter{chapter}{2}}{}
@@ -37,12 +36,12 @@ The byte code instructions are of variable length and automatically encoded and
 
 \begin{landscape}
        \begin{longtable}[c]{lllll}
-               \caption{Semantics for the bytecode instructions\label{tbl:instr_task}}\\
+               \caption{Semantics for the bytecode instructions.\label{tbl:instr_task}}\\
                \toprule
                Instruction & Arguments & Semantics & $sp$ & $pc$\\
                \midrule
                \endfirsthead%
-               \caption{Semantics for the bytecode instructions (cont.)}\\
+               \caption{Semantics for the bytecode instructions. (continued)}\\
                \toprule
                Instruction & Arguments & Semantics & $sp$ & $pc$\\
                \midrule
index 834b3e8..dfd39d1 100644 (file)
@@ -4,7 +4,7 @@
 \usepackage{pdfpages}
 
 \begin{document}
-\includepdf[landscape,booklet,pages={1-22}]{thesis.pdf}%chktex 29 chktex 8
+\includepdf[landscape,booklet,pages={3-18}]{top/imp.pdf}%chktex 29 chktex 8
 %\includepdf[landscape,booklet,pages={69-142}]{thesis.pdf}%chktex 29 chktex 8
 %\includepdf[landscape,booklet,pages={143-184}]{thesis.pdf}%chktex 29 chktex 8
 %\includepdf[landscape,booklet,pages={185-}]{thesis.pdf}%chktex 29 chktex 8
index 0fd46fe..f5a0f20 100644 (file)
@@ -7,7 +7,6 @@
 \ifSubfilesClassLoaded{\chapter*{Acknowledgements}}{\chapter{Acknowledgements}}%
 \label{chp:acknowledgements}
 %\begin{center}
-\noindent%
 While the research and writing carried out for this thesis was mostly done by me, it could not have been done without the support of many others.
 
 First of all I would like to thank Rinus Plasmeijer, Pieter Koopman, and Jan Martin Jansen for the supervision, I learned a lot from you, not only regarding academia but in many other aspects of life as well.
index 23977d4..8098844 100644 (file)
@@ -14,13 +14,13 @@ Mart Lubbers
 \begin{tabular}{rp{.75\linewidth}}
        1992         & Born May 27th, Oldenzaal\\
        2004{--}2011 & VWO at the Twents Carmelcollege De Thij, Oldenzaal\\
-       2011{--}2015 & Bachelor's Degree Artificial Intelligence at the Radboud University, Nijmegen\\
-       2013{--}2015 & Research Assistant at the Max Planck Institute for Psycholinguistics\\
-       2015{--}2017 & Master's Degree (cum laude) Computing Science (Software Science track) at the Radboud University, Nijmegen\\
+       2011{--}2015 & Bachelor's degree Artificial Intelligence at the Radboud University, Nijmegen\\
+       2013{--}2015 & Research assistant at the Max Planck Institute for Psycholinguistics\\
+       2015{--}2017 & Master's degree (cum laude) Computing Science (Software Science track) at the Radboud University, Nijmegen\\
        2015{--}2017 & Entrepeneur as IT Lubbers, Nijmegen\\
        2017         & Researcher at the Netherlands Defense Academy, Den Helder in the faculty of Military Sciences (fMIL).\\
-       2018         & Researcher at the Radboud University, Nijmegen in the Institute for Computing and Information Sciences (iCIS).\\
-       2018{--}2023 & PhD Candidate at the Radboud University, Nijmegen in the Institute for Computing and Information Sciences (iCIS).
+       2018         & Junior researcher at the Radboud University, Nijmegen in the Institute for Computing and Information Sciences (iCIS).\\
+       2018{--}2023 & PhD candidate at the Radboud University, Nijmegen in the Institute for Computing and Information Sciences (iCIS).
 \end{tabular}
 
 \input{subfilepostamble}
index 9f5c7f7..4d241d8 100644 (file)
@@ -25,38 +25,43 @@ The following research datasets have been produced during this PhD research:
                \end{itemize}
        \item \Fullref{chp:first-class_datatypes}:
                \begin{itemize}
-                       \item \rdmentry{\mlubbers}{2022}
+                       \item \rdmentry{\mlubbers; \& \pkoopman}{2022}
                                {Code for the paper ``First-Class Data Types in Shallow Embedded Domain-Specific Languages using Metaprogramming'': IFL 2022}
                                {Zenodo}{10.5281/zenodo.6416747}
                \end{itemize}
-       \item \crtCref{prt:top}: \hspace{8.28992pt}\nameref{prt:top}:%
-                       \todo{add set for sum\-mer scho\-ol?}%
+       \item \Fullref{prt:top}:
                \begin{itemize}
-                       \item \rdmentry{Crooijmans, S.\ (Radboud University); \mlubbers; \pkoopman}{2023}
-                               {Code for the paper ``Reducing the Power Consumption of IoT with Task-Oriented Programming'': TFP 2022}
-                               {Zenodo}{10.5281/zenodo.7634538} %chktex 8
-                       \item \rdmentry{\mlubbers; \pkoopman; \rplasmeijer}{2020}
+                       \item \rdmentry{\mlubbers; \pkoopman; \& \rplasmeijer}{2020}
                                {Source code for the mTask language}
                                {DANS}{10.17026/dans-xx4-8zs9} %chktex 8
-                       \item \rdmentry{\mlubbers; \pkoopman; \rplasmeijer}{2020}
+                       \item \rdmentry{\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{\mlubbers; \pkoopman; \rplasmeijer}{2020}
+                       \item \rdmentry{\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{\mlubbers; \pkoopman; \rplasmeijer}{2021}
+                       \item \rdmentry{\mlubbers; \pkoopman; \& \rplasmeijer}{2021}
                                {Source code for the interpreted mTask language}
                                {DANS}{10.17026/dans-zrn-2wv3} %chktex 8
+                       \item \rdmentry{Crooijmans, S.\ (Radboud University); \mlubbers; \& \pkoopman}{2023}
+                               {Code for the paper ``Reducing the Power Consumption of IoT with Task-Oriented Programming'': TFP 2022}
+                               {Zenodo}{10.5281/zenodo.7634538}
+                       \item \rdmentry{\mlubbers; \& \pkoopman; \rplasmeijer}{2023}
+                               {Code for the lecture notes: ``Writing Internet of Things Applications with Task Oriented Programming''}
+                               {Zenodo}{10.5281/zenodo.7643284}
+                       \item \rdmentry{\mlubbers; \& \pkoopman}{2023}
+                               {Code for the lecture notes: ``Green Computing for the Internet of Things''}
+                               {Zenodo}{10.5281/zenodo.7643316}
                \end{itemize}
        \item \Fullref{prt:tvt}:
                \begin{itemize}
-                       \item \rdmentry{\mlubbers; \pkoopman; \aramsingh; \jsinger; \ptrinder}{2021}
+                       \item \rdmentry{\mlubbers; \pkoopman; \aramsingh; \jsinger; \& \ptrinder}{2021}
                                {Source code, line counts and memory statistics for CRS, CWS, CRTS and CWTS}
                                {Zenodo}{10.5281/zenodo.5040754}
-                       \item \rdmentry{\mlubbers; \pkoopman; \aramsingh; \jsinger; \ptrinder}{2021}
+                       \item \rdmentry{\mlubbers; \pkoopman; \aramsingh; \jsinger; \& \ptrinder}{2021}
                                {Source code, line counts and memory stats for PRS, PWS, PRT and PWT}
                                {Zenodo}{10.5281/zenodo.5081386}
-                       \item \rdmentry{\mlubbers; \pkoopman; \aramsingh; \jsinger; \ptrinder}{2021}
+                       \item \rdmentry{\mlubbers; \pkoopman; \aramsingh; \jsinger; \& \ptrinder}{2021}
                                {Source code of the PRSS and CWSS applications}
                                {DANS}{10.17026/dans-zvf-4p9m} %chktex 8
                \end{itemize}
index ae94658..b1db2c7 100644 (file)
@@ -7,8 +7,6 @@
 \selectlanguage{dutch}
 \ifSubfilesClassLoaded{\chapter*{Samenvatting}}{\chapter{Samenvatting}}%
 \label{chp:samenvatting}
-%\begin{center}
-%\noindent%
 Het aantal computers om ons heen groeit enorm en hiermee ook de complexiteit van de systemen waarin ze zich bevinden.
 Veel van deze computers zijn \emph{randcomputers} die onderdeel zijn van het Internet of Things (IoT).
 Binnen deze orkesten interacteren randcomputers met de buitenwereld door sensoren en actuatoren.
@@ -36,7 +34,6 @@ Dit stuurprogramma voert de ontvangen taken energiezuinig uit en automatiseert t
 Alle aspecten van het mTask-systeem worden beschreven: voorbeeldprogramma's, taalontwerp, implementatiedetails, integratie met iTask en de energiezuinige functionaliteit.
 Indien samen met iTask gebruikt, kan een geheel IoT-systeem laagloos geprogrammeerd worden, gebruik makend van \'e\'en broncode, programmeertaal en paradigma, abstractieniveau en typesysteem.
 Eveneens wordt de semantische wrijving, onderhouds- en robuustheidsproblematiek en moeizame onderlinge samenwerking verzacht.
-%\end{center}
 \input{subfilepostamble}
 \selectlanguage{british}
 \end{document}
index 3fbb2a5..3713f33 100644 (file)
@@ -7,8 +7,6 @@
 \ifSubfilesClassLoaded{\chapter*{Summary}}{\chapter{Summary}}%
 \label{chp:summary}%
 \glsresetall%
-%\begin{center}
-%\noindent%
 The number of computers around us is growing exponentially, compounding the complexity of the systems in which they operate.
 Many of these computers are \emph{edge devices} operating in \gls{IOT} systems.
 Within these orchestrations of computers, they interact with the environment using sensors and actuators.
@@ -39,5 +37,4 @@ All aspects of the \gls{MTASK} system are shown: example applications, language
 When using \gls{MTASK} in conjunction with \gls{ITASK}, entire \gls{IOT} systems are programmed tierlessly from a single source, language, paradigm, high abstraction level, and type system.
 Many problems such as semantic friction; maintainability and robustness issues; and interoperation safety are mitigated when using tierless programming.
 %This is a summary of 350--400 words.
-%\end{center}
 \end{document}
index a2f169d..b5ca3c5 100644 (file)
@@ -19,7 +19,7 @@
 @incollection{lubbers_writing_2023,
        address = {Cham},
        series = {Lecture {Notes} in {Computer} {Science}},
-       title = {Writing {Internet} of {Things} applications with {Task} {Oriented} {Programming}},
+       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},
        number = {11950},
diff --git a/check.txt b/check.txt
new file mode 100644 (file)
index 0000000..b65dd16
--- /dev/null
+++ b/check.txt
@@ -0,0 +1,4 @@
+undefined references
+overfull hboxes
+windows
+orphans
index 89cf263..3b06443 100644 (file)
@@ -178,7 +178,7 @@ instance Sub_t Printer_t where
        sub_t (P_t e1) (P_t e2) = P_t ("(" ++ e1 ++ "-" ++ e2 ++ ")")
 \end{lstHaskellLhstex}
 
-\section{Lifting the backends}%
+\section{Lifting the interpretations}%
 Let us rethink the deeply embedded \gls{DSL} design.
 Remember that in shallow embedding, the semantics are embedded in the language construct functions.
 Obtaining extensibility both in constructs and semantics was accomplished by abstracting the semantics functions to type classes, making the constructs overloaded in the semantics.
@@ -761,7 +761,7 @@ The first type variable (\haskelllhstexinline{dt}) is the type or type construct
 This means that when \haskelllhstexinline{Cons} is pattern matched, the overloading of the type class constraint for \haskelllhstexinline{c dt} can be solved by the compiler.
 \GHCmod{KindSignatures} is used to force the kinds of the type parameters and the kind of \haskelllhstexinline{dt} is polymorphic (\GHCmod{PolyKinds}) so that the \haskelllhstexinline{Record} data type can be used for \glspl{DSL} using type classes but also type constructor classes (e.g.\ when using \glspl{GADT}).
 
-\begin{lstHaskellLhstex}[label={lst_cbde:record_type},caption={Data type for a list of constraints}]
+\begin{lstHaskellLhstex}[label={lst_cbde:record_type},caption={Data type for a list of constraints.}]
 data Record (dt :: k) (clist :: [k -> Constraint]) where
        Nil  :: Record dt '[]
        Cons :: c dt => Record dt cs -> Record dt (c ': cs)
@@ -769,7 +769,7 @@ data Record (dt :: k) (clist :: [k -> Constraint]) where
 
 To incorporate this type in the \haskelllhstexinline{Expr} type, the \haskelllhstexinline{Ext} constructor changes from containing a single witness dictionary to a \haskelllhstexinline{Record} type containing all the required dictionaries.
 
-\begin{lstHaskellLhstex}[caption={Data type for a list of constraints}]
+\begin{lstHaskellLhstex}[caption={Main data type with extension constructor.}]
 data Expr c
        = Lit Int
        | Add (Expr c) (Expr c)
@@ -779,7 +779,7 @@ data Expr c
 Furthermore, we define a type class (\haskelllhstexinline{In}) that allows us to extract explicit dictionaries \haskelllhstexinline{Dict} from these records if the constraint can is present in the list.
 Since the constraints become available as soon as the \haskelllhstexinline{Cons} constructor is matched, the implementation is a type-level list traversal.
 
-\begin{lstHaskellLhstex}[caption={Membership functions for constraints}]
+\begin{lstHaskellLhstex}[caption={Membership functions for constraints.}]
 class c `In` cs where
        project :: Record dt cs -> Dict (c dt)
 instance {-# OVERLAPPING #-} c `In` (c ': cs) where
@@ -792,7 +792,7 @@ The final scaffolding is a multi-parameter type class \haskelllhstexinline{Creat
 This type class creates a record structure cons by cons if and only if all type class constraints are available in the list of constraints.
 It is not required to provide instances for this for specific records or type classes, the two instances describe all the required constraints.
 
-\begin{lstHaskellLhstex}[caption={Membership functions for constraints}]
+\begin{lstHaskellLhstex}[caption={Functions for creating the witness records.}]
 class CreateRecord dt c where
        createRecord :: Record dt c
 instance CreateRecord d '[] where
@@ -894,7 +894,7 @@ data Eq_g d a  where
        EqLoop_g  ::                       Expr_g d a -> Eq_g d a
 \end{lstHaskellLhstex}
 
-\begin{lstHaskellLhstex}[caption={Smart constructions.}]
+\begin{lstHaskellLhstex}[caption={Smart constructors.}]
 sub_g :: (Typeable d, GDict (d (Sub_g d)), Eq a, Num a) =>
        Expr_g d a -> Expr_g d a -> Expr_g d a
 sub_g e1 e2 = Ext_g gdict (Sub_g e1 e2)
@@ -922,14 +922,14 @@ instance HasOpt_g OptDict_g where
        getOpt_g (OptDict_g e) = e
 \end{lstHaskellLhstex}
 
-\begin{lstHaskellLhstex}[caption={\texorpdfstring{\haskelllhstexinline{GDict}}{GDict} instances}]
+\begin{lstHaskellLhstex}[caption={\texorpdfstring{\haskelllhstexinline{GDict}}{GDict} instances.}]
 instance Print_g v => GDict (PrintDict_g v) where
        gdict = PrintDict_g print_g
 instance Opt_g v   => GDict (OptDict_g v)   where
        gdict = OptDict_g opt_g
 \end{lstHaskellLhstex}
 
-\begin{lstHaskellLhstex}[caption={Evaluator instances}]
+\begin{lstHaskellLhstex}[caption={Evaluator instances.}]
 instance HasEval_g d => Eval_g (Expr_g d) where
        eval_g (Lit_g v)     = v
        eval_g (Add_g e1 e2) = eval_g e1 + eval_g e2
@@ -952,7 +952,7 @@ instance HasEval_g d => Eval_g (Not_g d) where
        eval_g (NotLoop_g e) = eval_g e
 \end{lstHaskellLhstex}
 
-\begin{lstHaskellLhstex}[caption={Printer instances}]
+\begin{lstHaskellLhstex}[caption={Printer instances.}]
 instance HasPrint_g d => Print_g (Expr_g d) where
        print_g (Lit_g v)     = show v
        print_g (Add_g e1 e2) = "(" ++ print_g e1 ++ "+" ++ print_g e2 ++ ")"
@@ -975,7 +975,7 @@ instance HasPrint_g d => Print_g (Not_g d) where
        print_g (NotLoop_g e) = print_g e
 \end{lstHaskellLhstex}
 
-\begin{lstHaskellLhstex}[caption={Optimisation instances}]
+\begin{lstHaskellLhstex}[caption={Optimisation instances.}]
 instance HasOpt_g d => Opt_g (Expr_g d) where
        opt_g (Lit_g v)     = Lit_g v
        opt_g (Add_g e1 e2) = case (opt_g e1, opt_g e2) of
index 68a5baf..d3df08e 100644 (file)
@@ -785,7 +785,7 @@ If not the host language but the \gls{DSL} contains higher order functions, the
 \Citet{mcdonell_embedded_2022} extends on this idea, resulting in a very similar but different solution to ours.
 They used the technique that \citeauthor{atkey_unembedding_2009} showed and applied it to deep embedding using the concrete syntax of the host language.
 The scaffolding---e.g.\ generating the pairs, sums and injections---for embedding is automated using generics but the required pattern synonyms are generated using \gls{TH}.
-The key difference to our approach is that we specialise the implementation for each of the backends instead of providing a general implementation of data type handling operations.
+The key difference to our approach is that we specialise the implementation for each of the interpretations instead of providing a general implementation of data type handling operations.
 Furthermore, our implementation does not require a generic function to trace all constructors, resulting in problems with (mutual) recursion.
 
 \Citet{young_adding_2021} added pattern matching to a deeply \gls{EDSL} using a compiler plugin.
@@ -812,7 +812,7 @@ In practise, this means that the programmer selects a skeleton and, at compile t
 \Citet{duregard_embedded_2011} wrote a parser generator using \gls{TH} and the custom quasiquoting facilities.
 From a specification of the grammar, given in verbatim using a custom quasiquoter, a parser is generated at compile time.
 \Citet{shioda_libdsl_2014} used metaprogramming in the D programming language to create a \gls{DSL} toolkit.
-They also programmatically generate parsers and a backend for either compiling or interpreting the \gls{IR}.
+They also programmatically generate parsers and an interpretation for either compiling or interpreting the \gls{IR}.
 \Citet{blanchette_liquid_2022} use \gls{TH} to simplify the development of Liquid \gls{HASKELL} proofs.
 \Citet{folmer_high-level_2022} used \gls{TH} to synthesize C$\lambda$aSH \citep{baaij_digital_2015} \glspl{AST} to be processed.
 In similar fashion, \citet{materzok_generating_2022} used \gls{TH} to translate YieldFSM programs to {C$\lambda$aSH}.
index 54d4c5e..690ee71 100644 (file)
--- a/latexmkrc
+++ b/latexmkrc
@@ -1,6 +1,6 @@
 # Make and clean glossaries
 add_cus_dep('glo', 'gls', 0, 'run_makeglossaries');
-add_cus_dep('acn', 'acr', 0, 'run_makeglossaries');
+add_cus_dep('glo-abr', 'gls-abr', 0, 'run_makeglossaries');
 sub run_makeglossaries {
   if ( $silent ) {
     system "makeglossaries -q '$_[0]'";
@@ -10,7 +10,7 @@ sub run_makeglossaries {
   };
 }
 push @generated_exts, 'glo', 'gls', 'glg';
-push @generated_exts, 'acn', 'acr', 'alg';
+push @generated_exts, 'glo-abr', 'gls-abr', 'glg-abr';
 
 # Clean hyperref backrefs file
 push @generated_exts, 'brf';
index 67b5632..9f4a809 100644 (file)
@@ -4,14 +4,14 @@
 \newcommand{\dcolon}[0]{\mathbin{::}}
 \newcommand{\doifmt}[1]{\href{https://doi.org/#1}{#1}}
 \newcommand{\etc}{{\fontfamily{cmr}\selectfont{\itshape\/\&\kern-0.2em c}}}
-\newcommand{\jsinger}{Singer, dr.\ J.\ (University of Glasgow)}
+\newcommand{\jsinger}{Singer, J.\ (University of Glasgow)}
 \newcommand{\mlubbers}{Lubbers, M.\ (Radboud University)}
-\newcommand{\pkoopman}{Koopman, dr.\ P.\ (Radboud University)}
-\newcommand{\ptrinder}{Trinder, prof.~dr.\ P.\ (University of Glasgow)}
+\newcommand{\pkoopman}{Koopman, P.\ (Radboud University)}
+\newcommand{\ptrinder}{Trinder, P.\ (University of Glasgow)}
+\newcommand{\rplasmeijer}{Plasmeijer, R.\ (Radboud University)}
 \newcommand{\rdmentry}[5]{#1 (#2): #3. #4.\ \doifmt{#5}}
 \newcommand{\rewriterate}[2]{\langle{}\mathit{#1}, \mathit{#2}\rangle{}}
 \newcommand{\requiresGHCmod}[2][]{\footnote{Requires \GHCmod{#2} to be enabled. #1}}
-\newcommand{\rplasmeijer}{Plasmeijer, prof.\ dr.\ ir.\ R.\ (Radboud University)}
 \newcommand{\erasmusplus}{ERASMUS\raisebox{.25ex}{+}}
 \newcommand{\imtask}{\gls{ITASK}\slash\gls{MTASK}}
 \newcommand{\citask}{\gls{CLEAN}\slash\gls{ITASK}}
@@ -24,8 +24,6 @@
 \newcommand{\Ccpp}{\texorpdfstring{\Gls{C}\slash\gls{CPP}}{C\slash{}C\texttt{++}}}
 \newcommand{\stacksize}[1]{\parallel#1\parallel}
 
-\makeatletter
-\newenvironment{compilationscheme}
-       {\allowdisplaybreaks\startalign}
-       {\endalign}
-\makeatother
+\newcommand{\cschemeE}[2]{\mathcal{E}\llbracket#1\rrbracket~#2}
+\newcommand{\cschemeF}[1]{\mathcal{F}\llbracket#1\rrbracket}
+\newcommand{\cschemeS}[3]{\mathcal{S}\llbracket#1\rrbracket~#2~#3}
index e7b2415..722dcb7 100644 (file)
@@ -1,5 +1,5 @@
 \usepackage[nolangwarn,abbreviations,nonumberlist,prefix]{glossaries-extra}
-\setabbreviationstyle{long-short}
+\setabbreviationstyle{long-short-sc}
 \setabbreviationstyle[noexpand]{short-nolong}
 \Addlcwords{of}
 \usepackage{glossary-mcols}
 %      \newacronym[type=\glsdefaulttype,#1]{#2}{#3}{#4}
        \newabbreviation[#1]{#2}{#3}{#4}
 }
-\myacronym[category=noexpand]{3COWS}{3COWS}{The three ``CO'' (Composability, Comprehensibility, Correctness) winter school}
-\myacronym{ADC}{ADC}{analog-to-digital converter}
-\myacronym{ADT}{ADT}{algebraic data type}
-\myacronym{AST}{AST}{abstract syntax tree}
-\myacronym{API}{API}{application programming interface}
-\myacronym{ARDSL}{ARDSL}{\gls{ARDUINO} \glsxtrshort{DSL}}
-\myacronym[category=noexpand]{CEFP}{CEFP}{Central European \glsxtrlong{FP} School}
-\myacronym{CRS}{CRS}{\gls{CLEAN} Raspberry Pi system}
-\myacronym{CRTS}{CRTS}{\gls{CLEAN} Raspberry Pi temperature sensor}
-\myacronym{CWS}{CWS}{\gls{CLEAN} \gls{WEMOS} system}
-\myacronym{CWTS}{CWTS}{\gls{CLEAN} \gls{WEMOS} temperature sensor}
-\myacronym{DHT}{DHT}{digital humidity and temperature}
-\myacronym{DSL}{DSL}{domain-specific language}
-\myacronym{DVFS}{DVFS}{dynamic voltage and frequency scaling}
+\myacronym[category=noexpand]{3COWS}{3cows}{The three ``CO'' (Composability, Comprehensibility, Correctness) winter school}
+\myacronym{ADC}{adc}{analog-to-digital converter}
+\myacronym{ADT}{adt}{algebraic data type}
+\myacronym{AST}{ast}{abstract syntax tree}
+\myacronym{API}{api}{application programming interface}
+\myacronym{ARDSL}{ardsl}{\gls{ARDUINO} \glsxtrshort{DSL}}
+\myacronym[category=noexpand]{CEFP}{cefp}{Central European \glsxtrlong{FP} School}
+\myacronym{CRS}{crs}{\gls{CLEAN} Raspberry Pi system}
+\myacronym{CRTS}{crts}{\gls{CLEAN} Raspberry Pi temperature sensor}
+\myacronym{CWS}{cws}{\gls{CLEAN} \gls{WEMOS} system}
+\myacronym{CWTS}{cwts}{\gls{CLEAN} \gls{WEMOS} temperature sensor}
+\myacronym{DHT}{dht}{digital humidity and temperature}
+\myacronym{DSL}{dsl}{domain-specific language}
+\myacronym{DVFS}{dvfs}{dynamic voltage and frequency scaling}
 \myacronym{ECO2}{eCO\textsubscript{2}}{equivalent carbon dioxide}
-\myacronym{EDSL}{eDSL}{embedded \glsxtrlong{DSL}}
+\myacronym{EDSL}{edsl}{embedded \glsxtrlong{DSL}}
 \myacronym[prefixfirst={a\ },prefix={an\ }]{FP}{FP}{functional programming}
 \myacronym[prefixfirst={a\ },prefix={an\ }]{FRP}{FRP}{functional reactive programming}
 \myacronym[prefixfirst={a\ },prefix={an\ }]{FPGA}{FPGA}{field-programmable gate array}
-\myacronym{GADT}{GADT}{generalised \glsxtrshort{ADT}}
-\myacronym{GHC}{GHC}{Glasgow \gls{HASKELL} Compiler}
-\myacronym{GPIO}{GPIO}{general-purpose \glsxtrlong{IO}}
-\myacronym{GPL}{GPL}{general-purpose language}
-\myacronym{GRS}{GRS}{graph rewriting system}
-\myacronym{GUI}{GUI}{graphical \glsxtrlong{UI}}
-\myacronym{HOAS}{HOAS}{high-order abstract syntax}
+\myacronym{GADT}{gadt}{generalised \glsxtrshort{ADT}}
+\myacronym{GHC}{ghc}{Glasgow \gls{HASKELL} Compiler}
+\myacronym{GPIO}{gpio}{general-purpose \glsxtrlong{IO}}
+\myacronym{GPL}{gpl}{general-purpose language}
+\myacronym{GRS}{grs}{graph rewriting system}
+\myacronym{GUI}{gui}{graphical \glsxtrlong{UI}}
+\myacronym{HOAS}{hoas}{high-order abstract syntax}
 \myacronym{IOT}{Io\kern-.3mmT}{internet of things}
-\myacronym[category=noexpand]{IDE}{IDE}{integrated development environment}
-\myacronym[category=noexpand]{IO}{I/O}{input/output}
-\myacronym{IR}{IR}{intermediate representation}
-\myacronym{ISR}{ISR}{interrupt service routine}
-\myacronym{LEAN}{LEAN}{language of East-Anglia and Nijmegen}
+\myacronym[category=noexpand]{IDE}{ide}{integrated development environment}
+\myacronym[category=noexpand]{IO}{i/o}{input/output}
+\myacronym{IR}{ir}{intermediate representation}
+\myacronym{ISR}{isr}{interrupt service routine}
+\myacronym{LEAN}{lean}{language of East-Anglia and Nijmegen}
 \myacronym[category=noexpand,prefixfirst={a\ },prefix={an\ }]{LED}{LED}{light-emitting diode}
-\myacronym[category=noexpand]{OLED}{OLED}{organic \glsxtrshort{LED}}
-\myacronym[category=noexpand]{OS}{OS}{operating system}
-\myacronym{OTA}{OTA}{over-the-air}
-\myacronym{PIR}{PIR}{passive infrared}
-\myacronym{PFRP}{P-FRP}{priority-based \glsxtrshort{FRP}}
-\myacronym{PRS}{PRS}{\gls{PYTHON} Raspberry Pi system}
-\myacronym{PWS}{PWS}{\gls{MICROPYTHON} \gls{WEMOS} system}
-\myacronym{PRTS}{PRTS}{\gls{PYTHON} Raspberry Pi temperature sensor}
-\myacronym{PWTS}{PWTS}{\gls{MICROPYTHON} \gls{WEMOS} temperature sensor}
-\myacronym{QDSL}{QDSL}{quoted \glsxtrshort{DSL}}
-\myacronym[category=noexpand]{RAM}{RAM}{random-access memory}
-\myacronym{RFID}{RFID}{radio-frequency identification}
-\myacronym{RTOS}{RTOS}{real-time \glsxtrshort{OS}}
-\myacronym{RTS}{RTS}{run-time system}
-\myacronym[prefixfirst={a\ },prefix={an\ }]{SDS}{SDS}{shared data source}
-\myacronym[prefixfirst={a\ },prefix={an\ }]{SN}{SN}{sensor network}
-\myacronym{SLOC}{SLOC}{source lines of code}
-\myacronym{TH}{TH}{Template \gls{HASKELL}}
-\myacronym[category=noexpand]{TCP}{TCP}{transmission control protocol}
-\myacronym{TOP}{TOP}{task-oriented programming}
-\myacronym{TOSD}{TOSD}{task-oriented software development}
-\myacronym{TRS}{TRS}{term rewriting system}
-\myacronym{TTH}{TTH}{typed \glsxtrlong{TH}}
-\myacronym{TVOC}{TVOC}{total volatile organic compounds}
-\myacronym{UI}{UI}{user interface}
-\myacronym{UOD}{UoD}{universe of discourse}
-\myacronym{UOG}{UoG}{University of Glasgow}
-\myacronym{VM}{VM}{virtual machine}
+\myacronym[category=noexpand]{OLED}{oled}{organic \glsxtrshort{LED}}
+\myacronym[category=noexpand]{OS}{os}{operating system}
+\myacronym{OTA}{ota}{over-the-air}
+\myacronym{PIR}{pir}{passive infrared}
+\myacronym{PFRP}{p-frp}{priority-based \glsxtrshort{FRP}}
+\myacronym{PRS}{prs}{\gls{PYTHON} Raspberry Pi system}
+\myacronym{PWS}{pws}{\gls{MICROPYTHON} \gls{WEMOS} system}
+\myacronym{PRTS}{prts}{\gls{PYTHON} Raspberry Pi temperature sensor}
+\myacronym{PWTS}{pwts}{\gls{MICROPYTHON} \gls{WEMOS} temperature sensor}
+\myacronym{QDSL}{qdsl}{quoted \glsxtrshort{DSL}}
+\myacronym[category=noexpand]{RAM}{ram}{random-access memory}
+\myacronym{RFID}{rfid}{radio-frequency identification}
+\myacronym{RTOS}{rtos}{real-time \glsxtrshort{OS}}
+\myacronym{RTS}{rts}{run-time system}
+\myacronym[prefixfirst={a\ },prefix={an\ }]{SDS}{sds}{shared data source}
+\myacronym[prefixfirst={a\ },prefix={an\ }]{SN}{sn}{sensor network}
+\myacronym{SLOC}{sloc}{source lines of code}
+\myacronym{TH}{th}{Template \gls{HASKELL}}
+\myacronym[category=noexpand]{TCP}{tcp}{transmission control protocol}
+\myacronym{TOP}{top}{task-oriented programming}
+\myacronym{TOSD}{tosd}{task-oriented software development}
+\myacronym{TRS}{trs}{term rewriting system}
+\myacronym{TTH}{tth}{typed \glsxtrlong{TH}}
+\myacronym{TVOC}{tvoc}{total volatile organic compounds}
+\myacronym{UI}{ui}{user interface}
+\myacronym{UOD}{uod}{universe of discourse}
+\myacronym{UOG}{uog}{University of Glasgow}
+\myacronym{VM}{vm}{virtual machine}
 
 % Glossaries
 \newglossaryentry{ABC}{%
index 25e04ad..378497a 100644 (file)
@@ -30,9 +30,9 @@ The software is usually a cyclic executive instead of tasks that run in an \gls{
 Hence, all tasks must be manually combined into a single program.
 
 \begin{table}
+       \centering
        \caption{Hardware characteristics of a laptop and two typical microcontrollers.}%
        \label{tbl:mcu_laptop}
-       \centering
        \begin{tabular}{llll}
                \toprule
                        & Laptop & Atmega328P & ESP8266\\
@@ -104,7 +104,7 @@ To simulate a loop, the \cleaninline{rpeat} task combinator is used as this task
 The body of the \cleaninline{rpeat} task contanis a task that writes to the pins and waits 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{lstClean}[float=ht,caption={Blinking the \gls{LED} using the \cleaninline{rpeat} combinator.},label={lst:blinkImp}]
+\begin{lstClean}[caption={Blinking the \gls{LED} using the \cleaninline{rpeat} combinator.},label={lst:blinkImp}]
 blinkTask :: Main (MTask v ()) | mtask v
 blinkTask = declarePin D2 PMOutput \ledPin->
        {main = rpeat (
@@ -137,7 +137,7 @@ Now say that we want to blink multiple blinking patterns on different \glspl{LED
 For example, blink three \glspl{LED} connected to \gls{GPIO} pins $1,2$ and $3$ at intervals of \qtylist{500;300;800}{\ms}.
 Intuitively you would want to lift the blinking behaviour to a function in order to minimise duplicate code and increase modularity and call this function three times with different parameters as shown in \cref{lst:blinkthreadno}.
 
-\begin{lstArduino}[float=ht,caption={Naive approach to multiple blinking patterns.},label={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);
index 57c6b19..aea4fb9 100644 (file)
@@ -2,16 +2,16 @@
 \usepackage{stmaryrd}
 \usetikzlibrary{arrows.meta,shapes.symbols,matrix,positioning}
 \begin{document}
-\begin{tikzpicture}
-       \matrix (tree) [matrix of nodes,nodes in empty cells, row sep=1em] {
-                                       & \verb#>>|.#\\
-       \texttt{delay}  & & \verb#>>=.#$~\lambda$\verb#x#$\shortrightarrow$\\
-                                       & \texttt{writeD} & & |[fill=gray!15,label={[xshift=1em,label distance=-5pt]above:{\tiny interpreter}}]|\verb#blink (Not x)#\\
-       };
-       \draw (tree-1-2.south) -- (tree-2-1.north);
-       \draw (tree-1-2.south) -- (tree-2-3.north);
-       \draw (tree-2-3.south) -- (tree-3-2.north);
-       \draw (tree-2-3.south) -- ([xshift=-1.5em]tree-3-4.north);
-       \draw [->,dashed] ([xshift=-1.5em]tree-3-4.north) to [out=25,in=25] (tree-1-2.east);
+\begin{tikzpicture}[node distance=1em]
+       \node (s1) {\verb#>>|.#};
+       \node (d1) [left=of s1.north,yshift=-3em] {\verb#delay#};
+       \node (s2) [right=of s1.north,yshift=-3em] {\verb#>>=.# $\lambda x\shortrightarrow$};
+       \node (wd) [left=of s2.north,yshift=-3em] {\verb#writeD#};
+       \node (rec) [right=of s2.north,yshift=-3em,fill=gray!15,label={[xshift=1em,label distance=-5pt]above:{\tiny interpreter}}] {\verb#blink (Not x)#};
+       \draw (s1.south) -- (d1.north);
+       \draw (s1.south) -- (s2.north);
+       \draw (s2.south) -- (wd.north);
+       \draw (s2.south) -- ([xshift=-1.5em]rec.north);
+       \draw [->,dashed] ([xshift=-1.5em]rec.north) to [out=25,in=25] (s1.east);
 \end{tikzpicture}
 \end{document}
diff --git a/top/contexttree1.tex b/top/contexttree1.tex
new file mode 100644 (file)
index 0000000..e8555c3
--- /dev/null
@@ -0,0 +1,21 @@
+\documentclass[tikz]{standalone}
+\usepackage{stmaryrd}
+\usetikzlibrary{arrows.meta,shapes.symbols,matrix,positioning}
+\begin{document}
+\begin{tikzpicture}[node distance=1em]
+       \node (s1) {\verb#>>=.#};
+       \node (t1) [left=of s1.north,yshift=-3em] {$t_1$};
+       \node (v1) [right=of s1.north,yshift=-3em] {\verb#>>=.# $\lambda v_1\shortrightarrow$};
+       \node (t2) [left=of v1.north,yshift=-3em] {$t_2$};
+       \node (v2) [right=of v1.north,yshift=-3em] {\verb#>>=.# $\lambda v_2\shortrightarrow$};
+       \node (t3) [left=of v2.north,yshift=-3em] {$t_3$};
+       \node (ld) [right=of v2.north,yshift=-3em] {\ldots};
+
+       \draw (s1.south) -- (t1.north);
+       \draw (s1.south) -- (v1.north);
+       \draw (v1.south) -- (t2.north);
+       \draw (v1.south) -- (v2.north);
+       \draw (v2.south) -- (t3.north);
+       \draw (v2.south) -- (ld.north);
+\end{tikzpicture}
+\end{document}
diff --git a/top/contexttree2.tex b/top/contexttree2.tex
new file mode 100644 (file)
index 0000000..a149449
--- /dev/null
@@ -0,0 +1,29 @@
+\documentclass[tikz]{standalone}
+\usepackage{stmaryrd}
+\usetikzlibrary{arrows.meta,shapes.symbols,matrix,positioning}
+\begin{document}
+\begin{tikzpicture}[node distance=1em]
+       \node (s1) {\verb#>>=.#};
+       \node (t1) [left=of s1.north,yshift=-3em] {$t_1$};
+       \node (v1) [right=of s1.north,yshift=-3em] {\verb#>>=.# $\lambda v_1\shortrightarrow$};
+       \node (a1) [left=of v1.north,yshift=-3em] {\verb#.&&.#};
+       \node (a1v) [left=of a1.north,yshift=-3em] {\verb#rtrn# $v_1$};
+       \node (a1t) [right=of a1.north,yshift=-3em] {$t_1$};
+       \node (v2) [right=of v1.north,xshift=1em,yshift=-3em] {\verb#>>=.# $\lambda v_2\shortrightarrow$};
+       \node (a2) [left=of v2.north,yshift=-3em] {\verb#.&&.#};
+       \node (a2v) [left=of a2.north,yshift=-3em] {\verb#rtrn# $(v_1, v_2)$};
+       \node (a2t) [right=of a2.north,yshift=-3em] {$t_2$};
+       \node (ld) [right=of v2.north,yshift=-3em] {\ldots};
+
+       \draw (s1.south) -- (t1.north);
+       \draw (s1.south) -- (v1.north);
+       \draw (v1.south) -- (a1.north);
+       \draw (a1.south) -- (a1v.north);
+       \draw (a1.south) -- (a1t.north);
+       \draw (v1.south) -- (v2.north);
+       \draw (v2.south) -- (a2.north);
+       \draw (a2.south) -- (a2v.north);
+       \draw (a2.south) -- (a2t.north);
+       \draw (v2.south) -- (ld.north);
+\end{tikzpicture}
+\end{document}
index 687e79e..9e94d66 100644 (file)
@@ -281,7 +281,7 @@ This section provides an exhaustive overview of the work on \gls{MTASK} and its
 \subsection{Generating \ccpp{} code}
 A first throw at a class-based shallowly \gls{EDSL} for microcontrollers was made by \citet{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.
+A \gls{CPP} code generation interpretation was available together with an \gls{ITASK} simulation interpretation.
 There was no support for tasks nor functions.
 Some time later in the 2015 \gls{CEFP} summer school, an extended version was created that allowed the creation of imperative tasks, local \glspl{SDS} and the usage of functions \citep{koopman_type-safe_2019}.
 The name then changed from \gls{ARDSL} to \gls{MTASK}.
index cacceec..09c2ce7 100644 (file)
        This chapter shows the implementation of the \gls{MTASK} system by:
        \begin{itemize}
                \item elaborating on the implementation and architecture of the \gls{RTS} of \gls{MTASK};
-               \item giving details of the implementation of \gls{MTASK}'s \gls{TOP} engine that executes the \gls{MTASK} tasks on the microcontroller;
-               \item showing the implementation of the byte code compiler for \gls{MTASK}'s \gls{TOP} language;
-               \item explaining the machinery used to automatically serialise and deserialise data to-and-fro the device.
+               \item showing the implementation of the byte code compiler for the \gls{MTASK} language;
+               \item and explaining the machinery used to automatically serialise and deserialise data to-and-fro the device.
        \end{itemize}
 \end{chapterabstract}
 
-\todo[inline]{Dit hoofdstuk is het ruwst van allen}
-The \gls{MTASK} system targets resource-constrained edge devices that have little memory, processor speed and communication.
-Such edge devices are often powered by microcontrollers.
-They usually have flash-based program memory which wears out fairly quick.
-For example, the flash memory of the popular atmega328p powering the \gls{ARDUINO} UNO is just rated for 10000 write cycles.
+The \gls{MTASK} system targets resource-constrained edge devices that have little memory, processor speed, and communication.
+Such edge devices are often powered by microcontrollers, tiny computers specifically designed for embedded applications.
+The microcontrollers usually have flash-based program memory which wears out fairly quickly.
+For example, the flash memory of the popular atmega328p powering the \gls{ARDUINO} UNO is rated for 10000 write cycles.
 While this sounds like a lot, if new tasks are sent to the device every minute or so, a lifetime of only seven days is guaranteed.
-Hence, for dynamic applications, storing the program in the \gls{RAM} of the device and interpreting this code is necessary, saving precious write cycles of the program memory.
-In the \gls{MTASK} system, this is done by the \gls{MTASK} \gls{RTS}.
+Hence, for dynamic applications, storing the program in the \gls{RAM} of the device and interpreting this code is necessary in order to save precious write cycles of the program memory.
+In the \gls{MTASK} system, the \gls{MTASK} \gls{RTS}, a domain-specific \gls{OS}, is responsible for interpreting the programs.
 
 \section{\texorpdfstring{\Glsxtrlong{RTS}}{Run time system}}
-The \gls{RTS} is a customisable domain-specific \gls{OS} that takes care of the execution of tasks, but also low-level mechanisms such as the communication, multitasking, and memory management.
+The \gls{RTS} is a customisable domain-specific \gls{OS} that takes care of the execution of tasks.
+Furthermore, it also takes care of low-level mechanisms such as the communication, multitasking, and memory management.
 Once a device is programmed with the \gls{MTASK} \gls{RTS}, it can continuously receive new tasks without the need for reprogramming.
 The \gls{OS} is written in portable \ccpp{} and only contains a small device-specific portion.
 In order to keep the abstraction level high and the hardware requirements low, much of the high-level functionality of the \gls{MTASK} language is implemented not in terms of lower-level constructs from \gls{MTASK} language but in terms of \ccpp{} code.
 
-As most microcontrollers software is run solely by a cyclic executive instead of an \gls{OS}, the \gls{RTS} of the \gls{MTASK} system is implemented as such also.
+Most microcontrollers software consists of a cyclic executive instead of an \gls{OS}, the \gls{RTS} of the \gls{MTASK} system is implemented as such also.
 It consists of a loop function with a relatively short execution time, similar to the one in \gls{ARDUINO}, that gets called repeatedly.
 The event loop consists of three distinct phases.
 After doing the three phases, the devices goes to sleep for as long as possible (see \cref{chp:green_computing_mtask} for more details on task scheduling).
 
-\subsection{Communication}
+\subsection{Communication phase}
 In the first phase, the communication channels are processed.
 The exact communication method is a customisable device-specific option baked into the \gls{RTS}.
-The interface is deliberately kept simple and consists of a two layer interface: a link interface and a communication interface.
-Besides opening, closing and cleaning up, the link interface has only three functions that are shown in \cref{lst:link_interface}.
-Consequently, implementing this link interface is very simple but allows for many more advanced link settings such as buffering.
-There are implementations for this interface for serial or \gls{WIFI} connections using \gls{ARDUINO} and \gls{TCP} connections for Linux.
+The interface is kept deliberately simple and consists of two layers: a link interface and a communication interface.
+Besides opening, closing and cleaning up, the link interface has three functions that are shown in \cref{lst:link_interface}.
+Consequently, implementing this link interface is very simple but it is still possible to implement more advanced link features such as buffering.
+There are implementations for this interface for serial or \gls{WIFI} connections using \gls{ARDUINO}, and \gls{TCP} connections for Linux.
 
 \begin{lstArduino}[caption={Link interface of the \gls{MTASK} \gls{RTS}.},label={lst:link_interface}]
-bool link_input_available(void);
+bool    link_input_available(void);
 uint8_t link_read_byte(void);
-void link_write_byte(uint8_t b);
+void    link_write_byte(uint8_t b);
 \end{lstArduino}
 
 The communication interface abstracts away from this link interface and is typed instead.
@@ -67,17 +66,17 @@ There are several possible messages that can be received from the server:
 
 \begin{description}
        \item[SpecRequest]
-               is a message instructing the device to send its specification and is sent usually immediately after connecting.
+               is a message instructing the device to send its specification and it is received immediately after connecting.
                The \gls{RTS} responds with a \texttt{Spec} answer containing the specification.
        \item[TaskPrep]
-               tells the device a (big) task is on its way.
+               tells the device a task is on its way.
                Especially on faster connections, it may be the case that the communication buffers overflow because a big message is sent while the \gls{RTS} is busy executing tasks.
-               This allows the \gls{RTS} to postpone execution for a while, until the big task has been received.
-               The server sends the big task when the device acknowledges (by sending a \texttt{TaskPrepAck} message) the preparation.
+               This message allows the \gls{RTS} to postpone execution for a while, until the larger task has been received.
+               The server sends the task only after the device acknowledged the preparation by by sending a \texttt{TaskPrepAck} message.
        \item[Task]
-               contains a new task, its peripheral configuration, the \glspl{SDS}, and the bytecode.
-               The new task is immediately copied to the task storage but is only initialised during the next phase after which a \texttt{TaskAck} is sent.
-               Tasks are stored below the stack, but since the stack is only used in the middle phase, execution, it is no problem that it moves.
+               contains a new task, its peripheral configuration, the \glspl{SDS}, and the byte code.
+               The new task is immediately copied to the task storage but is only initialised during the next phase.
+               The device acknowledges the task by sending a \texttt{TaskAck} message.
        \item[SdsUpdate]
                notifies the device of the new value for a lowered \gls{SDS}.
                The old value of the lowered \gls{SDS} is immediately replaced with the new one.
@@ -86,18 +85,18 @@ There are several possible messages that can be received from the server:
                instructs the device to delete a running task.
                Tasks are automatically deleted when they become stable.
                However, a task may also be deleted when the surrounding task on the server is deleted, for example when the task is on the left-hand side of a step combinator and the condition to step holds.
-               The device acknowledges by sending a \texttt{TaskDelAck}.
+               The device acknowledges the deletion by sending a \texttt{TaskDelAck}.
        \item[Shutdown]
                tells the device to reset.
 \end{description}
 
-\subsection{Execution}
+\subsection{Execution phase}
 The second phase performs one execution step for all tasks that wish for it.
-Tasks are ordered in a priority queue ordered by the time a task needs to be executed, the \gls{RTS} selects all tasks that can be scheduled, see \cref{sec:scheduling} for more details.
-Execution of a task is always an interplay between the interpreter and the \emph{rewriter}.
+Tasks are ordered in a priority queue ordered by the time a task needs to execute, the \gls{RTS} selects all tasks that can be scheduled, see \cref{sec:scheduling} for more details.
+Execution of a task is always an interplay between the interpreter and the rewriter.
 
 When a new task is received, the main expression is evaluated to produce a task tree.
-A task tree is a tree in which each node represents a task combinator and the leaves are basic tasks.
+A task tree is a tree structure in which each node represents a task combinator and the leaves are basic tasks.
 If a task is not initialized yet, i.e.\ the pointer to the current task tree is still null, the byte code of the main function is interpreted.
 The main expression always produces a task tree.
 Execution of a task consists of continuously rewriting the task until its value is stable.
@@ -108,9 +107,9 @@ The rewriter and the interpreter use the same stack to store intermediate values
 Rewriting steps are small so that interleaving results in seemingly parallel execution.
 In this phase new task tree nodes may be allocated.
 Both rewriting and initialization are atomic operations in the sense that no processing on \glspl{SDS} is done other than \gls{SDS} operations from the task itself.
-The host is notified if a task value is changed after a rewrite step.
+The host is notified if a task value is changed after a rewrite step by sending a \texttt{TaskReturn} message.
 
-Take for example the blink task for which the code is shown in \cref{lst:blink_code}.
+Take for example a blink task for which the code is shown in \cref{lst:blink_code}.
 
 \begin{lstClean}[caption={Code for a blink program.},label={lst:blink_code}]
 fun \blink=(\st->delay (lit 500) >>|. writeD d3 st >>=. blink o Not)
@@ -121,11 +120,11 @@ On receiving this task, the task tree is still null and the initial expression \
 This results in the task tree shown in \cref{fig:blink_tree}.
 Rewriting always starts at the top of the tree and traverses to the leaves, the basic tasks that do the actual work.
 The first basic task encountered is the \cleaninline{delay} task, that yields no value until the time, \qty{500}{\ms} in this case, has passed.
-When the \cleaninline{delay} task yielded a stable value, the task continues with the right-hand side of the \cleaninline{>>\|.} combinator.
+When the \cleaninline{delay} task yielded a stable value after a number of rewrites, the task continues with the right-hand side of the \cleaninline{>>\|.} combinator.
 This combinator has a \cleaninline{writeD} task at the left-hand side that becomes stable after one rewrite step in which it writes the value to the given pin.
 When \cleaninline{writeD} becomes stable, the written value is the task value that is observed by the right-hand side of the \cleaninline{>>=.} combinator.
 This will call the interpreter to evaluate the expression, now that the argument of the function is known.
-The result of the function is basically the original task tree again, but now with the state inversed.
+The result of the function is the original task tree again, but now with the state inversed.
 
 \begin{figure}
        \centering
@@ -165,13 +164,53 @@ If a task is to be removed, tasks with higher memory addresses are moved down.
 For task trees---stored in the heap---the \gls{RTS} already marks tasks and task trees as trash during rewriting so the heap can be compacted in a single pass.
 This is possible because there is no sharing or cycles in task trees and nodes contain pointers pointers to their parent.
 
-\todo[inline]{plaa\-tje van me\-mo\-ry hier uitbreiden?}
-
 \section{Compiler}
+\subsection{Compiler infrastructure}
+The bytecode compiler interpretation for the \gls{MTASK} language is implemented as a monad stack containing a writer monad and a state monad.
+The writer monad is used to generate code snippets locally without having to store them in the monadic values.
+The state monad accumulates the code, and stores the state the compiler requires.
+\Cref{lst:compiler_state} shows the data type for the state, storing:
+function the compiler currently is in;
+code of the main expression;
+context (see \cref{ssec:step});
+code for the functions;
+next fresh label;
+a list of all the used \glspl{SDS}, either local \glspl{SDS} containing the initial value (\cleaninline{Left}) or lifted \glspl{SDS} (see \cref{sec:liftsds}) containing a reference to the associated \gls{ITASK} \gls{SDS};
+and finally there is a list of peripherals used.
+
+\begin{lstClean}[label={lst:compiler_state},caption={The type for the \gls{MTASK} byte code compiler.}]
+:: BCInterpret a :== StateT BCState (WriterT [BCInstr] Identity) a
+:: BCState =
+       { bcs_infun        :: JumpLabel
+       , bcs_mainexpr     :: [BCInstr]
+       , bcs_context      :: [BCInstr]
+       , bcs_functions    :: Map JumpLabel BCFunction
+       , bcs_freshlabel   :: JumpLabel
+       , bcs_sdses        :: [Either String255 MTLens]
+       , bcs_hardware     :: [BCPeripheral]
+       }
+:: BCFunction =
+       { bcf_instructions :: [BCInstr]
+       , bcf_argwidth     :: UInt8
+       , bcf_returnwidth  :: UInt8
+       }
+\end{lstClean}
+
+Executing the compiler is done by providing an initial state and running the monad.
+After compilation, several post-processing steps are applied to make the code suitable for the microprocessor.
+First, in all tail call \cleaninline{BCReturn} instructions are replaced by \cleaninline{BCTailCall} instructions to optimise the tail calls.
+Furthermore, all byte code is concatenated, resulting in one big program.
+Many instructions have commonly used arguments so shorthands are introduced to reduce the program size.
+For example, the \cleaninline{BCArg} instruction is often called with argument \numrange{0}{2} and can be replaced by the \numrange[parse-numbers=false]{\cleaninline{BCArg0}}{\cleaninline{BCArg2}} shorthands.
+Furthermore, redundant instructions such as pop directly after push are removed as well in order not to burden the code generation with these intricacies.
+Finally the labels are resolved to represent actual program addresses instead of the freshly generated identifiers.
+After the byte code is ready, the lifted \glspl{SDS} are resolved to provide an initial value for them.
+The byte code, \gls{SDS} specification and perpipheral specifications are the result of the process, ready to be sent to the device.
+
 \subsection{Instruction set}
 The instruction set is a fairly standard stack machine instruction set extended with special \gls{TOP} instructions for creating task tree nodes.
-All instructions are housed in a \gls{CLEAN} \gls{ADT} and serialised to the byte representation using a generic function.
-Type synonyms (\cref{lst:type_synonyms}) are used to provide insight on the arguments of the instructions.
+All instructions are housed in a \gls{CLEAN} \gls{ADT} and serialised to the byte representation using generic functions (see \cref{sec:ccodegen}).
+Type synonyms and newtypes are used to provide insight on the arguments of the instructions (\cref{lst:type_synonyms}).
 Labels are always two bytes long, all other arguments are one byte long.
 
 \begin{lstClean}[caption={Type synonyms for instructions arguments.},label={lst:type_synonyms}]
@@ -181,7 +220,7 @@ Labels are always two bytes long, all other arguments are one byte long.
 \end{lstClean}
 
 \Cref{lst:instruction_type} shows an excerpt of the \gls{CLEAN} type that represents the instruction set.
-For example, shorthand instructions are omitted for brevity.
+Shorthand instructions such as instructions with inlined arguments are omitted for brevity.
 Detailed semantics for the instructions are given in \cref{chp:bytecode_instruction_set}.
 One notable instruction is the \cleaninline{MkTask} instruction, it allocates and initialises a task tree node and pushes a pointer to it on the stack.
 
@@ -189,7 +228,8 @@ One notable instruction is the \cleaninline{MkTask} instruction, it allocates an
 :: BCInstr
        //Jumps
        = BCJumpF JumpLabel | BCLabel JumpLabel | BCJumpSR ArgWidth JumpLabel
-       | BCReturn ReturnWidth ArgWidth | BCTailcall ArgWidth ArgWidth JumpLabel
+       | BCReturn ReturnWidth ArgWidth
+       | BCTailcall ArgWidth ArgWidth JumpLabel
        //Arguments
        | BCArgs ArgWidth ArgWidth
        //Task node creation and refinement
@@ -226,61 +266,18 @@ One notable instruction is the \cleaninline{MkTask} instruction, it allocates an
        ...
 \end{lstClean}
 
-\subsection{Compiler infrastructure}
-The bytecode compiler interpretation for the \gls{MTASK} language is implemented as a monad stack containing a writer monad and a state monad.
-The writer monad is used to generate code snippets locally without having to store them in the monadic values.
-The state monad accumulates the code, and stores the stateful data the compiler requires.
-\Cref{lst:compiler_state} shows the data type for the state, storing:
-function the compiler currently is in;
-code of the main expression;
-context (see \cref{ssec:step});
-code for the functions;
-next fresh label;
-a list of all the used \glspl{SDS}, either local \glspl{SDS} containing the initial value (\cleaninline{Left}) or lifted \glspl{SDS} (see \cref{sec:liftsds}) containing a reference to the associated \gls{ITASK} \gls{SDS};
-and finally there is a list of peripherals used.
-
-\begin{lstClean}[label={lst:compiler_state},caption={The type for the \gls{MTASK} byte code compiler}]
-:: BCInterpret a :== StateT BCState (WriterT [BCInstr] Identity) a
-:: BCState =
-       { bcs_infun        :: JumpLabel
-       , bcs_mainexpr     :: [BCInstr]
-       , bcs_context      :: [BCInstr]
-       , bcs_functions    :: Map JumpLabel BCFunction
-       , bcs_freshlabel   :: JumpLabel
-       , bcs_sdses        :: [Either String255 MTLens]
-       , bcs_hardware     :: [BCPeripheral]
-       }
-:: BCFunction =
-       { bcf_instructions :: [BCInstr]
-       , bcf_argwidth     :: UInt8
-       , bcf_returnwidth  :: UInt8
-       }
-\end{lstClean}
-
-Executing the compiler is done by providing an initial state.
-After compilation, several post-processing steps are applied to make the code suitable for the microprocessor.
-First, in all tail call \cleaninline{BCReturn}'s are replaced by \cleaninline{BCTailCall} to implement tail call elimination.
-Furthermore, all byte code is concatenated, resulting in one big program.
-Many instructions have commonly used arguments so shorthands are introduced to reduce the program size.
-For example, the \cleaninline{BCArg} instruction is often called with argument \qtyrange{0}{2} and can be replaced by the \cleaninline{BCArg0}--\cleaninline{BCArg2} shorthands.
-Furthermore, redundant instructions (e.g.\ pop directly after push) are removed as well in order not to burden the code generation with these intricacies.
-Finally the labels are resolved to represent actual program addresses instead of freshly generated identifiers.
-After the byte code is ready, the lifted \glspl{SDS} are resolved to provide an initial value for them.
-The result---byte code, \gls{SDS} specification and perpipheral specifications---are the result of the process, ready to be sent to the device.
 
 \section{Compilation rules}
-This section describes the compilation rules, the translation from abstract syntax to byte code.
+This section describes the compilation rules, the translation from \gls{AST} to byte code.
 The compilation scheme consists of three schemes\slash{}functions.
-When something is surrounded by double vertical bars, e.g.\ $\stacksize{a_i}$, it denotes the number of stack cells required to store it.
+Double vertical bars, e.g.\ $\stacksize{a_i}$, denote the number of stack cells required to store the argument.
 
-Some schemes have a \emph{context} $r$ as an argument which contains information about the location of the arguments in scope.
+Some schemes have a context $r$ as an argument which contains information about the location of the arguments in scope.
 More information is given in the schemes requiring such arguments.
 
-\newcommand{\cschemeE}[2]{\mathcal{E}\llbracket#1\rrbracket~#2}
-\newcommand{\cschemeF}[1]{\mathcal{F}\llbracket#1\rrbracket}
-\newcommand{\cschemeS}[3]{\mathcal{S}\llbracket#1\rrbracket~#2~#3}
 \begin{table}
        \centering
+       \caption{An overview of the compilation schemes.}
        \begin{tabularx}{\linewidth}{l X}
                \toprule
                Scheme & Description\\
@@ -321,24 +318,24 @@ Function calls, function arguments and tasks are also compiled using $\mathcal{E
        \cschemeE{\text{\cleaninline{first}}~e}{r} & =
                        \cschemeE{e}{r};
                        \text{\cleaninline{BCPop}}\enskip w;\\
-               {} & \text{\emph{Where $w$ is the width of the left value and}}\\
+               {} & \text{\emph{Where $w$ is the width of the right value and}}\\
                {} & \text{\emph{similar for other unboxed compound data types}}\\
        \cschemeE{\text{\cleaninline{second}}\enskip e}{r} & =
                        \cschemeE{e}{r};
-                       \text{\cleaninline{BCRot}}\enskip w_1\enskip (w_1+w_2);
-                       \text{\cleaninline{BCPop}}\enskip w_2;\\
-               {} & \text{\emph{Where $w_1$ is the width of the left and, $w_2$ of the right value}}\\
+                       \text{\cleaninline{BCRot}}\enskip (w_l+w_r)\enskip w_r;
+                       \text{\cleaninline{BCPop}}\enskip w_l;\\
+               {} & \text{\emph{Where $w_l$ is the width of the left and, $w_r$ of the right value}}\\
                {} & \text{\emph{similar for other unboxed compound data types}}\\
 \end{align*}
 
-Translating $\mathcal{E}$ to \gls{CLEAN} code is very straightforward, it basically means executing the monad.
+Translating $\mathcal{E}$ to \gls{CLEAN} code is very straightforward, it basically means writing the instructions to the writer monad.
 Almost always, the type of the interpretation is not used, i.e.\ it is a phantom type.
 To still have the functions return the correct type, the \cleaninline{tell`}\footnote{\cleaninline{tell` :: [BCInstr] -> BCInterpret a}} helper is used.
 This function is similar to the writer monad's \cleaninline{tell} function but is casted to the correct type.
 \Cref{lst:imp_arith} shows the implementation for the arithmetic and conditional expressions.
-Note that $r$, the context, is not an explicit argument but stored in the state.
+Note that $r$, the context, is not an explicit argument here but stored in the state.
 
-\begin{lstClean}[caption={Interpretation implementation for the arithmetic and conditional classes.},label={lst:imp_arith}]
+\begin{lstClean}[caption={Interpretation implementation for the arithmetic and conditional functions.},label={lst:imp_arith}]
 instance expr BCInterpret where
        lit   t   = tell` [BCPush (toByteCode{|*|} t)]
        (+.)  a b = a >>| b >>| tell` [BCAdd]
@@ -350,10 +347,10 @@ instance expr BCInterpret where
 \end{lstClean}
 
 \subsection{Functions}\label{ssec:functions}
-Compiling functions occurs in $\mathcal{F}$, which generates bytecode for the complete program by iterating over the functions and ending with the main expression.
+Compiling functions and other top-level definitions is done using in $\mathcal{F}$, which generates bytecode for the complete program by iterating over the functions and ending with the main expression.
 When compiling the body of the function, the arguments of the function are added to the context so that the addresses can be determined when referencing arguments.
 The main expression is a special case of $\mathcal{F}$ since it neither has arguments nor something to continue.
-Therefore, it is just compiled using $\mathcal{E}$.
+Therefore, it is just compiled using $\mathcal{E}$ with an empty context.
 
 \begin{align*}
        \cschemeF{main=m} & =
@@ -373,54 +370,54 @@ Putting the arguments on top of pointers and not reserving space for the return
        \begin{subfigure}{.24\linewidth}
                \centering
                \includestandalone{memory1}
-               \caption{\cleaninline{BCPushPtrs}}\label{lst:funcall_pushptrs}
+               \caption{\cleaninline{BCPushPtrs}.}\label{lst:funcall_pushptrs}
        \end{subfigure}
        \begin{subfigure}{.24\linewidth}
                \centering
                \includestandalone{memory2}
-               \caption{Arguments}\label{lst:funcall_args}
+               \caption{Arguments.}\label{lst:funcall_args}
        \end{subfigure}
        \begin{subfigure}{.24\linewidth}
                \centering
                \includestandalone{memory3}
-               \caption{\cleaninline{BCJumpSR}}\label{lst:funcall_jumpsr}
+               \caption{\cleaninline{BCJumpSR}.}\label{lst:funcall_jumpsr}
        \end{subfigure}
        \begin{subfigure}{.24\linewidth}
                \centering
                \includestandalone{memory4}
-               \caption{\cleaninline{BCReturn}}\label{lst:funcall_ret}
+               \caption{\cleaninline{BCReturn}.}\label{lst:funcall_ret}
        \end{subfigure}
        \caption{The stack layout during function calls.}%
 \end{figure}
 
 Calling a function and referencing function arguments are an extension to $\mathcal{E}$ as shown below.
-Arguments may be at different places on the stack at different times (see \cref{ssec:step}) and therefore the exact location always has to be determined from the context using \cleaninline{findarg}\footnote{\cleaninline{findarg [l`:r] l = if (l == l`) 0 (1 + findarg r l)}}.
+Arguments may be at different places on the stack at different times (see \cref{ssec:step}) and therefore the exact location always is be determined from the context using \cleaninline{findarg}\footnote{\cleaninline{findarg [l`:r] l = if (l == l`) 0 (1 + findarg r l)}}.
 Compiling argument $a_{f^i}$, the $i$th argument in function $f$, consists of traversing all positions in the current context.
-Arguments wider than one stack cell are fetched in reverse to preserve the order.
+Arguments wider than one stack cell are fetched in reverse to reconstruct the original order.
 
 \begin{align*}
        \cschemeE{f(a_0, \ldots, a_n)}{r} & =
-               \text{\cleaninline{BCPushPtrs}}; \cschemeE{a_n}{r}; \cschemeE{a_{\ldots}}{r}; \cschemeE{a_0}{r}; \text{\cleaninline{BCJumpSR}}~n~f;\\
+               \text{\cleaninline{BCPushPtrs}}; \cschemeE{a_i}{r}~\text{for all}~i\in\{n\ldots 0\}; \text{\cleaninline{BCJumpSR}}~n~f;\\
        \cschemeE{a_{f^i}}{r} & =
                \text{\cleaninline{BCArg}~findarg}(r, f, i)~\text{for all}~i\in\{w\ldots v\};\\
                {} & v = \Sigma^{i-1}_{j=0}\stacksize{a_{f^j}}~\text{ and }~ w = v + \stacksize{a_{f^i}}\\
 \end{align*}
 
-Translating the compilation schemes for functions to Clean is not as straightforward as other schemes due to the nature of shallow embedding.
+Translating the compilation schemes for functions to \gls{CLEAN} is not as straightforward as other schemes due to the nature of shallow embedding in combination with the use of state.
 The \cleaninline{fun} class has a single function with a single argument.
-This argument is a Clean function that---when given a callable Clean function representing the mTask function---will produce \cleaninline{main} and a callable function.
-To compile this, the argument must be called with a function representing a function call in mTask.
-\Cref{lst:fun_imp} shows the implementation for this as Clean code.
+This argument is a \gls{CLEAN} function that---when given a callable \gls{CLEAN} function representing the \gls{MTASK} function---produces the \cleaninline{main} expression and a callable function.
+To compile this, the argument must be called with a function representing a function call in \gls{MTASK}.
+\Cref{lst:fun_imp} shows the implementation for this as \gls{CLEAN} code.
 To uniquely identify the function, a fresh label is generated.
 The function is then called with the \cleaninline{callFunction} helper function that generates the instructions that correspond to calling the function.
 That is, it pushes the pointers, compiles the arguments, and writes the \cleaninline{JumpSR} instruction.
 The resulting structure (\cleaninline{g In m}) contains a function representing the mTask function (\cleaninline{g}) and the \cleaninline{main} structure to continue with.
 To get the actual function, \cleaninline{g} must be called with representations for the argument, i.e.\ using \cleaninline{findarg} for all arguments.
-The arguments are added to the context and \cleaninline{liftFunction} is called with the label, the argument width and the compiler.
+The arguments are added to the context using \cleaninline{infun} and \cleaninline{liftFunction} is called with the label, the argument width and the compiler.
 This function executes the compiler, decorates the instructions with a label and places them in the function dictionary together with the metadata such as the argument width.
 After lifting the function, the context is cleared again and compilation continues with the rest of the program.
 
-\begin{lstClean}[label={lst:fun_imp},caption={The backend implementation for functions.}]
+\begin{lstClean}[label={lst:fun_imp},caption={The interpretation implementation for functions.}]
 instance fun (BCInterpret a) BCInterpret | type a where
        fun def = {main=freshlabel >>= \funlabel->
                let (g In m) = def \a->callFunction funlabel (toByteWidth a) [a]
@@ -436,10 +433,11 @@ instance fun (BCInterpret a) BCInterpret | type a where
 argOf :: ((m a) -> b) a -> UInt8 | toByteWidth a
 callFunction :: JumpLabel UInt8 [BCInterpret b] -> BCInterpret c | ...
 liftFunction :: JumpLabel UInt8 (BCInterpret a) (?UInt8) -> BCInterpret ()
+infun :: JumpLabel (BCInterpret a) -> BCInterpret a
 \end{lstClean}
 
 \subsection{Tasks}\label{ssec:scheme_tasks}
-Task trees are created with the \cleaninline{BCMkTask} instruction that allocates a node and pushes it to the stack.
+Task trees are created with the \cleaninline{BCMkTask} instruction that allocates a node and pushes a pointer to it on the stack.
 It pops arguments from the stack according to the given task type.
 The following extension of $\mathcal{E}$ shows this compilation scheme (except for the step combinator, explained in \cref{ssec:step}).
 
@@ -480,21 +478,21 @@ The following extension of $\mathcal{E}$ shows this compilation scheme (except f
                        \text{\cleaninline{BCMkTask BCAnd}};\\
 \end{align*}
 
-This simply translates to Clean code by writing the correct \cleaninline{BCMkTask} instruction as exemplified in \cref{lst:imp_ret}.
+This translates to Clean code by writing the correct \cleaninline{BCMkTask} instruction as exemplified in \cref{lst:imp_ret}.
 
-\begin{lstClean}[caption={The backend implementation for \cleaninline{rtrn}.},label={lst:imp_ret}]
+\begin{lstClean}[caption={The byte code interpretation implementation for \cleaninline{rtrn}.},label={lst:imp_ret}]
 instance rtrn BCInterpret
 where
        rtrn m = m >>| tell` [BCMkTask (bcstable m)]
 \end{lstClean}
 
 \subsection{Sequential combinator}\label{ssec:step}
-The \cleaninline{step} construct is a special type of task because the task value of the left-hand side may change over time.
-Therefore, the continuation tasks on the right-hand side are \emph{observing} this task value and acting upon it.
+The \cleaninline{step} construct is a special type of task because the task value of the left-hand side changes over time.
+Therefore, the task continuations on the right-hand side are \emph{observing} this task value and acting upon it.
 In the compilation scheme, all continuations are first converted to a single function that has two arguments: the stability of the task and its value.
 This function either returns a pointer to a task tree or fails (denoted by $\bot$).
-It is special because in the generated function, the task value of a task can actually be inspected.
-Furthermore, it is a lazy node in the task tree: the right-hand side may yield a new task tree after several rewrite steps (i.e.\ it is allowed to create infinite task trees using step combinators).
+It is special because in the generated function, the task value of a task is inspected.
+Furthermore, it is a lazy node in the task tree: the right-hand side may yield a new task tree after several rewrite steps, i.e.\ it is allowed to create infinite task trees using step combinators.
 The function is generated using the $\mathcal{S}$ scheme that requires two arguments: the context $r$ and the width of the left-hand side so that it can determine the position of the stability which is added as an argument to the function.
 The resulting function is basically a list of if-then-else constructions to check all predicates one by one.
 Some optimization is possible here but has currently not been implemented.
@@ -527,17 +525,21 @@ Some optimization is possible here but has currently not been implemented.
 First the context is evaluated.
 The context contains arguments from functions and steps that need to be preserved after rewriting.
 The evaluated context is combined with the left-hand side task value by means of a \cleaninline{.&&.} combinator to store it in the task tree so that it is available after a rewrite.
-This means that the task tree is be transformed as follows:
+This means that the task tree is be transformed as follows as
 
-\begin{lstClean}
-t1 >>= \v1->t2 >>= \v2->t3 >>= ...
-//is transformed to
-t1 >>= \v1->rtrn v1 .&&. t2 >>= \v2->rtrn (v1, v2) .&&. t3 >>= ...
-\end{lstClean}
+\begin{figure}
+       \begin{subfigure}{.5\textwidth}
+               \includestandalone{contexttree1}
+
+       \end{subfigure}
+       \begin{subfigure}{.5\textwidth}
+               \includestandalone{contexttree2}
+       \end{subfigure}
+\end{figure}
 
 The translation to \gls{CLEAN} is given in \cref{lst:imp_seq}.
 
-\begin{lstClean}[caption={Backend implementation for the step class.},label={lst:imp_seq}]
+\begin{lstClean}[caption={Byte code compilation interpretation implementation for the step class.},label={lst:imp_seq}]
 instance step BCInterpret where
        (>>*.) lhs cont
                //Fetch a fresh label and fetch the context
@@ -587,7 +589,7 @@ The compilation scheme for \gls{SDS} definitions is a trivial extension to $\mat
 
 The \gls{SDS} access tasks have a compilation scheme similar to other tasks (see \cref{ssec:scheme_tasks}).
 The \cleaninline{getSds} task just pushes a task tree node with the \gls{SDS} identifier embedded.
-The \cleaninline{setSds} task evaluates the value, lifts that value to a task tree node and creates an \gls{SDS} set node.
+The \cleaninline{setSds} task evaluates the value, lifts that value to a task tree node and creates \pgls{SDS} set node.
 
 \begin{align*}
        \cschemeE{\text{\cleaninline{getSds}}~s}{r} & =
@@ -604,20 +606,24 @@ For this, an \cleaninline{BCInterpret} is created that emits this identifier.
 When passing it to the function, the initial value of the \gls{SDS} is returned.
 This initial value is stored as a byte code encoded value in the state and the compiler continues with the rest of the program.
 
+First, the initial \gls{SDS} value is extracted from the expression by bootstrapping the fixed point with a dummy value.
+This is safe because the expression on the right-hand side of the \cleaninline{In} is never evaluated.
+Then, using \cleaninline{addSdsIfNotExist}, the identifier for this particular \gls{SDS} is either retrieved from the compiler state or generated freshly.
+This identifier is then used to provide a reference to the \cleaninline{def} definition to evaluate the main expression.
 Compiling \cleaninline{getSds} is a matter of executing the \cleaninline{BCInterpret} representing the \gls{SDS}, which yields the identifier that can be embedded in the instruction.
-Setting the \gls{SDS} is similar: the identifier is retrieved and the value is written to put in a task tree so that the resulting task can remember the value it has written.
 Lifted SDSs are compiled in a very similar way \cref{sec:liftsds}.
+Setting the \gls{SDS} is similar: the identifier is retrieved and the value is written to put in a task tree so that the resulting task can remember the value it has written.
 
 % VimTeX: SynIgnore on
 \begin{lstClean}[caption={Backend implementation for the SDS classes.},label={lst:comp_sds}]
 :: Sds a = Sds Int
 instance sds BCInterpret where
-       sds def = {main = freshsds >>= \sdsi->
-                       let sds = modify (\s->{s & bcs_sdses=put sdsi
-                                               (Left (toByteCode t)) s.bcs_sdses})
-                                       >>| pure (Sds sdsi)
-                           (t In e) = def sds
-                       in e.main}
+       sds def = {main =
+                       let (t In e) = def (abort "sds: expression too strict")
+                       in addSdsIfNotExist (Left $ String255 (toByteCode{|*|} t))
+                               >>= \sdsi-> let (t In e) = def (pure (Sds sdsi))
+                                       in e.main
+               }
        getSds f   = f >>= \(Sds i)-> tell` [BCMkTask (BCSdsGet (fromInt i))]
        setSds f v = f >>= \(Sds i)->v >>| tell`
                (  map BCMkTask (bcstable (byteWidth v))
@@ -626,19 +632,18 @@ instance sds BCInterpret where
 % VimTeX: SynIgnore off
 
 \section{\texorpdfstring{\Gls{C}}{C} code generation}\label{sec:ccodegen}
-\todo[inline]{Dit is nog zeer ruw}
 All communication between the \gls{ITASK} server and the \gls{MTASK} server is type-parametrised.
 From the structural representation of the type, a \gls{CLEAN} parser and printer is constructed using generic programming.
 Furthermore, a \ccpp{} parser and printer is generated for use on the \gls{MTASK} device.
-The technique for generating the \ccpp{} parser and printer is very similar to template metaprogramming and requires a generic programming library or compiler support that includes a lot of metadata in the record and constructor nodes.
+The technique for generating the \ccpp{} parser and printer is very similar to template metaprogramming and requires a rich generic programming library or compiler support that includes a lot of metadata in the record and constructor nodes.
 Using generic programming in the \gls{MTASK} system, both serialisation and deserialisation on the microcontroller and and the server is automatically generated.
 
 \subsection{Server}
 On the server, off-the-shelve generic programming techniques are used to make the serialisation and deserialisation functions (see \cref{lst:ser_deser_server}).
 Serialisation is a simple conversion from a value of the type to a string.
-Deserialisation is a little bit different in order to support streaming\footnotemark{}.
+Deserialisation is a little bit different in order to support streaming\footnotemark.
 \footnotetext{%
-       Here the \cleaninline{*!} variant of the generic interface is chosen that has less uniqueness constraints for the compiler-generated adaptors\citep{alimarine_generic_2005,hinze_derivable_2001}.%
+       Here the \cleaninline{*!} variant of the generic interface is chosen that has less uniqueness constraints for the compiler-generated adaptors \citep{alimarine_generic_2005,hinze_derivable_2001}.%
 }
 Given a list of available characters, a tuple is always returned.
 The right-hand side of the tuple contains the remaining characters, the unparsed input.
@@ -653,16 +658,16 @@ generic fromByteCode a *! :: [Char] -> (Either String (? a), [Char])
 
 \subsection{Client}
 The \gls{RTS} of the \gls{MTASK} system runs on resource-constrained microcontrollers and is implemented in portable \ccpp{}.
-In order to still achieve some type safety, the communication between the server and the client is automated, i.e.\ the serialisation and deserialisation code in the \gls{RTS} is generated.
+In order to achieve more interoperation safety, the communication between the server and the client is automated, i.e.\ the serialisation and deserialisation code in the \gls{RTS} is generated.
 The technique used for this is very similar to the technique shown in \cref{chp:first-class_datatypes}.
 However, instead of using template metaprogramming, a feature \gls{CLEAN} lacks, generic programming is used also as a two-stage rocket.
 In contrast to many other generic programming systems, \gls{CLEAN} allows for access to much of the metadata of the compiler.
 For example, \cleaninline{Cons}, \cleaninline{Object}, \cleaninline{Field}, and \cleaninline{Record} generic constructors are enriched with their arity, names, types, \etc.
 Furthermore, constructors can access the metadata of the objects and fields of their parent records.
-Using this metadata, generic functions can be created that generate \ccpp{} type definitions, parsers and printers for any first-order \gls{CLEAN} type.
-The exact details of this technique can be found later in a paper that is in preparation\todo{noe\-men?}.
+Using this metadata, generic functions are created that generate \ccpp{} type definitions, parsers and printers for any first-order \gls{CLEAN} type.
+The exact details of this technique can be found in the future in a paper that is in preparation.
 
-\Glspl{ADT} are converted to tagged unions, newtypes to typedefs, records to structs, and arrays to dynamically size-parametrised allocated arrays.
+\Glspl{ADT} are converted to tagged unions, newtypes to typedefs, records to structs, and arrays to dynamic size-parametrised allocated arrays.
 For example, the \gls{CLEAN} types in \cref{lst:ser_clean} are translated to the \ccpp{} types seen in \cref{lst:ser_c}
 
 \begin{lstClean}[caption={Simple \glspl{ADT} in \gls{CLEAN}.},label={lst:ser_clean}]
@@ -670,7 +675,7 @@ For example, the \gls{CLEAN} types in \cref{lst:ser_clean} are translated to the
 :: NT =: NT Real
 \end{lstClean}
 
-\begin{lstArduino}[caption={Simple \glspl{ADT} in \ccpp{}.},label={lst:ser_c}]
+\begin{lstArduino}[caption={Generated \ccpp{} type definitions for the simple \glspl{ADT}.},label={lst:ser_c}]
 typedef double Real;
 typedef char Char;
 
@@ -691,23 +696,22 @@ The parser functions are parametrised by a read function, an allocation function
 This allows for the use of these functions in environments where the communication is parametrised and the memory management is self-managed such as in the \gls{MTASK} \gls{RTS}.
 
 \begin{lstArduino}[caption={Printer and parser for the \glspl{ADT} in \ccpp{}.},label={lst:ser_pp}]
-struct T parse_T(uint8_t (*get)(), void *(*alloc)(size_t), void *(*parse_0)(uint8_t (*)(), void *(*)(size_t)));
+struct T parse_T(uint8_t (*get)(), void *(*alloc)(size_t),
+                 void *(*parse_0)(uint8_t (*)(), void *(*)(size_t)));
 
-void print_T(void (*put)(uint8_t), struct T r, void (*print_0)(void (*)(uint8_t), void *));
+void print_T(void (*put)(uint8_t), struct T r,
+             void (*print_0)(void (*)(uint8_t), void *));
 \end{lstArduino}
-\todo[inline]{uitbreiden, maar niet te veel}
 
 \section{Conclusion}
 It is not straightforward to execute \gls{MTASK} tasks on resources-constrained \gls{IOT} edge devices.
 To achieve this, the terms in the \gls{DSL} are compiled to domain-specific byte code.
 This byte code is sent for interpretation to the light-weight \gls{RTS} of the edge device.
-First the expression is evaluated.
+The \gls{RTS} first evaluates the main expression.
 The result of this evaluation, a run time representation of the task, is a task tree.
 This task tree is rewritten according to rewrite rules until a stable value is observed.
 Rewriting multiple tasks at the same time is achieved by interleaving the rewrite steps, resulting in seamingly parallel execution of the tasks.
-All communication is automated.
-
-\todo[inline]{conclusion}
+Furthermore, the \gls{RTS} automates communication and coordinates multi tasking.
 
 \input{subfilepostamble}
 \end{document}
index e5102fb..079730b 100644 (file)
@@ -291,7 +291,7 @@ The tuning combinator \cleaninline{<<@} adds a label to the web editor displayin
 
 \begin{lstClean}[%
        numbers=left,
-       caption={SimpleTempSensor: a \citask{} program to read a local room temperature sensor and display it on a web page},
+       caption={SimpleTempSensor: a \citask{} program to read a local room temperature sensor and display it on a web page.},
        label={lst_t4t:itaskTemp}]
 module simpleTempSensor
 
@@ -339,7 +339,7 @@ On \cref{lst_t4t:itaskTemp:launch} \cleaninline{task} is launched with an initia
 
 \begin{lstClean}[%
        numbers=left,
-       caption={TempHistory: a tierless \citask{} webapplication that records and manipulates timed temperatures},
+       caption={TempHistory: a tierless \citask{} webapplication that records and manipulates timed temperatures.},
        label={lst_t4t:TempHistory}]
 module TempHistory
 
@@ -594,7 +594,7 @@ A similar range of commodity sensors is connected to both the Raspberry Pi and \
        \begin{subfigure}[t]{.49\textwidth}
                \centering
                \includegraphics[width=.9\textwidth]{wemosg}
-               \caption{A \gls{WEMOS} used in \gls{PWS} and \gls{CWS}}.%
+               \caption{A \gls{WEMOS} used in \gls{PWS} and \gls{CWS}.}%
        \end{subfigure}%
        \begin{subfigure}[t]{.49\textwidth}
                \centering
@@ -946,7 +946,7 @@ The sensor node measures and reports the temperature every ten seconds to the se
 
 \begin{table}
        \centering
-       \caption{Comparing \gls{CLEAN} and \gls{PYTHON} programming abstractions using the \gls{PWTS} and \gls{CWTS} temperature sensors (\gls{SLOC} and total number of files.)}%
+       \caption{Comparing \gls{CLEAN} and \gls{PYTHON} programming abstractions using the \gls{PWTS} and \gls{CWTS} temperature sensors (\gls{SLOC} and total number of files).}%
        \label{table_t4t:temp}
        \begin{tabular}{llccl}
                \toprule