definition 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 iTasks._Framework.Generic
import iTasks._Framework.Task
import StdClass
from iTasks.API.Core.Types import :: Display
import gdynamic, gCons, GenEq, StdMisc, StdArray

import mTaskSerial, mTaskLCD

// =================== 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

class pin p | type, == p where
  pin :: p -> Pin
instance pin DigitalPin
instance pin AnalogPin

:: Upd   = Upd
:: Expr  = Expr
:: Stmt  = Stmt
:: MTask = MTask Int // String

class isExpr a :: a -> Int
instance isExpr Upd
instance isExpr Expr

class isStmt a :: a -> Int
instance isStmt Upd
instance isStmt Expr
instance isStmt Stmt

instance == MTask
instance toCode MTask

:: Main a = {main :: a}

unMain :: (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
instance pio AnalogPin Bool
instance pio DigitalPin Bool

int :: (v Int p) -> (v Int p)
bool :: (v Bool p) -> (v Bool p)
char :: (v Char p) -> (v Char p)

class type t | showType, dyn, toCode, ==, type2string, varName t
class type2string t :: t -> String
instance type2string Int
instance type2string Long
instance type2string Real
instance type2string Bool
instance type2string Char
instance type2string MTask
instance type2string DigitalPin
instance type2string AnalogPin
instance type2string String
instance type2string ()
class varName a :: a -> String
instance varName Int
instance varName Long
instance varName Bool
instance varName Char
instance varName Real
instance varName x

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

class argTypes t :: ((t->Code b Expr)->In (t->Code b2 q) (Main (Code c s))) -> t
instance argTypes (Code a p) | showType a
instance argTypes (Code a p, Code b q) | showType a & showType b
instance argTypes (Code a p, Code b q, Code c r) | showType a & showType b & showType c

resType :: ((t->Code b Expr)->In (t->Code b q) (Main (Code c s))) -> Code b q | showType b

var2Type :: (Code t p) -> Code t p | showType t

resType2 :: ((t->Code b Expr)->In (t->Code b q) (Main (Code c s))) -> SV b | showType2 b

:: SV t = SV String
instance toCode (SV t)

class showType2 t :: SV t
instance showType2 ()
instance showType2 Int
instance showType2 Char
instance showType2 Bool
instance showType2 a

class showType t | showType2 /*, type*/ t :: (Code t p)
instance showType ()
instance showType Int
instance showType Long
instance showType Char
instance showType Bool
instance showType a

class typeSelector t | showType2, type t :: (Code t p)
instance typeSelector Int
instance typeSelector Char
instance typeSelector Bool
instance typeSelector a

:: In a b = In infix 0 a b

read` :: Int (ReadWrite a) State -> (a,State) | dyn a

// ----- code generation ----- //

instance arith Code
instance boolExpr Code
instance If Code Stmt Stmt Stmt
instance If Code e    Stmt Stmt
instance If Code Stmt e    Stmt
instance If Code x    y    Expr
instance IF Code
instance sds Code

defCode :: ((Code t p) -> In t (Main (Code u q))) -> Main (Code u r) | type t

var :: String (ReadWrite (Code v q)) CODE -> CODE

instance assign Code
instance seq Code
instance step` Code
codeSteps :: [Step Code t] -> Code u p
optBreak :: Mode -> Code u p

instance setDelay Code
instance mtask Code a | taskImp2 a & types a
instance mtasks Code a b | taskImp2 a & types a  & taskImp2 b & types b

loopCode :: Int (Code a b) -> Code c d

class taskImp2 a :: Int a -> ((Code Long p) a->Code MTask Expr, a) | /*long Code delay &*/ isExpr p
instance taskImp2 ()
instance taskImp2 (Code t p)
instance taskImp2 (Code a p, Code b q)
instance taskImp2 (Code a p, Code b q, Code c r)
instance taskImp2 (Code a p, Code b q, Code c r, Code d s)

class taskImp a :: Int a -> (Int a->Code MTask Expr, a)
instance taskImp ()
instance taskImp (Code t p)
instance taskImp (Code a p, Code b q)
instance taskImp (Code a p, Code b q, Code c r)
instance taskImp (Code a p, Code b q, Code c r, Code d s)

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
class types a :: a
instance types ()
instance types (Code a p) | typeSelector a & isExpr p
instance types (Code a p, Code b q) | typeSelector a & isExpr p & typeSelector b & isExpr q 
instance types (Code a p, Code b q, Code c r) | typeSelector a & isExpr p & typeSelector b & isExpr q & typeSelector c & isExpr r 
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 

codeMTaskBody :: (Code v w) (Code c d) -> Code e f
instance fun Code ()
instance fun Code (Code t p) | type, showType t & isExpr p
instance fun Code (Code a p, Code b q) | showType a & showType b
instance fun Code (Code a p, Code b q, Code c r) | showType a & showType b & showType c
instance output Code
instance pinMode Code
instance digitalIO Code
instance dIO Code
instance aIO Code
instance analogIO Code
instance noOp Code

:: 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)

:: Def = Var | Fun | Setup | Loop
:: Mode = /*MainMode |*/ NoReturn | Return String | SubExp | Assign String

setMode :: Mode -> Code a p
getMode :: (Mode -> Code a p) -> Code a p
embed :: (Code a p) -> Code a p
(+.+) infixl 5 :: (Code a p) (Code b q) -> Code c r
fresh :: (Int -> (Code a p)) -> (Code a p)
freshMTask :: (Int -> (Code a p)) -> (Code a p)
setCode :: Def -> (Code a p)
getCode :: (Def -> Code a p) -> (Code a p)
brac :: (Code a p) -> Code b q
funBody :: (Code a p) -> Code b q
codeOp2 :: (Code a p) String (Code b q) -> Code c r
include :: String -> Code a b
argList :: [a] -> String | toCode a
c :: a -> Code b p | toCode a
indent :: Code a p
unindent :: Code a p
nl :: Code a p
setBinds :: [String] -> Code a p
addBinds :: String -> Code a p
getBinds :: ([String] -> Code a p) -> (Code a p)

// ----- driver ----- //

compile :: (Main (Code a p)) -> [String]
mkset :: [a] -> [a] | Eq a
newCode :: CODE

// ----- simulation ----- //

eval :: (Main (Eval t p)) -> [String] | toString t
:: State = 
  { tasks :: [(Int, State->State)]
  , store :: [Dyn]
  , dpins :: [(DigitalPin, Bool)]
  , apins :: [(AnalogPin, Int)]
  , serial:: [String]
  , millis:: Int
  }

state0 :: State

//:: TaskSim :== (Int, State->State)
:: Eval t p = E ((ReadWrite t) State -> (t, State))
toS2S :: (Eval t p) -> (State->State)

unEval :: (Eval t p) -> ((ReadWrite t) State -> (t, State))

:: 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

rtrn :: t -> Eval t p

yield :: t (Eval s p) -> Eval t Expr
//yield a (E f) = E (\r s.(\(_,t).(a,t)) (f r s))

instance arith Eval
instance boolExpr Eval
instance If Eval p q Expr
instance IF Eval
instance var2 Eval

defEval2 :: t ((Eval t p)->Main (Eval u q)) -> (Main (Eval u q)) | dyn t
instance sds Eval

defEval :: ((Eval t p)->In t (Main (Eval u q))) -> (Main (Eval u q)) | dyn t
instance fun Eval x | arg x
instance mtask Eval x | arg x
instance mtasks Eval x y | arg x & arg y
instance setDelay Eval

class toExpr v where toExpr :: (v t p) -> v t Expr
instance toExpr Eval
instance toExpr Code
instance seq Eval
instance assign Eval
instance output Eval
instance pinMode Eval
instance digitalIO Eval
instance analogIO Eval
instance noOp Eval

class arg x :: x -> Int
instance arg ()
instance arg (Eval t p) | type t
instance arg (Eval t p, Eval u q) | type t & type u
instance arg (Eval t p, Eval u q, Eval v r) | type t & type u & type v
instance arg (Eval t p, Eval u q, Eval v r, Eval w s) | type t & type u & type v

instance + String

readPinA :: AnalogPin [(AnalogPin, Int)] -> Int
writePinA :: AnalogPin Int State -> State

class readPinD p :: p [(DigitalPin,Bool)] [(AnalogPin,Int)] -> Bool
instance readPinD DigitalPin
instance readPinD AnalogPin

class writePinD p :: p Bool State -> State
instance writePinD DigitalPin
instance writePinD AnalogPin

// ----- Interactive Simulation ----- //

derive class iTask DigitalPin, AnalogPin, Dyn, StateInterface, DisplayVar, Pin

simulate :: (Main (Eval a p)) -> Task ()
toView :: State -> StateInterface
mergeView :: State StateInterface -> State
:: StateInterface =
  { serialOut   :: Display [String]
  , analogPins  :: [(AnalogPin, Int)]
  , digitalPins :: [(DigitalPin, Bool)]
  , var2iables   :: [DisplayVar]
  , timer     :: Int
  , taskCount   :: Display Int
  }

toDisplayVar :: Dyn -> DisplayVar
fromDisplayVar :: DisplayVar Dyn -> Dyn
:: DisplayVar
    = Variable String
    | INT Int
    | LONG Int
    | Servo Pin Int
    | LCD16x2 String String
    | DisplayVar [String]

step` :: State -> State

class stringQuotes t | type t :: (Code t p) -> Code t p
instance stringQuotes String
instance stringQuotes t

derive   toGenDynamic (), MTask, DigitalPin, AnalogPin, Pin, [], Long //, Servo
derive fromGenDynamic (), MTask, DigitalPin, AnalogPin, Pin, [], Long //, Servo
instance toCode ()
instance ==   ()

// ----- long ----- //

:: Long = L Int // 32 bit on Arduino
instance toCode Long
instance + Long
instance - Long
instance * Long
instance / Long
instance == Long
instance one Long
instance zero Long

class long v t :: (v t p) -> v Long Expr | isExpr p
instance long Code Int
instance long Code Long
instance long Eval Int
instance long Eval Long

// ----- tools ----- //

class toCode a :: a -> String
instance toCode Bool
instance toCode Int
instance toCode Real
instance toCode Char
instance toCode String
instance toCode DigitalPin
instance toCode AnalogPin
derive consName DigitalPin, AnalogPin, PinMode

instance == DigitalPin
instance == AnalogPin

derive consIndex DigitalPin, AnalogPin

tab =: toString (repeatn tabSize ' ')
tabSize :== 2

instance toString ()

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