; Author: Juergen Lorenz ; ju (at) jugilo (dot) de
;
; Copyright (c) 2016, Juergen Lorenz
; All rights reserved.
; 
; Redistribution and use in source and binary forms, with or without
; modification, are permitted provided that the following conditions are
; met:
; 
; Redistributions of source code must retain the above copyright
; notice, this list of conditions and the following dispasser.
; 
; Redistributions in binary form must reproduce the above copyright
; notice, this list of conditions and the following dispasser in the
; documentation and/or other materials provided with the distribution.
; 
; Neither the name of the author nor the names of its contributors may be
; used to endorse or promote products derived from this software without
; specific prior written permission. 
; 
; THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
; IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
; TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
; PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
; HOLDERS OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
; SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED
; TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
; PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
; LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
; NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
; SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

#|[
This is my third attempt to implement Bertrand Meyer's Design by
contract in Chicken. The other two, contracts and dbc are now considered
obsolete.
We enhance arguments and return values of lambda-expressions by pre- and
postconditions respectively, thus marking a clear distinction between
the duties of suppliers and clients. If the arguments of a procedure
call pass the preconditions and a post-exception is raised, then the
supplier is to blame. On the other hand, if a pre-exception is raised
when a procedure-call is issued, then the client has violenced its
duties and the supplier is not even forced to do anything at all. In
other words, the supplier can safely assume a procedure is called
with correct arguments, he or she need not and should not check tehem
again.

Off course, pre- and postconditions must be stored in the procedure
itself and a representation of them must be exportable, so that both
parties of the contract know their duties. Here is the syntax of
xdefine, a macro to implement queries, i.e. routines without state
changes.

(xdefine ((r r? ...) ... name (a a? ...) ... [as as? ...]) xpr ....)

where name is the name of the procedure, r ... are retrurn values with
corresponding postconditions r? ..., a ... are fixed variables with
preconditions a? ... and as is an optional variable argument with
preconditions as? ...

For state-changing routines, so called commands, xlambda must
be used. The syntax is

(xlambda k ((r r? ...) ... (a a? ...) ... [as as? ...]) xpr ....)

where k is the number of return values. xlambda can be defined on top of
a let, thus supplying state. But even those routines must return values,
namely the values of state variables before a state change has taken
place. So one can check, if the state change did what it should have
done.

Note, that a parameter, contract-check-level, is supplied, so that one
can always control what to check, nothing, only preconditions or pre-
and postconditions. Only precondition check is the default.

]|#

(require-library simple-exceptions)

(module simple-contracts
  (simple-contracts %% pipe xlambda xdefine contract-check-level)

(import scheme 
        (only chicken define-inline signum make-parameter case-lambda error print)
        (only data-structures conjoin)
        (only simple-exceptions make-exception raise pre-exception
              post-exception << >> true? false?))

(import-for-syntax (only chicken receive))

;;; (contract-check-level arg ..)
;;; --------------------
;;; parameter
(define contract-check-level
  (make-parameter 0
                  (lambda (x)
                   (if (and (integer? x)
                            (exact? x))
                     (signum x)
                     0))))

;;; (define-er-macro (name form rename compare?) xpr . xprs)
;;; --------------------------------------------------------
(define-syntax define-er-macro
  (syntax-rules ()
    ((_ (name form rename compare?) xpr . xprs)
     (define-syntax name
       (er-macro-transformer
         (lambda (form rename compare?) xpr . xprs))))))

;;; (define-ir-macro (name form inject compare?) xpr . xprs)
;;; --------------------------------------------------------
(define-syntax define-ir-macro
  (syntax-rules ()
    ((_ (name form inject compare?) xpr . xprs)
     (define-syntax name
       (ir-macro-transformer
         (lambda (form inject compare?) xpr . xprs))))))

;;; (pipe combination ...)
;;; ----------------------
;;; sequencing curried combinations
(define-er-macro (pipe form rename compare)
  (let ((combinations (cdr form))
        (%lambda (rename 'lambda))
        (%pipe (rename 'pipe))
        (%x (rename 'x)))
    (cond
      ((null? combinations)
       `(,%lambda (,%x) ,%x))
      ((null? (cdr combinations))
       (if (pair? (car combinations))
         `(,%lambda (,%x)
            (,(caar combinations)
             ,%x ,@(cdar combinations)))
         `(,%lambda (,%x) ;,(car combinations))))
                          ,(rename (car combinations)))))
      (else
        `(,%lambda (,%x)
           ((,%pipe ,@(cdr combinations))
            ((,%pipe ,(car combinations))
             ,%x)))))))

;;; (%% proc)
;;; --------
;;; multi argument version of flip, which can be used in pipe
(define (%% proc)
  (lambda args
    (if (null? args)
      (proc)
      (apply proc (append (cdr args)
                          (list (car args)))))))

;;; TODO: replace prec and cons by contracts
;;;(preconditions proc pre post)
;;;(postconditions proc pre post)
;;; -----------------------------
;;; to be used in call-with-values
(define-inline (preconditions proc pre post) pre)
(define-inline (postconditions proc pre post) post)

;;; dbc for procedures
;;; ==================
;;; (xlambda [k] ((r1 r1? ...) ...(rk rk? ...)
;;;               (x x? ...) ... xs xs? ...)
;;;   xpr ....)
;;; -------------------------------------------
;;; contract-handling lambda:
;;; k -- if provided -- is the number of return values r1 ... rk,
;;; 1 otherwise,
;;; the following predicates naming the corresponding postconditions,
;;; x ... are the fixed arguments, xs the optional variable arguments,
;;; the following predicates naming the corresponding preconditions.
(define-ir-macro (xlambda form inject compare?)
  (let ((multi? (integer? (cadr form))))
    (let ((k (if multi? (cadr form) 1))
          (header (if multi?
                    (caddr form)
                    (cadr form)))
          (xpr (if multi?
                 (cadddr form)
                 (caddr form)))
          (xprs (if multi?
                  (cddddr form)
                  (cdddr form))))
      (receive (xargs returns)
        (let loop ((n 0) (tail header) (head '()))
          (if (= n k)
            (values tail (reverse head))
            (loop (+ n 1) (cdr tail) (cons (car tail) head))))
        (receive (xhead xrest)
          (let loop ((tail xargs) (head '()))
            (cond
              ((null? tail)
               (values (reverse head) tail))
              ((symbol? (car tail))
               (values (reverse head) tail))
              (else
                (loop (cdr tail) (cons (car tail) head)))))
          (let ((fargs (map car xhead))
                (vargs (if (null? xrest)
                         '()
                         (car xrest))))
            (let* (
              ;; no checks
              (proc `(lambda (,@fargs ,@vargs)
                       ,xpr ,@xprs))
              ;; check preconditions
              (xproc 
                (if (null? xrest)
                  `(lambda (,@fargs)
                     (apply ,proc
                            (map (lambda (p a) (p a))
                                 (list ,@(map (lambda (x)
                                                `(pipe (<< ,@(cdr x))))
                                              xhead))
                                 (list ,@fargs))))
                  `(lambda (,@fargs ,@vargs)
                     (apply ,proc
                            (append
                              (map (lambda (p a) (p a))
                                   (list ,@(map (lambda (x)
                                                  `(pipe (<< ,@(cdr x))))
                                                xhead))
                                   (list ,@fargs))
                              (map (lambda (a)
                                     (<< a ,@(cdr xrest)))
                                   ,vargs))))))
              ;; check postconditions
              (xxproc
                (let ((args->vals
                        (lambda (fargs vargs)
                          (if (null? vargs)
                              `(list ,@fargs)
                              `(append (list ,@fargs) ,vargs)))))
                  (if (null? (cdr returns))
                      ;(symbol? (car returns))
                    ;; only one returned value
                    `(lambda (,@fargs ,@vargs)
                       (>> (apply ,xproc
                                  ,(args->vals fargs vargs))
                           ,@(cdar returns)))
                           ;,@(cdr returns)))
                    ;; multiple returned values
                    `(lambda (,@fargs ,@vargs)
                       (call-with-values
                         (lambda ()
                           (apply ,xproc ,(args->vals fargs vargs)))
                         (lambda ,(map car returns)
                           (values ,@(map (lambda (r) `(>> ,@r))
                                          returns))))))))
              )
              `(values
                  (case (contract-check-level)
                     ((-1) ,proc)
                     ((0)  ,xproc)
                     ((+1) ,xxproc))
                 ;; preconditions
                 ',(append
                     (map (lambda (x)
                            `(,(car x) ;(conjoin ,@(cdr x))))
                              ,(cond
                                 ((null? (cdr x)) 'true?)
                                 ((null? (cddr x)) (cadr x))
                                 (else `(conjoin ,@(cdr x))))))
                          xhead)
                     (if (null? xrest)
                       '()
                       `(,(car xrest) ;(conjoin ,@(cdr xrest)))))
                         ,(cond
                            ((null? (cdr xrest)) 'true?)
                            ((null? (cddr xrest)) (cadr xrest))
                            (else `(conjoin ,@(cdr xrest)))))))
                 ;; postconditions
                 ',(if (null? (cdr returns)) ; one return value
                       ;(symbol? (car returns))
                     (let ((returns (car returns)))
                       `(,(car returns)
                         ,(cond
                            ((null? (cdr returns)) 'true?)
                            ((null? (cddr returns)) (cadr returns))
                            (else `(conjoin ,@(cdr returns))))))
                     (map (lambda (x)
                            `(,(car x)
                              ,(cond
                                 ((null? (cdr x)) 'true?)
                                 ((null? (cddr x)) (cadr x))
                                 (else `(conjoin ,@(cdr x))))))
                          returns))
                 ))))))))

;;; (xdefine ((r1 r1? ...) ... (rk rk? ...)
;;;           name
;;;           (x x? ...) ... xs xs? ...)
;;;            xpr . xprs)
;;; ----------------------------------------------
(define-er-macro (xdefine form rename compare?)
  (let ((header (cadr form))
        (xpr (caddr form))
        (xprs (cdddr form))
        (%define (rename 'define))
        (%xlambda (rename 'xlambda)))
    (receive (k main returns)
      (let loop ((n 0) (tail header) (head '()))
        (if (symbol? (car tail))
          (values n tail (reverse head))
          (loop (+ n 1) (cdr tail) (cons (car tail) head))))
      `(,%define ,(car main)
                 (,%xlambda ,k ,(append returns (cdr main)) ,xpr ,@xprs)))))

;;; (simple-contracts sym ..)
;;; -------------------------
;;; documentation procedure
(define simple-contracts
  (let ((als '(
    (simple-contracts
      procedure:
      (bindings sym ..)
      "documentation procedure")
    (contract-check-level
      parameter:
      (contract-check-level n ..)
      "no contract checks if n is -1"
      "only precondition checks if n is 0, the default"
      "pre- and postcondition checks if n is +1")
    (xdefine
      macro:
      (xdefine ((r r? ...) ... name (a a? ...) ... [as as? ...]) . body)
      "contract guarded version of define for procedures, where"
      "name is the name of the procedure"
      "r ... are return values with corresponding postcondition r?"
      "a ... are fixed arguments with preconditions a? ..."
      "as is an optional variable argument with preconditions as? ...")
    (xlambda
      macro:
      (xlambda k ((r r? ...) ... (a a? ...) ... [as as? ...]) . body)
      "contract guarded version of lambda, where"
      "k is the number of returned values r ..."
      "r? ... their corresponding postconditions"
      "a ... are fixed arguments with preconditions a? ..."
      "as is an optional variable argument with preconditions as? ..."
      "procedures with state change should return old versions"
      "of state variables before the state change")
    (%%
      procedure:
     (%% proc)
     "multi argument version of flip, which can be used in pipe")
    (pipe
      macro:
      (pipe combination ...)
      "sequencing curried combinations")
    )))
    (case-lambda
      (()
       (map car als))
      ((sym)
       (let ((pair (assq sym als)))
         (if pair
           (for-each print (cdr pair))
           (error "Not in list"
                  sym
                  (map car als))))))))

) ; module simple-contracts