From: Mart Lubbers Date: Sun, 2 Jul 2017 23:13:52 +0000 (+0200) Subject: add notion on existential types, update interface X-Git-Tag: hand-in~17 X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=f3e07851e96744138c972a7b875b6cff82c44fe5;p=msc-thesis1617.git add notion on existential types, update interface --- diff --git a/arch.example.tex b/arch.example.tex index db9a2a7..a5f3684 100644 --- 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 -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}] @@ -14,8 +14,7 @@ w = makeDevice "dev1" (...) >>= connectDevice >>= \dev2->... ... >>* [OnAction (Action "Shutdown") $ always - $ deleteDevice dev1 - >>| deleteDevice dev2 + $ deleteDevice dev1 >>| deleteDevice dev2 >>| ... >>| shutDown 0 ] @@ -23,8 +22,36 @@ w = makeDevice "dev1" (...) >>= connectDevice \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}} @@ -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. -\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) @@ -59,3 +86,11 @@ where ( 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 --- a/listings/interface.h +++ b/listings/interface.h @@ -1,24 +1,29 @@ #ifndef INTERFACE_H #define INTERFACE_H +#ifdef __cplusplus +extern "C" { +#endif + #include #include #include #ifdef LINUX -#define APINS 7 -#define DPINS 14 +#define APINS 128 +#define DPINS 128 #define STACKSIZE 1024 #define MEMSIZE 1024 #define HAVELED 1 +#define HAVEHB 1 #elif defined STM ... #endif /* Communication */ -bool input_available(void); +bool input_available(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 @@ -26,7 +31,7 @@ void write_dpin(uint8_t i, bool b); 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 @@ -36,14 +41,25 @@ void led_on(uint8_t i); 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); -void debug(char *fmt, ...); +void real_debug(char *fmt, ...); void pdie(char *s); void die(char *fmt, ...); +void reset(void); +#ifdef __cplusplus +} +#endif #endif diff --git a/mtaskext.bytecode.tex b/mtaskext.bytecode.tex index 833d964..33f5f70 100644 --- 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 -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 ())