add notion on existential types, update interface

diff --git a/arch.example.tex b/arch.example.tex
index db9a2a7..a5f3684 100644 (file)
--- a/arch.example.tex
+++ b/arch.example.tex
@@ -4,7 +4,7 @@ pattern. First the devices are created --- with or without the interaction of
 the user --- and they are then connected. When all devices are registered, the
 \gls{mTask}-\glspl{Task} can be sent and \gls{iTasks}-\glspl{Task} can be
 started to monitor the output. When everything is finished, the devices are
 the user --- and they are then connected. When all devices are registered, the
 \gls{mTask}-\glspl{Task} can be sent and \gls{iTasks}-\glspl{Task} can be
 started to monitor the output. When everything is finished, the devices are

-removed and the system is powered off.
+removed and the system is shut down.

 
 \begin{lstlisting}[language=Clean,label={lst:framework},
        caption={\gls{mTask} framework for building applications}]
 
 \begin{lstlisting}[language=Clean,label={lst:framework},
        caption={\gls{mTask} framework for building applications}]


@@ -14,8 +14,7 @@ w =         makeDevice "dev1" (...) >>= connectDevice
        >>= \dev2->...
        ...
        >>* [OnAction (Action "Shutdown") $ always
        >>= \dev2->...
        ...
        >>* [OnAction (Action "Shutdown") $ always

-               $   deleteDevice dev1
-               >>| deleteDevice dev2
+               $   deleteDevice dev1 >>| deleteDevice dev2

                >>| ...
                >>| shutDown 0
        ]
                >>| ...
                >>| shutDown 0
        ]


@@ -23,8 +22,36 @@ w =         makeDevice "dev1" (...) >>= connectDevice
 
 \subsection{Thermostat}
 The thermostat is a classic example program for showing interactions between
 
 \subsection{Thermostat}
 The thermostat is a classic example program for showing interactions between

-peripherals. The following program shows a system containing two devices. One
-device is connected via \gls{TCP} and contains a temperature sensor. The second
+peripherals. The following program shows a system containing two devices. The
+first device --- the sensor -- contains a temperature sensor that measures the
+room temperature. The second device --- the actor --- contains a heater,
+connected to the digital pin \CI{D5}. Moreover, this device contains a led to
+indicate whether the heater is on. The following code shows an implementation
+for this. The code fully uses the framework. Note that a little bit of type
+twiddling is required to fully us the result from the \gls{SDS}. This approach
+is still type safe due to the type safety of \CI{Dynamic}s.
+
+\begin{lstlisting}[caption={Thermostat example}]
+thermos :: Task ()
+thermos =           makeDevice "nodeM" nodeMCU >>= connectDevice
+       >>= \nod->      makeDevice "stm32" stm32   >>= connectDevice
+       >>= \stm->      sendTaskToDevice "sensing" sensing (nod, OnInterval 1000)
+       >>= \(st, [t])->sendTaskToDevice "acting" acting (stm, OnInterval 1000)
+                       (\(BCValue s)->set (BCValue $ dynInt (dynamic s) > 0) (shareShare nod a))
+       >>| treturn ()
+where
+       dynInt :: Dynamic -> Int
+       dynInt (a :: Int) = a
+
+       sensing = sds \x=0 In {main=
+                       x =. analogRead A0 :. pub x
+               }
+       acting = sds \cool=False In {main=
+                       IF cool (ledOn LED1) (ledOff LED1) :.
+                       digitalWrite D5 cool
+               }
+       nodeMCU = TCP
+\end{lstlisting}

 
 \subsection[Lifting mTasks to iTasks-Tasks]%
        {Lifting \gls{mTask}-\glspl{Task} to \gls{iTasks}-\glspl{Task}}
 
 \subsection[Lifting mTasks to iTasks-Tasks]%
        {Lifting \gls{mTask}-\glspl{Task} to \gls{iTasks}-\glspl{Task}}


@@ -34,7 +61,7 @@ an \gls{iTasks}-\gls{Task}. The function is called with a name, \gls{mTask},
 device and interval specification and it will return a \gls{Task} that finishes
 if and only if the \gls{mTask} has returned.
 
 device and interval specification and it will return a \gls{Task} that finishes
 if and only if the \gls{mTask} has returned.
 

-\begin{lstlisting}[caption={Starting up the devices}]
+\begin{lstlisting}[caption={Lifting \gls{mTask}-\glspl{Task} to \gls{iTasks}}]

 liftmTask :: String (Main (ByteCode () Stmt)) (MTaskDevice, MTaskInterval) -> Task [MTaskShare]
 liftmTask wta mTask c=:(dev, _)= sendTaskToDevice wta mTask c
        >>= \(t, shs)->wait "Waiting for mTask to return" (taskRemoved t) (deviceShare dev)
 liftmTask :: String (Main (ByteCode () Stmt)) (MTaskDevice, MTaskInterval) -> Task [MTaskShare]
 liftmTask wta mTask c=:(dev, _)= sendTaskToDevice wta mTask c
        >>= \(t, shs)->wait "Waiting for mTask to return" (taskRemoved t) (deviceShare dev)


@@ -59,3 +86,11 @@ where
                        ( pub x :. retrn                  )
                        ( x =. x *. y :.  y =. y -. lit 1 )}
 \end{lstlisting}
                        ( pub x :. retrn                  )
                        ( x =. x *. y :.  y =. y -. lit 1 )}
 \end{lstlisting}

+
+\subsection{Heartbeat \& Oxygen Saturation Sensor}
+As an example, the addition of a new sensor will be demonstrated. The heartbeat
+and oxygen saturation sensor is a \textsc{PCB} the size of a fingernail with a
+red \gls{LED} and a light sensor on it. Moreover, it contains an \textsc{I2C}
+chip to communicate. The company producing the chip provides the programmer
+with example code for \gls{Arduino} and \textsc{mbed}. So suppose %TODO
+Adding peripheral is supposedly simple.

diff --git a/listings/interface.h b/listings/interface.h
index 7faaab2..31fa4d3 100644 (file)
--- a/listings/interface.h
+++ b/listings/interface.h
@@ -1,24 +1,29 @@
 #ifndef INTERFACE_H
 #define INTERFACE_H
 
 #ifndef INTERFACE_H
 #define INTERFACE_H
 

+#ifdef __cplusplus
+extern "C" {
+#endif
+

 #include <stdbool.h>
 #include <stdint.h>
 #include <stdarg.h>
 
 #ifdef LINUX
 #include <stdbool.h>
 #include <stdint.h>
 #include <stdarg.h>
 
 #ifdef LINUX

-#define APINS 7
-#define DPINS 14
+#define APINS 128
+#define DPINS 128

 #define STACKSIZE 1024
 #define MEMSIZE 1024
 #define HAVELED 1
 #define STACKSIZE 1024
 #define MEMSIZE 1024
 #define HAVELED 1

+#define HAVEHB 1

 #elif defined STM
 ...
 #endif
 
 /* Communication */
 #elif defined STM
 ...
 #endif
 
 /* Communication */

-bool input_available(void);
+bool    input_available(void);

 uint8_t read_byte(void);
 uint8_t read_byte(void);

-void write_byte(uint8_t b);
+void    write_byte(uint8_t b);

 
 /* Analog and digital pins */
 #if DPINS > 0
 
 /* Analog and digital pins */
 #if DPINS > 0


@@ -26,7 +31,7 @@ void write_dpin(uint8_t i, bool b);
 bool read_dpin(uint8_t i);
 #endif
 #if APINS > 0
 bool read_dpin(uint8_t i);
 #endif
 #if APINS > 0

-void write_apin(uint8_t i, uint8_t a);
+void    write_apin(uint8_t i, uint8_t a);

 uint8_t read_apin(uint8_t i);
 #endif
 
 uint8_t read_apin(uint8_t i);
 #endif
 


@@ -36,14 +41,25 @@ void led_on(uint8_t i);
 void led_off(uint8_t i);
 #endif
 
 void led_off(uint8_t i);
 #endif
 

+#if HAVEHB == 1
+uint16_t get_hb();
+bool     valid_hb();
+uint16_t get_spo2();
+bool     valid_spo2();
+#endif
+

 /* Delay and communication */
 unsigned long getmillis(void);
 void msdelay(unsigned long ms);
 
 /* Auxilliary */
 void real_setup(void);
 /* Delay and communication */
 unsigned long getmillis(void);
 void msdelay(unsigned long ms);
 
 /* Auxilliary */
 void real_setup(void);

-void debug(char *fmt, ...);
+void real_debug(char *fmt, ...);

 void pdie(char *s);
 void die(char *fmt, ...);
 void pdie(char *s);
 void die(char *fmt, ...);

+void reset(void);

 
 

+#ifdef __cplusplus
+}
+#endif

 #endif
 #endif

diff --git a/mtaskext.bytecode.tex b/mtaskext.bytecode.tex
index 833d964..33f5f70 100644 (file)
--- a/mtaskext.bytecode.tex
+++ b/mtaskext.bytecode.tex
@@ -24,7 +24,10 @@ the content. Most notably, the type must be bytecode encodable. A \CI{BCValue}
 must be encodable and decodable without losing type or value information. At
 the moment a simple encoding scheme is used that uses single byte prefixes to
 detect the type of the value. The devices know these prefixes and can apply the
 must be encodable and decodable without losing type or value information. At
 the moment a simple encoding scheme is used that uses single byte prefixes to
 detect the type of the value. The devices know these prefixes and can apply the

-same detection if necessary.
+same detection if necessary. Note that \CI{BCValue} uses existentially
+quantified type variables and therefore it is not possible to derive class
+instances such as \CI{iTasks}. Tailor-made instances for these functions have
+been made.

 
 \begin{lstlisting}[label={lst:bcview},caption={Bytecode view}]
 :: ByteCode a p = BC (RWS () [BC] BCState ())
 
 \begin{lstlisting}[label={lst:bcview},caption={Bytecode view}]
 :: ByteCode a p = BC (RWS () [BC] BCState ())