1#lang racket/base
2
3(require redex/reduction-semantics
4         (only-in redex/private/generate-term pick-an-index)
5         racket/match racket/bool)
6
7(provide (all-defined-out))
8
9(define-language rbtrees
10  (t E
11     (c t n t))
12  (c R B)
13  (n O (s n)))
14
15(define-judgment-form rbtrees
16  #:mode (rb-tree I)
17  [(rb-tree t)
18   (rbt t n_1 n_2 n_3)])
19
20(define-judgment-form rbtrees
21  #:mode (rbt I O O O)
22  [(rbt (R E n E) n n O)]
23  [(rbt (B E n E) n n (s O))]
24  [(rbt (R (B t_l1 n_l t_l2)
25           n
26           (B t_r1 n_r t_r2))
27        n_1min n_2max n_bd)
28   (rbt (B t_l1 n_l t_l2) n_1min n_1max n_bd)
29   (rbt (B t_r1 n_r t_r2) n_2min n_2max n_bd)
30   (< n_1max n)
31   (< n n_2min)]
32  [(rbt (B E n (c_2 t_21 n_2 t_22)) n n_2max (s O))
33   (rbt (c_2 t_21 n_2 t_22) n_2min n_2max O)
34   (< n n_2min)]
35  [(rbt (B (c_1 t_11 n_1 t_12) n E) n_1min n (s O))
36   (rbt (c_1 t_11 n_1 t_12) n_1min n_1max O)
37   (< n_1max n)]
38  [(rbt (B (c_1 t_11 n_1 t_12) n (c_2 t_21 n_2 t_22)) n_1min n_2max (s n_bd))
39   (rbt (c_1 t_11 n_1 t_12) n_1min n_1max n_bd)
40   (rbt (c_2 t_21 n_2 t_22) n_2min n_2max n_bd)
41   (< n_1max n)
42   (< n n_2min)])
43
44(define-relation rbtrees
45  [(< O (s n))]
46  [(< (s n_1) (s n_2))
47   (< n_1 n_2)])
48
49(define-judgment-form rbtrees
50  #:mode (ordered? I O O)
51  [(ordered? (c E n E) n n)]
52  [(ordered? (c E n t_2) n n_2max)
53   (ordered? t_2 n_2min n_2max)
54   (< n n_2min)]
55  [(ordered? (c t_1 n E) n_1min n)
56   (ordered? t_1 n_1min n_1max)
57   (< n_1max n)]
58  [(ordered? (c t_1 n t_2) n_1min n_2max)
59   (ordered? t_1 n_1min n_1max)
60   (ordered? t_2 n_2min n_2max)
61   (< n_1max n)
62   (< n n_2min)])
63
64(define-metafunction rbtrees
65  [(insert n t)
66   (B t_1 n_1 t_2)
67   (where (c t_1 n_1 t_2) (ins n t))])
68
69(define-metafunction rbtrees
70  [(ins n E)
71   (R E n E)]
72  [(ins n_1 (c t_1 n_2 t_2))
73   (balance (c (ins n_1 t_1) n_2 t_2))
74   (where #t (< n_1 n_2))]
75  [(ins n_1 (c t_1 n_2 t_2))
76   (balance (c t_1 n_2 (ins n_1 t_2)))
77   (where #t (< n_2 n_1))]
78  [(ins n t)
79   t])
80
81(define-metafunction rbtrees
82  [(balance (B (R (R t_1 n_1 t_2) n_2 t_3) n_3 t_4))
83   (R (B t_1 n_1 t_2) n_2 (B t_3 n_3 t_4))]
84  [(balance (B (R t_1 n_1 (R t_2 n_2 t_3)) n_3 t_4))
85   (R (B t_1 n_1 t_2) n_2 (B t_3 n_3 t_4))]
86  [(balance (B t_1 n_1 (R (R t_2 n_2 t_3) n_3 t_4)))
87   (R (B t_1 n_1 t_2) n_2 (B t_3 n_3 t_4))]
88  [(balance (B t_1 n_1 (R t_2 n_2 (R t_3 n_3 t_4))))
89   (R (B t_1 n_1 t_2) n_2 (B t_3 n_3 t_4))]
90  [(balance t)
91   t])
92
93
94(define-metafunction rbtrees
95  [(n->num O)
96   0]
97  [(n->num (s n))
98   ,(+ 1 (term (n->num n)))])
99
100(define-metafunction rbtrees
101  [(t->num E)
102   E]
103  [(t->num (c t_1 n t_2))
104   (c (t->num t_1) (n->num n) (t->num t_2))])
105
106(define-metafunction rbtrees
107  [(num->n 0)
108   O]
109  [(num->n number)
110   (s (num->n ,(sub1 (term number))))])
111
112(define-metafunction rbtrees
113  [(numt->t E)
114   E]
115  [(numt->t (c any_1 number any_2))
116   (c (numt->t any_1) (num->n number) (numt->t any_2))])
117
118(define (rand-ordt depth)
119  (match (generate-term
120          rbtrees
121          #:satisfying
122          (ordered? t n_1 n_2)
123          depth)
124    [#f #f]
125    [`(ordered? ,t ,min ,max)
126     (term (t->num ,t))]))
127
128(define (rand-ordts depth num)
129  (for/list ([_ (in-range num)])
130    (rand-ordt depth)))
131
132(module+
133    test
134  (require rackunit)
135  (check-true (judgment-holds
136               (ordered?
137                (B (R E (s O) E)
138                   (s (s (s O)))
139                   E)
140                n_1 n_2)))
141  (check-true (judgment-holds
142               (rb-tree (B (R E (s O) E)
143                          (s (s (s O)))
144                          E))))
145  (check-true (judgment-holds
146               (rb-tree (B (R E (s O) E)
147                        (s (s (s O)))
148                        E))))
149  (check-true (judgment-holds
150               (rb-tree (R (B E (s O) E)
151                        (s (s (s O)))
152                        (B E
153                           (s (s (s (s (s O)))))
154                           E)))))
155  (check-false (judgment-holds
156                (rb-tree (R (B E (s (s O)) E)
157                         (s O)
158                         (R E O E))))))
159
160(define (ins-preserves-rb-tree t)
161  (or (not (judgment-holds (rb-tree ,t)))
162      (match (judgment-holds (ordered? ,t n_1 n_2) (n_1 n_2))
163        [`((,min-n ,max-n))
164         (define nmin (term (n->num ,min-n)))
165         (define nmax (term (n->num ,max-n)))
166         (for/and ([n (in-range (max 0 (sub1 nmin)) (+ 2 nmax))])
167           (judgment-holds
168            (rb-tree
169             (insert (num->n ,n) ,t))))])))
170
171(module+
172    test
173  (define (check-rbsts n)
174    (for ([_ (in-range n)])
175      (match (generate-term rbtrees
176                            #:satisfying
177                            (rb-tree t)
178                            8)
179        [#f (void)]
180        [`(rbst ,t)
181         (check-not-false (or (ins-preserves-rb-tree t)
182                              (printf "~s\n" t)))])))
183
184  (define (check-rbst/rb-tree tries)
185    (for ([_ tries])
186      (match (generate-term rbtrees
187                            #:satisfying
188                            (rb-tree t)
189                            8)
190        [#f (void)]
191        [`(rbst ,t)
192         (define res
193           (judgment-holds
194            (rb-tree ,t)))
195         (unless res (displayln t))
196         (check-not-false res)]))
197    (for ([_ tries])
198      (match (generate-term rbtrees
199                            #:satisfying
200                            (rb-tree t)
201                            8)
202        [#f (void)]
203        [`(rb-tree ,t)
204         (define res
205           (judgment-holds
206            (rb-tree ,t)))
207         (unless res (displayln t))
208         (check-not-false res)]))))
209
210