Initial commit
authorMart Lubbers <mart@martlubbers.net>
Tue, 1 Nov 2016 13:13:33 +0000 (14:13 +0100)
committerMart Lubbers <mart@martlubbers.net>
Tue, 1 Nov 2016 13:13:33 +0000 (14:13 +0100)
.gitignore [new file with mode: 0644]
Makefile [new file with mode: 0644]
gCons.dcl [new file with mode: 0644]
gCons.icl [new file with mode: 0644]
gdynamic.dcl [new file with mode: 0644]
gdynamic.icl [new file with mode: 0644]
mTask.icl [new file with mode: 0644]

diff --git a/.gitignore b/.gitignore
new file mode 100644 (file)
index 0000000..23d53e6
--- /dev/null
@@ -0,0 +1,4 @@
+Clean System Files
+mTask
+sapl
+mTask-data
diff --git a/Makefile b/Makefile
new file mode 100644 (file)
index 0000000..70565ce
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,32 @@
+CLEAN_HOME?=/opt/clean
+CLM:=clm
+CLMFLAGS+=-dynamics -l -no-pie -h 200M -t -nt
+CLMLIBS:=\
+       -I $(CLEAN_HOME)/lib/iTasks-SDK/Patches/Dynamics\
+       -I $(CLEAN_HOME)/lib/iTasks-SDK/Patches/Generics\
+       -I $(CLEAN_HOME)/lib/iTasks-SDK/Patches/StdEnv\
+       -I $(CLEAN_HOME)/lib/iTasks-SDK/Patches/TCPIP\
+       -I $(CLEAN_HOME)/lib/iTasks-SDK/Server\
+       -I $(CLEAN_HOME)/lib/iTasks-SDK/Dependencies/clean-platform/src/libraries/OS-Independent\
+       -I $(CLEAN_HOME)/lib/iTasks-SDK/Dependencies/clean-platform/src/libraries/OS-Independent/Deprecated/StdLib\
+       -I $(CLEAN_HOME)/lib/iTasks-SDK/Dependencies/clean-platform/src/libraries/OS-Posix\
+       -I $(CLEAN_HOME)/lib/iTasks-SDK/Dependencies/clean-platform/src/libraries/OS-Linux\
+       -I $(CLEAN_HOME)/lib/iTasks-SDK/Dependencies/clean-platform/src/libraries/OS-Linux-64\
+       -I $(CLEAN_HOME)/lib/iTasks-SDK/Dependencies/graph_copy/linux64\
+       -I $(CLEAN_HOME)/lib/iTasks-SDK/Dependencies/graph_copy/common\
+       -I $(CLEAN_HOME)/lib/iTasks-SDK/Dependencies/SAPL\
+       -I $(CLEAN_HOME)/lib/iTasks-SDK/Dependencies/clean-sapl/src\
+       -I $(CLEAN_HOME)/lib/iTasks-SDK/Server/lib\
+       -I $(CLEAN_HOME)/lib/StdEnv\
+       -I $(CLEAN_HOME)/lib/Generics\
+       -I $(CLEAN_HOME)/lib/Dynamics\
+       -I $(CLEAN_HOME)/lib/TCPIP\
+       -I ./CleanSerial
+
+all: mTask
+
+%: %.icl
+       $(CLM) $(CLMLIBS) $(CLMFLAGS) $(basename $<) -o $@
+
+clean:
+       $(RM) -r mTask Clean\ System\ Files
diff --git a/gCons.dcl b/gCons.dcl
new file mode 100644 (file)
index 0000000..827c637
--- /dev/null
+++ b/gCons.dcl
@@ -0,0 +1,16 @@
+definition module gCons
+
+/*
+       Pieter Koopman 2015
+       pieter@cs.ru.nl
+       Radboud University, Nijmegen, The Netherlands
+       ARDSL project
+*/
+
+import StdGeneric
+
+generic consName a :: a -> String
+derive consName CONS of {gcd_name},UNIT,PAIR,EITHER,OBJECT,RECORD,FIELD,Int,Bool,Char,(->)
+
+generic consIndex a :: a -> Int
+derive consIndex CONS of {gcd_index},UNIT,PAIR,EITHER,OBJECT,Int,Bool,Char
diff --git a/gCons.icl b/gCons.icl
new file mode 100644 (file)
index 0000000..fff9450
--- /dev/null
+++ b/gCons.icl
@@ -0,0 +1,35 @@
+implementation module gCons
+
+/*
+       Pieter Koopman 2015
+       pieter@cs.ru.nl
+       Radboud University, Nijmegen, The Netherlands
+       ARDSL project
+*/
+
+import StdEnv, StdGeneric
+
+generic consName a :: a -> String
+consName{|CONS of {gcd_name}|} f x = gcd_name
+consName{|UNIT|}   _ = "UNIT"
+consName{|PAIR|}   f g (PAIR x y) = f x
+consName{|EITHER|} f g (LEFT x)   = f x
+consName{|EITHER|} f g (RIGHT y)  = g y
+consName{|OBJECT|} f   (OBJECT x) = f x
+consName{|RECORD|} f   (RECORD x) = f x
+consName{|FIELD|}  f   (FIELD x)  = f x
+consName{|Int|}        i = toString i
+consName{|Bool|}       b = toString b
+consName{|Char|}       c = toString c
+consName{|(->)|}   f g x = g (x undef)
+
+generic consIndex a :: a -> Int
+consIndex{|CONS of {gcd_index}|} f x = gcd_index
+consIndex{|UNIT|} _ = 0
+consIndex{|PAIR|} f g (PAIR x y) = f x
+consIndex{|EITHER|} f g (LEFT x) = f x
+consIndex{|EITHER|} f g (RIGHT y) = g y
+consIndex{|OBJECT|} f (OBJECT x) = f x
+consIndex{|Int|} i = i
+consIndex{|Bool|} b = if b 1 0
+consIndex{|Char|} c = toInt c
diff --git a/gdynamic.dcl b/gdynamic.dcl
new file mode 100644 (file)
index 0000000..2dea3c1
--- /dev/null
@@ -0,0 +1,28 @@
+definition module gdynamic
+
+/*
+       Pieter Koopman 2015
+       pieter@cs.ru.nl
+       Radboud University, Nijmegen, The Netherlands
+       ARDSL project
+*/
+
+import StdGeneric, StdMaybe
+
+//:: Dyn
+
+:: DYNAMIC :== [String] 
+:: Dyn = Dyn DYNAMIC // to derive generic functions like iTask
+
+class dyn a | toGenDynamic{|*|}, fromGenDynamic{|*|} a
+
+generic   toGenDynamic a :: a -> [String]
+generic fromGenDynamic a :: [String] -> Maybe (a, [String])
+
+derive   toGenDynamic Int, Real, Char, Bool, String, UNIT, PAIR, EITHER, OBJECT, CONS of gcd, FIELD, RECORD of r
+derive fromGenDynamic Int, Real, Char, Bool, String, UNIT, PAIR, EITHER, OBJECT, CONS of gcd, FIELD, RECORD of r
+
+
+toDyn :: a -> Dyn | dyn a
+fromDyn :: Dyn -> Maybe a | dyn a
+
diff --git a/gdynamic.icl b/gdynamic.icl
new file mode 100644 (file)
index 0000000..28966bf
--- /dev/null
@@ -0,0 +1,98 @@
+implementation module gdynamic
+
+/*
+       Pieter Koopman 2015
+       pieter@cs.ru.nl
+       Radboud University, Nijmegen, The Netherlands
+       ARDSL project
+*/
+
+import StdEnv, StdGeneric, StdMaybe
+
+:: DYNAMIC :== [String]
+:: Dyn = Dyn DYNAMIC
+
+class dyn a | toGenDynamic{|*|}, fromGenDynamic{|*|} a
+derive class dyn [], (,), (,,), (,,,)
+
+//derive fromGenDynamic [], (,), (,,)
+//derive toGenDynamic [], (,), (,,)
+
+generic toGenDynamic a :: a -> [String]
+
+toGenDynamic{|Int|} x = [toString x]
+toGenDynamic{|Real|} x = [toString x]
+toGenDynamic{|Char|} x = ["'" +++ toString x +++ "'"]
+toGenDynamic{|String|} x = ["\"" +++ toString x +++ "\""]
+toGenDynamic{|Bool|} x = [toString x]
+toGenDynamic{|UNIT|} x = []
+toGenDynamic{|PAIR|} f g (PAIR x y) = f x ++ g y
+toGenDynamic{|EITHER|} f g (LEFT x) = f x
+toGenDynamic{|EITHER|} f g (RIGHT y) = g y
+toGenDynamic{|OBJECT|} f (OBJECT x) = f x
+toGenDynamic{|CONS of gcd|} f (CONS x) = [gcd.gcd_name:f x]
+toGenDynamic{|FIELD|} f (FIELD x) = f x
+toGenDynamic{|RECORD of r|} f (RECORD x) = [r.grd_name:f x]
+
+// ----------------------------
+
+generic fromGenDynamic a :: [String] -> Maybe (a, [String])
+fromGenDynamic{|UNIT|} l = Just(UNIT,l)
+fromGenDynamic{|Char|} [a:x] 
+       | size a == 3 && a.[0] == '\'' && a.[2] == '\''
+               = Just (toChar a.[1],x)
+               = Nothing
+fromGenDynamic{|String|} [a:x]
+       # len = size a
+       | len >= 2 && a.[0] == '"' && a.[len-1] == '"'
+               = Just (a%(1,len-2),x)
+               = Nothing
+fromGenDynamic{|String|} [] = Nothing
+fromGenDynamic{|Bool|} ["True" :l] = Just (True ,l)
+fromGenDynamic{|Bool|} ["False":l] = Just (False,l)
+fromGenDynamic{|Bool|} l = Nothing
+fromGenDynamic{|Int|} [a:x] = if (toString i == a) (Just (i,x)) Nothing where i = toInt a
+fromGenDynamic{|Int|} [] = Nothing
+fromGenDynamic{|Real|} [a:x] = if (toString i == a) (Just (i,x)) Nothing where i = toReal a
+fromGenDynamic{|Real|} [] = Nothing
+fromGenDynamic{|PAIR|} f g l =
+       case f l of
+               Just (x,l) = case g l of
+                                               Just (y,l) = Just (PAIR x y, l)
+                                               _ = Nothing
+               _ = Nothing
+fromGenDynamic{|EITHER|} f g l =
+       case f l of
+               Just (x,l) = Just (LEFT x,l)
+               _ = case g l of
+                               Just (x,l) = Just (RIGHT x,l)
+                               _ = Nothing
+fromGenDynamic{|OBJECT|} f l = case f l of  Just (x,l) = Just (OBJECT x,l); _ = Nothing
+fromGenDynamic{|FIELD|} f l = case f l of  Just (x,l) = Just (FIELD x,l); _ = Nothing
+fromGenDynamic{|RECORD of r|} f [n:l] | n == r.grd_name
+    = case f l of
+       Just (x,l) = Just (RECORD x,l)
+       _ = Nothing
+    = Nothing
+fromGenDynamic{|CONS of gcd|} f l
+       | [gcd.gcd_name] == take 1 l
+               = case f (tl l) of  Just (x,l) = Just (CONS x,l); _ = Nothing
+               = Nothing
+
+// ----------------------------
+
+toDyn :: a -> Dyn | dyn a
+toDyn a = Dyn (toGenDynamic{|*|} a)
+
+fromDyn :: Dyn -> Maybe a | dyn a
+fromDyn (Dyn a) =
+       case fromGenDynamic{|*|} a of 
+               Just (x,[]) = Just x
+               _ = Nothing 
+
+Start1 = toLIBC (toDyn [(1,True,'a'),(2,False,'1')])
+Start = toGenDynamic{|*->*|} (\b.if b ["I"] ["O"]) [True,False,True]
+
+toLIBC :: Dyn -> Maybe [(Int,Bool,Char)]
+toLIBC l = fromDyn l
+
diff --git a/mTask.icl b/mTask.icl
new file mode 100644 (file)
index 0000000..6c6ddc5
--- /dev/null
+++ b/mTask.icl
@@ -0,0 +1,1553 @@
+module mTask
+
+/*
+    Pieter Koopman pieter@cs.ru.nl
+    Final version for TFP2016
+    
+    -2: assignment =. suited for digital and analog input and output
+    -3: ad hoc tasks
+    
+todo:
+       move task-loop ti setup()
+       adhoc tasks
+       task combinators
+       imporove setp: >>*.
+*/
+
+import iTasks
+import gdynamic, gCons, GenEq, StdMisc, StdArray
+
+// =================== examples ===================
+
+Start =
+    [["//mTaskTFP16_3 \n"]
+/*  ,["// --- p1 \n"]
+  ,compile p1
+    ,["// --- p2 \n"]
+  ,compile p2
+    ,["// --- p3 \n"]
+  ,compile p3
+    ,["// --- p4 \n"]
+  ,compile p4
+    ,["// --- p5 \n"]
+  ,compile p5
+    ,["// --- p6 \n"]
+  ,compile p6
+    ,["// --- p7 \n"]
+  ,compile p7
+    ,["// --- p8 \n"]
+  ,compile p8
+    ,["// --- p9 \n"]
+  ,compile p9
+    ,["// --- p10 \n"]
+  ,compile p10
+    ,["// --- p11 \n"]
+  ,compile p11
+    ,["// --- p12 \n"]
+  ,compile p12
+    ,["// --- fac \n"]
+  ,compile fac
+    ,["// --- blink \n"]
+  ,compile blink
+    ,["// --- heatingDemo \n"]
+  ,compile heatingDemo
+    ,["// --- hpinDemo \n"]
+  ,compile pinDemo
+    ,["// --- blink2 \n"]
+  ,compile blink2
+  ,["// --- blink3 \n"]
+  ,compile blink3
+  ,["// --- blinks \n"]
+  ,compile blinks
+  ,["// --- lcdCount \n"]
+  ,compile lcdCount
+*/
+  ,["// --- heating \n"]
+  ,compile heating
+  ]
+
+lcdHello = LCD 16 2 [] \lcd = {main = print lcd (lit "Hello world")}
+
+lcdCount =
+       LCD 16 2 [] \lcd =
+       task \t = (\c.
+               If (pressed upButton) (
+                       setCursor lcd Zero Zero :.
+                       print lcd c :.
+                       t (sec 1) (c +. One)
+               ) (t (msec 10) c)) In
+       {main = t (sec 0) Zero}
+printD0 = {main = serialPrint (Not d0)}
+
+print36 = sds \x = 6 In {main = x =. x *. x :. serialPrint x}
+
+pinDemo =
+    {main = a1 =. a0 =. lit 1 +. a0 :.  a0 =. Not a0}
+
+fac = fun \fac = (\n. If (n <. One) One (n *. fac (n -. One)))
+    In {main = fac (lit 6)}
+One = lit 1
+Zero = lit 0
+
+blink =
+  task \t = (\s. setLED s :. t (If s (sec 1) (sec 3)) (Not s)) In {main = t (sec 0) (lit True)}
+blink2 =
+  task \t = (\(). d13 =. Not d13 :. t (sec 1) ()) In {main = t (sec 0) ()}
+blink3 =
+  task \t = (\s. d13 =. s :. t (If s (msec 100) (sec 1)) (Not s)) In {main = t (sec 0) (lit False)}
+blinks =
+       task \t = (\b. d13 =. b :. t (sec 1) b) In {main = t (msec 0) true :. t (msec 100) false}
+
+setLED b = d13 =. b
+sec n = long (lit (n * 1000))
+msec n = long (lit n)
+
+qt = task \plus = (\(x,y).x +. y) In {main = plus (sec 0) (lit 3, lit 4)}
+qs = fun  \plus = (\(x,y).x +. y) In {main = plus (lit 3, lit 4)}
+
+q1 =
+ tasks \(switch, heat) = 
+  (\s1 = digitalWrite D2 s1:. heat (sec 60) s1
+    ,\s2 = analogRead A3 >>*. \v.
+    [Cond (v >. upper) (switch (sec 0) off)
+    ,Cond (v <. lower) (switch (sec 0) on)
+    ,Ever (heat (sec 1) s2)
+    ])
+ In {main = heat (sec 0) off}
+where
+    upper = lit 876
+    lower = lit 123
+
+serialReadInt = serialParseInt >>=. \i. serialRead >>*. \c. [Cond (c ==. lit '\n') i]
+
+heating =
+  sds \goal     = 500 In
+  fun \switch   = (\s. d13 =. s) In
+  task \control = (\isOn. 
+    a0 <. goal >>*. \mustOn.
+    [Cond (Not isOn &. mustOn) (switch on :. control minOnTime on)
+    ,Cond (isOn &. Not mustOn) (switch off:. control minOffTime off)
+    ,Ever (control (msec 100) isOn)
+   ]) In
+  task \change = (\().
+    serialAvailable ? (serialReadInt >>=. \g.goal =. g) :.
+    change (sec 1) ()) In
+  {main = switch off :. control (sec 0) off :. change (sec 1) ()}
+where
+  minOnTime  = sec 2
+  minOffTime = sec 1
+
+heating2 =
+  sds \goal = 500 In
+//  fun \switch  = setLED In
+  fun \switch  = (\b. setLED b :. serialPrintln b) In
+  task \control = (\isOn. 
+   a0 <. goal >>*. \mustOn.
+    [Cond (Not isOn &. mustOn) (switch on :. control minOnTime on)
+    ,Cond (isOn &. Not mustOn) (switch off:. control minOffTime off)
+    ,Ever (control (msec 100) isOn)
+   ]) In
+  task \change = (\().
+    serialAvailable ? (serialReadInt >>=. \i. serialPrintln (goal =. i)) :.
+    change (sec 1) ()) In
+  {main = switch off :. control (sec 0) off :. change (sec 1) ()}
+where
+  minOnTime  = sec 2
+  minOffTime = sec 1
+
+thermoTask =
+       sds \goal = 500 In
+       fun \switch = (\on. d13 =. bool on :. a0 =. on) In
+       task \control =
+               (\isOn. a0 <. goal >>*. \mustOn.
+                       [Cond (mustOn &. Not isOn) (switch mustOn :. control minOnTime mustOn)
+                       ,Cond (Not mustOn &. isOn) (switch mustOn :. control minOffTime mustOn)
+                       ,Ever (control (msec 100) isOn)
+                       ]) In
+       {main = switch off :. control (sec 0) off}
+where
+       minOnTime = sec 1 // 60
+       minOffTime = sec 2 //10
+       off = lit False
+
+heatingDemo =
+ sds \heat = False In
+ sds \temp = 500 In
+ LCD 16 2 [] \lcd.
+ task \tempChange = (\().
+    lit 0 <. temp &. Not heat ? temp =. temp -. One:.
+    temp <. lit 1000 &. heat ? temp =. temp +. One :.
+    setCursor lcd (lit 5) Zero :.
+    print lcd (lit "temp ") :.
+    print lcd temp :.
+    print lcd (lit " ") :.
+    tempChange (msec 789) ()) In
+ fun  \switch  = (\s.
+  heat =. s :.
+    setCursor lcd Zero Zero :.
+    If s
+        (print lcd (lit "On "))
+        (print lcd (lit "Off"))) In
+ fun \measure = (\(). 
+    analogRead A0 >>=. \a0.
+    setCursor lcd Zero One :.
+    print lcd a0 :.
+    print lcd (lit "   ") :.
+  a0) In
+ task \control = (\isOn. 
+   measure () >>=. \val.temp <. val
+   >>*. \mustOn.
+    [Cond (Not isOn &. mustOn) (switch on :. control minOnTime on)
+    ,Cond (isOn &. Not mustOn) (switch off:. control minOffTime off)
+    ,Ever (control (msec 100) isOn)
+   ] 
+   ) In
+ {main = switch off :. control (msec 10) off :. tempChange (sec 0) ()}
+where
+  limit   = lit 512
+  minOnTime  = sec 3
+  minOffTime = sec 2
+true = lit True
+on = true
+false = lit False
+off = false
+
+count =
+    LCD 16 2 [] \lcd.
+    task \count = (\n. 
+      setCursor lcd Zero Zero :.
+      print lcd n :.
+      count (sec 1) (n +. One)) In
+    {main = count (sec 0) Zero}
+
+p0 = sds \x = 6 In {main = x =. x *. lit 7}
+p1 = {main = lit 2 +. lit 4 >>=. \x. (x +. lit 1) *. x}
+p2 =
+    fun \f. (\x. lit 6 *. x)
+    In {main = lit 3 +. lit 4 >>=. \x. f x}
+p3 =
+    fun \f. (\x. lit 6 *. x)
+    In {main = lit 3 +. lit 4 >>=. f} // higher order, somewhat remarkable that this works
+p4 =
+    fun \f. (\x. lit 6 *. x)
+    In {main = lit 3 +. lit 4 >>=. \x. f x >>=. serialPrint}
+p5 = {main = lit 7 >>*. \x. [Cond (x <. lit 36) (x *. x),Ever (lit 42)]}
+p6 = sds \y = 1 In {main = lit 7 >>*. \x. [Cond (x <. lit 36) (y =. x *. x),Ever (y =. x)]}
+p7 = sds \y = 1 In {main = y +. lit 1 >>*. \x. [Cond (x <. lit 36) ((y =. x *. x) >>*. \z.[Cond (z ==. x) y, Ever y]),Ever (y =. x)]}
+p8 = sds \y = 1 In {main = pressed upButton >>*. \x. [Cond x (y =. y +. y),Ever (y =. lit 36)]}
+//p8 = sds \y = 1 In {main = pressed upButton >>*. \x. [Cond x ((y =. lit 42) >>*. \z.[Cond (z ==. y) y, Ever y]),Ever (y =. lit 36)]}
+//p9 = {main = If (pressed upButton) (lit 1) (lit 7)} // Overloading error [mTaskTFP16.icl,61,p9]: "isExpr" no instance available of type Stmt
+p9 = {main = pressed upButton >>=. \b.If b (lit 1) (lit 7)}
+p10 = 
+    sds \y = 1 In 
+    {main = 
+        (pressed upButton >>*. \x. 
+            [Cond x (y =. y +. y :.
+             x)
+            ,Ever (y =. lit 36 :.
+             lit False)
+            ])
+        >>=. \z. z &. z}
+p11 =
+    sds \y = 1 In
+    {main = 
+         y =. lit 2 :.
+         (pressed upButton >>=. \b.
+          If b
+            (y =. lit 3 :.
+             y +. lit 1)
+            (lit 42))
+        >>*. \x.
+            [Cond (x <. lit 36)
+                    ((y =. x *. x) >>*. \z.
+                        [Cond (z ==. x) (serialPrint y)
+                        ,Ever (serialPrint (lit 0))
+                        ])
+            ,Ever (y =. x)
+            ]
+    }
+p12 =
+    task \t = (\(). pressed upButton >>*. \b.[Cond b (serialPrintln (lit 7)),Ever (t (lit 250) ():. lit 0)]) In
+    {main = t (lit 0) ()}
+
+// ----- serial definition ----- //
+
+class serial v where
+  serialAvailable :: (v Bool Expr)
+  serialPrint     :: (v t p) -> v Int Expr | stringQuotes t & isExpr p
+  serialPrintln   :: (v t p) -> v Int Expr | stringQuotes t & isExpr p
+  serialRead      :: (v t Expr)
+  serialParseInt  :: (v Int Expr)
+
+instance serial Code where
+  serialAvailable = embed (c "Serial.available()")
+  serialPrint   x = embed (c "Serial.print(" +.+ x +.+ c ")")
+  serialPrintln x = embed (c "Serial.println(" +.+ x +.+ c ")")
+  serialRead      = embed (c "Serial.read()")
+  serialParseInt  = embed (c "Serial.parseInt()")
+
+instance serial Eval where
+  serialAvailable = rtrn False
+  serialPrint   x = x >>==  \a.E \r s.let str = toCode a in (size str,{s & serial = s.serial ++ [str]})
+  serialPrintln x = x >>==  \a.E \r s.let str = toCode a + "\n" in (size str,{s & serial = s.serial ++ [str]})
+  serialRead      = rtrn undef
+  serialParseInt  = rtrn undef
+
+class char2int v :: (v Char p) -> v Int Expr
+instance char2int Code where char2int (C f) = C \rw c.f Rd c 
+
+:: SerialObject v t p =
+  { available :: v Bool Expr
+  , print     :: (v t p) -> v Int Expr
+  , println   :: (v t p) -> v Int Expr
+  , read      :: (v Char Expr)
+  }
+
+// =================== shields ===================
+
+// ----- LCD definition ----- //
+
+:: LCD =
+  { cursorRow :: Int
+  , cursorCol :: Int
+  , sizeH     :: Int
+  , sizeW     :: Int
+  , lcdtxt    :: [String]
+  }
+
+:: Button = RightButton | UpButton | DownButton | LeftButton | SelectButton | NoButton
+
+rightButton = lit RightButton
+upButton = lit UpButton
+downButton = lit DownButton
+leftButton = LeftButton
+selectButton = lit SelectButton
+noButton = lit NoButton
+
+class lcd v where
+  begin          :: (v LCD Expr) (v Int p) (v Int q) -> v () Expr
+  print          :: (v LCD Expr) (v t p) -> v Int Expr  | stringQuotes t     // returns bytes written
+  setCursor      :: (v LCD Expr) (v Int p) (v Int q) -> v () Expr
+  liquidCrystal0 :: [DigitalPin] ((v LCD Expr)->Main (v b q)) -> Main (v b q)
+  LCD            :: Int Int [DigitalPin] ((v LCD Expr)->Main (v b q)) -> Main (v b q)
+  scrollLeft     :: (v LCD Expr) -> v () Expr
+  scrollRight    :: (v LCD Expr) -> v () Expr
+  pressed        :: (v Button Expr) -> v Bool Expr
+
+instance lcd Code where
+  begin     v x y = embed (v +.+ c ".begin" +.+ codeOp2 x ", " y)
+  print     v x   = embed (v +.+ c ".print (" +.+ stringQuotes x +.+ c ")")
+  setCursor v x y = embed (v +.+ c ".setCursor" +.+ codeOp2 x ", " y)
+  scrollLeft  v   = embed (v +.+ c ".scrollDisplayLeft()")
+  scrollRight v   = embed (v +.+ c ".scrollDisplayRight()")
+  liquidCrystal0 [] f = liquidCrystal0 [D8, D9, D4, D5, D6, D7] f
+  liquidCrystal0 pins f =
+    {main =
+     getCode \cd. fresh \n.
+      let
+          name = "lcd" + toString n
+          rest = f (c name)
+      in
+      include "LiquidCrystal" +.+
+      setCode Var +.+
+        c ("LiquidCrystal " + name + "(" + argList pins + ");\n") +.+
+      setCode cd +.+
+        rest.main
+    }
+  LCD x y [] f = LCD x y [D8, D9, D4, D5, D6, D7] f
+  LCD x y pins f =
+    {main =
+     getCode \cd. fresh \n.
+      let
+          name = "lcd" + toString n
+          rest = f (c name)
+      in
+          include "LiquidCrystal" +.+
+          setCode Var +.+
+            c ("LiquidCrystal " + name + "(" + argList pins + ");\n") +.+
+          setCode Setup +.+
+            c (name + ".begin(" + toCode x + ", " + toCode y +");") +.+ nl +.+
+          setCode cd +.+
+            rest.main
+    }
+  pressed b = embed (c "pressed(" +.+ setMode SubExp +.+ b +.+ c ")")
+
+RightBound  = 50
+UpBound   = 190
+DownBound   = 380
+LeftBound   = 555
+SelectBound = 790
+
+instance lcd Eval where
+  begin   (E v) x y = 
+   x >>== \w. 
+   y >>== \h. 
+   yield () (E \r.v (Updt \lcd.{lcd & sizeH = h, sizeW = w, lcdtxt = repeatn h (toString (repeatn w ' '))}))
+  print   (E v) x   =
+    x >>== \a. let str = toCode a in 
+    yield (size str) (E \r.v (Updt \lcd.lcdPrintStr str lcd))
+  setCursor (E v) x y = 
+    x >>== \w.
+    y >>== \h.
+    yield () (E \r.v (Updt \lcd.{lcd & cursorRow = h, cursorCol = w}))
+  scrollLeft  v = rtrn ()
+  scrollRight v = rtrn ()
+  LCD w h pins f = defEval2 lcd f where
+      lcd =
+              { cursorRow = 0
+              , cursorCol = 0
+              , sizeH = h
+              , sizeW = w
+              , lcdtxt = repeatn h (toString (repeatn w ' '))
+              }
+  liquidCrystal0 pins f = defEval2 lcd f where
+    lcd =
+          { cursorRow = 0
+          , cursorCol = 0
+          , sizeH = 0
+          , sizeW = 0
+          , lcdtxt = []
+          }
+  pressed b = rtrn False
+
+lcdPrintStr str lcd
+  | lcd.cursorRow < 0 || lcd.cursorRow >= length lcd.lcdtxt ||
+    lcd.cursorCol < 0 || lcd.cursorCol >= size (lcd.lcdtxt !! lcd.cursorRow)
+    = lcd
+  # line = lcd.lcdtxt !! lcd.cursorRow
+  # endPos = size str + lcd.cursorCol
+  | endPos >= lcd.sizeW
+      # newLine = line % (0, lcd.cursorCol - 1) + str % (0, size str - lcd.cursorCol)
+    = {lcd & lcdtxt = updateAt lcd.cursorRow newLine lcd.lcdtxt, cursorCol = lcd.sizeW - 1}
+    # newLine = line % (0, lcd.cursorCol - 1) + str + line % (endPos, lcd.sizeW - 1)
+    = {lcd & lcdtxt = updateAt lcd.cursorRow newLine lcd.lcdtxt, cursorCol = endPos}
+
+printAt :: (v LCD Expr) (v Int b) (v Int c) (v t e) -> v Int Stmt 
+    | lcd, seq v & stringQuotes t
+printAt lcd x y z = setCursor lcd x y :. print lcd z
+
+keySwitch :: (a Int b) (a c d,a c e,a c f,a c g,a c h,a c a0) -> a c Stmt | arith, boolExpr, seq a & If a h a0 b0 & If a g b0 c0 & If a f c0 d0 & If a e d0 e0 & If a d e0 f0 & type c
+keySwitch v (right, up, down, left, select, nokey)
+ =  v >>=. \w.
+  If (w <. lit RightBound)
+    right
+  (If (w <. lit UpBound)
+    up
+  (If (w <. lit DownBound)
+    down
+  (If (w <.lit  LeftBound)
+    left
+  (If (w <. lit SelectBound)
+    select
+    nokey
+  ))))
+
+// =================== mTask ===================
+
+
+// ----- dsl definition ----- //
+
+:: DigitalPin 
+   = D0 | D1 | D2 | D3 | D4 | D5 |D6 | D7 | D8 | D9 | D10 | D11 | D12 | D13
+:: AnalogPin = A0 | A1 | A2 | A3 | A4 | A5
+:: PinMode   = INPUT | OUTPUT | INPUT_PULLUP
+:: Pin     = Digital DigitalPin | Analog AnalogPin
+instance toCode Pin where
+    toCode (Digital p) = toCode p
+    toCode (Analog  p) = toCode p
+instance toCode Button where toCode b = toCode (consIndex{|*|} b)
+derive consIndex Button
+
+class pin p | type, == p where
+  pin :: p -> Pin
+instance pin DigitalPin where
+       pin p = Digital p
+instance pin AnalogPin  where
+  pin p = Analog  p
+
+:: Upd   = Upd
+:: Expr  = Expr
+:: Stmt  = Stmt
+:: MTask = MTask Int // String
+
+class isExpr a :: a -> Int
+instance isExpr Upd  where isExpr _ = 0
+instance isExpr Expr where isExpr _ = 1
+
+class isStmt a :: a -> Int
+instance isStmt Upd where isStmt _ = 10
+instance isStmt Expr   where isStmt _ = 11
+instance isStmt Stmt   where isStmt _ = 12
+
+instance == MTask where (==) (MTask x) (MTask y) = x == y
+instance toCode MTask where toCode (MTask x) = "Task " + toCode x 
+
+:: Main a = {main :: a}
+
+unMain :: (Main x) -> x
+unMain m = m.main //{main=x} = x
+
+class arith v where
+  lit :: t -> v t Expr | toCode t
+  (+.) infixl 6 :: (v t p) (v t q) -> v t Expr | type, +, zero t & isExpr p & isExpr q //& toExpr2 p & toExpr2 q
+  (-.) infixl 6 :: (v t p) (v t q) -> v t Expr | type, -, zero t & isExpr p & isExpr q //& toExpr2 p & toExpr2 q
+  (*.) infixl 7 :: (v t p) (v t q) -> v t Expr | type, *, zero, one t & isExpr p & isExpr q //& toExpr2 p & toExpr2 q
+  (/.) infixl 7 :: (v t p) (v t q) -> v t Expr | type, / t & isExpr p & isExpr q //& toExpr2 p & toExpr2 q
+class boolExpr v where
+  (&.) infixr 3 :: (v Bool p) (v Bool q) -> v Bool Expr | isExpr p & isExpr q //& toExpr2 p & toExpr2 q
+  (|.) infixr 2 :: (v Bool p) (v Bool q) -> v Bool Expr | isExpr p & isExpr q //& toExpr2 p & toExpr2 q
+  Not           :: (v Bool p) -> v Bool Expr | isExpr p //& toExpr2 p
+  (==.) infix 4 :: (v a p) (v a q) -> v Bool Expr | ==, toCode a & isExpr p & isExpr q //& toExpr2 p & toExpr2 q
+  (!=.) infix 4 :: (v a p) (v a q) -> v Bool Expr | ==, toCode a & isExpr p & isExpr q //& toExpr2 p & toExpr2 q
+  (<.)  infix 4 :: (v a p) (v a q) -> v Bool Expr | <, Ord,  toCode a & isExpr p & isExpr q //& toExpr2 p & toExpr2 q
+  (>.)  infix 4 :: (v a p) (v a q) -> v Bool Expr | <, Ord,  toCode a & isExpr p & isExpr q //& toExpr2 p & toExpr2 q
+  (<=.) infix 4 :: (v a p) (v a q) -> v Bool Expr | <, Ord,  toCode a & isExpr p & isExpr q //& toExpr2 p & toExpr2 q
+  (>=.) infix 4 :: (v a p) (v a q) -> v Bool Expr | <, Ord,  toCode a & isExpr p & isExpr q //& toExpr2 p & toExpr2 q
+// using functional dependencies
+class If v q r ~s where
+  If :: (v Bool p) (v t q) (v t r) -> v t s | isExpr p & type t
+class IF v where
+  IF :: (v Bool p) (v t q) (v s r) -> v () Stmt | isExpr p
+  (?) infix 1 :: (v Bool p) (v t q) -> v () Stmt | isExpr p
+class var2 v where
+  var2 :: t ((v t Upd)->(Main (v c s))) -> (Main (v c s)) | type, toCode t
+  con2 :: t ((v t Expr)  ->(Main (v c s))) -> (Main (v c s)) | type t
+class sds v where
+  sds :: ((v t Upd)->In t (Main (v c s))) -> (Main (v c s)) | type, toCode t
+  con :: ((v t Expr)  ->In t (Main (v c s))) -> (Main (v c s)) | type t
+class seq v where
+  (>>=.) infixr 0 :: (v t p) ((v t Expr) -> (v u q)) -> (v u Stmt) | type t & type u
+  (:.) infixr 0 :: (v t p) (v u q) -> v u Stmt | type t & type u
+class step v where
+    (>>*.) infixl 1 :: (v t p) ((v t Expr) -> [Step v u]) -> v u Stmt | type t & type u
+:: Step v t = E.p.q: Cond (v Bool q) (v t p) | E.p: Ever (v t p)
+class assign v where
+  (=.) infixr 2 :: (v t Upd) (v t p) -> v t Expr | type t & isExpr p
+class fun v t where
+  fun :: ((t->v s Expr)->In (t->v s p) (Main (v u q))) -> Main (v u q) | type s
+class mtask v a where
+  task :: (((v delay r) a->v MTask Expr)->In (a->v u p) (Main (v t q))) -> Main (v t q) | type t & type u & isExpr r & long v delay
+class lag v where
+  lag :: (v delay r) (v t p) -> v MTask Expr | type t & long v delay
+class setDelay v where
+  setDelay :: (v Long p) (v MTask Expr) -> (v MTask Expr) | isExpr p
+class mtasks v a b where
+  tasks :: (((v delay r1) a->v MTask Expr, (v delay r2) b->v MTask Expr)->In (a->v t p, b->v u p) (Main (v s q))) -> Main (v s q) | type s & isExpr r1 & isExpr r2 & long v delay
+class output v where
+  output :: (v t p) -> v () Expr | type t & isExpr p
+class noOp v where noOp :: v t p
+
+class pinMode v where
+  pinmode :: p PinMode -> v () Expr | pin p
+class digitalIO v where
+  digitalRead  :: p -> v Bool Expr | pin, readPinD p
+  digitalWrite :: p (v Bool q) -> v Bool Expr | pin, writePinD  p
+class analogIO v where
+  analogRead  :: AnalogPin -> v Int Expr 
+  analogWrite :: AnalogPin (v Int p) -> v Int Expr 
+class dIO v where
+    dIO :: p -> v Bool Upd | pin, readPinD p
+class aIO v where
+    aIO :: AnalogPin -> v Int Upd
+class time v where
+  delay  :: (v Long p) -> (v Long Expr)
+  millis ::         (v Long Expr)
+
+class pio p t where pio :: p -> v t Upd | aIO v & dIO v
+instance pio AnalogPin Int where pio p = aIO p
+instance pio AnalogPin Bool where pio p = dIO p
+instance pio DigitalPin Bool where pio p = dIO p
+
+a0 = pio A0
+a1 = pio A1
+a2 = pio A2
+a3 = pio A3
+a4 = pio A4
+a5 = pio A5
+
+d0 = pio D0
+d1 = pio D1
+d2 = pio D2
+d3 = pio D3
+d4 = pio D4
+d5 = pio D5
+d6 = pio D6
+d7 = pio D7
+d8 = pio D8
+d9 = pio D9
+d10 = pio D10
+d11 = pio D11
+d12 = pio D12
+d13 = pio D13
+
+int :: (v Int p) -> (v Int p)
+int x = x
+bool :: (v Bool p) -> (v Bool p)
+bool x = x
+char :: (v Char p) -> (v Char p)
+char x = x
+
+class type t | showType, dyn, toCode, ==, type2string, varName t
+class type2string t :: t -> String
+instance type2string Int        where type2string _ = "int"
+instance type2string Long       where type2string _ = "long"
+instance type2string Real       where type2string _ = "float"
+instance type2string Bool       where type2string _ = "bool" //"boolean"
+instance type2string Char       where type2string _ = "char"
+instance type2string MTask      where type2string _ = "task"
+instance type2string DigitalPin where type2string _ = "int"
+instance type2string AnalogPin  where type2string _ = "int"
+instance type2string String     where type2string _ = "Char []"
+instance type2string ()         where type2string _ = ""
+class varName a :: a -> String
+instance varName Int    where varName _ = "vInt"
+instance varName Long   where varName _ = "vLong"
+instance varName Bool   where varName _ = "vBool"
+instance varName Char   where varName _ = "vChar"
+instance varName Real   where varName _ = "vFloat"
+instance varName x      where varName _ = ""
+
+class dsl t | arith, boolExpr, sds, assign, seq t 
+
+argType :: (((Code a p)->Code b q)->In ((Code a p)->Code b q) (Code c s)) -> a | type a
+argType f = undef
+
+class argTypes t :: ((t->Code b Expr)->In (t->Code b2 q) (Main (Code c s))) -> t
+instance argTypes (Code a p) | showType a where argTypes f = showType
+instance argTypes (Code a p, Code b q) | showType a & showType b where argTypes f = (showType, showType)
+instance argTypes (Code a p, Code b q, Code c r) | showType a & showType b & showType c where argTypes f = (showType, showType, showType)
+
+resType :: ((t->Code b Expr)->In (t->Code b q) (Main (Code c s))) -> Code b q | showType b
+resType f = showType
+
+var2Type :: (Code t p) -> Code t p | showType t
+var2Type x = showType
+
+resType2 :: ((t->Code b Expr)->In (t->Code b q) (Main (Code c s))) -> SV b | showType2 b
+resType2 f = showType2
+
+:: SV t = SV String
+instance toCode (SV t) where toCode (SV s) = s
+
+class showType2 t :: SV t
+instance showType2 ()   where showType2 = SV "void "
+instance showType2 Int  where showType2 = SV "int "
+instance showType2 Char where showType2 = SV "char "
+instance showType2 Bool where showType2 = SV "bool "
+instance showType2 a    where showType2 = SV "word /* default */"
+
+class showType t | showType2 /*, type*/ t :: (Code t p)
+instance showType ()   where showType = c "void "
+instance showType Int  where showType = c "int "
+instance showType Long where showType = c "long "
+instance showType Char where showType = c "char "
+instance showType Bool where showType = c "bool "
+instance showType a    where showType = c "word /* default */ "
+
+class typeSelector t | showType2, type t :: (Code t p)
+instance typeSelector Int  where typeSelector = c ".i"
+instance typeSelector Char where typeSelector = c ".c"
+instance typeSelector Bool where typeSelector = c ".b"
+instance typeSelector a    where typeSelector = c ".w"
+
+:: In a b = In infix 0 a b
+
+read :: Int (ReadWrite a) State -> (a,State) | dyn a
+read n Rd       s = (fromJust (fromDyn (s.store !! n)), s)
+read n (Wrt a)  s = (a,{s&store=updateAt n (toDyn a) s.store})
+read n (Updt f) s=:{store}
+  # obj = f (fromJust (fromDyn (store !! n)))
+  = (obj, {s & store = updateAt n (toDyn obj) store})
+
+// ----- code generation ----- //
+
+instance arith Code where
+  lit a = embed (c a)
+  (+.) x y = codeOp2 x " + " y 
+  (-.) x y = codeOp2 x " - " y 
+  (*.) x y = codeOp2 x " * " y
+  (/.) x y = codeOp2 x " / " y
+instance boolExpr Code where
+  (&.) x y  = codeOp2 x " && " y
+  (|.) x y  = codeOp2 x " || " y
+  Not x     = embed (brac (c "! " +.+ brac x))
+  (==.) x y = codeOp2 x " == " y
+  (!=.) x y = codeOp2 x " != " y
+  (<.)  x y = codeOp2 x " < "  y
+  (<=.) x y = codeOp2 x " <= " y
+  (>.)  x y = codeOp2 x " > "  y
+  (>=.) x y = codeOp2 x " >= " y
+instance If Code Stmt Stmt Stmt where If c t e = IfStmt c t e
+instance If Code e    Stmt Stmt where If c t e = IfStmt c t e
+instance If Code Stmt e    Stmt where If c t e = IfStmt c t e
+instance If Code x    y    Expr where If c t e = IfExpr c t e
+IfExpr b t e = embed (brac (b +.+ indent +.+ nl +.+ c " ? " +.+ t +.+ nl +.+ c " : " +.+ e +.+ unindent))
+IfStmt b t e =
+  getMode \mode.
+  let
+    v = varName t
+    newMode = 
+      case mode of
+        Return s = Return s
+        Assign v = Assign v
+        _    = if (v == "") NoReturn (Assign v)
+  in
+    setMode SubExp +.+
+    c "if " +.+ brac b +.+ c " {" +.+ 
+      indent +.+ nl +.+ setMode newMode +.+ t +.+ unindent +.+ nl +.+ c "} else {" +.+
+      indent +.+ nl +.+ setMode newMode +.+ e +.+ unindent +.+ nl +.+ c "}" 
+instance IF Code where
+  IF b t e  = IfStmt b t e
+  (?) b t = 
+    getMode \mode.
+    c "if " +.+ setMode SubExp +.+ brac b +.+ c " {" +.+ 
+    indent +.+ nl +.+ setMode mode +.+ t +.+ c ";" +.+ unindent +.+ nl +.+ c "}" 
+
+instance sds Code where
+  sds f = // defCode f
+   {main = fresh \n.
+    let name = "sds"+toCode n
+        (v In body) = f (C (var name))
+    in setCode Var +.+ c (type2string v + " " + name + " = " + toCode v + 
+       ";\n") +.+ setCode Setup +.+ unMain body}
+  con f = defCode f
+
+defCode :: ((Code t p) -> In t (Main (Code u q))) -> Main (Code u r) | type t
+defCode f =
+  {main = fresh \n.
+    let name = "sds"+toCode n
+        (v In body) = f (C (var name))
+    in  setCode Var +.+ c (type2string v + " " + name + " = " + toCode v + 
+        ";\n") +.+ setCode Setup +.+ unMain body}
+
+var :: String (ReadWrite (Code v q)) CODE -> CODE
+var sds Rd      s = unC (embed (c sds)) Rd s
+var sds (Wrt v) s = unC (embed (c ("(" + sds + " = ") +.+ v +.+ c ")")) Rd s
+
+instance assign Code where
+  (=.) (C v) e = embed (setMode SubExp +.+ C \rw c.v (Wrt (toExpr e)) c)
+instance seq Code where
+  (>>=.) x f = 
+    getMode \mode. fresh \n. let v = "b" + toCode n in
+    addBinds v +.+ var2Type x +.+ c (v + ";") +.+ nl +.+
+    setMode (Assign v) +.+ x +.+ nl +.+ setMode mode +.+ f (embed (c v))
+  (:.) x y = getMode \mode. setMode NoReturn +.+ embed x +.+ nl +.+ setMode mode +.+ y
+instance step Code where
+    (>>*.) x f =
+        getMode \mode. fresh \n.
+            let v = "s" + toCode n in
+            c "while(true) {" +.+ indent +.+ nl +.+
+            var2Type x +.+ c (v + ";") +.+ nl +.+
+            setMode (Assign v) +.+ x +.+ nl +.+
+            setMode mode +.+ codeSteps (f (c v)) +.+
+            unindent +.+ nl +.+ c "}" 
+codeSteps :: [Step Code t] -> Code u p
+codeSteps [] = C \rw c.c
+codeSteps [Cond b e:x] =
+    getMode \mode. setMode SubExp +.+
+    c "if (" +.+ b +.+ c ") {" +.+ indent +.+ nl +.+ 
+    setMode mode +.+ e +.+ 
+    optBreak mode +.+ unindent +.+ nl +.+ c "}" +.+ nl +.+ setMode mode +.+ codeSteps x
+codeSteps [Ever e:x] =
+    getMode \mode. e +.+ optBreak mode
+
+optBreak :: Mode -> Code u p
+optBreak mode =
+    case mode of
+        Return s    = C \rw c.c
+        _           = nl +.+ c "break;" 
+
+instance setDelay Code where
+  setDelay d t = embed (c "setDelay" +.+ brac (t +.+ c ", " +.+ d))
+instance mtask Code a | taskImp2 a & types a where
+  task f =
+   {main = freshMTask \n.
+   let (app, a)  = taskImp2 n types
+       (b In main) = f (\d a.app (long d) a)
+   in codeMTaskBody (loopCode n (b a)) (unMain main)}
+instance mtasks Code a b | taskImp2 a & types a  & taskImp2 b & types b  where
+  tasks f = 
+    {main = 
+           freshMTask \t1. 
+           freshMTask \t2.
+           let (app1, a1) = taskImp2 t1 types
+               (app2, a2) = taskImp2 t2 types
+               ((b1, b2) In main) = f ((\d a.app1 (long d) a),(\d a.app2 (long d) a))
+           in codeMTaskBody (loopCode t2 (b2 a2)) (codeMTaskBody (loopCode t1 (b1 a1)) (unMain main))}
+loopCode :: Int (Code a b) -> Code c d
+loopCode n b =
+  nl +.+ c "case " +.+ c n +.+ c ": {" +.+ indent +.+ nl +.+
+  setMode NoReturn +.+ b +.+ nl +.+ c "break;" +.+ 
+  unindent +.+ nl +.+ c "} "
+
+class taskImp2 a :: Int a -> ((Code Long p) a->Code MTask Expr, a) | /*long Code delay &*/ isExpr p
+instance taskImp2 () where
+  taskImp2 n () = (app, ())
+  where app d a = setBinds [] +.+ embed (c "newTask(" +.+ c n +.+ c ", " +.+ d +.+ c ")")
+instance taskImp2 (Code t p) where
+  taskImp2 n type1 = (app, ta)
+    where
+      n0 = "t0p->a[0]"
+      ta = c n0 +.+ type1
+      app d a = 
+        setBinds [n0] +.+ embed (c "newTask(" +.+ 
+          c n +.+ c ", " +.+ 
+          d +.+ c ", " +.+
+          a +.+ c ")")
+instance taskImp2 (Code a p, Code b q) where 
+  taskImp2 n (type1, type2) = (app, (ta1, ta2)) where
+    n0 = "t0p->a[0]"
+    n1 = "t0p->a[1]"
+    ta1 = c n0 +.+ type1
+    ta2 = c n1 +.+ type2
+    app d (a1, a2) = 
+           setBinds [n0,n1] +.+ embed (c "newTask(" +.+ c n +.+ c ", " +.+ long d +.+ 
+           c ", " +.+ a1 +.+ c ", " +.+ a2 +.+ c ")")
+instance taskImp2 (Code a p, Code b q, Code c r) where 
+  taskImp2 n (type1, type2, type3) = (app, (ta1, ta2, ta3))
+    where
+      n0 = "t0p->a[0]"
+      n1 = "t0p->a[1]"
+      n2 = "t0p->a[2]"
+      ta1 = c n0 +.+ type1
+      ta2 = c n1 +.+ type2
+      ta3 = c n2 +.+ type3
+      app d (a1, a2, a3) = 
+        setBinds [n0,n1,n2] +.+ embed (c "newTask(" +.+ 
+          c n +.+ c ", " +.+ 
+          d  +.+ c ", " +.+
+          a1 +.+ c ", " +.+ 
+          a2 +.+ c ", " +.+ 
+          a3 +.+ c ", 0)")
+instance taskImp2 (Code a p, Code b q, Code c r, Code d s) where 
+  taskImp2 n (type1, type2, type3, type4) = (app, (ta1, ta2, ta3, ta4))
+    where
+      n0 = "t0p->a[0]"
+      n1 = "t0p->a[1]"
+      n2 = "t0p->a[2]"
+      n3 = "t0p->a[3]"
+      ta1 = c n0 +.+ type1
+      ta2 = c n1 +.+ type2
+      ta3 = c n2 +.+ type3
+      ta4 = c n3 +.+ type4
+      app d (a1, a2, a3, a4) = 
+        setBinds [n0,n1,n2,n3] +.+ embed (c "newTask(" +.+ 
+          c n +.+ c ", " +.+ 
+          d  +.+ c ", " +.+
+          a1 +.+ c ", " +.+ 
+          a2 +.+ c ", " +.+ 
+          a3 +.+ c ", " +.+ 
+          a4 +.+ c ")")
+
+class taskImp a :: Int a -> (Int a->Code MTask Expr, a)
+instance taskImp () where
+  taskImp n () = (app, ())
+    where app i a = embed (c "newTask(" +.+ c n +.+ c ", " +.+ c i +.+ c ")")
+instance taskImp (Code t p) where
+  taskImp n type1 = (app, ta)
+    where
+      ta = c "t0p->a[0]" +.+ type1
+      app i a = 
+        embed (c "newTask(" +.+ 
+          c n +.+ c ", " +.+ 
+          c i +.+ c ", " +.+
+          a +.+ c ")")
+instance taskImp (Code a p, Code b q) where 
+  taskImp n (type1, type2) = (app, (ta1, ta2)) where
+         ta1 = c "t0p->a[0]" +.+ type1
+         ta2 = c "t0p->a[1]" +.+ type2
+         app i (a1, a2) = 
+           embed (c "newTask(" +.+ c n +.+ c ", " +.+  c i +.+ 
+           c ", " +.+ a1 +.+ c ", " +.+ a2 +.+ c ")")
+instance taskImp (Code a p, Code b q, Code c r) where 
+  taskImp n (type1, type2, type3) = (app, (ta1, ta2, ta3))
+    where
+      ta1 = c "t0p->a[0]" +.+ type1
+      ta2 = c "t0p->a[1]" +.+ type2
+      ta3 = c "t0p->a[2]" +.+ type3
+      app i (a1, a2, a3) = 
+        embed (c "newTask(" +.+ 
+          c n +.+ c ", " +.+ 
+          c i +.+ c ", " +.+
+          a1 +.+ c ", " +.+ 
+          a2 +.+ c ", " +.+ 
+          a3 +.+ c ")")
+instance taskImp (Code a p, Code b q, Code c r, Code d s) where 
+  taskImp n (type1, type2, type3, type4) = (app, (ta1, ta2, ta3, ta4))
+    where
+      ta1 = c "t0p->a[0]" +.+ type1
+      ta2 = c "t0p->a[1]" +.+ type2
+      ta3 = c "t0p->a[2]" +.+ type3
+      ta4 = c "t0p->a[3]" +.+ type4
+      app i (a1, a2, a3, a4) = 
+        embed (c "newTask(" +.+ 
+          c n +.+ c ", " +.+ 
+          c i +.+ c ", " +.+
+          a1 +.+ c ", " +.+ 
+          a2 +.+ c ", " +.+ 
+          a3 +.+ c ", " +.+ 
+          a4 +.+ c ")")
+
+tasksMain :: Int Int ((a->Code MTask Expr,b->Code MTask Expr) -> In (a->Code c d,b->Code e f) (Main (Code g h))) -> Main (Code i j) | taskImp a & types a & taskImp b & types b
+tasksMain i j f =
+    { main =
+      freshMTask \n. freshMTask \m.
+        let
+          (app1, a1) = taskImp n types
+          (app2, a2) = taskImp m types
+          ((b1, b2) In {main = e}) = f (app1 i, app2 j)
+        in
+          codeMTaskBody (loopCode n (b1 a1) +.+ setMode NoReturn +.+ loopCode m (b2 a2)) e
+    }
+class types a :: a
+instance types () where types = ()
+instance types (Code a p) | typeSelector a & isExpr p
+  where types = typeSelector
+instance types (Code a p, Code b q) | typeSelector a & isExpr p & typeSelector b & isExpr q 
+  where types = (typeSelector, typeSelector)
+instance types (Code a p, Code b q, Code c r) | typeSelector a & isExpr p & typeSelector b & isExpr q & typeSelector c & isExpr r 
+  where types = (typeSelector, typeSelector, typeSelector)
+instance types (Code a p, Code b q, Code c r, Code d s) | typeSelector a & isExpr p & typeSelector b & isExpr q & typeSelector c & isExpr r & typeSelector d & isExpr s 
+  where types = (typeSelector, typeSelector, typeSelector, typeSelector)
+
+codeMTaskBody :: (Code v w) (Code c d) -> Code e f
+codeMTaskBody loop e =
+  getMode \mode. 
+    setMode NoReturn +.+
+    setCode Loop +.+ loop +.+
+    setMode mode +.+ setCode Setup +.+ embed e
+instance fun Code () where
+  fun f  =
+   {main = getMode \mode. fresh \n.
+       let fname = c ("f" + toCode n)
+        (g In {main=e}) = f (\x.embed (fname +.+ c " ()"))
+    in setCode Fun +.+ c "\n" +.+ resType f +.+ c " " +.+ fname +.+ c " () " +.+ 
+       funBody (setMode (Return (toCode (resType2 f))) +.+ setBinds [] +.+ g ()) +.+ setCode Setup +.+ setMode mode +.+ e
+   }
+instance fun Code (Code t p) | type, showType t & isExpr p  where
+  fun f  =
+    {main =
+      getMode \mode. fresh \n.
+        let fname = c ("f" + toCode n)
+            aname = "a" + toCode n
+            (g In {main=e}) = f (\x.embed (fname +.+ c " " +.+ brac x))
+        in  setCode Fun +.+ c "\n" +.+ resType f +.+ c " " +.+ fname +.+ c " " +.+
+          brac (argTypes f +.+ c (" " + aname)) +.+ 
+          funBody (setMode (Return (toCode (resType2 f))) +.+ setBinds [aname] +.+ g (embed (c aname))) +.+ setCode Setup +.+ setMode mode +.+ e
+    }
+instance fun Code (Code a p, Code b q) | showType a & showType b where
+  fun f =
+        {main =
+         getMode \mode. fresh \n.
+         let fname = c ("f" + toCode n + " ")
+             aname = "a" + toCode n //+ " "
+             bname = "b" + toCode n //+ " "
+             (atype, btype) = argTypes f
+             (g In main)
+              = f (\(x,y).embed (fname +.+ codeOp2 x ", " y))
+         in setCode Fun +.+ nl +.+ resType f +.+ fname +.+ 
+            codeOp2 (atype +.+ c aname) ", " (btype +.+ c bname) +.+ 
+            funBody (setMode (Return (toCode (resType2 f))) +.+ 
+            setBinds [aname,bname] +.+ g (embed (c aname), embed (c bname))) +.+ 
+            setCode Setup +.+ setMode mode +.+ unMain main
+        }
+instance fun Code (Code a p, Code b q, Code c r) | showType a & showType b & showType c where
+  fun f  =
+    {main =
+      getMode \mode. fresh \n.
+        let fname = c ("f" + toCode n)
+            aname = "a" + toCode n
+            bname = "b" + toCode n
+            cname = "c" + toCode n
+            (atype,btype,ctype) = argTypes f
+            (g In {main=e}) = f (\(x,y,z).embed (fname +.+ c " " +.+ brac (x +.+ c ", " +.+ y +.+ c ", " +.+ z)))
+        in setCode Fun +.+ c "\n" +.+ resType f +.+ c " " +.+ fname +.+ c " " +.+
+           brac (atype +.+ c (" " + aname + ", ") +.+ btype +.+ c (" " + bname + ", ") +.+ ctype +.+ c (" " + cname)) +.+ 
+           funBody (setMode (Return (toCode (resType2 f))) +.+ 
+           setBinds [aname,bname,cname] +.+ g (embed (c aname), embed (c bname), embed (c cname))) +.+ setCode Setup +.+ setMode mode +.+ e
+    }
+instance output Code where
+  output x = embed (c "Serial.println(" +.+ x +.+ c ")")
+instance pinMode Code where
+  pinmode p m = embed (c ("pinMode(" + toCode p + ", " + consName{|*|} m + ")"))
+instance digitalIO Code where
+  digitalRead p = embed (c ("digitalRead(" + toCode p + ")"))
+  digitalWrite p b = embed (c ("digitalWrite(" + toCode p + ", ") +.+ b +.+ c ")")
+instance dIO Code where
+  dIO p = C (ioc p) where
+    ioc :: p (ReadWrite (Code t q)) CODE -> CODE | pin, readPinD p
+    ioc p Rd   s = f Rd s where (C f) = embed (c ("digitalRead(" + toCode p + ")"))
+    ioc p (Wrt v) s = f Rd s where (C f) = embed (c ("pWrite(" + toCode p + ", ") +.+ v +.+ c ")")
+instance aIO Code where
+  aIO p = C (ioc p)  where
+    ioc :: p (ReadWrite (Code t q)) CODE -> CODE | pin p
+    ioc p Rd      s = unC (embed (c ("analogRead(" + toCode p + ")"))) Rd s
+    ioc p (Wrt v) s = unC (embed (c ("pWrite(" + toCode p + ", ") +.+ v +.+ c ")")) Rd s
+instance analogIO Code where
+  analogRead p = embed (c ("analogRead(" + toCode p + ")"))
+  analogWrite p b = embed (c ("analogWrite(" + toCode p + ", ") +.+ b +.+ c ")")
+instance noOp Code where noOp = C \rw c.c
+
+:: Code a p = C ((ReadWrite (Code a Expr)) CODE -> CODE)
+:: CODE =
+  { fresh      :: Int
+  , freshMTask :: Int
+  , funs       :: [String]
+  , ifuns                      :: Int
+  , vars         :: [String]
+  , ivars                      :: Int
+  , setup                      :: [String]
+  , isetup       :: Int
+  , loop         :: [String]
+  , iloop                      :: Int
+  , includes  :: [String]
+  , def          :: Def
+  , mode         :: Mode
+  , binds                      :: [String]
+  }
+
+unC :: (Code a p) -> ((ReadWrite (Code a Expr)) CODE -> CODE)
+unC (C f) = f
+
+:: Def = Var | Fun | Setup | Loop
+:: Mode = /*MainMode |*/ NoReturn | Return String | SubExp | Assign String
+
+setMode :: Mode -> Code a p
+setMode m = C \rw c.{c & mode = m}
+
+getMode :: (Mode -> Code a p) -> Code a p
+getMode f = C \rw c.unC (f c.mode) rw c
+
+embed :: (Code a p) -> Code a p
+embed e =
+  getMode \m. case m of
+    NoReturn  = setMode SubExp +.+ e +.+ c ";"
+    Return "void" = setMode SubExp +.+ e +.+ c ";"
+    Return t  = c "return " +.+ setMode SubExp +.+ e +.+ c ";"
+    Assign s  = c (s + " = ") +.+ setMode SubExp +.+ e +.+ c ";"
+    SubExp    = e
+    _       = abort "\n\nembed: unknown mode.\n"
+
+(+.+) infixl 5 :: (Code a p) (Code b q) -> Code c r
+(+.+) (C f) (C g) = C \rw c.g Rd (f Rd c)
+
+fresh :: (Int -> (Code a p)) -> (Code a p)
+fresh f = C \rw c.unC (f c.fresh) rw {c & fresh = c.fresh + 1}
+
+freshMTask :: (Int -> (Code a p)) -> (Code a p)
+freshMTask f = C \rw c.unC (f c.freshMTask) rw {c & freshMTask = c.freshMTask + 1}
+
+setCode :: Def -> (Code a p)
+setCode d = C \rw c.{c & def = d}
+
+getCode :: (Def -> Code a p) -> (Code a p)
+getCode f = C \rw c.unC (f c.def) rw c
+
+brac :: (Code a p) -> Code b q
+brac e = c "(" +.+ e +.+ c ")"
+
+funBody :: (Code a p) -> Code b q
+funBody e = c "{" +.+ indent +.+ nl +.+ e +.+ unindent +.+ nl +.+ c "}" +.+ nl
+
+codeOp2 :: (Code a p) String (Code b q) -> Code c r
+codeOp2 x n y = embed (brac (x +.+ c n +.+ y))
+
+include :: String -> Code a b
+include lib = C \rw c.{c & includes = [lib:c.includes]}
+
+argList :: [a] -> String | toCode a
+argList [a] = toCode a
+argList [a:x] = toCode a + "," + argList x
+argList [] = ""
+
+c :: a -> Code b p | toCode a
+c a = C \rw c.case c.def of
+    Fun   = {c & funs = [toCode a: c.funs]}
+    Var   = {c & vars = [toCode a: c.vars]}
+    Setup   = {c & setup = [toCode a: c.setup]}
+    Loop  = {c & loop = [toCode a: c.loop]}
+
+indent :: Code a p
+indent = 
+  C \rw c.case c.def of
+    Fun   = {c & ifuns = inc c.ifuns}
+    Var   = {c & ivars = inc c.ivars}
+    Setup   = {c & isetup = inc c.isetup}
+    Loop  = {c & iloop = inc c.iloop}
+
+unindent :: Code a p
+unindent =
+  C \rw c.case c.def of
+    Fun   = {c & ifuns = dec c.ifuns}
+    Var   = {c & ivars = dec c.ivars}
+    Setup   = {c & isetup = dec c.isetup}
+    Loop  = {c & iloop = dec c.iloop}
+where
+  dec n | n > 1
+    = n - 1
+    = 0
+
+nl :: Code a p
+nl = 
+  C \rw c.case c.def of
+    Fun   = {c & funs = [str c.ifuns: c.funs]}
+    Var   = {c & vars = [str c.ivars: c.vars]}
+    Setup   = {c & setup = [str c.isetup: c.setup]}
+    Loop  = {c & loop = [str c.iloop: c.loop]}
+where
+  str n = toString ['\n':repeatn (tabSize * n) ' ']
+
+setBinds :: [String] -> Code a p
+setBinds list = C \rw c.{c & binds = list}
+
+addBinds :: String -> Code a p
+addBinds name = C \rw c.{c & binds = [name:c.binds]}
+
+getBinds :: ([String] -> Code a p) -> (Code a p)
+getBinds f = C \rw c.unC (f c.binds) rw c
+
+// ----- driver ----- //
+
+compile :: (Main (Code a p)) -> [String]
+compile {main=(C f)} = 
+  ["/*\n"
+  ,"  Generated code for Arduino\n"
+  ,"  Pieter Koopman, pieter@cs.ru.nl\n"
+  ,"*/\n"
+  ,"\n"
+  ,"#define MAX_ARGS 4\n"
+  ,"#define MAX_TASKS 20\n"
+  ,"#define MAX_TASK_NO MAX_TASKS - 1\n"
+  ,"#define NEXT_TASK(n) ((n) == MAX_TASK_NO ? 0 : (n) + 1)\n"
+  ,"\n"
+  ,"typedef union Arg {\n"
+  ,"  int i;\n"
+  ,"  bool b;\n"
+  ,"  char c;\n"
+//  ,"  float f;\n" // requires 4 bytes
+  ,"  word w;\n"
+  ,"} ARG;\n"
+  ,"\n"
+  ,"typedef struct Task {\n"
+  ,"  byte id;\n"
+  ,"  long wait;\n"
+  ,"  ARG a[MAX_ARGS];\n"
+  ,"} TASK;\n"
+  ,"\n"
+  ] ++
+  foldr (\lib c.["#include <":lib:".h>\n":c]) [] (mkset c.includes) ++
+  ["\n// --- variables ---\n"
+  ,"TASK tasks[MAX_TASKS];\n"
+  ,"byte t0 = 0, tc = 0, tn = 0;\n"
+  ,"long delta;\n"
+  ,"\n"
+  ,"int vInt;\n"
+  ,"bool vBool;\n"
+  ,"char vChar;\n"
+  ,"float vFloat;\n"
+  ,"unsigned long time = 0;\n"
+  :reverse c.vars
+  ] ++
+  ["\n// --- functions ---\n"
+  ,"byte newTask(byte id, long wait, word a0 = 0, word a1 = 0, word a2 = 0, word a3 = 0) {\n"
+  ,"  TASK *tnp = &tasks[tn];\n"
+  ,"  tnp->id = id;\n"
+  ,"  tnp->wait = wait;\n"
+  ,"  tnp->a[0].w = a0;\n"
+  ,"  tnp->a[1].w = a1;\n"
+  ,"  tnp->a[2].w = a2;\n"
+  ,"  tnp->a[3].w = a3;\n"
+  ,"  byte r = tn;\n"
+  ,"  tn = NEXT_TASK(tn);\n"
+  ,"  return r;\n"
+  ,"}\n"
+  ,"\n"
+  ,"byte setDelay(byte t, long d) {\n"
+  ,"  tasks[t].wait = d;\n"
+  ,"  return t;\n"
+  ,"}\n"
+  ,"boolean pressed(int b) {\n"
+  ,"  pinMode(A0, INPUT);\n"
+  ,"  int a0 = analogRead(A0);\n"
+  ,"  switch (b) {\n"
+  ,"  case 0: return a0 < ",toString RightBound,";       // right\n"
+  ,"  case 1: return ",toString RightBound," < a0 && a0 < ",toString UpBound,"; // up\n"
+  ,"  case 2: return ",toString UpBound," < a0 && a0 < ",toString DownBound,";// down\n"
+  ,"  case 3: return ",toString DownBound," < a0 && a0 < ",toString LeftBound,";//left\n"
+  ,"  case 4: return ",toString LeftBound," < a0 && a0 < ",toString SelectBound,";//select\n"
+  ,"  default: return ",toString SelectBound," < a0;       //no button\n"
+  ,"  }\n"
+  ,"}\n"
+  ,"boolean pWrite (int pin, boolean b) {\n"
+  ,"  pinMode(pin, OUTPUT);\n"
+  ,"  digitalWrite(pin, b);\n"
+  ,"  return b;\n"
+  ,"}\n"
+  ,"int pWrite (int pin, int i) {\n"
+  ,"  pinMode(pin, OUTPUT);\n"
+  ,"  analogWrite(pin, i);\n"
+  ,"  return i;\n"
+  ,"}\n"
+  :reverse c.funs
+  ] ++
+  ["\n// --- setup --- \n"
+  ,"void setup () {\n" 
+  ,"  Serial.begin(9600);\n"
+  ,"  "
+  :reverse c.setup
+  ] ++
+  ["\n}\n"
+  ,"\n// --- loop --- \n"
+  ,"void loop () {\n"
+  ,"  if (t0 != tn) {\n"
+  ,"  if (t0 == tc) {\n"
+  ,"    unsigned long time2 = millis();\n"
+  ,"    delta = time2 - time;\n"
+  ,"    time = time2;\n"
+  ,"    tc = tn;\n"
+  ,"  };\n"
+  ,"  TASK* t0p = &tasks[t0];\n"
+  ,"  t0p->wait -= delta;\n"
+  ,"  if (t0p->wait > 0L) {\n"
+  ,"    newTask(t0p->id, t0p->wait, t0p->a[0].w, t0p->a[1].w, t0p->a[2].w, t0p->a[3].w);\n"
+  ,"  } else {\n"
+  ,"    switch (t0p->id) {"
+  :reverse c.loop
+  ] ++
+  ["\n"
+  ,"    default:\n"
+  ,"    Serial.println(\"stopped\");\n"
+  ,"    t0 = tn; // no known task: force termination of tasks\n"
+  ,"    return;\n"
+  ,"    };\n"
+  ,"  }\n"
+  ,"  t0 = NEXT_TASK(t0);\n"
+  ,"  }\n"
+  ,"}\n"
+  ]
+where c = f Rd newCode
+
+mkset :: [a] -> [a] | Eq a
+mkset [a:x] = [a:mkset (filter ((<>) a) x)]
+mkset [] = []
+
+newCode :: CODE
+newCode =
+  { fresh   = 0
+  , freshMTask = 0
+  , funs    = []
+  , ifuns   = 0
+  , vars    = []
+  , ivars   = 0
+  , setup   = []
+  , isetup  = 1
+  , loop    = []
+  , iloop   = 4
+  , includes  = []
+  , def     = Setup
+  , mode    = NoReturn
+  , binds              = []
+  }
+
+// ----- simulation ----- //
+
+eval :: (Main (Eval t p)) -> [String] | toString t
+eval {main=(E f)} = [toString (fst (f Rd state0))]
+
+:: State = 
+  { tasks :: [(Int, State->State)]
+  , store :: [Dyn]
+  , dpins :: [(DigitalPin, Bool)]
+  , apins :: [(AnalogPin, Int)]
+  , serial:: [String]
+  , millis:: Int
+  }
+
+state0 :: State
+state0 = {store = [], tasks = [], serial = [], millis = 0, dpins = [] , apins = []}
+
+//:: TaskSim :== (Int, State->State)
+:: Eval t p = E ((ReadWrite t) State -> (t, State))
+toS2S :: (Eval t p) -> (State->State)
+toS2S (E f) = \state.snd (f Rd state)
+
+unEval :: (Eval t p) -> ((ReadWrite t) State -> (t, State))
+unEval (E f) = f
+
+:: ReadWrite t = Rd | Wrt t | Updt (t->t)
+
+(>>==) infixl 1 :: (Eval a p) (a -> Eval b q) -> Eval b r
+//(>>== ) (E f) g = E \r s. let (a, s2) = f Rd s; (E h) = g a in h Rd s2
+(>>==) (E f) g = E\r s.let (a,t) = f Rd s in unEval (g a) Rd t
+
+rtrn :: t -> Eval t p
+rtrn a = E \r s -> (a, s)
+
+yield :: t (Eval s p) -> Eval t Expr
+//yield a (E f) = E (\r s.(\(_,t).(a,t)) (f r s))
+yield a (E f) = E \r s.(a,snd (f Rd s))
+
+instance arith Eval where
+  lit a = rtrn a
+  (+.) x y = x >>==  \a. y >>==  \b. rtrn (a + b)
+  (-.) x y = x >>==  \a. y >>==  \b. rtrn (a - b)
+  (*.) x y = x >>==  \a. y >>==  \b. rtrn (a * b)
+  (/.) x y = x >>==  \a. y >>==  \b. rtrn (a / b)
+instance boolExpr Eval where
+  (&.) x y = x >>==  \a. if a y (rtrn False) // lazy AND
+  (|.) x y = x >>==  \a. if a (rtrn True) (y >>==  rtrn)
+  Not x   = x >>==  \a. rtrn (not a)
+  (==.) x y = x >>==  \a. y >>==  \b. rtrn (a == b)
+  (!=.) x y = x >>==  \a. y >>==  \b. rtrn (a <> b)
+  (<.)  x y = x >>==  \a. y >>==  \b. rtrn (a < b)
+  (>.)  x y = x >>==  \a. y >>==  \b. rtrn (a > b)
+  (<=.)  x y = x >>==  \a. y >>==  \b. rtrn (a <= b)
+  (>=.)  x y = x >>==  \a. y >>==  \b. rtrn (a >= b)
+instance If Eval p q Expr where
+  If  c t e = c >>==  \b.if b (toExpr t) (toExpr e)
+instance IF Eval where
+  IF  c t e = c >>==  \b.if b (yield () t) (yield () e)
+  (?) c t   = c >>==  \b.if b (yield () t) (rtrn ())
+instance var2 Eval where
+  var2 v f = defEval2 v f
+  con2 v f = defEval2 v f
+
+defEval2 :: t ((Eval t p)->Main (Eval u q)) -> (Main (Eval u q)) | dyn t
+defEval2 v f = 
+  {main = E (\r s.(length s.store
+          , {s & store = s.store ++ [toDyn v]}))
+  >>==  \n.unMain (f (E (read n)))}
+instance sds Eval where
+  sds f = defEval f
+  con f = defEval f
+
+defEval :: ((Eval t p)->In t (Main (Eval u q))) -> (Main (Eval u q)) | dyn t
+defEval f = 
+  {main = E \r s.let (v In g) = f (E (read (length s.store))) in
+          unEval (unMain g) r {s & store = s.store ++ [toDyn v]}}
+instance fun Eval x | arg x where
+  fun f = e where (g In e) = f (\a.toExpr (g a))
+instance mtask Eval x | arg x where
+ task f = e where
+  (t In e) = f (\d a.long d >>== \(L i).E\r s.(MTask (length s.tasks),{s&tasks=[(i,toS2S (t a)):s.tasks]}))
+instance mtasks Eval x y | arg x & arg y where
+ tasks f = e where
+  ((t,u) In e) = 
+   f ((\d a.long d >>== \(L i).E\r s.(MTask (length s.tasks),{s&tasks=[(i,toS2S (t a)):s.tasks]}))
+   ,(\d b.long d >>== \(L j).E\r s.(MTask (length s.tasks),{s&tasks=[(j,toS2S (u b)):s.tasks]}))
+   )
+instance setDelay Eval where
+  setDelay d t = d >>==  \(L x). t >>==  \(MTask n).E \r s.(MTask n,{s & tasks = updateAt n (x,snd (s.tasks !! n)) s.tasks})
+class toExpr v where toExpr :: (v t p) -> v t Expr
+instance toExpr Eval where toExpr (E f) = E f
+instance toExpr Code where toExpr (C f) = C f
+instance seq Eval where
+  (>>=.) x f = x >>==   f o rtrn
+  (:.) x y = x >>==  \_. y
+instance assign Eval where
+  (=.) (E v) e = e >>==  \a. E \r s.v (Wrt a) s
+instance output Eval where
+  output x = x >>==  \a.E \r s.((),{s & serial = s.serial ++ [toCode a]})
+instance pinMode Eval where
+  pinmode p m = rtrn ()
+instance digitalIO Eval where
+  digitalRead  p   = E \rw s=:{dpins, apins}.(readPinD p dpins apins, s)
+  digitalWrite p b = b >>== \a. E \rw s.(a, writePinD p a s)
+instance analogIO Eval where
+  analogRead  p   = E \rw s=:{apins}. (readPinA p apins, s)
+  analogWrite p b = b >>== \a. E \rw s.(a, writePinA p a s)
+instance noOp Eval where noOp = E \r s.(undef,s)
+
+class arg x :: x -> Int
+instance arg () where arg _ = 0
+instance arg (Eval t p) | type t where arg _ = 1
+instance arg (Eval t p, Eval u q) | type t & type u where arg _ = 2
+instance arg (Eval t p, Eval u q, Eval v r) | type t & type u & type v where arg _ = 3
+instance arg (Eval t p, Eval u q, Eval v r, Eval w s) | type t & type u & type v where arg _ = 4
+
+instance + String where (+) x y = x +++ y
+
+readPinA :: AnalogPin [(AnalogPin, Int)] -> Int
+readPinA p lista
+  = case [b \\ (q, b) <- lista | p == q] of
+  []  = 0
+  [a:x] = a
+
+writePinA :: AnalogPin Int State -> State
+writePinA p x s
+  = {s & apins = [(p, x):[(q, y) \\ (q, y) <- s.apins | p <> q]]}
+
+class readPinD p :: p [(DigitalPin,Bool)] [(AnalogPin,Int)] -> Bool
+instance readPinD DigitalPin where
+  readPinD p listd lista
+  = case [b \\ (q,b) <- listd | p == q] of
+    [] = False
+    [a:x] = a
+instance readPinD AnalogPin where
+  readPinD p listd lista
+  = case [b \\ (q,b) <- lista | p == q] of
+    [] = False
+    [a:x] = a <> 0
+class writePinD p :: p Bool State -> State
+instance writePinD DigitalPin where
+  writePinD p b s=:{dpins} = {s & dpins = [(p, b):[(q, c) \\ (q, c) <- dpins | p <> q]]}
+instance writePinD AnalogPin where
+  writePinD p b s=:{apins} = {s & apins = [(p, if b 1 0):[(q, c) \\ (q, c) <- apins | p <> q]]}
+
+
+// ----- Interactive Simulation ----- //
+
+derive class iTask DigitalPin, AnalogPin, Dyn, StateInterface, DisplayVar, Pin
+
+simulate :: (Main (Eval a p)) -> Task ()
+simulate {main=(E f)} = setup state0 where
+  setup s =
+         updateInformation "State" [] (toView s)
+         >>* [ OnAction ActionFinish (always shutDown)
+           , OnAction (Action "setup" []) (hasValue 
+             (\si.simloop (snd (f Rd (mergeView s si)))))
+           ]
+  simloop s =
+         updateInformation "State" [] (toView s)
+         >>* [ OnAction ActionFinish (always shutDown)
+           , OnAction (Action "clear serial" []) (always (simloop {s & serial = []}))
+           , OnAction ActionNew (always (setup state0))
+           : if (isEmpty s.tasks)
+               []
+               [OnAction (Action "loop" []) (hasValue
+             \si.simloop (step (mergeView s si)))
+             ]
+           ]
+
+toView :: State -> StateInterface
+toView s = 
+  { serialOut = Display s.serial
+  , analogPins = s.apins
+  , digitalPins = s.dpins
+  , var2iables = map toDisplayVar s.store
+  , timer = s.millis
+  , taskCount = Display (length s.tasks)
+  }
+
+mergeView :: State StateInterface -> State
+mergeView s si = 
+  { s
+  & store = [fromDisplayVar new old \\ new <- si.var2iables & old <- s.store]
+  , dpins = si.digitalPins
+  , apins = si.analogPins
+//  , serial = si.serialOut
+  , millis = si.timer
+  }
+
+:: StateInterface =
+  { serialOut   :: Display [String]
+  , analogPins  :: [(AnalogPin, Int)]
+  , digitalPins :: [(DigitalPin, Bool)]
+  , var2iables   :: [DisplayVar]
+  , timer     :: Int
+  , taskCount   :: Display Int
+  }
+
+toDisplayVar :: Dyn -> DisplayVar
+toDisplayVar (Dyn [v])
+    # i = toInt v
+    | toString i == v
+        = INT i
+        = Variable v
+toDisplayVar (Dyn ["L",v]) = LONG (toInt v)
+toDisplayVar (Dyn ["Servo",pinKind,pin,pos]) = Servo (fromJust (fromDyn (Dyn [pinKind,pin]))) (toInt pos)
+toDisplayVar (Dyn ["LCD",_,_,_,_,_,l1,_,l2,_]) = LCD16x2 l1 l2
+toDisplayVar (Dyn l) = DisplayVar l
+
+fromDisplayVar :: DisplayVar Dyn -> Dyn
+fromDisplayVar (Variable v)  dyn = Dyn [v]
+fromDisplayVar (INT v)     dyn = Dyn [toString v]
+fromDisplayVar (LONG v)    dyn = Dyn ["L",toString v]
+fromDisplayVar (Servo pin pos) dyn = Dyn (["Servo":let (Dyn p) = toDyn pin in p] ++ [toString pos])
+fromDisplayVar (LCD16x2 l1 l2) (Dyn list) = Dyn (updateAt 6 l1 (updateAt 8 l2 list))
+fromDisplayVar (DisplayVar l)  dyn = Dyn l
+
+:: DisplayVar
+    = Variable String
+    | INT Int
+    | LONG Int
+    | Servo Pin Int
+    | LCD16x2 String String
+    | DisplayVar [String]
+
+
+step :: State -> State
+step s = 
+  foldr appTask {s & millis = s.millis + delta, tasks = []}
+    [(w - delta, f) \\ (w, f) <- s.tasks]
+where delta = foldl1 min (map fst s.tasks) // smallest wait
+
+appTask t=:(w,f) s | w <= 0
+  = f s
+  = {s & tasks = [t:s.tasks]}
+
+foldl1 op [a:x] = foldl op a x
+foldr1 op l :== foldr l
+  where
+    foldr [a]     = a
+    foldr [a:x] = op a (foldr x)
+
+class stringQuotes t | type t :: (Code t p) -> Code t p
+instance stringQuotes String where stringQuotes x = c "\"" +.+ x +.+ c "\""
+instance stringQuotes t    where stringQuotes x = x
+
+
+derive   toGenDynamic (), MTask, DigitalPin, AnalogPin, Pin, [], Long, LCD //, Servo
+derive fromGenDynamic (), MTask, DigitalPin, AnalogPin, Pin, [], Long, LCD //, Servo
+instance toCode () where toCode _ = ""
+instance ==   () where (==) _ _ = True
+
+// ----- long ----- //
+
+:: Long = L Int // 32 bit on Arduino
+instance toCode Long where toCode (L i) = toCode i + "L"
+instance + Long where (+) (L x) (L y) = L (x + y)
+instance - Long where (-) (L x) (L y) = L (x + y)
+instance * Long where (*) (L x) (L y) = L (x + y)
+instance / Long where (/) (L x) (L y) = L (x + y)
+instance == Long where (==) (L x) (L y) = x == y
+instance one Long where one = L one
+instance zero Long where zero = L zero
+now = lit (L 0)
+
+class long v t :: (v t p) -> v Long Expr | isExpr p
+instance long Code Int where
+  long x = embed (c "long" +.+ brac x)
+instance long Code Long where
+  long x = embed (c "long" +.+ brac x)
+instance long Eval Int where
+  long x = x >>== rtrn o L
+instance long Eval Long where
+  long (E x) = E x
+
+// ----- tools ----- //
+
+class toCode a :: a -> String
+instance toCode Bool where toCode b = if b "true" "false"
+instance toCode Int where toCode a = toString a
+instance toCode Real where toCode a = toString a
+instance toCode Char where
+  toCode '\0' = "'\\0'"
+  toCode '\n' = "'\\n'"
+  toCode '\\' = "\\"
+  toCode a = "'" + toString a + "'"
+instance toCode String where toCode s = s
+instance toCode DigitalPin where toCode x = s%(1, size s - 1) where s = consName{|*|} x
+instance toCode AnalogPin  where toCode x = consName{|*|} x
+derive consName DigitalPin, AnalogPin, PinMode
+
+instance == DigitalPin where (==) x y = x === y
+instance == AnalogPin   where (==) x y = x === y
+
+derive consIndex DigitalPin, AnalogPin
+
+tab =: toString (repeatn tabSize ' ')
+tabSize :== 2
+
+instance toString () where toString _ = "()"