~nytpu/dbc-scheme

a9e2d7490fa6991da15c2fc34ee8a619c76b1fc5 — nytpu 1 year, 9 months ago 76e749c 
implement function contracts
patch browse .tar.gz 
2 files changed, 182 insertions(+), 3 deletions(-)

M contracts.scm
M contracts.sld

M contracts.scm => contracts.scm +174 -1
@@ 4,4 4,177 @@
;;; SPDX-License-Identifier: MPL-2.0
;;; Home Page: <https://git.sr.ht/~nytpu/dbc-scheme>

;; TODO
;; Given a list \var{l1} of promises and a list \var{l2} of quoted
;; representations of those promises, verify that all of \var{l1}'s
;; expressions are true, otherwise raise an exception with the given
;; \var{msg} and the quoted version of the expression consed with the
;; \var{addl-irritants}.
(define (execute-contracts l1 l2 msg . addl-irritants)
  (every
    (lambda (expr quoted)
      (if (force expr)
          #t
          (error msg
                 (append (if (list? quoted) quoted (list quoted))
                         addl-irritants))))
    l1 l2))

;; Transform a series of expressions into a list of \scheme{quote}d
;; expressions.
(define-syntax quotify
  (syntax-rules ()
    ((_ q ...)
     (list (quote q) ...))))

;; \scheme{verify-contracts} will verify that a series of expressions returns
;; true, otherwise raising an exception with the quoted representation of the
;; expression that failed.
;;
;; It has two variants:
;; \itemlist[
;;   \item{
;;     Given a series of predicates taking a single argument and a "return"
;;     value \var{r}, evaluate each predicate with \var{r} and ensure all of
;;     them return true.
;;   }
;;   \item{
;;     Given a series of thunk expressions, verify that all of them return
;;     true.
;;   }
;; ]
(define-syntax verify-contracts
  (syntax-rules (return)
    ((_) #t)
    ((_ (return r)) r)
    ((_ c1 c2 ... (return r))
     (let ((return r))
       (if (execute-contracts (list (delay (c1 return))
                                    (delay (c2 return)) ...)
                              (quotify c1 c2 ...)
                              "postcondition assertion violation"
                              return)
           return
           #f)))
    ((_ c1 c2 ...)
     (execute-contracts (list (delay c1) (delay c2) ...)
                        (quotify c1 c2 ...)
                        "precondition assertion violation"))))

;;> Define a lambda expression as with \scheme{lambda}, however add
;;> precondition and/or postcondition contracts.
;;>
;;> Given a \scheme{(pre contracts ...)}, where \var{contracts ...} is zero
;;> or more thunk expressions, evaluate each thunk sequentially in the same
;;> scope as the function body.  If a thunk returns \scheme{#f}, then raise
;;> an exception noting a precondition violation with the irritants being the
;;> (\scheme{quote}d) thunk that failed.
;;>
;;> Given a \scheme{(post contracts ...)}, where \var{contracts ...} is zero
;;> or more predicate functions taking a single argument, evaluate each
;;> expression sequentially given the return value of the function; in the
;;> same scope as the function body and after the function has completed
;;> evaluation.  If a predicate returns \scheme{#f}, then raise an exception
;;> noting a postcondition violation with the irritants being the expression
;;> that failed and the original return value.
;;>
;;> The contracts are short-circuit evaluated, i.e. they are evaluated
;;> sequentially from left to right and evaluation terminates if a contract
;;> fails.  As such, it is recommended to have contracts sorted from most
;;> general to most specific.
;;>
;;> \bold{Example:}
;;>
;;> \schemeblock{
;;>   (define add-map
;;>     (lambda-contract (add-map . lists)
;;>       (pre (every list? lists)
;;>            (>= (length lists) 2)
;;>            (apply = (map length lists)))
;;>       (post list?
;;>             (lambda (ret) (= (length ret) (length (car lists)))))
;;>       (apply map + lists)))
;;> }
;;> \scheme{(add-map '(1 2 3) '(4 5 6))} => \scheme{(5 7 9)}.
;;>
;;> \scheme{(add-map '(1 2 3) '(4 5))} => \code{Error: precondition assertion violation: (apply = (map length lists))}.
;;>
;;> \scheme{(add-map '(1 2 3) 1)} => \code{Error: precondition assertion violation: (every list? lists)}
;;>
;;> \scheme{(add-map '(1 2 3))} => \code{Error: precondition assertion violation: (>= (length lists) 2)}
;;>
;;> \bold{Known issues:}
;;>
;;> Postcondition contract checking will not operate on functions returning
;;> multiple values.  If the postcondition is omitted then the multiple
;;> values will be returned as normal.  Precondition contracts are not
;;> affected.
(define-syntax lambda-contract
  (syntax-rules (pre post)
    ((_ formals (pre c1 ...) (post c2 ...) e1 e2 ...)
     (lambda formals
         (verify-contracts
           c2 ...
           (return (begin (verify-contracts c1 ...)
                          e1 e2 ...)))))
    ((_ formals (post c2 ...) (pre c1 ...) e1 e2 ...)
     (lambda-contract formals (pre c1 ...) (post c2 ...) e1 e2 ...))
    ((_ formals (pre c ...) e1 e2 ...)
     (lambda-contract params (pre c ...) (post) e1 e2 ...))
    ((_ formals (post c ...) e1 e2 ...)
     (lambda-contract formals (pre) (post c ...) e1 e2 ...))
    ((_ formals e1 e2 ...)
     (lambda formals e1 e2 ...))))

;;> Define a top-level function binding as with \scheme{define}'s "defun"
;;> syntax, however use \scheme{lambda-contract} instead of a regular lambda.
;;>
;;> The semantics of the pre- and post-conditions is equivalent to
;;> \scheme{define-lambda.}
;;>
;;> \bold{Example:}
;;>
;;> \schemeblock{
;;>   (define-contract (add-map . lists)
;;>     (pre (every list? lists)
;;>          (>= (length lists) 2)
;;>          (apply = (map length lists)))
;;>     (post list?
;;>           (lambda (ret) (= (length ret) (length (car lists)))))
;;>     (apply map + lists))
;;> }
;;> The above is equivalent to:
;;> \schemeblock{
;;>   (define add-map
;;>     (lambda-contract lists
;;>       (pre (every list? lists)
;;>            (>= (length lists) 2)
;;>            (apply = (map length lists)))
;;>       (post list?
;;>             (lambda (ret) (= (length ret) (length (car lists)))))
;;>       (apply map + lists)))
;;? }
;;>
;;> \bold{Known issues:}
;;>
;;> Binding to a \scheme{lambda} expression instead of using the "defun"
;;> syntax breaks contract checking.  Use a plain \scheme{define} with
;;> \scheme{lambda-contract} instead.
;;>
;;> See \scheme{lambda-contract} for issues with the contract system in
;;> general.
(define-syntax define-contract
  (syntax-rules (pre post)
    ((_ formals (pre c1 ...) (post c2 ...) e1 e2 ...)
     (define formals
         (verify-contracts
           c2 ...
           (return (begin (verify-contracts c1 ...)
                          e1 e2 ...)))))
    ((_ formals (post c2 ...) (pre c1 ...) e1 e2 ...)
     (define-contract formals (pre c1 ...) (post c2 ...) e1 e2 ...))
    ((_ formals (pre c ...) e1 e2 ...)
     (define-contract formals (pre c ...) (post) e1 e2 ...))
    ((_ formals (post c ...) e1 e2 ...)
     (define-contract formals (pre) (post c ...) e1 e2 ...))
    ((_ formals e1 e2 ...)
     (define formals e1 e2 ...))))


M contracts.sld => contracts.sld +8 -2
@@ 5,7 5,13 @@
;;; Home Page: <https://git.sr.ht/~nytpu/dbc-scheme>

;;> TODO
;;>
;;> View additional details at the
;;> \hyperlink[https://git.sr.ht/~nytpu/dbc-scheme]{project's repository}.
(define-library (nytpu contracts)
  #;(export)
  #;(import)
  (export lambda-contract
          define-contract)
  (import (scheme base)
          (scheme lazy)
          (srfi 1))
  (include "contracts.scm"))