contract Remote =
  stateful function remote_spend : (address, int) => ()
  function remote_pure : int => int

contract Stateful =

  private function pure(x) = x + 1
  private stateful function local_spend(a) =
    Chain.spend(a, 1000)

  // Non-stateful functions cannot mention stateful functions
  function fail1(a : address) = Chain.spend(a, 1000)
  function fail2(a : address) = local_spend(a)
  function fail3(a : address) =
    let foo = Chain.spend
    foo(a, 1000)

  // Private functions must also be annotated
  private function fail4(a) = Chain.spend(a, 1000)

  // If annotated, stateful functions are allowed
  stateful function ok1(a : address) = Chain.spend(a, 1000)

  // And pure functions are always allowed
  stateful function ok2(a : address) = pure(5)
  stateful function ok3(a : address) =
    let foo = pure
    foo(5)

  // No error here (fail4 is annotated as not stateful)
  function ok4(a : address) = fail4(a)

  // Lamdbas are checked at the construction site
  private function fail5() : address => () = (a) => Chain.spend(a, 1000)

  // .. so you can pass a stateful lambda to a non-stateful higher-order
  // function:
  private function apply(f : 'a => 'b, x) = f(x)
  stateful function ok5(a : address) =
    apply((val) => Chain.spend(a, val), 1000)

  // It doesn't matter if remote calls are stateful or not
  function ok6(r : Remote) = r.remote_spend(Contract.address, 1000)
  function ok7(r : Remote) = r.remote_pure(5)

  // But you can't send any tokens if not stateful
  function fail6(r : Remote) = r.remote_spend(value = 1000, Contract.address, 1000)
  function fail7(r : Remote) = r.remote_pure(value = 1000, 5)
  function fail8(r : Remote) =
    let foo = r.remote_pure
    foo(value = 1000, 5)
  function ok8(r : Remote) = r.remote_spend(Contract.address, 1000, value = 0)