test_fun.idr

module Main

%default total

data Event = Started Int | Stopped Int | Completed Int
data State = Idle | Running | Finished

data S : s -> Type

data Activity : Type -> Event -> Type -> Type where
  Start            : Activity (S Idle)    (Started x)   (S Running)
  Stop             : Activity (S Running) (Stopped x)   (S Idle)
  Complete_Idle    : Activity (S Idle)    (Completed x) (S Finished)
  Complete_Running : Activity (S Running) (Completed x) (S Finished)

data MyAct = Idle0 Int | Running0 Int Int | Finished0 Int

inject : (s: MyAct) -> Type
inject (Idle0 _)      = S Idle
inject (Running0 _ _) = S Running
inject (Finished0 _)  = S Finished

onEvent : (m: MyAct) -> (e: Event) -> {auto prf: Activity (inject m) e _}
  -> (r ** Activity (inject m) e (inject r))
onEvent (Idle0 x)      (Started y)   = (Running0 x y          ** Start)
onEvent (Running0 x y) (Stopped z)   = (Idle0 (x + z - y)     ** Stop)
onEvent (Idle0 x)      (Completed z) = (Finished0 x           ** Complete_Idle)
onEvent (Running0 x y) (Completed z) = (Finished0 (x + z - y) ** Complete_Running)

str : MyAct -> String
str (Idle0 _) = "idle"
str (Running0 _ _) = "running"
str (Finished0 _) = "finished"

main : IO ()
main = let (x ** _) = onEvent (Idle0 0) (Started 10) {prf = Start} in
  print (str x)