--- /dev/null
+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
repositories / mTask.git / blobdiff