(import scheme
        (chicken base)
        checks
        simple-tests
        simple-contracts)
(contract-check-level 1)

(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?)
  "SOME DEFINITIONS"
  (set!-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))))

  (set!-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)
        )))

  (set!-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)))

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

  (set!-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))))))

  "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 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 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 argument) #f)))
  '(xdefine ((result list?)
             wrong-sum
             (a integer?) as integer?)
    (apply + a as))
  (not (condition-case (wrong-sum 1 2 3) ((exn result) #f)))
  )
  
(compound-test (SIMPLE-CONTRACTS)
  (contracts?)
  )