-- This file defines the State Monad

--#include "Monads.alfa"

--#include "Alfa/Tuples.alfa"

package State where
  open Tuples  use  Unit,  unit,  Pair,  pair,  curry,  fst,  snd
  open Monads  use  Monad
  StateM (S::Set)(A::Set) :: Set
    = S -> Pair A S
  return (S::Set)(A::Set) :: A -> StateM S A
    = pair A S
  uncurry (A::Set)(B::Set)(C::Set)(f::A -> B -> C)(p::Pair A B) :: C
    = f (fst A B p) (snd A B p)
  (>>=) (S::Set)(A::Set)(B::Set)(m1::StateM S A)(xm2::A -> StateM S B)
    :: StateM S B
    = \(s::S) -> uncurry A S (Pair B S) xm2 (m1 s)
  inst (S::Set) :: Monad (StateM S)
    = struct {
        unit = return S;
        bind = (>>=) S;}
  load (S::Set) :: StateM S S
    = \(s::S) -> pair S S s s
  store (S::Set)(s::S) :: StateM S Unit
    = \(s'::S) -> Pair@_ unit s
  update (S::Set)(f::S -> S) :: StateM S Unit
    = \(s::S) -> Pair@_ unit (f s)
  inFst (S1::Set)(S2::Set)(A::Set)(m::StateM S1 A)
    :: StateM (Pair S1 S2) A
    = \(s1s2::Pair S1 S2) ->
      case s1s2 of {
        (Pair s1 s2) ->
          case m s1 of { (Pair a s1') -> Pair@_ a (Pair@_ s1' s2);};}
  inSnd (S1::Set)(S2::Set)(A::Set)(m::StateM S2 A)
    :: StateM (Pair S1 S2) A
    = \(s1s2::Pair S1 S2) ->
      case s1s2 of {
        (Pair s1 s2) ->
          case m s2 of { (Pair a s2') -> Pair@_ a (Pair@_ s1 s2');};}
{-# Alfa unfoldgoals off
brief on
hidetypeannots off
wide

nd
hiding on
var "load" hide 2
var "inFst" hide 3
var "inSnd" hide 3
var "store" hide 1
var "update" hide 1
 #-}