
  0 | module Control.Cont.State
  1 | 
  2 | import Control.HigherOrder
  3 | 
  4 | import Control.Monad.Free
  5 | 
  6 | public export
  7 | data StateC1 : Type -> Type -> Type where
  8 |   Get : (s -> x) -> StateC1 s x
  9 |   Put : s -> x -> StateC1 s x
 10 | 
 11 | public export
 12 | Functor (StateC1 s) where
 13 |   map f (Get g) = Get (f . g)
 14 |   map f (Put s x) = Put s (f x)
 15 | 
 16 | public export
 17 | StateC : Type -> (Type -> Type) -> Type -> Type
 18 | StateC s = Lift (StateC1 s)
 19 | 
 20 | public export
 21 | runStateC : Syntax sig
 22 |          => s
 23 |          -> Free (StateC s :+: sig) a
 24 |          -> Free sig (s, a)
 25 | runStateC s (Return x) = Return (s, x)
 26 | runStateC s (Op (Inl (MkLift (Get k)))) =
 27 |   runStateC s (k s)
 28 | runStateC s (Op (Inl (MkLift (Put s' k)))) =
 29 |   runStateC s' k
 30 | runStateC s (Op (Inr op)) =
 31 |   Op (weave {m1 = ?t} {s = Pair _} (s, ()) (uncurry runStateC) op)
 32 | 
 33 | public export
 34 | get : (Inj (StateC s) sig) => Free sig s
 35 | get = inject {sub = StateC s} (MkLift (Get Return))
 36 | 
 37 | public export
 38 | put : (Inj (StateC s) sig) => s -> Free sig ()
 39 | put val = inject {sub = StateC s} (MkLift (Put val (Return ())))
 40 | 
 41 | public export
 42 | modify : Syntax sig => Inj (StateC s) sig => (s -> s) -> Free sig ()
 43 | modify f = do
 44 |   v <- get
 45 |   put (f v)
 46 | 
 47 | public export
 48 | withSt : Syntax sig => Inj (StateC st) sig => a -> Free sig (st, a)
 49 | withSt x = map (, x) get
 50 | 
 51 |