1 | (import scheme |
---|
2 | (chicken base) |
---|
3 | checks |
---|
4 | simple-tests |
---|
5 | simple-contracts) |
---|
6 | |
---|
7 | (contract-check-level 1) |
---|
8 | |
---|
9 | (define-values (counter! counter) |
---|
10 | (let ((state 0)) |
---|
11 | (values |
---|
12 | (xlambda ((new (cut = <> (add1 old))) |
---|
13 | ;integer? (lambda (x) (= x (add1 old)))) |
---|
14 | (old integer?) |
---|
15 | <-) |
---|
16 | (let ((old state)) |
---|
17 | (set! state (add1 state)) |
---|
18 | (values state old))) |
---|
19 | (xlambda ((result (cut = <> state)) |
---|
20 | <-) |
---|
21 | state)))) |
---|
22 | |
---|
23 | (define-values (push pop top) |
---|
24 | (let ((stk '())) |
---|
25 | (let ( |
---|
26 | (push |
---|
27 | (xlambda ((new list? (cut equal? <> (cons arg old))) |
---|
28 | (old list?) |
---|
29 | <- |
---|
30 | (arg)) |
---|
31 | (let ((old stk)) |
---|
32 | (set! stk (cons arg stk)) |
---|
33 | (values stk old)))) |
---|
34 | (pop |
---|
35 | (xlambda ((new list? (cut equal? <> (cdr old))) |
---|
36 | (old list?) |
---|
37 | <-) |
---|
38 | (let ((old (<<< 'pop stk (o not null?)))) |
---|
39 | (set! stk (cdr stk)) |
---|
40 | (values stk old)))) |
---|
41 | (top |
---|
42 | (xlambda ((result) <-) |
---|
43 | (car (<<< 'top stk (o not null?))))) |
---|
44 | ) |
---|
45 | (values push pop top) |
---|
46 | ))) |
---|
47 | |
---|
48 | (define-values (add add-pre add-post) |
---|
49 | (xlambda ((result integer? odd? (cut = <> (apply + x y ys))) |
---|
50 | <- |
---|
51 | (x integer? odd?) (y integer? even?) ys integer? even?) |
---|
52 | (apply + x y ys))) |
---|
53 | |
---|
54 | (define wrong-add |
---|
55 | (xlambda ((result integer? even?) |
---|
56 | <- |
---|
57 | (x integer? odd?) xs integer? even?) |
---|
58 | (apply + x xs))) |
---|
59 | |
---|
60 | (define-values (divide divide-pre divide-post) |
---|
61 | (xlambda ((q integer?) |
---|
62 | (r (lambda (x) (= (+ x (* n q)) m))) |
---|
63 | <- |
---|
64 | (m integer? (cut >= <> 0)) |
---|
65 | (n integer? positive?)) |
---|
66 | (let loop ((q 0) (r m)) |
---|
67 | (if (< r n) |
---|
68 | (values q r) |
---|
69 | (loop (+ q 1) (- r n)))))) |
---|
70 | |
---|
71 | (xdefine ((result integer?) |
---|
72 | #(sum-post sum sum-pre) |
---|
73 | (a integer?) as integer?) |
---|
74 | (apply + a as)) |
---|
75 | |
---|
76 | (xdefine ((result list?) |
---|
77 | wrong-sum |
---|
78 | (a integer?) as integer?) |
---|
79 | (apply + a as)) |
---|
80 | |
---|
81 | (define-test (contracts?) |
---|
82 | |
---|
83 | "QUERIES" |
---|
84 | '(define-values (add add-pre add-post) |
---|
85 | (xlambda ((result integer? odd? (cut = <> (apply + x y ys))) |
---|
86 | <- |
---|
87 | (x integer? odd?) (y integer? even?) ys integer? even?) |
---|
88 | (apply + x y ys))) |
---|
89 | (= (add 1 2 4 6) 13) |
---|
90 | (equal? add-pre |
---|
91 | '((x integer? odd?) |
---|
92 | (y integer? even?) |
---|
93 | ys integer? even?)) |
---|
94 | (equal? add-post |
---|
95 | '(result integer? odd? (cut = <> (apply + x y ys)))) |
---|
96 | (not (condition-case (add 1 2 3) ((exn) #f))) |
---|
97 | ;(not (condition-case (add 1 2 3) ((exn argument) #f))) |
---|
98 | |
---|
99 | '(define wrong-add |
---|
100 | (xlambda ((result integer? even?) |
---|
101 | <- |
---|
102 | (x integer? odd?) xs integer? even?) |
---|
103 | (apply + x xs))) |
---|
104 | (not (condition-case (wrong-add 1 2 4) ((exn) #f))) |
---|
105 | ;(not (condition-case (wrong-add 1 2 4) ((exn result) #f))) |
---|
106 | |
---|
107 | '(define-values (divide divide-pre divide-post) |
---|
108 | (xlambda ((q integer?) |
---|
109 | (r (lambda (x) (= (+ x (* n q)) m)) |
---|
110 | <- |
---|
111 | (m integer? (cut >= <> 0)) |
---|
112 | (n integer? positive?)) |
---|
113 | (let loop ((q 0) (r m)) |
---|
114 | (if (< r n) |
---|
115 | (values q r) |
---|
116 | (loop (+ q 1) (- r n))))))) |
---|
117 | (equal? |
---|
118 | (call-with-values |
---|
119 | (lambda () (divide 385 25)) |
---|
120 | list) |
---|
121 | '(15 10)) |
---|
122 | (equal? divide-pre |
---|
123 | '((m integer? (cut >= <> 0)) |
---|
124 | (n integer? positive?))) |
---|
125 | (equal? divide-post |
---|
126 | '((q integer?) |
---|
127 | (r (lambda (x) (= (+ x (* n q)) m))))) |
---|
128 | |
---|
129 | "COMMANDS" |
---|
130 | '(define-values (counter! counter) |
---|
131 | (let ((state 0)) |
---|
132 | (values |
---|
133 | (xlambda ((new (cut = <> (add1 old))) |
---|
134 | (old integer?) |
---|
135 | <-) |
---|
136 | (let ((old state)) |
---|
137 | (set! state (add1 state)) |
---|
138 | (values state old))) |
---|
139 | (xlambda ((result (cut = <> state)) <-) |
---|
140 | state)))) |
---|
141 | (zero? (counter)) |
---|
142 | (counter!) |
---|
143 | (= (counter) 1) |
---|
144 | (counter!) |
---|
145 | (= (counter) 2) |
---|
146 | |
---|
147 | '(define-values (push pop top) |
---|
148 | (let ((stk '())) |
---|
149 | (let ( |
---|
150 | (push |
---|
151 | (xlambda ((new list? (cut equal? <> (cons arg old))) |
---|
152 | (old list?) |
---|
153 | <- |
---|
154 | (arg)) |
---|
155 | (let ((old stk)) |
---|
156 | (set! stk (cons arg stk)) |
---|
157 | (values stk old)))) |
---|
158 | (pop |
---|
159 | (xlambda ((new list? (cut equal? <> (cdr old))) |
---|
160 | (old list?) |
---|
161 | <-) |
---|
162 | (let ((old (<<< 'pop stk (o not null?)))) |
---|
163 | (set! stk (cdr stk)) |
---|
164 | (values stk old)))) |
---|
165 | (top |
---|
166 | (xlambda ((result) <-) |
---|
167 | (car (<<< 'top stk (o not null?))))) |
---|
168 | ) |
---|
169 | (values push pop top) |
---|
170 | ))) |
---|
171 | ;(top) ; precondition violated |
---|
172 | ;(pop) ; precondition violated |
---|
173 | (push 0) |
---|
174 | (push 1) |
---|
175 | (= 1 (top)) |
---|
176 | (equal? (call-with-values (lambda () (push 2)) list) |
---|
177 | '((2 1 0) (1 0))) |
---|
178 | (= 2 (top)) |
---|
179 | (equal? (call-with-values (lambda () (pop)) list) |
---|
180 | '((1 0) (2 1 0))) |
---|
181 | "XDEFINE" |
---|
182 | ;(xdefine ((result integer?) sum (a integer?) as integer?) |
---|
183 | '(xdefine ((result integer?) |
---|
184 | #(sum-post sum sum-pre) |
---|
185 | (a integer?) as integer?) |
---|
186 | (apply + a as)) |
---|
187 | ;(print sum-post) |
---|
188 | ;(print sum-pre) |
---|
189 | (= (sum 1 2 3) 6) |
---|
190 | (not (condition-case (sum 1 2 #f) ((exn) #f))) |
---|
191 | ;(not (condition-case (sum 1 2 #f) ((exn argument) #f))) |
---|
192 | '(xdefine ((result list?) |
---|
193 | wrong-sum |
---|
194 | (a integer?) as integer?) |
---|
195 | (apply + a as)) |
---|
196 | (not (condition-case (wrong-sum 1 2 3) ((exn) #f))) |
---|
197 | ;(not (condition-case (wrong-sum 1 2 3) ((exn result) #f))) |
---|
198 | ) |
---|
199 | |
---|
200 | (compound-test (SIMPLE-CONTRACTS) |
---|
201 | (contracts?) |
---|
202 | ) |
---|
203 | |
---|