;;; File: contracts-run.scm

(require 'contracts)
(import contracts)
(import-for-syntax (only contracts
                     ir-macro-rules
                     er-macro-rules))

(define (true? x) #t)

(doclist '())

;;; Example with procedure body wrapped into a let expression
(define-with-contract adder! ;ok!
  (let ((state 0))
    (contract (adder! arg)
      "adds its argument to its state"
      (domain (number? arg))
      (effect (old state (+ old arg))))
      ;(effect: (old state (+ old arg 1)))) ;wrong on purpose
    (lambda (arg)
      (set! state (+ state arg))
      ;; export state for error checking
      (set! exported state)
      )))

;; to check adder!
(define exported #f)

;Example: An implementation of the single datatype 
;-------------------------------------------------
;Here is a simple, but realistic example, in which commands and queries
;are involved, the single datatype, which does the same what boxes do.

;;; predicate
(define-with-contract (single? xpr)
  "check, if xpr evaluates to a single"
  (and (procedure? xpr)
       (condition-case (eq? 'single (xpr (lambda (a b c) a)))
         ((exn) #f))))

;;; constructor
(define-with-contract (single xpr)
  "package the value of xpr into a single object"
  (domain (true? xpr))
  (range (single? result))
  (lambda (sel)
    (sel 'single xpr (lambda (new) (set! xpr new)))))

;;; query
(define-with-contract (single-state sg)
  "returns the state of the single object sg"
  (domain (single? sg))
  (range (true? result))
  (sg (lambda (a b c) b)))

;;; command
(define-with-contract (single-state! sg arg)
  "replaces state of sg with arg"
  (domain (single? sg) (true? arg))
  ;(effect: (state (single-state sg) (+ arg 1))) ; wrong on purpose
  (effect (state (single-state sg) arg))
  ((sg (lambda (a b c) c)) arg))

;;; macros
;;; the freeze macro implemented in the different styles
(define-syntax-with-contract (sefreeze xpr)
  "short er-version of freeze"
  (with-renamed (%lambda) `(,%lambda () ,xpr)))
(define-syntax-with-contract (sifreeze xpr)
  "short ir-version of freeze"
  (with-injected () `(lambda () ,xpr)))
(define-syntax-with-contract sfreeze
  "syntax-rules version of freeze"
  (syntax-rules ()
    ((_ xpr) (lambda () xpr))))
(define-syntax-with-contract ifreeze
  "ir-macro-rules version of freeze"
  (ir-macro-rules ()
    ((_ xpr) `(lambda () ,xpr))))
(define-syntax-with-contract efreeze
  "er-macro-rules version of freeze"
  (er-macro-rules (%lambda)
    ((_ xpr) `(,%lambda () ,xpr))))
(define-syntax-with-contract lifreeze
  (syntax-contract (lifreeze xpr)
    "ir-macro-transformer version of freeze")
  (ir-macro-transformer
    (lambda (f i c) `(lambda () ,(cadr f)))))
(define-syntax-with-contract lefreeze
  (syntax-contract (lefreeze xpr)
    "er-macro-transformer version of freeze")
  (er-macro-transformer
    (lambda (f r c) `(,(r 'lambda) () ,(cadr f)))))
(define-syntax-with-contract er-or
  "er-version of or"
  (er-macro-rules (%if %er-or)
    ((_) #f)
    ((_ arg . args)
     `(,%if ,arg ,arg (,%er-or ,@args)))))
  
(define-syntax-with-contract ir-or
  "ir-version of or"
  (ir-macro-rules ()
    ((_) #f)
    ((_ arg . args)
     `(if ,arg ,arg (ir-or ,@args)))))
  
(define-syntax-with-contract ior
  "limited ir-version of or to test match errors"
  (ir-macro-rules ()
    ((_) #f)
    ((_ arg) arg)
    ((_ arg arg1)
     `(if ,arg ,arg (ior ,arg1)))))
  
(define-syntax-with-contract eor
  "limited er-version of or to test match errors"
  (er-macro-rules (%if %eor)
    ((_) #f)
    ((_ arg) arg)
    ((_ arg arg1)
     `(,%if ,arg ,arg (,%eor ,arg1)))))
  
(define docs (doclist->dispatcher (doclist)))

(define sg (single 5))

;;; (run xpr0 xpr1 ...)
;;; -------------------
(define (run . xprs)
  (let loop ((xprs xprs))
    (if (null? xprs)
      (print "All tests passed!")
      (if (car xprs)
        (loop (cdr xprs))
        (error 'run "#### Some test failed! ####")))))

(run
  (= (begin (adder! 5) exported) 5)
      (= (begin (adder! 3) exported) 8)
      (eq? (single? (single 3)) #t)
      (eq? (single? sg) #t)
      (eq? (single? 5) #f)
      (= (single-state sg) 5)
      (= (begin (single-state! sg 3) (single-state sg)) 3)
      (= (bind x 1 x) 1)
      (equal? (bind (x (y (z . u) v) . w) '(1 (2 (3) 4) 5 6)
                (list x y z u v w))
              '(1 2 3 () 4 (5 6)))
      (equal? (bind (x (y (z . u) v) . w) '(1 (2 (3 . 3) 4) 5 6)
                (list x y z u v w))
              '(1 2 3 3 4 (5 6)))
      (equal? (bind-case '(1 (2 3))
                ((x (y z)) (list x y z))
                ((x (y . z)) (list x y z))
                ((x y) (list x y)))
              '(1 2 3))
      (equal? (bind-case '(1 (2 3))
                ((x (y . z)) (list x y z))
                ((x y) (list x y))
                ((x (y z)) (list x y z)))
              '(1 2 (3)))
      (equal? (bind-case '(1 (2 3))
                ((x y) (list x y))
                ((x (y . z)) (list x y z))
                ((x (y z)) (list x y z)))
              '(1 (2 3)))
      (equal? (bind-case '(1 (2 . 3))
                ((x (y . z)) (list x y z))
                ((x (y z)) (list x y z)))
              '(1 2 3))
      (equal? (bind-case '(1 (2 . 3))
                ((x y) (list x y))
                ((x (y . z)) (list x y z))
                ((x (y z)) (list x y z)))
              '(1 (2 . 3)))
;      (eqv? (matches? 1 x) #t)
;      (eqv? (matches? '(1 2) x (x y)) #t)
;      (eqv? (matches? '(1 2) x) #t)
;      (eqv? (matches? '(1 2) (x y z)) #f)
;      (eqv? (matches? '(1 2) (x (y z))) #f)
;      (eqv? (matches? '(1 (2 3)) (x (y . z))) #t)
;      (eqv? (matches? '(1 (2 3)) (x y z)) #f)
;      (eqv? (matches? '(1 (2 3)) (a b) (x y z)) #t)
;      (eqv? (matches? '(1 (2 3)) (a b) (x y z) (x (y z))) #t)
      (= (er-or #f 1 #f) 1)
      (= (ir-or #f 1 #f) 1)
      (eqv? (er-or #f #f #f) #f)
      (eqv? (ir-or #f #f #f) #f)
      (= ((efreeze 3)) 3)
      (= ((ifreeze 3)) 3)
      (= ((sfreeze 3)) 3)
      (= ((lefreeze 3)) 3)
      (= ((lifreeze 3)) 3)
      (= ((sefreeze 3)) 3)
      (= ((sifreeze 3)) 3)
      )