-
-
Notifications
You must be signed in to change notification settings - Fork 647
/
and.rkt
397 lines (373 loc) · 14.8 KB
/
and.rkt
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
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
#lang racket/base
(require (for-syntax racket/base
"arr-util.rkt")
racket/promise
(only-in "../../private/promise.rkt" prop:force promise-forcer)
"../../private/math-predicates.rkt"
"prop.rkt"
"blame.rkt"
"guts.rkt"
"rand.rkt"
"generate.rkt"
"generate-base.rkt"
"misc.rkt"
"list.rkt")
(provide and/c integer-in)
(define (and-name ctc)
(apply build-compound-type-name 'and/c (base-and/c-ctcs ctc)))
(define (and-first-order ctc)
(let ([tests (map contract-first-order (base-and/c-ctcs ctc))])
(λ (x) (for/and ([test (in-list tests)]) (test x)))))
(define (late-neg-and-proj ctc)
(define mk-pos-projs (map get/build-late-neg-projection (base-and/c-ctcs ctc)))
(λ (blame)
(define projs
(for/list ([c (in-list mk-pos-projs)]
[n (in-naturals 1)])
(c (blame-add-context blame (format "the ~a conjunct of" (n->th n))))))
(λ (val neg-party)
(let loop ([projs (cdr projs)]
[val ((car projs) val neg-party)])
(cond
[(null? projs) val]
[else
(loop (cdr projs)
((car projs) val neg-party))])))))
(define (first-order-late-neg-and-proj ctc)
(define predicates (first-order-and/c-predicates ctc))
(define blame-accepters (map get/build-late-neg-projection (base-and/c-ctcs ctc)))
(λ (blame)
(define new-blame (blame-add-context blame "an and/c case of"))
(define projs (map (λ (f) (f new-blame)) blame-accepters))
(λ (val neg-party)
(let loop ([predicates predicates]
[projs projs])
(cond
[(null? predicates) val]
[else
(cond
[((car predicates) val)
(loop (cdr predicates) (cdr projs))]
[else
((car projs) val neg-party)])])))))
(define (and-stronger? this that)
(and (base-and/c? that)
(pairwise-stronger-contracts? (base-and/c-ctcs this)
(base-and/c-ctcs that))))
(define (and-equivalent? this that)
(and (base-and/c? that)
(pairwise-equivalent-contracts? (base-and/c-ctcs this)
(base-and/c-ctcs that))))
(define (and/c-generate? ctc)
(cond
[(and/c-check-nonneg ctc real?) => values]
[(and/c-check-nonneg ctc rational?) => values]
[(null? (base-and/c-ctcs ctc)) => (λ (fuel) #f)]
[else
(define flat (filter flat-contract? (base-and/c-ctcs ctc)))
(define ho (filter (λ (x) (not (flat-contract? x))) (base-and/c-ctcs ctc)))
(cond
[(null? ho)
(λ (fuel)
(define candidates
(let loop ([sub-contracts-after (cdr (base-and/c-ctcs ctc))]
[sub-contract (car (base-and/c-ctcs ctc))]
[sub-contracts-before '()]
[candidates '()])
(define sub-gen (contract-random-generate/choose sub-contract fuel))
(define new-candidates
(cond
[sub-gen
(cons (cons sub-gen (append (reverse sub-contracts-before) sub-contracts-after))
candidates)]
[else candidates]))
(cond
[(null? sub-contracts-after) new-candidates]
[else (loop (cdr sub-contracts-after)
(car sub-contracts-after)
(cons sub-contract sub-contracts-before)
new-candidates)])))
(cond
[(null? candidates) #f]
[else
(λ ()
(let loop ([attempts 10])
(cond
[(zero? attempts) contract-random-generate-fail]
[else
(define which (oneof candidates))
(define val ((car which)))
(cond
[(andmap (λ (p?) (p? val)) (cdr which))
val]
[else
(loop (- attempts 1))])])))]))]
[(null? (cdr ho))
(λ (fuel)
(define ho-gen (contract-random-generate/choose (car ho) fuel))
(cond
[ho-gen
(λ ()
(let loop ([attempts 10])
(cond
[(zero? attempts) contract-random-generate-fail]
[else
(define val (ho-gen))
(cond
[(andmap (λ (p?) (p? val)) flat)
val]
[else
(loop (- attempts 1))])])))]
[else #f]))]
[else
(λ (fuel) #f)])]))
(define (and/c-check-nonneg ctc pred)
(define sub-contracts (base-and/c-ctcs ctc))
(cond
[(pairwise-stronger-contracts?
(list (coerce-contract 'and/c-check-nonneg pred) (not/c negative?))
sub-contracts)
(define go (hash-ref predicate-generator-table pred))
(λ (fuel)
(λ ()
(abs (go fuel))))]
[else #f]))
(define-struct base-and/c (ctcs))
(define-struct (first-order-and/c base-and/c) (predicates)
#:property prop:custom-write custom-write-property-proc
#:property prop:flat-contract
(build-flat-contract-property
#:trusted trust-me
#:late-neg-projection first-order-late-neg-and-proj
#:name and-name
#:first-order and-first-order
#:stronger and-stronger?
#:generate and/c-generate?
#:equivalent and-equivalent?))
(define-struct (chaperone-and/c base-and/c) ()
#:property prop:custom-write custom-write-property-proc
#:property prop:chaperone-contract
(build-chaperone-contract-property
#:trusted trust-me
#:late-neg-projection late-neg-and-proj
#:name and-name
#:first-order and-first-order
#:stronger and-stronger?
#:generate and/c-generate?
#:equivalent and-equivalent?))
(define-struct (impersonator-and/c base-and/c) ()
#:property prop:custom-write custom-write-property-proc
#:property prop:contract
(build-contract-property
#:trusted trust-me
#:late-neg-projection late-neg-and-proj
#:name and-name
#:first-order and-first-order
#:stronger and-stronger?
#:generate and/c-generate?
#:equivalent and-equivalent?))
(define-syntax (and/c stx)
(syntax-case stx (pair? listof)
[(_ pair? (listof e))
#'(non-empty-listof e)]
[(_ (listof e) pair?)
#'(non-empty-listof e)]
[(_ . args)
#'(real-and/c . args)]
[x
(identifier? #'x)
#'real-and/c]))
(define/subexpression-pos-prop/name real-and/c-name (real-and/c . raw-fs)
(let ([contracts (coerce-contracts 'and/c raw-fs)])
(cond
[(null? contracts) any/c]
[(andmap flat-contract? contracts)
(define preds (map flat-contract-predicate contracts))
(cond
[(and (pair? (cdr preds))
(null? (cddr preds)))
(cond
[(chaperone-of? (car preds) real?)
(define second-pred (cadr preds))
(cond
[(chaperone-of? second-pred negative?)
(renamed-<-ctc 0 `(and/c real? negative?))]
[(chaperone-of? second-pred positive?)
(renamed->-ctc 0 `(and/c real? positive?))]
[else
(define second-contract (cadr contracts))
(cond
[(equal? (contract-name second-contract) '(not/c positive?))
(renamed-between/c -inf.0 0 `(and/c real? (not/c positive?)))]
[(equal? (contract-name second-contract) '(not/c negative?))
(renamed-between/c 0 +inf.0 `(and/c real? (not/c negative?)))]
[else
(make-first-order-and/c contracts preds)])])]
[(or (chaperone-of? (car preds) exact-nonnegative-integer?)
(chaperone-of? (car preds) natural?)
(chaperone-of? (cadr preds) exact-nonnegative-integer?)
(chaperone-of? (cadr preds) natural?))
(define other (if (procedure? (car preds)) (cadr contracts) (car contracts)))
(cond
[(between/c-s? other)
(define other-low (between/c-s-low other))
(define other-high (between/c-s-high other))
(integer-in (exact-ceiling (max 0 (if (= other-low -inf.0) 0 other-low)))
(if (= other-high +inf.0) #f (exact-floor other-high)))]
[else (make-first-order-and/c contracts preds)])]
[(or (chaperone-of? (car preds) exact-positive-integer?)
(chaperone-of? (cadr preds) exact-positive-integer?))
(define other (if (procedure? (car preds)) (cadr contracts) (car contracts)))
(cond
[(between/c-s? other)
(define other-low (between/c-s-low other))
(define other-high (between/c-s-high other))
(integer-in (exact-ceiling (max 1 (if (= other-low -inf.0) 1 other-low)))
(if (= other-high +inf.0) #f (exact-floor other-high)))]
[else (make-first-order-and/c contracts preds)])]
[(or (chaperone-of? (car preds) exact-integer?)
(chaperone-of? (cadr preds) exact-integer?))
(define other (if (procedure? (car preds)) (cadr contracts) (car contracts)))
(cond
[(between/c-s? other)
(define other-low (between/c-s-low other))
(define other-high (between/c-s-high other))
(integer-in (if (= other-low -inf.0) #f (exact-ceiling other-low))
(if (= other-high +inf.0) #f (exact-floor other-high)))]
[else (make-first-order-and/c contracts preds)])]
[else
(make-first-order-and/c contracts preds)])]
[(and (pair? (cdr preds))
(pair? (cddr preds))
(null? (cdddr preds)))
(cond
[(or (chaperone-of? (car preds) exact-integer?)
(chaperone-of? (cadr preds) exact-integer?)
(chaperone-of? (caddr preds) exact-integer?))
(define lb #f)
(define ub #f)
(for ([ctc (in-list contracts)])
(cond
[(between/c-s? ctc)
(define lo (between/c-s-low ctc))
(define hi (between/c-s-high ctc))
(cond
[(and (= lo -inf.0) (integer? hi))
(set! ub (inexact->exact hi))]
[(and (= hi +inf.0) (integer? lo))
(set! lb (inexact->exact lo))])]
[(</>-ctc? ctc)
(define x (</>-ctc-x ctc))
(when (integer? x)
(cond
[(<-ctc? ctc) (set! ub (- (inexact->exact x) 1))]
[(>-ctc? ctc) (set! lb (+ (inexact->exact x) 1))]))]))
(cond
[(and lb ub)
(integer-in lb ub)]
[else (make-first-order-and/c contracts preds)])]
[else (make-first-order-and/c contracts preds)])]
[else
(make-first-order-and/c contracts preds)])]
[(andmap chaperone-contract? contracts)
(make-chaperone-and/c contracts)]
[else (make-impersonator-and/c contracts)])))
(define (exact-floor x) (floor (inexact->exact x)))
(define (exact-ceiling x) (ceiling (inexact->exact x)))
(define (integer-in-name ctc)
(define start (integer-in-ctc-start ctc))
(define end (integer-in-ctc-end ctc))
(cond
[(and (not end) (equal? start 0)) 'natural?]
[(and (not end) (equal? start 1)) 'exact-positive-integer?]
[(or start end)
`(integer-in ,(integer-in-ctc-start ctc)
,(integer-in-ctc-end ctc))]
[else 'exact-integer?]))
(define (integer-in-first-order ctc)
(define start (integer-in-ctc-start ctc))
(define end (integer-in-ctc-end ctc))
(cond
[(and start end) (λ (x) (and (exact-integer? x) (<= start x end)))]
[start
(case start
[(0) exact-nonnegative-integer?]
[(1) exact-positive-integer?]
[else
(λ (x) (and (exact-integer? x) (<= start x)))])]
[end (λ (x) (and (exact-integer? x) (<= x end)))]
[else exact-integer?]))
(define (integer-in-stronger this that)
(cond
[(integer-in-ctc? that)
(define this-start (or (integer-in-ctc-start this) -inf.0))
(define this-end (or (integer-in-ctc-end this) +inf.0))
(define that-start (or (integer-in-ctc-start that) -inf.0))
(define that-end (or (integer-in-ctc-end that) +inf.0))
(<= that-start this-start this-end that-end)]
[else #f]))
(define (integer-in-equivalent this that)
(cond
[(integer-in-ctc? that)
(define this-start (or (integer-in-ctc-start this) -inf.0))
(define this-end (or (integer-in-ctc-end this) +inf.0))
(define that-start (or (integer-in-ctc-start that) -inf.0))
(define that-end (or (integer-in-ctc-end that) +inf.0))
(and (= that-start this-start) (= this-end that-end))]
[else #f]))
(define (integer-in-generate ctc)
(define start (integer-in-ctc-start ctc))
(define end (integer-in-ctc-end ctc))
(define max-random-range 4294967087)
(cond
[(or start end)
(define _start (or start (- end max-random-range)))
(define _end (or end (+ start max-random-range)))
(λ (fuel)
(λ ()
(+ _start (random (min 4294967087 (+ (- _end _start) 1))))))]
[else
(λ (fuel)
(λ ()
(cond
[(zero? (random 20)) 0]
[else
(* (if (zero? (random 2)) -1 1)
(+ (expt 2 (geo-dist 1/2))
(geo-dist 1/2)))])))]))
(struct integer-in-ctc (start end)
#:property prop:custom-write custom-write-property-proc
#:property prop:flat-contract
(build-flat-contract-property
#:trusted trust-me
#:name integer-in-name
#:first-order integer-in-first-order
#:stronger integer-in-stronger
#:generate integer-in-generate
#:equivalent integer-in-equivalent))
(struct renamed-integer-in integer-in-ctc (name)
#:property prop:flat-contract
(build-flat-contract-property
#:trusted trust-me
#:name (λ (ctc) (renamed-integer-in-name ctc))
#:first-order integer-in-first-order
#:stronger integer-in-stronger
#:equivalent integer-in-equivalent
#:generate integer-in-generate))
(define (geo-dist p)
(let loop ([n 0])
(cond
[(< (random) p) (loop (+ n 1))]
[else n])))
(define/final-prop (integer-in start end)
(define (|(or/c #f exact-integer?)| x) (or (not x) (exact-integer? x)))
(check-two-args 'integer-in start end |(or/c #f exact-integer?)| |(or/c #f exact-integer?)|)
(cond
[(and start end (= start end))
(and/c start exact?)]
[else
(integer-in-ctc start end)]))
(set-some-basic-integer-in-contracts! renamed-integer-in
(integer-in #f #f)
(integer-in 0 #f)
(integer-in 1 #f))