~nytpu/dbc-scheme

dbc-scheme/contracts.scm -rw-r--r-- 6.8 KiB
c2dccf9anytpu add license file 7 months ago
                                                                                
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
;;; contracts.scm --- R7RS Design by Contracts
;;;
;;; Copyright (c) 2022 nytpu <alex [at] nytpu.com>
;;; SPDX-License-Identifier: MPL-2.0
;;; Home Page: <https://git.sr.ht/~nytpu/dbc-scheme>

;; 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))

;; \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 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)) ...)
                              (list (quote c1) (quote c2) ...)
                              "postcondition assertion violation"
                              return)
           return
           #f)))
    ((_ c1 c2 ...)
     (execute-contracts (list (delay c1) (delay c2) ...)
                        (list (quote c1) (quote 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 expressions, evaluate each thunk sequentially in the same scope
;;> as the function body.  If an expression returns \scheme{#f}, then raise
;;> an exception noting a precondition violation with the irritants being the
;;> (\scheme{quote}d) expression that failed.
;;>
;;> Given a \scheme{(post contracts ...)}, where \var{contracts ...} is zero
;;> or more predicate functions taking a single argument, evaluate each
;;> contract 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.
;;>
;;> A continuation captured within the function will include the
;;> postcondition checks.
;;>
;;> \bold{Example:}
;;>
;;> \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)))
;;> }
;;> \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, with the addition of precondition and/or postcondition contracts.
;;>
;;> 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))
;;> }
;;> 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)
    ((_ (name . ff) (pre c1 ...) (post c2 ...) e1 e2 ...)
     (define name
       (lambda-contract ff
         (pre c1 ...) (post c2 ...)
         e1 e2 ...)))
    ((_ (name f ...) (pre c1 ...) (post c2 ...) e1 e2 ...)
     (define name
       (lambda-contract (f ...)
         (pre c1 ...) (post c2 ...)
         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 ...))))