#lang scheme/load

(module inside scheme
  (require (planet tov/affine-contracts:2:0))
  
  ;; adder : number? -> number? -o number?
  ;; A curried addition function.  The result of partial application
  ;; should be applied at most once, since subsequent applications would
  ;; try to add a symbol.
  (define ((adder x) y)
    (let ([result (+ x y)])
      (set! x 'symbol)
      result))

  (define-affine-box counter number?)

  ;; new-counter : -> counter/c
  (define (new-counter)
    (make-counter 0))
  
  ;; next-counter : counter/c -> (values number? counter/c)
  (define (next-counter b)
    (let ([v (counter-ref b)])
      (values v (make-counter (+ v 1)))))
  
  (provide/contract
   [adder        (number? . -> . (number? . -o . number?))]
   [new-counter  (-> counter/c)]
   [next-counter (counter/c . -> . (values number? counter/c))])
  )

(require 'inside)

(define a (new-counter))
(define-values (b c) (next-counter a))
(define-values (d e) (next-counter c))

(define f (adder 3))

;; Applying bad1 or bad2 is a contract violation:
(define (bad1)
  (next-counter a))

(define (bad2)
  (next-counter c))

;; Applying either of these twice is a contract violation:
(define (bad-if-twice1)
  (next-counter e))

(define (bad-if-twice2)
  (f 4))