(import scheme
        (chicken base)
        checks
        simple-tests
        simple-contracts)

(contract-check-level 1)

(define-values (counter! counter)
  (let ((state 0))
    (values
      (xlambda ((new (cut = <> (add1 old)))
                ;integer? (lambda (x) (= x (add1 old))))
                (old integer?)
                <-)
        (let ((old state))
          (set! state (add1 state))
          (values state old)))
      (xlambda ((result (cut = <> state))
                <-)
        state))))

(define-values (push pop top)
  (let ((stk '()))
    (let (
          (push
            (xlambda ((new list? (cut equal? <> (cons arg old))) 
                      (old list?)
                      <-
                      (arg))
              (let ((old stk))
                (set! stk (cons arg stk))
                (values stk old))))
          (pop
            (xlambda ((new list? (cut equal? <> (cdr old)))
                      (old list?)
                      <-)
              (let ((old (<<< 'pop stk (o not null?))))
                (set! stk (cdr stk))
                (values stk old))))
          (top
            (xlambda ((result) <-)
              (car (<<< 'top stk (o not null?)))))
          )
      (values push pop top)
      )))

(define-values (add add-pre add-post)
  (xlambda ((result integer? odd? (cut = <> (apply + x y ys)))
            <-
            (x integer? odd?) (y integer? even?) ys integer? even?)
    (apply + x y ys)))

(define wrong-add
  (xlambda ((result integer? even?)
            <-
            (x integer? odd?) xs integer?  even?)
    (apply + x xs)))

(define-values (divide divide-pre divide-post)
  (xlambda ((q integer?)
            (r (lambda (x) (= (+ x (* n q)) m)))
            <-
            (m integer? (cut >= <> 0))
            (n integer? positive?))
    (let loop ((q 0) (r m))
      (if (< r n)
        (values q r)
        (loop (+ q 1) (- r n))))))

(xdefine ((result integer?)
          #(sum-post sum sum-pre)
          (a integer?) as integer?)
  (apply + a as))

(xdefine ((result list?)
          wrong-sum
          (a integer?) as integer?)
  (apply + a as))

(define-test (contracts?)

  "QUERIES"
  '(define-values (add add-pre add-post)
     (xlambda ((result integer? odd? (cut = <> (apply + x y ys)))
               <-
               (x integer? odd?) (y integer? even?) ys integer? even?)
       (apply + x y ys)))
  (= (add 1 2 4 6) 13)
  (equal? add-pre
          '((x integer? odd?)
            (y integer? even?)
            ys integer?  even?))
  (equal? add-post
          '(result integer? odd? (cut = <> (apply + x y ys))))
  (not (condition-case (add 1 2 3) ((exn) #f)))
  ;(not (condition-case (add 1 2 3) ((exn argument) #f)))

  '(define wrong-add
     (xlambda ((result integer? even?)
               <-
               (x integer? odd?) xs integer?  even?)
       (apply + x xs)))
  (not (condition-case (wrong-add 1 2 4) ((exn) #f)))
  ;(not (condition-case (wrong-add 1 2 4) ((exn result) #f)))

  '(define-values (divide divide-pre divide-post)
     (xlambda ((q integer?)
               (r (lambda (x) (= (+ x (* n q)) m))
               <-
               (m integer? (cut >= <> 0))
               (n integer? positive?))
       (let loop ((q 0) (r m))
         (if (< r n)
           (values q r)
           (loop (+ q 1) (- r n)))))))
  (equal?
    (call-with-values
      (lambda () (divide 385 25))
      list)
    '(15 10))
  (equal? divide-pre
          '((m integer? (cut >= <> 0))
            (n integer? positive?)))
  (equal? divide-post
          '((q integer?)
            (r (lambda (x) (= (+ x (* n q)) m)))))

  "COMMANDS"
  '(define-values (counter! counter)
     (let ((state 0))
       (values
         (xlambda ((new (cut = <> (add1 old)))
                   (old integer?)
                   <-)
           (let ((old state))
             (set! state (add1 state))
             (values state old)))
         (xlambda ((result (cut = <> state)) <-)
           state))))
  (zero? (counter))
  (counter!)
  (= (counter) 1)
  (counter!)
  (= (counter) 2)

  '(define-values (push pop top)
     (let ((stk '()))
       (let (
             (push
               (xlambda ((new list? (cut equal? <> (cons arg old)))
                         (old list?)
                         <-
                         (arg))
                 (let ((old stk))
                   (set! stk (cons arg stk))
                   (values stk old))))
             (pop
               (xlambda ((new list? (cut equal? <> (cdr old)))
                         (old list?)
                         <-)
                 (let ((old (<<< 'pop stk (o not null?))))
                   (set! stk (cdr stk))
                   (values stk old))))
             (top
               (xlambda ((result) <-)
                 (car (<<< 'top stk (o not null?)))))
             )
         (values push pop top)
         )))
  ;(top) ; precondition violated
  ;(pop) ; precondition violated
  (push 0)
  (push 1)
  (= 1 (top))
  (equal? (call-with-values (lambda () (push 2)) list)
          '((2 1 0) (1 0)))
  (= 2 (top))
  (equal? (call-with-values (lambda () (pop)) list)
          '((1 0) (2 1 0)))
  "XDEFINE"
  ;(xdefine ((result integer?) sum (a integer?) as integer?)
  '(xdefine ((result integer?)
             #(sum-post sum sum-pre)
             (a integer?) as integer?)
     (apply + a as))
  ;(print sum-post)
  ;(print sum-pre)
  (= (sum 1 2 3) 6)
  (not (condition-case (sum 1 2 #f) ((exn) #f)))
  ;(not (condition-case (sum 1 2 #f) ((exn argument) #f)))
  '(xdefine ((result list?)
             wrong-sum
             (a integer?) as integer?)
    (apply + a as))
  (not (condition-case (wrong-sum 1 2 3) ((exn) #f)))
  ;(not (condition-case (wrong-sum 1 2 3) ((exn result) #f)))
  )
  
(compound-test (SIMPLE-CONTRACTS)
  (contracts?)
  )