unison/unison-src/tests/state3.u

31 lines
639 B
Plaintext

--State3 effect
effect State se2 where
put : ∀ se . se -> {State se} ()
get : ∀ se . () -> {State se} se
state : ∀ s a . s -> Effect (State s) a -> (s, a)
state woot eff = case eff of
{ State.get () -> k } -> handle (state woot) in (k woot)
{ State.put snew -> k } -> handle (state snew) in (k ())
{ a } -> (woot, a)
ex1 : (UInt64, UInt64)
ex1 = handle (state 42) in State.get ()
ex1a : (UInt64, UInt64)
ex1a = handle (state 42) in 49
ex1b = handle (x -> 10) in 0
ex1c : UInt64
ex1c = handle (x -> 10) in 0
ex1d = handle (state 42) in 49
ex2 = handle (state 42) in State.get ()
ex3 : (UInt64, UInt64)
ex3 = ex2
()