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