;;;; File: contracts.scm
;;;; Author: Juergen Lorenz
;;;; ju (at) jugilo (dot) de
;;;; Date: Oct 24, 2010
;;;;       Nov 28, 2010
;;;;       Dec 06, 2010
;;;;       Jan 04, 2011
;;;;       Jan 07, 2011
;;;;       Jan 12, 2011
;;;;       Jan 20, 2011
;;;;       Jan 31, 2011
;;;;       Feb 16, 2011
;;;;       Feb 22, 2011
;;;;       Jun 19, 2011

;Design by Contract
;==================
;
;Design by Contract is a programming paradigm invented by Bertrand Meyer
;for his purely Object Oriented Language Eiffel. The objective is to
;reduce the complexity of software by means of a clear separation of
;concerns between its suppliers and clients. One of the rules is: Never
;do a check an both sides of the abstraction barrier. To achieve this,
;Eiffel fosters a style, in which each routine clearly specifies, what
;are the assumptions (preconditions) of a routine and what are its
;propositions (postconditions). Moreover, the runtime system is able to
;check these conditions. If now a routine call fails because of illegal
;arguments, the client is to blame, but if it fails with violated
;propositions, it is the supplier's fault. The routine's body will not
;even be accessed with wrong arguments, and the routine will not even
;return with wrong propositions.
;
;The metaphor is that of a contract between supplier and client. The
;supplier guarantees correct results, provided the client fulfills his
;duties. If not, the supplier is not obligated to start work at all. As
;in real life, both parties need a copy of the contract, and there must
;be a judge in case of troubles. Translated to programming, this means,
;the contract needs to be documented, and both parties can trust each
;other, so that they need not - and should not - check the other's
;duties, the runtime system will do it. It's a bit like proving a
;mathematical theorem: to prove its proposition, the assumptions can be 
;taken for granted. Without them, the proposition is simply meaningless.
;
;There is still another metaphor of Meyer's, Command-Query-Separation.
;That means, that the programmer should never write routines both for a
;result and for a side-effect (like the ++ operators in C). Instead, two
;routines should be written, one that returns a result, the other that
;changes state. The former are called queries by Meyer, the latter
;commands (because all of Eiffel's routines operate on objects, they
;either query or command its state). In Scheme we have functions without
;side-effect, written for their results only (the recommended style), and
;state-changing procedures, which are normally denoted with a trailing
;bang. But independent of the different terminology, the principle
;applies to Scheme as well, in fact to every language.
;
;Design by Contract is such a powerful paradigm, that anybody, who ever
;has programmed in Eiffel, would like to have it in his favorite
;language. Outside the Lisp family of languages, you where out of luck,
;but Lisps, being programmable programming languages, allow you to add
;to the language what you miss. In Lisp, you are a language designer as
;well as a programmer! In what follows, you'll see, how easy it is to
;implement Design by Contract in Chicken Scheme. 
;
;Let's start with the design. We'll package the needed macros and
;procedures in a Chicken module called contracts. The fundamental macros
;are called define-with-contract and define-syntax-with-contract, which
;replace and wrap define and define-syntax respectively. So
;instead of
;
;  (define name proc)
;
;you will write
;
;  (define-with-contract name 
;    contract-expression
;    proc)
;
;or - for closures with state -
;
;instead of 
;
;  (define name
;    (let (...)
;    proc))
;
;  (define-with-contract name
;    (let (...)
;      contract-expression
;      proc))
;
;where other binding constructs will work as well.
;
;And instead of
;
; (define-syntax name transformer)
;
;you'll write
;
;  (define-syntax-with-contract name
;    contract-expression
;    transformer)
;
;where proc is a lambda expression and transformer a syntax-rules
;expression in most cases. In both cases, there are short forms as well.
;
;But before we go into the details, how such a contract-expression looks
;like, it should be noted, that this macro should automate the
;documentation of the contract to be supplied.  After all, a contract
;without the contract document - the small print - is useless. To do
;this, we export a parameter, doclist, and a procedure,
;doclist->dispatcher, which are used by client code, preferably a
;module, as follows: At the start of the client module, doclist is
;initialized to the empty list, (doclist '()) and at the end it is saved
;to a dispatcher, say client, with
;
;  (define client (doclist->dispatcher (doclist))).
;
;Between these two calls every instance of define-with-contract and
;define-syntax-with-contract will store its textual representation of
;contract-expression under the symbol name, so that a client of the
;client-module, client, say, can either call (client) to get a list of
;available names, or (client 'name) to get documentation of the name
;routine.
;
;Let's start with the contract-expression above, in other words, how
;does a contract look like? The answer differs for procedures and macros
;as well as for queries and commands, or - to express this more
;Lisp-like - for functions (in the strict mathematical sense, i.e.
;without side-effects) and procedures with state, and it is different
;for macros as well.
;
;Let's start with functions.
;---------------------------
;
;Mathematical functions have a domain and a range, Lisp functions have
;arguments (possibly none at all) and results (possibly more than one).
;The former are named in the declaration, not so the latter. So, if we
;want to check results, we must name them in the contract. This is done
;with a (results: ...) clause.  If no (results: ...) clause is supplied,
;then it is assumed, that only one result is produced and named
;"result".  The checks of arguments and results must involve predicates,
;so there are clauses (domain: ...) and (range: ...) which collect
;predicate-expressions on arguments and results. And last, but not
;least, for documentation purposes, there should be a docstring. All
;this should appear after the call structure of the routine to be
;checked, which is the only required argument.
;
;So for Euclid's integer division, to give a typical example, the
;contract should look like this
;
;  (contract (quotient+remainder m n)
;    "integer division"
;    (results: q r)
;    (domain:
;      (integer? m)
;      (not (negative? m))
;      (integer? n)
;      (positive? n)
;      (<= n m))
;    (range:
;      (integer? q)
;      (integer? r)
;      (= (+ (* q n) r) m)))
;
;Put together, the whole checked quotient+remainder routine will look
;like this
;
;  (define-with-contract quotient+remainder
;    (contract (quotient+remainder m n) ...) ; see above
;    (lambda (m n)
;      (let loop ((q 0) (r m))
;        (if (< r n)
;          (values q r)
;          (loop (add1 q) (- r n))))))
;
;You should note, that contract and implementation are strictly
;separated. You as the supplier can write the implementation without
;worrying about the parameters in the implementation, it's checked by
;the contract. In fact, you mustn't, it's the client's duty. On the
;other hand, the client can be sure, that the routine delivers the
;correct results, provided it runs through.
;
;How is this black magic possible? It's simple: In Scheme, procedures are
;first class values. They can be arguments and results of procedures.
;Hence, we only need to implement the contract-expression as a macro,
;which returns a procedure, accepting the implementation as argument and
;returning the contract-checked implementation. 
;
;Isn't that a lot of checking, you might ask. Yes, it is. But you
;needn't include all of this checking into the ultimate compiled code.
;Remember, that development in Scheme is different than development in a
;language without an interpreter: Only after you have tested your
;routine interactively you'll compile it. So you'll arrange matters in
;such a way, that only interpreted code will check both the domain and
;the range, while compiled code will only test the former. Chicken
;allows to include interpreted-only code into an (eval-when (eval) ...)
;expression - a feature borrowed from Common Lisp -  which provides this
;distinction. Moreover, if you are really concerned about speed, you can
;avoid domain checking as well, compiling your code with the unsafe
;switch, because the actual checks will be done in assert epressions,
;which are ignored in unsave code. But that's like driving without a
;security belt ....
;
;If you look at the above code, you'll note still some redundancy. So,
;like the short form of procedure definitions
;
;  (define (name . args) xpr . xprs)
;
;we'll supply a short form of define-with-contract as well, omitting
;the contract-line and the lambda-line:

;  (define-with-contract (quotient+remainder m n)
;    "integer division"
;    (results: q r)
;    (domain:
;     (integer? m)
;     (not (negative? m))
;     (integer? n)
;     (positive? n)
;     (<= n m))
;    (range:
;     (integer? q)
;     (integer? r)
;     (= (+ (* q n) r) m))
;    (let loop ((q 0) (r m))
;      (if (< r n)
;        (values q r)
;        (loop (add1 q) (- r n)))))
;
;State changing procedures
;-------------------------
;
;Now to the commands, procedures which change state. The state may be
;internal, e.g. a let before the defining lambda, or external, i.e. a
;hidden variable in the defining module. Or it might be encapsulated in
;required arguments of the routine.
;
;Now remember command-query-separation. To change the state of a routine
;and to return this state should be separate operations. In other words,
;usually a command is accompanied by a query. Hence a typical
;effect-checking clause would look like (state query change), where
;state is a variable to be bound by the query expression before the
;command call, and change is an expression describing how state is
;changed by the command. The actual check is done by the call
;(equal? change query), where now query is evaluated again after the
;command call. Note, that this clause is similar to a binding clause in
;do.
;
;But there are two problems with it. First, equal? is slow, and more
;specialized equality predicates seem preferable. This issue is not such
;important, since effects aren't checked in compiled code anyway.  But
;the other problem is important: What if command changes some state with
;some inexact computations? Than you can control the result only
;approximately. In other words, in some rare cases we need a fourth item
;in the effect clause above, an equality predicate.

;The whole effect check now consists of a list of such clauses, prefixed
;by the effect: keyword (effect: (state query change [equ?]) ...), where
;equ? is optional and set to equal?, if not given.

;Here is a trivial example:
;
;(define-with-contract adder!
;  (let ((state 0))
;    (contract (adder! arg)
;      "adds its argument to its state"
;      (domain: (number? arg))
;      (effect: (old state (+ old arg))))
;    (lambda (arg)
;      (set! state (+ state arg)))))

;Note that command-query-separation demands that there is either a range
;or an effect check, whence either a (range: ...) or an (effect: ...)
;expression.

;Example: An implementation of the single datatype 
;-------------------------------------------------
;Here is a simple, but realistic example, in which commands and queries
;are involved, the single datatype, an alternative to boxes.

;;;; 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))
;  ((sg (lambda (a b c) c)) arg))

;What to do with macros?
;-----------------------
;
;As for procedures
;
;  (define-syntax-with-contract name
;    contract-expression
;    transformer)
;
;should result in a checked syntax-definition including its automatic
;documentation.
;
;But macros are different from procedures in many aspects. First, they
;operate an forms only, i.e. they accept literal lists and return lists.
;Second, the transformer is evaluated at preprocessing time, that is,
;before runtime. So it has no access to runtime values. 
;
;What are transformers? In R5RS-Scheme, they are syntax-rules
;expressions. Well, syntax-rules matches a series of patterns against a
;series of templates and returns the template of the first matching
;pattern. On the other hand, a domain check for a macro could only test,
;if the macro code, which is a list, matches some patterns. In other
;words, the pattern-matching of syntax-rules could be considered as a
;domain-check, provided we are able to expose the admissible patterns
;for the documentation. Exposing those patterns would considerably
;improve the error message in case of failure as well.  After all, the
;standard error message
;
;  during expansion of (name ...) - no rule matches form (name ...)
;
;is not of much help, unless we check the documentation, which, of
;course, must exist and be actual. The result of this considerations is,
;that the contract-expression doesn't need a domain clause, but the
;admissible patterns have to be exposed.

;But what about a range clause?  Does it make sense, to check the range
;of a macro-transformer?  Well, one could match the macro-expansion
;against some patterns as well. But I don't think that this is worth
;one's efforts, since one can always check that range with a simple call
;of the Chicken extension expand. To sum up this discussion, the
;contract-expression of macros will simply be a documentation string.
;
;All this applies to high-level syntax-rules macros only, not to raw
;low-level explicit renaming ones. The defining lambda expression
;can't export any patterns, because there are none. The solution of this
;problem is, that we'll have to supply them. Or, alternatively, to
;package the definition of low-level macros into exactly the same syntax
;as high-level macros. In other words, we need to supply a macro,
;er-macro-rules, with exactly the same call syntax as syntax-rules
;
;  (er-macro-rules (%sym ...) (pat0 xpr0) (pat1 xpr1) ...)
;
;where each sym is a symbol to be renamed and %sym represents its
;renamed version (any other one-character prefix will work as well).
;Each xpr, xpr1, ... on the other hand, is a procedure of one argument,
;compare?. Like syntax-rules, this macro should expand into a
;lambda-expression with the standard three arguments form, rename,
;compare?.
;
;To give a nontrivial example, the ordinary definition of a do-for macro
;with explicit renaming could look like this
;  
;  (define-syntax do-for
;    (er-macro-rules (%let %loop %unless %+ %>= %stop)
;      ((_ var (start stop . steps) . body)
;       (lambda (compare?)
;         (let ((step (if (null? steps) 1 (car steps))))
;           `(,%let ((,%stop ,stop))
;               (,%let ,%loop ((,var ,start))
;                  (,%unless (,%>= ,var ,%stop)
;                     ,@body
;                     (,%loop (,%+ ,step ,var))))))))))
;  
;and a hygienic low-level or macro like this
;
;  (define-syntax our-or
;    (er-macro-rules (%if %my-or)
;      ((_)
;       (lambda (compare?) #f))
;      ((_ arg . args)
;       (lambda (compare?)
;         `(,%if ,arg ,arg (,%my-or ,@args))))))
;  
;By the way, using this macro, er-macro-rules, we'll avoid the tedious
;work of destructuring the macro-code by hand and facilitate the
;renaming as well. 
;
;The implementation of er-macro-rules is not hard, provided there is
;some help with pattern matching. The Chicken egg matchable exports a
;macro, match, which might do that job, as well as the macro bind-case
;from my bindings module.
;
;Since the advent of Chicken-4.7 there is even a cleaner and easier way:
;Use implicit renaming instead of explicit renaming macros. Whereas the
;latter has to rename every free symbol in the macro expansion, which
;must not be captured - resulting in a rather long list (%sym ...) -
;the former needs only inject explicitly those symbols, which should be
;captured by design, resulting in an empty list for all hygienic macros.
;
;So we define another macro, ir-macro-rules, with the call syntax of
;syntax-rules

;  (ir-macro-rules (sym ...) (pat0 xpr0) (pat1 xpr1) ...)
;
;and an empty symbol list most of the times which expands into a
;(lambda (form inject compare?) ...) expression and does all the
;renaming in the background like syntax-rules. With this macro, our two
;examples above look like this:
;
;  (define-syntax do-for
;    (ir-macro-rules ()
;      ((_ var (start stop . steps) . body)
;       (lambda (compare?)
;         (let ((step (if (null? steps) 1 (car steps))))
;           `(let ((stop ,stop))
;               (let loop ((,var ,start))
;                  (unless (>= ,var stop)
;                     ,@body
;                     (loop (+ ,step ,var))))))))))
;  
;  (define-syntax our-or
;    (ir-macro-rules ()
;      ((_)
;       (lambda (compare?) #f))
;      ((_ arg . args)
;       (lambda (compare?)
;         `(if ,arg ,arg (my-or ,@args))))))
;  
;With implicit renaming macros at your disposal you'll hardly ever use
;explicit renaming ones.
;
;Now, we have unified the definition of high- and low-level macros and
;can process them in the same way. 

;The short form of define-syntax-with-contract is easy insofar, as the
;contract-expression is simply a docstring. But this short form is
;possible only for transformers with one pattern only.  There still
;remains the problem, what to do with the identifier arguments.  Well,
;in syntax-rules, most of the time there are none, so we consider only
;this case for syntax-rules (like in Chicken's define-syntax-rule). In
;sum, the syntax is one of
;
;  (define-syntax-with-contract (name . rest) xpr)
;  (define-syntax-with-contract (name . rest) docstring xpr)
;  (define-syntax-with-contract name transformer)
;  (define-syntax-with-contract name docstring transformer)
;
;where transformer is either a syntax-rules, an er-macro-rules or an
;ir-macro-rules expression.

;Here is the implementation of the contracts module.

(module contracts
        (contract define-with-contract define-syntax-with-contract
         doclist->dispatcher doclist print-doclist contracts)

(import scheme
        (only chicken use print make-parameter void error
              eval-when assert case-lambda))

(use (only data-structures sort)
     (only extras pp)
     (only srfi-13 string<))

(import-for-syntax (only data-structures ->string))

;Before we give the definition of the contract macro, we need two helper
;macros, the second of which does the actual checking with a meaningful
;error message in case of failure.  The first, collect, causes a lambda
;list of parameters to be transformed into the list of arguments when
;called. For example,
;
;  ((lambda (a b . c) (list a b c)) 1 2 3)
;
;will produce (1 2 (3)), while
;
;  ((lambda (a b . c) (collect (a b . c))) 1 2 3)
;
;results in (1 2 3).  It's needed, because all our checking macros will
;transform a procedure with arbitrary parameter lambda-list into a
;checked one with the same parameter lambda-list. In that latter
;procedure we can call (apply proc (collect args)) instead of (proc .
;args), which would only work for lists, not lambda-lists.

;;; (collect lambda-list)
;;; ---------------------
;;; helper macro returning the list of actual arguments
(define-syntax collect
  (syntax-rules ()
    ((_ ()) '())
    ((_ (a . b)) (cons a (collect b)))
    ((_ a)  (apply list a))))

;The second helper macro, check-em, uses a helper-procedure, pzip, which
;zips a flat pseudo-list of arguments, as, with a list of values, vs. It
;is implemented as a letrec in check-em so that it is available while
;preprocessing. The macro check-em returns a procedure, which checks
;each of its xpr ... expressions with assert and prints the offending
;xpr with a list of variable-value pairs in case of failure. This way
;you can trace what went wrong.

;;; (check-em name args msg xpr ...)
;;; --------------------------------
;;; helper macro returning a procedure which when called checks a number
;;; of assertions and prints a meaningful error message in case of
;;; failure
(define-syntax check-em
  (syntax-rules ()
    ((_ name args msg xpr ...)
     (letrec (
       (pzip (lambda (as vs)
               (cond
                 ((null? as) '())
                 ((pair? as)
                  (cons (list (car as) (car vs))
                        (pzip (cdr as) (cdr vs))))
                 (else (list (list as vs))))))
       )
       (lambda args
         (if (null? 'args)
           (begin
             (assert xpr name msg 'xpr)
             ...)
           (begin
             (assert xpr name msg 'xpr `(where ,@(pzip 'args (collect args)))) 
             ...)))))))

;The following three helper macros, domain, range and effect do the real work.
;They all accept a procedure argument and return that procedure argument
;checked, the same as the eventually exported contract macro will do.

;The first macro, domain, will simply use check-em on the arguments
;before calling the procedure proper.

;;; (domain name args . xprs)
;;; -------------------------
;;; helper macro checking the domain of its procedure argument
;;; and returning a checked version.
(define-syntax domain
  (syntax-rules ()
    ((_ name args . xprs)
     (lambda (proc)
       (lambda args
         (apply (check-em 'name args "domain violation ..." . xprs)
                (collect args))
         (apply proc (collect args)))))))

;The second, range, should do the domain and range check for queries on
;the one hand and the invariant check for commands on the other. To do
;the first, it must have a list of assumptions and to do the second it
;should contain a list of result names, as well as message argument
;(since invariant checks are simply range checks with different error
;message). As you might expect, the domain check is done by the domain
;macro just defined.
;Remember, that in Scheme multiple results are produced by a values
;expression and referenced by call-with-values.

;;; (range name args (result0 result1 ...) (assumption ...) . xprs)
;;; ---------------------------------------------------------------
;;; helper macro checking range and domain of its procedure argument
(define-syntax range
  (syntax-rules ()
    ;; range check: empty argument list, no assumptions, multiple results
    ((_ name () (result0 result1 ...) () . xprs)
     (lambda (proc)
       (lambda ()
         (call-with-values
           (lambda () (proc))
           (lambda (result0 result1 ...)
             (eval-when (eval)
               ((check-em 'name (result0 result1 ...)
                          "range violation ..." . xprs)
                result0 result1 ...))
             (values result0 result1 ...))))))
    ;; range and domain check: possibly non-empty argument pseudolist, multiple results
    ((_ name args (result0 result1 ...) (assumption ...) . xprs)
     (lambda (proc)
       (lambda args
         (call-with-values
           (lambda ()
             ;; check domain
             (apply ((domain name args assumption ...) proc)
                    (collect args)))
           (lambda (result0 result1 ...)
             ;; check range
             (eval-when (eval)
               (apply (check-em 'name (result0 result1 ... . args)
                                "range violation ..."
                                . xprs)
                      (collect (result0 result1 ... . args))))
             (values result0 result1 ...))))))))

;Note, that in the replacement text of this macro, you find the dotted
;list (result0 result1 ... . args) twice. This works in the
;macro-transformer. It would not work in the macro code, at least not in
;R5RS-Scheme.
;Note also, that the range check is wrapped into a call of eval-when, so
;that it will only be included in interpreted code.

;Now to the third essential helper macro, effect. It controls the
;effect of a command call.

;;; (effect name args (assumption ...) (state query change equ?) ...)
;;; -----------------------------------------------------------------
;;; helper macro checking domain and side-effects of its command
;;; argument returning it checked.
;;; Binds state to the value of the query expression before the command
;;; call and checks if the change expression is equ? to the value of a
;;; second evaluation of query after the command call.
(define-syntax effect
  (syntax-rules ()
    ((_ name args (assumption ...) (state query change equ?) ...)
     (lambda (command)
       (lambda args
         ;; check domain
         (apply (check-em 'name args "domain violation ..." assumption ...)
                (collect args))
         ;; check state change
         (let ((state query) ...) ; query value before command call
           (command . args)
           (eval-when (eval)
             ;; evaluate query again and compare to change
             (apply (check-em 'name
                              (state ... . args)
                              (string-append 
                                "side-effect violation with "
                                (string-append (->string `(query ,query)) " ")
                                ...
                                "...")
                              (equ? change query)
                              ...)
                    (collect (state ... . args))))))))))

;Note, that query ... can't be appended to the args pseudolist like
;state ..., because the latter are variables, but the former
;expressions. So we must add them to the message argument with ->string.
;Note also, that the effect check is wrapped into an eval-when, so that
;it is not executed in compiled code. The same happened with the range
;check above.

;Now, these three internal macros are used in the exported contract
;macro. This is implemented as an explicit renaming low-level macro for
;a simple reason: A high-level macro would need literally dozens of
;cases to cope with all possible calls. The procedural low-level macro
;could simply implement a loop to populate the variables results,
;assumptions, propositions and effects, which can be handed over to the
;three macros above. With the exceptions of the results variable, they
;are all initialized with the empty list. results, on the other hand, is
;initialized with (results: result), so that, if no results clause is
;given, it is assumed that there is only one return value named result.

;;; (contract (name . args) . xprs)
;;; -------------------------------
;;; where args is a lambda-list and xprs can contain any of the following
;;; expressions
;;; - a docstring
;;; - a list of domain checks (domain: assumption ...)
;;; - a list of result names (results: result0 result1 ...)
;;;   if not supplied (results: result) is assumed
;;; - a list of range checks (range: proposition ...)
;;; - a list of effect checks (effect: (state query change [equ?]) ...)
(define-syntax contract
  (er-macro-transformer
    (lambda (form rename compare?)
      (let (
        (name (caadr form))
        (args (cdadr form))
        (xprs (cddr form))
        (gproc (gensym 'proc))
        (%range (rename 'range))
        (%effect (rename 'effect))
        (%domain (rename 'domain))
        (%lambda (rename 'lambda))
        ) 
        (let loop (
          (xprs xprs)
          (results '(result))
          (assumptions '())
          (propositions '())
          (effects '())
          )
          (if (null? xprs)
            ;; apply the collected results
            (cond
              ;; nothing to check
              ((and (null? effects) (null? propositions) (null?  assumptions))
               `(,%lambda (,gproc) ,gproc))
              ;; check assumptions only
              ((and (null? effects) (null? propositions))
               `(,%lambda (,gproc)
                  ((,%domain ,name ,args ,@assumptions) ,gproc)))
              ;; check propositions and assumptions
              ((null? effects)
               `(,%lambda (,gproc)
                  ((,%range ,name ,args ,results
                            ,assumptions ,@propositions) ,gproc)))
              ;; check side effects and assumptions
              ((null? propositions)
                `(,%lambda (,gproc)
                   ((,%effect ,name ,args ,assumptions ,@effects) ,gproc)))
              (else
                (error 'contract "Either propositions or effects can be checked")))
            ;; collect the variables
            (let ((xpr (car xprs)))
              ;; xpr is either a string or a list starting with a keyword
              (cond
                ;; docstring: skip
                ((string? xpr)
                 (loop (cdr xprs)
                       results assumptions propositions effects))
                ;; result names
                ((compare? (car xpr) results:)
                 (loop (cdr xprs)
                       (cdr xpr) assumptions propositions effects))
                ;; domain expressions
                ((compare? (car xpr) domain:)
                 (loop (cdr xprs)
                       results (cdr xpr) propositions effects))
                ;; range expressions
                ((compare? (car xpr) range:)
                 (loop (cdr xprs)
                       results assumptions (cdr xpr) effects))
                ;; side effect expressions
                ((compare? (car xpr) effect:)
                 (loop (cdr xprs)
                       results  assumptions propositions
                       ;; append equal? if no comparison is given
                       (map (lambda (x)
                              (if (= (length x) 3)
                                `(,@x equal?) ; ok
                                ;(append x '(equal?))  ; ok
                                x))
                            (cdr xpr))))))))))))


;The define-with-contract macro should reflect the two forms, either
;couple a name to a contract and a lambda-expression, or couple the form
;of a procedure-call with contract clauses followed by the expressions
;of the body of a lambda-expression. It's simple to dissect the latter
;two, because a contract clause is either a string or a list starting
;with one of the keywords results:, state:, domain:, range:,
;invariant: and effect:. This is tested by the internal predicate
;clause?

;;; (define-with-contract name contract proc)
;;; (define-with-contract (name . args) contract-clause ... . body)
;;; ---------------------------------------------------------------
;;; checks the procedure proc with contract, appends contract to the
;;; documentation (via doclist), and defines name as the checked
;;; procedure.
(define-syntax define-with-contract
  (er-macro-transformer
    (lambda (form rename compare?)
      (let ((rest (cdr form)))
        (if (symbol? (car rest)) ; name
          ;; long form:
          ;; we have to consider the case, that the contract and proc
          ;; are wrapped within a binding construct, as well
          (let (
            (body (cdr rest))
            (list-head 
              (lambda (lst upto)
                (let loop ((lst lst) (n upto) (head '()))
                  (if (zero? n)
                    (reverse head)
                    (loop (cdr lst)
                          (- n 1)
                          (cons (car lst) head))))))
            )
            (let (
              (head&tail
                (if (null? (cdr body))
                  ;; one element list containing a binding expression like
                  ;; (let decls contr proc) or (bind vars vals contr proc)
                  (let* ((binds (car body)) (split (- (length binds) 2)))
                    `(,(list-head binds split) ,(list-tail binds split)))
                  ;; two element list (contr proc)
                  `(() ,body)))
              )
              (let ((head (car head&tail)) (tail (cadr head&tail)))
                (let (
                  (contract-xpr (car tail))
                  (proc (cadr tail))
                  )
                  (let (
                    (name (caadr contract-xpr))
                    (args (cdadr contract-xpr))
                    (%begin (rename 'begin))
                    (%cdr (rename 'cdr))
                    (%cons (rename 'cons))
                    (%if (rename 'if))
                    (%define (rename 'define))
                    (%doclist (rename 'doclist))
                    )
                    `(,%begin
                       (,%doclist
                         (,%cons (,%cons ',name (,%cdr ',contract-xpr))
                                 (,%doclist)))
                       (,%if ,(null? head) ;(,%null? ,head)
                         (,%define ,name (,contract-xpr ,proc))
                         (,%define ,name (,@head (,contract-xpr ,proc))))))))))
          ;; short form: (_ (name . args) contract-clause ... . body)
          (let (
            (code (car rest))
            (xprs (cdr rest))
            (clause? (lambda (xpr)
                       (or (string? xpr)
                           (and (list? xpr)
                                (not (null? xpr))
                                (memq (car xpr)
                                      '(results: domain: range: effect:))))))
                                      ;;;'(results: state: domain: range:
                                      ;;;  invariant: effect:))))))
            )
            (let (
              (name (car code))
              (args (cdr code))
              (split (lambda (lst)
                       (let loop ((clauses '()) (body lst))
                         (if (not (clause? (car body)))
                           (list (reverse clauses) body)
                           (loop (cons (car body) clauses) (cdr body))))))
              )
              (let (
                (pair (split xprs))
                (%define-with-contract (rename 'define-with-contract))
                (%contract (rename 'contract))
                (%lambda (rename 'lambda))
                )
                `(,%define-with-contract ,name
                   (,%contract ,code ,@(car pair))
                   (,%lambda ,args ,@(cadr pair)))))))))))
          
;Now we start with the contracts for macros.

;;; (define-syntax-with-contract name docstring transformer)
;;; (define-syntax-with-contract (name . rest) docstring xpr)
;;; --------------------------------------------------------
;;; where transformer is one of syntax-rules, er-macro-rules,
;;; ir-macro-rules espression.
;;; Registers transformer as a syntax-transformer under name, after
;;; having collected docstring and the transformer's pattern forms in
;;; (doclist).
;;; The second case evaluates to syntax-rules.
(define-syntax define-syntax-with-contract
  (syntax-rules (forms:)
    ;; short form (syntax-rules only)
    ((_ (name . args) xpr)
     (define-syntax-with-contract (name . args) "" xpr))
    ((_ (name . args) docstring xpr)
     (define-syntax-with-contract name
       docstring
       (syntax-rules ()
         ((_ . args) xpr))))
    ;; long form
    ((_ name transformer)
     (define-syntax-with-contract name "" transformer))
    ((_ name docstring transformer)
     (if (memq (car 'transformer)
               '(syntax-rules macro-rules ir-macro-rules er-macro-rules))
       (begin
         (doclist
           (cons
             (append (list 'name
                           (cons forms:
                                 (map (lambda (pat) (cons 'name (cdr pat)))
                                      (map car (cddr 'transformer))))
                           docstring))
             (doclist)))
         (define-syntax name
           (er-macro-transformer
             (lambda (form rename compare?)
               (letrec (
                 (in?
                   (lambda (x lst)
                     (let loop ((lst lst))
                       (cond
                         ((null? lst) #f)
                         ((matches? x (car lst)) #t)
                         (else
                           (loop (cdr lst)))))))
                 (matches? (lambda (xpr1 xpr2)
                             (cond
                               ((null? xpr1)
                                (null? xpr2))
                               ((pair? xpr1)
                                (and (pair? xpr2)
                                     (matches? (car xpr1) (car xpr2))
                                     (matches? (cdr xpr1) (cdr xpr2))))
                               (else #t))))
                 )
                 (if (in? 'form (map car (cddr 'transformer)))
                   (transformer form rename compare?)
                   (error 'define-syntax-with-contract
                                 "no rule matches"
                                 (cadr (assq 'name (doclist))))))))))
       (error 'define-syntax-with-contract
              "neither syntax-rules nor (er- | ir- ) macro-rules"
              'transformer)))))

;Now here is the parameter doclist mentioned in the introduction

;;; (doclist [alist])
;;; --------------------
;;; parameter, which produces an empty list to be populated by
;;; define-with-contract with the '(name [docstring] [contract]) 
;;; lists.
(define doclist
  (make-parameter '() (lambda (x)
                        (if (list? x)
                          x
                          '()))))

;Now the routine, which transforms the association list (doclist) into a
;dispatcher, i.e. function, which accepts a symbol and returns the
;corresponding association, saving the alist by the way.  Called with no
;arguments it returns the available symbols.
;In contrast to dispatcher, doclist->dispatecher can be implemented as a
;function.

;;; (doclist->dispatcher alist)
;;; ---------------------------
;;; transforms an association list, e.g. constructed by (doclist),
;;; into a dispatcher routine, which prints the association's values.
(define doclist->dispatcher
  (lambda (alist)
    (let (
      (syms (sort (map car alist)
                  (lambda (x y)
                    (string< (symbol->string x) (symbol->string y)))))
      )
      (case-lambda 
        (()
         ;(begin
         ;  (newline)
         ;  (print "Choose one of:")
         ;  (print "--------------")
         ;  (for-each print syms)))
         syms)
        ((sym)
         (let ((found (assq sym alist)))
           (if found
             (if (and (null? (cddr found)) (procedure? (cadr found)))
               (cadr found)
               (for-each print (cdr found)))
             (begin
               (newline)
               (print "Not found: " sym)
               (print "Choose one of:")
               (print "--------------")
               (for-each print syms)))))))))


;;; (print-chars char n)
;;; --------------------
;;; print char n times
(define (print-chars char n)
  (if (= n 1)
    (display char)
    (begin
      (display char)
      (print-chars char (- n 1)))))

;;; (print-doclist)
;;; ---------------
;;; prints actual parameter (doclist) in readable form
(define print-doclist
  (lambda ()
    (let loop (
      (syms (sort (map car (doclist))
                  (lambda (x y)
                    (string< (symbol->string x) (symbol->string y)))))
      )
      (if (null? syms)
        (void)
        (let ((found (assq (car syms) (doclist))))
          (print (car syms))
          (print-chars #\- (string-length (symbol->string (car syms))))
          (newline)
          (for-each pp (cdr found))
          (newline)
          (loop (cdr syms)))))))

;Last but not least here is the documentation which does by hand for
;the exported symbols in this module what define-with-contract and
;define-syntax-with-contract will do automatically in other modules.

;;; (contracts [sym])
;;; -----------------
;;; documentation procedure. Returns the list of available symbols if
;;; called with no arguments and i.a. the call structure of a macro, if
;;; called with the macro's name
(define contracts
  (doclist->dispatcher
    '((contract
        "checks the domain of its procedure argument proc"
        "and returns a checked version of proc"
        (contract (name . args))
        (contract (name . args) (results: result0 result1 ...))
        (contract (name . args) (domain: xpr ...))
        (contract (name) (results: result0 result1 ...)
          (range: xpr ...))
        (contract (name . args) (results: result0 result1 ...)
          (domain: pre ...) (range: xpr ...))
        (contract (name . args) 
          (effect: (state query change [equ?]) ...))
        (contract (name . args) 
          (domain: pre ...) (effect: (state query change [equ?]) ...)))
      (define-with-contract
        "wraps (define name proc) and saves contract in (doclist)"
        (define-with-contract name docstring contract proc)
        "where docstring and contract are mandatory")
      (define-syntax-with-contract
        "wraps (define-syntax name transformer) and saves docstring"
        "and the transformer's rules in (doclist)"
        (define-syntax-with-contract name docstring transformer)
        "transformer must be of the same syntax as syntax-rules"
        (define-syntax-with-contract (name . args) docstring xpr)
        "wraps (syntax-rules () ((_ . args) xpr))")
      (doclist
        "parameter collecting documentation as a association list."
        "default is the empty list"
        (doclist)
        (doclist (cons (list 'name doc contract) (doclist))))
      (print-doclist
        "print actual parameter (doclist) in readable form"
        (print-doclist))
      (doclist->dispatcher
        "transforms an association list into a dispatcher"
        "i.e. a procedure returning the association of a symbol"
        "or all available symbols when called with no arguments."
        (doclist->dispatcher lst)))))

) ; module contracts