X-Git-Url: https://git.martlubbers.net/?a=blobdiff_plain;ds=sidebyside;f=pres.mtask.tex;h=ef80aaff8672d534acf9988f3d10608e32965e2b;hb=8755061062b9738c80da1f5966c93ac6ec832a5c;hp=f878ecf89711dfacc5c1467650bccdbd4368a7f4;hpb=73ae126c560b79464769b58668f7543f7c4734c0;p=msc-thesis1617.git diff --git a/pres.mtask.tex b/pres.mtask.tex index f878ecf..ef80aaf 100644 --- a/pres.mtask.tex +++ b/pres.mtask.tex @@ -147,9 +147,108 @@ instance intArith PrettyPrinter where \item Type safe \item Embedded in Clean \item Extendable - \item \ldots\pause{} but\ldots - \item No interaction - \item Compilation requires reprogramming \end{itemize} \end{block} \end{frame} + +\begin{frame}[fragile] + \frametitle{Expressions} + \begin{block}{mTask} + \begin{itemize} + \item Two phantom types + \item Hierarchy + \end{itemize} + \end{block} + \pause{} + \begin{lstlisting} +class arith v where + lit :: t -> v t Expr + (+.) infixl 6 :: (v t p) (v t q) -> v t Expr | +, zero t & isExpr p & isExpr q + (-.) infixl 6 :: (v t p) (v t q) -> v t Expr | -, zero t & ... + ... +class boolExpr v where + Not :: (v Bool p) -> v Bool Expr | ... + (&.) infixr 3 :: (v Bool p) (v Bool q) -> v Bool Expr | ... + ... + (==.) infix 4 :: (v a p) (v a q) -> v Bool Expr | ... + \end{lstlisting} +\end{frame} + +\begin{frame}[fragile] + \frametitle{Control flow} + \begin{lstlisting} +class If v q r ~s where + If :: (v Bool p) (v t q) (v t r) -> v t s | ... + +class IF v where + IF :: (v Bool p) (v t q) (v s r) -> v () Stmt | ... + (?) infix 1 :: (v Bool p) (v t q) -> v () Stmt | ... + +instance If Code Stmt Stmt Stmt +instance If Code e Stmt Stmt +instance If Code Stmt e Stmt +instance If Code x y Expr + +class seq v where + (:.) infixr 0 :: (v t p) (v u q) -> v u Stmt | ... + \end{lstlisting} +\end{frame} + +\begin{frame}[fragile] + \frametitle{Assignment and Input/Output} + \begin{lstlisting} +:: DigitalPin = D0 | D1 | D2 ... +:: AnalogPin = A0 | A1 | A2 ... + +class dIO v where dIO :: DigitalPin -> v Bool Upd +class aIO v where aIO :: AnalogPin -> v Int Upd + +class analogRead v where + analogRead :: AnalogPin -> v Int Expr + analogWrite :: AnalogPin (v Int p) -> v Int Expr + +class digitalRead v where + digitalRead :: DigitalPin -> v Bin Expr + digitalWrite :: DigitalPin (v Bool p) -> v Int Expr + \end{lstlisting} +\end{frame} + +\begin{frame}[fragile] + \frametitle{Shared Data Sources and Assignment} + \begin{lstlisting} +:: In a b = In infix 0 a b +:: Main a = {main :: a} + +class sds v where + sds :: ((v t Upd)->In t (Main (v c s))) -> (Main (v c s)) | ... + +class assign v where + (=.) infixr 2 :: (v t Upd) (v t p) -> v t Expr | ... + \end{lstlisting} +\end{frame} + +\begin{frame}[fragile] + \frametitle{Examples} + \begin{lstlisting} +blink = task \blink=(\x. + IF (x ==. lit True) + (ledOn led) + (ledOff led) :. + blink (lit 1000) (Not x)) + In {main=blink (lit 1000) True} + +thermostat :: Main (View () Stmt) +thermostat = {main = IF (analogRead A0 >. lit 50) + ( digitalWrite D0 (lit True) ) + ( digitalWrite D0 (lit False) ) + } + +thermostat2 :: Main (View () Stmt) +thermostat2 = let a0 = aIO A0 + d0 = dIO D0 + in {main = IF (a0 >. lit 50) + (d0 =. lit True) + (d0 =. lit False) + } + \end{lstlisting} +\end{frame}