; Author: Juergen Lorenz ; ju (at) jugilo (dot) de
;
; Copyright (c) 2016-2017, 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 result-exception is raised, then the
supplier is to blame. On the other hand, if a argument-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 them
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? ...) ...) xpr ....)
or -- with variable arguments --
(xdefine ((r r? ...) .. name (a a? ...) ... as as? ...) xpr ....)

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

If you want to export the documentation of pre- and postcoditions, you
can use (here without varible arguments)

(xdefine ((r r? ...) .. #(name-post name name-pre) (a a? ...) ...) xpr ....)

Note, that post- and precondition documentation is placed next to
the corresponding conditions.

xdefine is implemented with xlambda, whose syntax --for variable
argument lists -- is

(xlambda ((r r? ...) .. <- (a a? ...) ... as as? ...) xpr ....)

where <- separates the return values from the arguments. These
expressions can be bound via define or define-values to export the
documentation as well. But note that in the latter case the routine must
be named first, of course, so that we have

(define-values (proc proc-pre proc-post) (xlambda ...))

For state-changing routines, so called commands, xlambda can be defined
on top of a let, thus supplying state.

To make postcondition-checking easy and command-chaining possible,
commands should return values as well, namely the changed state
variables after and before the change, for example

(let ((state ...))
  (xlambda ((new new? ...) (old old? ...)
            <-
            (a a? ...) ...) | (a a? ...) ... as as? ...)
            xpr ....)

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 argument-exception
              result-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 proc 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
;;; ==================
;;; old version, used in new version below
;;; (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?)
;(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)))
                (loc (inject 'xlambda%)))
                ;(loc (inject 'xlambda)))
            (let* (
              ;; no checks
              (proc `(lambda (,@fargs ,@vargs)
                       ,xpr ,@xprs))
              ;; check preconditions
              (xproc 
                (if (null? xrest)
                  ;; no dotted argument
                  `(lambda (,@fargs)
                     (apply ,proc
                            (map (lambda (p a) (p a))
                                 (list ,@(map (lambda (x)
                                                `(pipe ((<<< ',loc) ;,@(cdr x))))
                                                        ,@(cons `',(car x)
                                                                (cdr x)))))
                                              xhead))
                                 (list ,@fargs))))
                  ;; with dotted argument
                  `(lambda (,@fargs ,@vargs)
                     (apply ,proc
                            (append
                              (map (lambda (p a) (p a))
                                   (list ,@(map (lambda (x)
                                                  `(pipe ((<<< ',loc) ;,@(cdr x))))
                                                          ,@(cons `',(car x)
                                                                  (cdr x)))))
                                                xhead))
                                   (list ,@fargs))
                              (map (lambda (as)
                                     ((<<< ',loc) as ,@(cons `',(car xrest)
                                                             (cdr xrest))))
                                     ;((<<< ',loc) as ,@(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))
                    ;; only one returned value
                    `(lambda (,@fargs ,@vargs)
                       ((>>> ',loc) (apply ,xproc
                                            ,(args->vals fargs vargs))
                                     ,@(cons `',(caar returns)
                                             (cdar returns))))
                                     ;,@(cdar 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)
                                            `((>>> ',loc) ;,@r))
                                              ,@(cons (car r)
                                                      (cons `',(car r)
                                                            (cdr 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))
                 ))))))))

;;; new version:
;;; (xlambda ((r r? ...) .. <- (x x? ...) ...) xpr ....)
;;; or
;;; (xlambda ((r r? ...) .. <- (x x? ...) ... xs xs? ...) xpr ....)
;;; or old versions (deprecated):
;;; (xlambda k ((r1 r1? ...) ...(rk rk? ...)
;;;             (x x? ...) ... ) xpr ....)
;;; (xlambda k ((r1 r1? ...) ... (rk rk? ...)
;;;             (x x? ...) ... xs xs? ...) xpr ....)
;;; (xlambda ((r r? ...) (x x? ...) ... ) xpr ....)
;;; (xlambda ((r r? ...) (x x? ...) ... xs xs? ...) xpr ....)
;;; --------------------------------------------------------
(define-er-macro (xlambda form rename compare?)
  (let* ((k (cadr form)) (iform (if (integer? k)
                                  (cddr form)
                                  (cdr form))))
    (let ((header (car iform)) (body (cdr iform))
          (%xlambda% (rename 'xlambda%)) (%<- (rename '<-)))
      (if (integer? k)
        `(,%xlambda% ,k ,header ,@body)
        (receive (results args)
          (let loop ((header header) (results '()))
            (cond
              ((null? header) ; no <- symbol
               (let ((header (reverse results)))
                 (values (list (car header)) (cdr header))))
              ((compare? (car header) %<-)
               (values (reverse results) (cdr header)))
              (else
                (loop (cdr header) (cons (car header) results)))))
          `(,%xlambda% ,(length results) (,@results ,@args) ,@body))))))

;;; (xdefine ((r r? ...) .. name (x x? ...) ...) xpr ....)
;;; or
;;; (xdefine ((r r? ...) .. #(post name pre) (x x? ...) ...) xpr ....)
;;; or
;;; (xdefine ((r r? ...) .. name (x x? ...) ... xs xs? ...) xpr ....)
;;; or
;;; (xdefine ((r r? ...) .. #(post name pre) (x x? ...) ... xs xs? ...) xpr ....)
;;; -----------------------------------------------------------------------------
;;; defines name -- and possibly post- and precondition documentation -- as a
;;; contract-checked procedure with postconditions named r checked by
;;; predicates r? ... and preconditions x ... xs .. checked by x? ...
;;; and xs? ...
(define-er-macro (xdefine form rename compare?)
  (let ((header (cadr form))
        (xpr (caddr form))
        (xprs (cdddr form))
        (%<- (rename '<-))
        (%define (rename 'define))
        (%xlambda (rename 'xlambda))
        (%define-values (rename 'define-values)))
    (receive (posts names pres)
      (let loop ((tail header) (head '()))
        (if (or (symbol? (car tail)) (vector? (car tail)))
          (values (reverse head) (car tail) (cdr tail))
          (loop (cdr tail) (cons (car tail) head))))
      (if (symbol? names)
        `(,%define ,names
                   (,%xlambda (,@posts ,%<- ,@pres) ,xpr ,@xprs))
        `(,%define-values ,(list (vector-ref names 1) ; name
                                 (vector-ref names 2) ; pres
                                 (vector-ref names 0)); posts
                   (,%xlambda (,@posts ,%<- ,@pres) ,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? ...) ...) xpr ....)
      (xdefine ((r r? ...) .. #(post name pre) (a a? ...) ...) xpr ....)
      (xdefine ((r r? ...) .. name (a a? ...) ... as as? ...) xpr ....)
      (xdefine ((r r? ...) .. #(post name pre) (a a? ...) ... as as? ...) xpr ....)
      "contract guarded version of define for procedures, where"
      "name is the name of the procedure, post and pre"
      "the documentations of the pre- and postconditions respectively"
      "r ... are return values with corresponding postcondition r?"
      "a ... are fixed arguments with preconditions a? ..."
      "as is an optional variable argument with preconditions as? ..."
      "xpr starts the body")
    (xlambda
      macro:
      (xlambda ((r r? ...) .. <- (a a? ...) ...) xpr ...)
      (xlambda ((r r? ...) .. <- (a a? ...) ... as as? ...) xpr ...)
      "contract guarded version of lambda, where"
      "<- separates returned values r .. from arguments"
      "r? ... are their corresponding postconditions"
      "a ... are fixed arguments with preconditions a? ..."
      "as is an optional variable argument with preconditions as? ..."
      "xpr starts the body"
      "procedures with state change should return new and 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 from left to right")
    )))
    (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