Adding fixed test mode and small examples for all diffs
This commit is contained in:
Jay McCarthy
parent
65a83b1e7a
commit
e545926e76
2
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/.gitignore
vendored
Normal file
2
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/.gitignore
vendored
Normal file
|
|
@ -0,0 +1,2 @@
|
|||
*.orig
|
||||
/*.rktd
|
||||
|
|
@ -950,3 +950,9 @@
|
|||
(begin0
|
||||
(generate-term abort-lang e #:i-th index)
|
||||
(set! index (add1 index)))))
|
||||
|
||||
(define fixed
|
||||
(term
|
||||
(;; 1, 2 & 3 [designed for 1]
|
||||
(ccm (MG (flat (λ (x : Num) #t)) key:test "k" "l" "j") Num)
|
||||
)))
|
||||
|
|
|
|||
|
|
@ -948,3 +948,9 @@
|
|||
(begin0
|
||||
(generate-term abort-lang e #:i-th index)
|
||||
(set! index (add1 index)))))
|
||||
|
||||
(define fixed
|
||||
(term
|
||||
(;; 1, 2 & 3 [designed for 1]
|
||||
(ccm (MG (flat (λ (x : Num) #t)) key:test "k" "l" "j") Num)
|
||||
)))
|
||||
|
|
|
|||
|
|
@ -948,3 +948,9 @@
|
|||
(begin0
|
||||
(generate-term abort-lang e #:i-th index)
|
||||
(set! index (add1 index)))))
|
||||
|
||||
(define fixed
|
||||
(term
|
||||
(;; 1, 2 & 3 [designed for 1]
|
||||
(ccm (MG (flat (λ (x : Num) #t)) key:test "k" "l" "j") Num)
|
||||
)))
|
||||
|
|
|
|||
|
|
@ -945,3 +945,9 @@
|
|||
(begin0
|
||||
(generate-term abort-lang e #:i-th index)
|
||||
(set! index (add1 index)))))
|
||||
|
||||
(define fixed
|
||||
(term
|
||||
(;; 1, 2 & 3 [designed for 1]
|
||||
(ccm (MG (flat (λ (x : Num) #t)) key:test "k" "l" "j") Num)
|
||||
)))
|
||||
|
|
|
|||
|
|
@ -443,3 +443,11 @@
|
|||
(generate-term list-machine-typing (l0 : ι p) #:i-th index)
|
||||
(set! index (add1 index))))))
|
||||
|
||||
(define fixed
|
||||
(term
|
||||
;; 1, 2, and 3 [but designed for 3]
|
||||
((l0 : (begin (cons x y z)
|
||||
(begin (branch-if-nil z loop)
|
||||
halt))
|
||||
(loop : (jump loop)
|
||||
end)))))
|
||||
|
|
|
|||
|
|
@ -443,3 +443,11 @@
|
|||
(generate-term list-machine-typing (l0 : ι p) #:i-th index)
|
||||
(set! index (add1 index))))))
|
||||
|
||||
(define fixed
|
||||
(term
|
||||
;; 1, 2, and 3 [but designed for 3]
|
||||
((l0 : (begin (cons x y z)
|
||||
(begin (branch-if-nil z loop)
|
||||
halt))
|
||||
(loop : (jump loop)
|
||||
end)))))
|
||||
|
|
|
|||
|
|
@ -439,3 +439,11 @@
|
|||
(generate-term list-machine-typing (l0 : ι p) #:i-th index)
|
||||
(set! index (add1 index))))))
|
||||
|
||||
(define fixed
|
||||
(term
|
||||
;; 1, 2, and 3 [but designed for 3]
|
||||
((l0 : (begin (cons x y z)
|
||||
(begin (branch-if-nil z loop)
|
||||
halt))
|
||||
(loop : (jump loop)
|
||||
end)))))
|
||||
|
|
|
|||
|
|
@ -439,3 +439,11 @@
|
|||
(generate-term list-machine-typing (l0 : ι p) #:i-th index)
|
||||
(set! index (add1 index))))))
|
||||
|
||||
(define fixed
|
||||
(term
|
||||
;; 1, 2, and 3 [but designed for 3]
|
||||
((l0 : (begin (cons x y z)
|
||||
(begin (branch-if-nil z loop)
|
||||
halt))
|
||||
(loop : (jump loop)
|
||||
end)))))
|
||||
|
|
|
|||
|
|
@ -274,11 +274,14 @@
|
|||
(v? term)
|
||||
(let ([red-res (apply-reduction-relation red term)]
|
||||
[t-type (type-check term)])
|
||||
;; xxx should this also be t-type IMPLIES?
|
||||
(and
|
||||
(= (length red-res) 1)
|
||||
(or
|
||||
(equal? (car red-res) "error")
|
||||
(equal? t-type (type-check (car red-res))))))))
|
||||
(let ([red-t (car red-res)])
|
||||
(or
|
||||
(equal? red-t "error")
|
||||
(let ([red-type (type-check red-t)])
|
||||
(equal? t-type red-type))))))))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term poly-stlc M #:i-th (pick-an-index 0.001)))
|
||||
|
|
@ -289,3 +292,21 @@
|
|||
(begin0
|
||||
(generate-term poly-stlc M #:i-th index)
|
||||
(set! index (add1 index))))))
|
||||
|
||||
(define fixed
|
||||
(term
|
||||
(;; 2
|
||||
(([cons @ int] 1) nil)
|
||||
|
||||
;; 3 & 10 [designed for 3]
|
||||
((λ (x int) [nil @ int]) 1)
|
||||
|
||||
;; 5, 6, 7, 8 & 9 [designed for 4]
|
||||
((λ (x int) x)
|
||||
(([cons @ int] 1) [nil @ int]))
|
||||
|
||||
;; 4
|
||||
([tl @ int]
|
||||
(([cons @ int] 1) [nil @ int]))
|
||||
|
||||
)))
|
||||
|
|
|
|||
|
|
@ -272,11 +272,14 @@
|
|||
(v? term)
|
||||
(let ([red-res (apply-reduction-relation red term)]
|
||||
[t-type (type-check term)])
|
||||
;; xxx should this also be t-type IMPLIES?
|
||||
(and
|
||||
(= (length red-res) 1)
|
||||
(or
|
||||
(equal? (car red-res) "error")
|
||||
(equal? t-type (type-check (car red-res))))))))
|
||||
(let ([red-t (car red-res)])
|
||||
(or
|
||||
(equal? red-t "error")
|
||||
(let ([red-type (type-check red-t)])
|
||||
(equal? t-type red-type))))))))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term poly-stlc M #:i-th (pick-an-index 0.001)))
|
||||
|
|
@ -287,3 +290,21 @@
|
|||
(begin0
|
||||
(generate-term poly-stlc M #:i-th index)
|
||||
(set! index (add1 index))))))
|
||||
|
||||
(define fixed
|
||||
(term
|
||||
(;; 2
|
||||
(([cons @ int] 1) nil)
|
||||
|
||||
;; 3 & 10 [designed for 3]
|
||||
((λ (x int) [nil @ int]) 1)
|
||||
|
||||
;; 5, 6, 7, 8 & 9 [designed for 4]
|
||||
((λ (x int) x)
|
||||
(([cons @ int] 1) [nil @ int]))
|
||||
|
||||
;; 4
|
||||
([tl @ int]
|
||||
(([cons @ int] 1) [nil @ int]))
|
||||
|
||||
)))
|
||||
|
|
|
|||
|
|
@ -274,11 +274,14 @@
|
|||
(v? term)
|
||||
(let ([red-res (apply-reduction-relation red term)]
|
||||
[t-type (type-check term)])
|
||||
;; xxx should this also be t-type IMPLIES?
|
||||
(and
|
||||
(= (length red-res) 1)
|
||||
(or
|
||||
(equal? (car red-res) "error")
|
||||
(equal? t-type (type-check (car red-res))))))))
|
||||
(let ([red-t (car red-res)])
|
||||
(or
|
||||
(equal? red-t "error")
|
||||
(let ([red-type (type-check red-t)])
|
||||
(equal? t-type red-type))))))))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term poly-stlc M #:i-th (pick-an-index 0.001)))
|
||||
|
|
@ -289,3 +292,21 @@
|
|||
(begin0
|
||||
(generate-term poly-stlc M #:i-th index)
|
||||
(set! index (add1 index))))))
|
||||
|
||||
(define fixed
|
||||
(term
|
||||
(;; 2
|
||||
(([cons @ int] 1) nil)
|
||||
|
||||
;; 3 & 10 [designed for 3]
|
||||
((λ (x int) [nil @ int]) 1)
|
||||
|
||||
;; 5, 6, 7, 8 & 9 [designed for 4]
|
||||
((λ (x int) x)
|
||||
(([cons @ int] 1) [nil @ int]))
|
||||
|
||||
;; 4
|
||||
([tl @ int]
|
||||
(([cons @ int] 1) [nil @ int]))
|
||||
|
||||
)))
|
||||
|
|
|
|||
|
|
@ -274,11 +274,14 @@
|
|||
(v? term)
|
||||
(let ([red-res (apply-reduction-relation red term)]
|
||||
[t-type (type-check term)])
|
||||
;; xxx should this also be t-type IMPLIES?
|
||||
(and
|
||||
(= (length red-res) 1)
|
||||
(or
|
||||
(equal? (car red-res) "error")
|
||||
(equal? t-type (type-check (car red-res))))))))
|
||||
(let ([red-t (car red-res)])
|
||||
(or
|
||||
(equal? red-t "error")
|
||||
(let ([red-type (type-check red-t)])
|
||||
(equal? t-type red-type))))))))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term poly-stlc M #:i-th (pick-an-index 0.001)))
|
||||
|
|
@ -289,3 +292,21 @@
|
|||
(begin0
|
||||
(generate-term poly-stlc M #:i-th index)
|
||||
(set! index (add1 index))))))
|
||||
|
||||
(define fixed
|
||||
(term
|
||||
(;; 2
|
||||
(([cons @ int] 1) nil)
|
||||
|
||||
;; 3 & 10 [designed for 3]
|
||||
((λ (x int) [nil @ int]) 1)
|
||||
|
||||
;; 5, 6, 7, 8 & 9 [designed for 4]
|
||||
((λ (x int) x)
|
||||
(([cons @ int] 1) [nil @ int]))
|
||||
|
||||
;; 4
|
||||
([tl @ int]
|
||||
(([cons @ int] 1) [nil @ int]))
|
||||
|
||||
)))
|
||||
|
|
|
|||
|
|
@ -274,11 +274,14 @@
|
|||
(v? term)
|
||||
(let ([red-res (apply-reduction-relation red term)]
|
||||
[t-type (type-check term)])
|
||||
;; xxx should this also be t-type IMPLIES?
|
||||
(and
|
||||
(= (length red-res) 1)
|
||||
(or
|
||||
(equal? (car red-res) "error")
|
||||
(equal? t-type (type-check (car red-res))))))))
|
||||
(let ([red-t (car red-res)])
|
||||
(or
|
||||
(equal? red-t "error")
|
||||
(let ([red-type (type-check red-t)])
|
||||
(equal? t-type red-type))))))))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term poly-stlc M #:i-th (pick-an-index 0.001)))
|
||||
|
|
@ -289,3 +292,21 @@
|
|||
(begin0
|
||||
(generate-term poly-stlc M #:i-th index)
|
||||
(set! index (add1 index))))))
|
||||
|
||||
(define fixed
|
||||
(term
|
||||
(;; 2
|
||||
(([cons @ int] 1) nil)
|
||||
|
||||
;; 3 & 10 [designed for 3]
|
||||
((λ (x int) [nil @ int]) 1)
|
||||
|
||||
;; 5, 6, 7, 8 & 9 [designed for 4]
|
||||
((λ (x int) x)
|
||||
(([cons @ int] 1) [nil @ int]))
|
||||
|
||||
;; 4
|
||||
([tl @ int]
|
||||
(([cons @ int] 1) [nil @ int]))
|
||||
|
||||
)))
|
||||
|
|
|
|||
|
|
@ -274,11 +274,14 @@
|
|||
(v? term)
|
||||
(let ([red-res (apply-reduction-relation red term)]
|
||||
[t-type (type-check term)])
|
||||
;; xxx should this also be t-type IMPLIES?
|
||||
(and
|
||||
(= (length red-res) 1)
|
||||
(or
|
||||
(equal? (car red-res) "error")
|
||||
(equal? t-type (type-check (car red-res))))))))
|
||||
(let ([red-t (car red-res)])
|
||||
(or
|
||||
(equal? red-t "error")
|
||||
(let ([red-type (type-check red-t)])
|
||||
(equal? t-type red-type))))))))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term poly-stlc M #:i-th (pick-an-index 0.001)))
|
||||
|
|
@ -289,3 +292,21 @@
|
|||
(begin0
|
||||
(generate-term poly-stlc M #:i-th index)
|
||||
(set! index (add1 index))))))
|
||||
|
||||
(define fixed
|
||||
(term
|
||||
(;; 2
|
||||
(([cons @ int] 1) nil)
|
||||
|
||||
;; 3 & 10 [designed for 3]
|
||||
((λ (x int) [nil @ int]) 1)
|
||||
|
||||
;; 5, 6, 7, 8 & 9 [designed for 4]
|
||||
((λ (x int) x)
|
||||
(([cons @ int] 1) [nil @ int]))
|
||||
|
||||
;; 4
|
||||
([tl @ int]
|
||||
(([cons @ int] 1) [nil @ int]))
|
||||
|
||||
)))
|
||||
|
|
|
|||
|
|
@ -273,11 +273,14 @@
|
|||
(v? term)
|
||||
(let ([red-res (apply-reduction-relation red term)]
|
||||
[t-type (type-check term)])
|
||||
;; xxx should this also be t-type IMPLIES?
|
||||
(and
|
||||
(= (length red-res) 1)
|
||||
(or
|
||||
(equal? (car red-res) "error")
|
||||
(equal? t-type (type-check (car red-res))))))))
|
||||
(let ([red-t (car red-res)])
|
||||
(or
|
||||
(equal? red-t "error")
|
||||
(let ([red-type (type-check red-t)])
|
||||
(equal? t-type red-type))))))))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term poly-stlc M #:i-th (pick-an-index 0.001)))
|
||||
|
|
@ -288,3 +291,21 @@
|
|||
(begin0
|
||||
(generate-term poly-stlc M #:i-th index)
|
||||
(set! index (add1 index))))))
|
||||
|
||||
(define fixed
|
||||
(term
|
||||
(;; 2
|
||||
(([cons @ int] 1) nil)
|
||||
|
||||
;; 3 & 10 [designed for 3]
|
||||
((λ (x int) [nil @ int]) 1)
|
||||
|
||||
;; 5, 6, 7, 8 & 9 [designed for 4]
|
||||
((λ (x int) x)
|
||||
(([cons @ int] 1) [nil @ int]))
|
||||
|
||||
;; 4
|
||||
([tl @ int]
|
||||
(([cons @ int] 1) [nil @ int]))
|
||||
|
||||
)))
|
||||
|
|
|
|||
|
|
@ -274,11 +274,14 @@
|
|||
(v? term)
|
||||
(let ([red-res (apply-reduction-relation red term)]
|
||||
[t-type (type-check term)])
|
||||
;; xxx should this also be t-type IMPLIES?
|
||||
(and
|
||||
(= (length red-res) 1)
|
||||
(or
|
||||
(equal? (car red-res) "error")
|
||||
(equal? t-type (type-check (car red-res))))))))
|
||||
(let ([red-t (car red-res)])
|
||||
(or
|
||||
(equal? red-t "error")
|
||||
(let ([red-type (type-check red-t)])
|
||||
(equal? t-type red-type))))))))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term poly-stlc M #:i-th (pick-an-index 0.001)))
|
||||
|
|
@ -289,3 +292,21 @@
|
|||
(begin0
|
||||
(generate-term poly-stlc M #:i-th index)
|
||||
(set! index (add1 index))))))
|
||||
|
||||
(define fixed
|
||||
(term
|
||||
(;; 2
|
||||
(([cons @ int] 1) nil)
|
||||
|
||||
;; 3 & 10 [designed for 3]
|
||||
((λ (x int) [nil @ int]) 1)
|
||||
|
||||
;; 5, 6, 7, 8 & 9 [designed for 4]
|
||||
((λ (x int) x)
|
||||
(([cons @ int] 1) [nil @ int]))
|
||||
|
||||
;; 4
|
||||
([tl @ int]
|
||||
(([cons @ int] 1) [nil @ int]))
|
||||
|
||||
)))
|
||||
|
|
|
|||
|
|
@ -274,11 +274,14 @@
|
|||
(v? term)
|
||||
(let ([red-res (apply-reduction-relation red term)]
|
||||
[t-type (type-check term)])
|
||||
;; xxx should this also be t-type IMPLIES?
|
||||
(and
|
||||
(= (length red-res) 1)
|
||||
(or
|
||||
(equal? (car red-res) "error")
|
||||
(equal? t-type (type-check (car red-res))))))))
|
||||
(let ([red-t (car red-res)])
|
||||
(or
|
||||
(equal? red-t "error")
|
||||
(let ([red-type (type-check red-t)])
|
||||
(equal? t-type red-type))))))))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term poly-stlc M #:i-th (pick-an-index 0.001)))
|
||||
|
|
@ -289,3 +292,21 @@
|
|||
(begin0
|
||||
(generate-term poly-stlc M #:i-th index)
|
||||
(set! index (add1 index))))))
|
||||
|
||||
(define fixed
|
||||
(term
|
||||
(;; 2
|
||||
(([cons @ int] 1) nil)
|
||||
|
||||
;; 3 & 10 [designed for 3]
|
||||
((λ (x int) [nil @ int]) 1)
|
||||
|
||||
;; 5, 6, 7, 8 & 9 [designed for 4]
|
||||
((λ (x int) x)
|
||||
(([cons @ int] 1) [nil @ int]))
|
||||
|
||||
;; 4
|
||||
([tl @ int]
|
||||
(([cons @ int] 1) [nil @ int]))
|
||||
|
||||
)))
|
||||
|
|
|
|||
|
|
@ -274,11 +274,14 @@
|
|||
(v? term)
|
||||
(let ([red-res (apply-reduction-relation red term)]
|
||||
[t-type (type-check term)])
|
||||
;; xxx should this also be t-type IMPLIES?
|
||||
(and
|
||||
(= (length red-res) 1)
|
||||
(or
|
||||
(equal? (car red-res) "error")
|
||||
(equal? t-type (type-check (car red-res))))))))
|
||||
(let ([red-t (car red-res)])
|
||||
(or
|
||||
(equal? red-t "error")
|
||||
(let ([red-type (type-check red-t)])
|
||||
(equal? t-type red-type))))))))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term poly-stlc M #:i-th (pick-an-index 0.001)))
|
||||
|
|
@ -289,3 +292,21 @@
|
|||
(begin0
|
||||
(generate-term poly-stlc M #:i-th index)
|
||||
(set! index (add1 index))))))
|
||||
|
||||
(define fixed
|
||||
(term
|
||||
(;; 2
|
||||
(([cons @ int] 1) nil)
|
||||
|
||||
;; 3 & 10 [designed for 3]
|
||||
((λ (x int) [nil @ int]) 1)
|
||||
|
||||
;; 5, 6, 7, 8 & 9 [designed for 4]
|
||||
((λ (x int) x)
|
||||
(([cons @ int] 1) [nil @ int]))
|
||||
|
||||
;; 4
|
||||
([tl @ int]
|
||||
(([cons @ int] 1) [nil @ int]))
|
||||
|
||||
)))
|
||||
|
|
|
|||
|
|
@ -37,9 +37,9 @@
|
|||
(define-judgment-form rbtrees
|
||||
#:mode (rbtree I O)
|
||||
[(rbtree E O)]
|
||||
[(rbtree (R (B t_l1 n_l t_l2)
|
||||
n
|
||||
(B t_r1 n_r t_r2))
|
||||
[(rbtree (R (B t_l1 n_l t_l2)
|
||||
n
|
||||
(B t_r1 n_r t_r2))
|
||||
n_bd)
|
||||
(rbtree (B t_l1 n_l t_l2) n_bd)
|
||||
(rbtree (B t_r1 n_r t_r2) n_bd)]
|
||||
|
|
@ -59,8 +59,8 @@
|
|||
#:mode (rbt I O O O)
|
||||
[(rbt (R E n E) n n O)]
|
||||
[(rbt (B E n E) n n (s O))]
|
||||
[(rbt (R (B t_l1 n_l t_l2)
|
||||
n
|
||||
[(rbt (R (B t_l1 n_l t_l2)
|
||||
n
|
||||
(B t_r1 n_r t_r2))
|
||||
n_1min n_2max n_bd)
|
||||
(rbt (B t_l1 n_l t_l2) n_1min n_1max n_bd)
|
||||
|
|
@ -128,7 +128,7 @@
|
|||
(s (num->n ,(sub1 (term number))))])
|
||||
|
||||
(define-metafunction rbtrees
|
||||
[(numt->t E)
|
||||
[(numt->t E)
|
||||
E]
|
||||
[(numt->t (c any_1 number any_2))
|
||||
(c (numt->t any_1) (num->n number) (numt->t any_2))])
|
||||
|
|
@ -179,35 +179,35 @@
|
|||
(for/list ([_ (in-range num)])
|
||||
(rand-rb-tree depth)))
|
||||
|
||||
(module+
|
||||
test
|
||||
(require rackunit)
|
||||
(check-true (judgment-holds
|
||||
(ordered?
|
||||
(B (R E (s O) E)
|
||||
(s (s (s O)))
|
||||
E)
|
||||
n_1 n_2)))
|
||||
(check-true (judgment-holds
|
||||
(rbtree (B (R E (s O) E)
|
||||
(s (s (s O)))
|
||||
E)
|
||||
n_1)))
|
||||
(check-true (judgment-holds
|
||||
(rbst (B (R E (s O) E)
|
||||
(s (s (s O)))
|
||||
E))))
|
||||
(check-true (judgment-holds
|
||||
(rbst (R (B E (s O) E)
|
||||
(s (s (s O)))
|
||||
(B E
|
||||
(s (s (s (s (s O)))))
|
||||
E)))))
|
||||
(check-false (judgment-holds
|
||||
(rbst (R (B E (s (s O)) E)
|
||||
(s O)
|
||||
(R E O E)))))
|
||||
)
|
||||
(module+
|
||||
test
|
||||
(require rackunit)
|
||||
(check-true (judgment-holds
|
||||
(ordered?
|
||||
(B (R E (s O) E)
|
||||
(s (s (s O)))
|
||||
E)
|
||||
n_1 n_2)))
|
||||
(check-true (judgment-holds
|
||||
(rbtree (B (R E (s O) E)
|
||||
(s (s (s O)))
|
||||
E)
|
||||
n_1)))
|
||||
(check-true (judgment-holds
|
||||
(rbst (B (R E (s O) E)
|
||||
(s (s (s O)))
|
||||
E))))
|
||||
(check-true (judgment-holds
|
||||
(rbst (R (B E (s O) E)
|
||||
(s (s (s O)))
|
||||
(B E
|
||||
(s (s (s (s (s O)))))
|
||||
E)))))
|
||||
(check-false (judgment-holds
|
||||
(rbst (R (B E (s (s O)) E)
|
||||
(s O)
|
||||
(R E O E)))))
|
||||
)
|
||||
|
||||
(define (ins-preserves-rb-tree t)
|
||||
(or (not (judgment-holds (rb-tree ,t)))
|
||||
|
|
@ -221,50 +221,50 @@
|
|||
(insert (num->n ,n) ,t))))])))
|
||||
|
||||
(module+
|
||||
test
|
||||
(define (check-rbsts n)
|
||||
(for ([_ (in-range n)])
|
||||
(match (generate-term rbtrees
|
||||
#:satisfying
|
||||
(rbst t)
|
||||
8)
|
||||
[#f (void)]
|
||||
[`(rbst ,t)
|
||||
(check-not-false (or (ins-preserves-rb-tree t)
|
||||
(printf "~s\n" t)))])))
|
||||
|
||||
(define (check-rbst/rb-tree tries)
|
||||
(for ([_ tries])
|
||||
(match (generate-term rbtrees
|
||||
#:satisfying
|
||||
(rbst t)
|
||||
8)
|
||||
[#f (void)]
|
||||
[`(rbst ,t)
|
||||
(define res
|
||||
(judgment-holds
|
||||
(rb-tree ,t)))
|
||||
(unless res (displayln t))
|
||||
(check-not-false res)]))
|
||||
(for ([_ tries])
|
||||
(match (generate-term rbtrees
|
||||
#:satisfying
|
||||
(rb-tree t)
|
||||
8)
|
||||
[#f (void)]
|
||||
[`(rb-tree ,t)
|
||||
(define res
|
||||
(judgment-holds
|
||||
(rb-tree ,t)))
|
||||
(unless res (displayln t))
|
||||
(check-not-false res)])))
|
||||
)
|
||||
test
|
||||
(define (check-rbsts n)
|
||||
(for ([_ (in-range n)])
|
||||
(match (generate-term rbtrees
|
||||
#:satisfying
|
||||
(rbst t)
|
||||
8)
|
||||
[#f (void)]
|
||||
[`(rbst ,t)
|
||||
(check-not-false (or (ins-preserves-rb-tree t)
|
||||
(printf "~s\n" t)))])))
|
||||
|
||||
(define (check-rbst/rb-tree tries)
|
||||
(for ([_ tries])
|
||||
(match (generate-term rbtrees
|
||||
#:satisfying
|
||||
(rbst t)
|
||||
8)
|
||||
[#f (void)]
|
||||
[`(rbst ,t)
|
||||
(define res
|
||||
(judgment-holds
|
||||
(rb-tree ,t)))
|
||||
(unless res (displayln t))
|
||||
(check-not-false res)]))
|
||||
(for ([_ tries])
|
||||
(match (generate-term rbtrees
|
||||
#:satisfying
|
||||
(rb-tree t)
|
||||
8)
|
||||
[#f (void)]
|
||||
[`(rb-tree ,t)
|
||||
(define res
|
||||
(judgment-holds
|
||||
(rb-tree ,t)))
|
||||
(unless res (displayln t))
|
||||
(check-not-false res)])))
|
||||
)
|
||||
|
||||
(define (generate-M-term)
|
||||
(generate-term rbtrees t 5))
|
||||
|
||||
(define (generate-typed-term)
|
||||
(match (generate-term rbtrees
|
||||
(match (generate-term rbtrees
|
||||
#:satisfying
|
||||
(rb-tree t)
|
||||
5)
|
||||
|
|
@ -276,10 +276,10 @@
|
|||
(judgment-holds (rb-tree ,t)))
|
||||
|
||||
(define (typed-generator)
|
||||
(let ([g (redex-generator rbtrees
|
||||
(let ([g (redex-generator rbtrees
|
||||
(rb-tree t)
|
||||
5)])
|
||||
(λ ()
|
||||
(λ ()
|
||||
(match (g)
|
||||
[`(rb-tree ,t)
|
||||
t]
|
||||
|
|
@ -298,3 +298,22 @@
|
|||
(begin0
|
||||
(generate-term rbtrees t #:i-th index)
|
||||
(set! index (add1 index))))))
|
||||
|
||||
(define fixed
|
||||
(term
|
||||
(;; 1 and 2
|
||||
(B (R E (num->n 1) E)
|
||||
(num->n 3)
|
||||
E)
|
||||
;; 3
|
||||
(B
|
||||
;;; size should be 1, but in 3 it's 0
|
||||
(B
|
||||
;; size is 0
|
||||
(R E (num->n 1) E)
|
||||
(num->n 2)
|
||||
;; size is 0
|
||||
(R E (num->n 3) E))
|
||||
(num->n 5)
|
||||
;; size is 0
|
||||
(R E (num->n 10) E)))))
|
||||
|
|
|
|||
|
|
@ -37,9 +37,9 @@
|
|||
(define-judgment-form rbtrees
|
||||
#:mode (rbtree I O)
|
||||
[(rbtree E O)]
|
||||
[(rbtree (R (B t_l1 n_l t_l2)
|
||||
n
|
||||
(B t_r1 n_r t_r2))
|
||||
[(rbtree (R (B t_l1 n_l t_l2)
|
||||
n
|
||||
(B t_r1 n_r t_r2))
|
||||
n_bd)
|
||||
(rbtree (B t_l1 n_l t_l2) n_bd)
|
||||
(rbtree (B t_r1 n_r t_r2) n_bd)]
|
||||
|
|
@ -59,8 +59,8 @@
|
|||
#:mode (rbt I O O O)
|
||||
[(rbt (R E n E) n n O)]
|
||||
[(rbt (B E n E) n n (s O))]
|
||||
[(rbt (R (B t_l1 n_l t_l2)
|
||||
n
|
||||
[(rbt (R (B t_l1 n_l t_l2)
|
||||
n
|
||||
(B t_r1 n_r t_r2))
|
||||
n_1min n_2max n_bd)
|
||||
(rbt (B t_l1 n_l t_l2) n_1min n_1max n_bd)
|
||||
|
|
@ -126,7 +126,7 @@
|
|||
(s (num->n ,(sub1 (term number))))])
|
||||
|
||||
(define-metafunction rbtrees
|
||||
[(numt->t E)
|
||||
[(numt->t E)
|
||||
E]
|
||||
[(numt->t (c any_1 number any_2))
|
||||
(c (numt->t any_1) (num->n number) (numt->t any_2))])
|
||||
|
|
@ -177,35 +177,35 @@
|
|||
(for/list ([_ (in-range num)])
|
||||
(rand-rb-tree depth)))
|
||||
|
||||
(module+
|
||||
test
|
||||
(require rackunit)
|
||||
(check-true (judgment-holds
|
||||
(ordered?
|
||||
(B (R E (s O) E)
|
||||
(s (s (s O)))
|
||||
E)
|
||||
n_1 n_2)))
|
||||
(check-true (judgment-holds
|
||||
(rbtree (B (R E (s O) E)
|
||||
(s (s (s O)))
|
||||
E)
|
||||
n_1)))
|
||||
(check-true (judgment-holds
|
||||
(rbst (B (R E (s O) E)
|
||||
(s (s (s O)))
|
||||
E))))
|
||||
(check-true (judgment-holds
|
||||
(rbst (R (B E (s O) E)
|
||||
(s (s (s O)))
|
||||
(B E
|
||||
(s (s (s (s (s O)))))
|
||||
E)))))
|
||||
(check-false (judgment-holds
|
||||
(rbst (R (B E (s (s O)) E)
|
||||
(s O)
|
||||
(R E O E)))))
|
||||
)
|
||||
(module+
|
||||
test
|
||||
(require rackunit)
|
||||
(check-true (judgment-holds
|
||||
(ordered?
|
||||
(B (R E (s O) E)
|
||||
(s (s (s O)))
|
||||
E)
|
||||
n_1 n_2)))
|
||||
(check-true (judgment-holds
|
||||
(rbtree (B (R E (s O) E)
|
||||
(s (s (s O)))
|
||||
E)
|
||||
n_1)))
|
||||
(check-true (judgment-holds
|
||||
(rbst (B (R E (s O) E)
|
||||
(s (s (s O)))
|
||||
E))))
|
||||
(check-true (judgment-holds
|
||||
(rbst (R (B E (s O) E)
|
||||
(s (s (s O)))
|
||||
(B E
|
||||
(s (s (s (s (s O)))))
|
||||
E)))))
|
||||
(check-false (judgment-holds
|
||||
(rbst (R (B E (s (s O)) E)
|
||||
(s O)
|
||||
(R E O E)))))
|
||||
)
|
||||
|
||||
(define (ins-preserves-rb-tree t)
|
||||
(or (not (judgment-holds (rb-tree ,t)))
|
||||
|
|
@ -219,50 +219,50 @@
|
|||
(insert (num->n ,n) ,t))))])))
|
||||
|
||||
(module+
|
||||
test
|
||||
(define (check-rbsts n)
|
||||
(for ([_ (in-range n)])
|
||||
(match (generate-term rbtrees
|
||||
#:satisfying
|
||||
(rbst t)
|
||||
8)
|
||||
[#f (void)]
|
||||
[`(rbst ,t)
|
||||
(check-not-false (or (ins-preserves-rb-tree t)
|
||||
(printf "~s\n" t)))])))
|
||||
|
||||
(define (check-rbst/rb-tree tries)
|
||||
(for ([_ tries])
|
||||
(match (generate-term rbtrees
|
||||
#:satisfying
|
||||
(rbst t)
|
||||
8)
|
||||
[#f (void)]
|
||||
[`(rbst ,t)
|
||||
(define res
|
||||
(judgment-holds
|
||||
(rb-tree ,t)))
|
||||
(unless res (displayln t))
|
||||
(check-not-false res)]))
|
||||
(for ([_ tries])
|
||||
(match (generate-term rbtrees
|
||||
#:satisfying
|
||||
(rb-tree t)
|
||||
8)
|
||||
[#f (void)]
|
||||
[`(rb-tree ,t)
|
||||
(define res
|
||||
(judgment-holds
|
||||
(rb-tree ,t)))
|
||||
(unless res (displayln t))
|
||||
(check-not-false res)])))
|
||||
)
|
||||
test
|
||||
(define (check-rbsts n)
|
||||
(for ([_ (in-range n)])
|
||||
(match (generate-term rbtrees
|
||||
#:satisfying
|
||||
(rbst t)
|
||||
8)
|
||||
[#f (void)]
|
||||
[`(rbst ,t)
|
||||
(check-not-false (or (ins-preserves-rb-tree t)
|
||||
(printf "~s\n" t)))])))
|
||||
|
||||
(define (check-rbst/rb-tree tries)
|
||||
(for ([_ tries])
|
||||
(match (generate-term rbtrees
|
||||
#:satisfying
|
||||
(rbst t)
|
||||
8)
|
||||
[#f (void)]
|
||||
[`(rbst ,t)
|
||||
(define res
|
||||
(judgment-holds
|
||||
(rb-tree ,t)))
|
||||
(unless res (displayln t))
|
||||
(check-not-false res)]))
|
||||
(for ([_ tries])
|
||||
(match (generate-term rbtrees
|
||||
#:satisfying
|
||||
(rb-tree t)
|
||||
8)
|
||||
[#f (void)]
|
||||
[`(rb-tree ,t)
|
||||
(define res
|
||||
(judgment-holds
|
||||
(rb-tree ,t)))
|
||||
(unless res (displayln t))
|
||||
(check-not-false res)])))
|
||||
)
|
||||
|
||||
(define (generate-M-term)
|
||||
(generate-term rbtrees t 5))
|
||||
|
||||
(define (generate-typed-term)
|
||||
(match (generate-term rbtrees
|
||||
(match (generate-term rbtrees
|
||||
#:satisfying
|
||||
(rb-tree t)
|
||||
5)
|
||||
|
|
@ -274,10 +274,10 @@
|
|||
(judgment-holds (rb-tree ,t)))
|
||||
|
||||
(define (typed-generator)
|
||||
(let ([g (redex-generator rbtrees
|
||||
(let ([g (redex-generator rbtrees
|
||||
(rb-tree t)
|
||||
5)])
|
||||
(λ ()
|
||||
(λ ()
|
||||
(match (g)
|
||||
[`(rb-tree ,t)
|
||||
t]
|
||||
|
|
@ -296,3 +296,22 @@
|
|||
(begin0
|
||||
(generate-term rbtrees t #:i-th index)
|
||||
(set! index (add1 index))))))
|
||||
|
||||
(define fixed
|
||||
(term
|
||||
(;; 1 and 2
|
||||
(B (R E (num->n 1) E)
|
||||
(num->n 3)
|
||||
E)
|
||||
;; 3
|
||||
(B
|
||||
;;; size should be 1, but in 3 it's 0
|
||||
(B
|
||||
;; size is 0
|
||||
(R E (num->n 1) E)
|
||||
(num->n 2)
|
||||
;; size is 0
|
||||
(R E (num->n 3) E))
|
||||
(num->n 5)
|
||||
;; size is 0
|
||||
(R E (num->n 10) E)))))
|
||||
|
|
|
|||
|
|
@ -37,9 +37,9 @@
|
|||
(define-judgment-form rbtrees
|
||||
#:mode (rbtree I O)
|
||||
[(rbtree E O)]
|
||||
[(rbtree (R (B t_l1 n_l t_l2)
|
||||
n
|
||||
(B t_r1 n_r t_r2))
|
||||
[(rbtree (R (B t_l1 n_l t_l2)
|
||||
n
|
||||
(B t_r1 n_r t_r2))
|
||||
n_bd)
|
||||
(rbtree (B t_l1 n_l t_l2) n_bd)
|
||||
(rbtree (B t_r1 n_r t_r2) n_bd)]
|
||||
|
|
@ -59,8 +59,8 @@
|
|||
#:mode (rbt I O O O)
|
||||
[(rbt (R E n E) n n O)]
|
||||
[(rbt (B E n E) n n (s O))]
|
||||
[(rbt (R (B t_l1 n_l t_l2)
|
||||
n
|
||||
[(rbt (R (B t_l1 n_l t_l2)
|
||||
n
|
||||
(B t_r1 n_r t_r2))
|
||||
n_1min n_2max n_bd)
|
||||
(rbt (B t_l1 n_l t_l2) n_1min n_1max n_bd)
|
||||
|
|
@ -128,7 +128,7 @@
|
|||
(s (num->n ,(sub1 (term number))))])
|
||||
|
||||
(define-metafunction rbtrees
|
||||
[(numt->t E)
|
||||
[(numt->t E)
|
||||
E]
|
||||
[(numt->t (c any_1 number any_2))
|
||||
(c (numt->t any_1) (num->n number) (numt->t any_2))])
|
||||
|
|
@ -179,35 +179,35 @@
|
|||
(for/list ([_ (in-range num)])
|
||||
(rand-rb-tree depth)))
|
||||
|
||||
(module+
|
||||
test
|
||||
(require rackunit)
|
||||
(check-true (judgment-holds
|
||||
(ordered?
|
||||
(B (R E (s O) E)
|
||||
(s (s (s O)))
|
||||
E)
|
||||
n_1 n_2)))
|
||||
(check-true (judgment-holds
|
||||
(rbtree (B (R E (s O) E)
|
||||
(s (s (s O)))
|
||||
E)
|
||||
n_1)))
|
||||
(check-true (judgment-holds
|
||||
(rbst (B (R E (s O) E)
|
||||
(s (s (s O)))
|
||||
E))))
|
||||
(check-true (judgment-holds
|
||||
(rbst (R (B E (s O) E)
|
||||
(s (s (s O)))
|
||||
(B E
|
||||
(s (s (s (s (s O)))))
|
||||
E)))))
|
||||
(check-false (judgment-holds
|
||||
(rbst (R (B E (s (s O)) E)
|
||||
(s O)
|
||||
(R E O E)))))
|
||||
)
|
||||
(module+
|
||||
test
|
||||
(require rackunit)
|
||||
(check-true (judgment-holds
|
||||
(ordered?
|
||||
(B (R E (s O) E)
|
||||
(s (s (s O)))
|
||||
E)
|
||||
n_1 n_2)))
|
||||
(check-true (judgment-holds
|
||||
(rbtree (B (R E (s O) E)
|
||||
(s (s (s O)))
|
||||
E)
|
||||
n_1)))
|
||||
(check-true (judgment-holds
|
||||
(rbst (B (R E (s O) E)
|
||||
(s (s (s O)))
|
||||
E))))
|
||||
(check-true (judgment-holds
|
||||
(rbst (R (B E (s O) E)
|
||||
(s (s (s O)))
|
||||
(B E
|
||||
(s (s (s (s (s O)))))
|
||||
E)))))
|
||||
(check-false (judgment-holds
|
||||
(rbst (R (B E (s (s O)) E)
|
||||
(s O)
|
||||
(R E O E)))))
|
||||
)
|
||||
|
||||
(define (ins-preserves-rb-tree t)
|
||||
(or (not (judgment-holds (rb-tree ,t)))
|
||||
|
|
@ -221,50 +221,50 @@
|
|||
(insert (num->n ,n) ,t))))])))
|
||||
|
||||
(module+
|
||||
test
|
||||
(define (check-rbsts n)
|
||||
(for ([_ (in-range n)])
|
||||
(match (generate-term rbtrees
|
||||
#:satisfying
|
||||
(rbst t)
|
||||
8)
|
||||
[#f (void)]
|
||||
[`(rbst ,t)
|
||||
(check-not-false (or (ins-preserves-rb-tree t)
|
||||
(printf "~s\n" t)))])))
|
||||
|
||||
(define (check-rbst/rb-tree tries)
|
||||
(for ([_ tries])
|
||||
(match (generate-term rbtrees
|
||||
#:satisfying
|
||||
(rbst t)
|
||||
8)
|
||||
[#f (void)]
|
||||
[`(rbst ,t)
|
||||
(define res
|
||||
(judgment-holds
|
||||
(rb-tree ,t)))
|
||||
(unless res (displayln t))
|
||||
(check-not-false res)]))
|
||||
(for ([_ tries])
|
||||
(match (generate-term rbtrees
|
||||
#:satisfying
|
||||
(rb-tree t)
|
||||
8)
|
||||
[#f (void)]
|
||||
[`(rb-tree ,t)
|
||||
(define res
|
||||
(judgment-holds
|
||||
(rb-tree ,t)))
|
||||
(unless res (displayln t))
|
||||
(check-not-false res)])))
|
||||
)
|
||||
test
|
||||
(define (check-rbsts n)
|
||||
(for ([_ (in-range n)])
|
||||
(match (generate-term rbtrees
|
||||
#:satisfying
|
||||
(rbst t)
|
||||
8)
|
||||
[#f (void)]
|
||||
[`(rbst ,t)
|
||||
(check-not-false (or (ins-preserves-rb-tree t)
|
||||
(printf "~s\n" t)))])))
|
||||
|
||||
(define (check-rbst/rb-tree tries)
|
||||
(for ([_ tries])
|
||||
(match (generate-term rbtrees
|
||||
#:satisfying
|
||||
(rbst t)
|
||||
8)
|
||||
[#f (void)]
|
||||
[`(rbst ,t)
|
||||
(define res
|
||||
(judgment-holds
|
||||
(rb-tree ,t)))
|
||||
(unless res (displayln t))
|
||||
(check-not-false res)]))
|
||||
(for ([_ tries])
|
||||
(match (generate-term rbtrees
|
||||
#:satisfying
|
||||
(rb-tree t)
|
||||
8)
|
||||
[#f (void)]
|
||||
[`(rb-tree ,t)
|
||||
(define res
|
||||
(judgment-holds
|
||||
(rb-tree ,t)))
|
||||
(unless res (displayln t))
|
||||
(check-not-false res)])))
|
||||
)
|
||||
|
||||
(define (generate-M-term)
|
||||
(generate-term rbtrees t 5))
|
||||
|
||||
(define (generate-typed-term)
|
||||
(match (generate-term rbtrees
|
||||
(match (generate-term rbtrees
|
||||
#:satisfying
|
||||
(rb-tree t)
|
||||
5)
|
||||
|
|
@ -276,10 +276,10 @@
|
|||
(judgment-holds (rb-tree ,t)))
|
||||
|
||||
(define (typed-generator)
|
||||
(let ([g (redex-generator rbtrees
|
||||
(let ([g (redex-generator rbtrees
|
||||
(rb-tree t)
|
||||
5)])
|
||||
(λ ()
|
||||
(λ ()
|
||||
(match (g)
|
||||
[`(rb-tree ,t)
|
||||
t]
|
||||
|
|
@ -298,3 +298,22 @@
|
|||
(begin0
|
||||
(generate-term rbtrees t #:i-th index)
|
||||
(set! index (add1 index))))))
|
||||
|
||||
(define fixed
|
||||
(term
|
||||
(;; 1 and 2
|
||||
(B (R E (num->n 1) E)
|
||||
(num->n 3)
|
||||
E)
|
||||
;; 3
|
||||
(B
|
||||
;;; size should be 1, but in 3 it's 0
|
||||
(B
|
||||
;; size is 0
|
||||
(R E (num->n 1) E)
|
||||
(num->n 2)
|
||||
;; size is 0
|
||||
(R E (num->n 3) E))
|
||||
(num->n 5)
|
||||
;; size is 0
|
||||
(R E (num->n 10) E)))))
|
||||
|
|
|
|||
|
|
@ -37,9 +37,9 @@
|
|||
(define-judgment-form rbtrees
|
||||
#:mode (rbtree I O)
|
||||
[(rbtree E O)]
|
||||
[(rbtree (R (B t_l1 n_l t_l2)
|
||||
n
|
||||
(B t_r1 n_r t_r2))
|
||||
[(rbtree (R (B t_l1 n_l t_l2)
|
||||
n
|
||||
(B t_r1 n_r t_r2))
|
||||
n_bd)
|
||||
(rbtree (B t_l1 n_l t_l2) n_bd)
|
||||
(rbtree (B t_r1 n_r t_r2) n_bd)]
|
||||
|
|
@ -59,8 +59,8 @@
|
|||
#:mode (rbt I O O O)
|
||||
[(rbt (R E n E) n n O)]
|
||||
[(rbt (B E n E) n n (s O))]
|
||||
[(rbt (R (B t_l1 n_l t_l2)
|
||||
n
|
||||
[(rbt (R (B t_l1 n_l t_l2)
|
||||
n
|
||||
(B t_r1 n_r t_r2))
|
||||
n_1min n_2max n_bd)
|
||||
(rbt (B t_l1 n_l t_l2) n_1min n_1max n_bd)
|
||||
|
|
@ -128,7 +128,7 @@
|
|||
(s (num->n ,(sub1 (term number))))])
|
||||
|
||||
(define-metafunction rbtrees
|
||||
[(numt->t E)
|
||||
[(numt->t E)
|
||||
E]
|
||||
[(numt->t (c any_1 number any_2))
|
||||
(c (numt->t any_1) (num->n number) (numt->t any_2))])
|
||||
|
|
@ -179,35 +179,35 @@
|
|||
(for/list ([_ (in-range num)])
|
||||
(rand-rb-tree depth)))
|
||||
|
||||
(module+
|
||||
test
|
||||
(require rackunit)
|
||||
(check-true (judgment-holds
|
||||
(ordered?
|
||||
(B (R E (s O) E)
|
||||
(s (s (s O)))
|
||||
E)
|
||||
n_1 n_2)))
|
||||
(check-true (judgment-holds
|
||||
(rbtree (B (R E (s O) E)
|
||||
(s (s (s O)))
|
||||
E)
|
||||
n_1)))
|
||||
(check-true (judgment-holds
|
||||
(rbst (B (R E (s O) E)
|
||||
(s (s (s O)))
|
||||
E))))
|
||||
(check-true (judgment-holds
|
||||
(rbst (R (B E (s O) E)
|
||||
(s (s (s O)))
|
||||
(B E
|
||||
(s (s (s (s (s O)))))
|
||||
E)))))
|
||||
(check-false (judgment-holds
|
||||
(rbst (R (B E (s (s O)) E)
|
||||
(s O)
|
||||
(R E O E)))))
|
||||
)
|
||||
(module+
|
||||
test
|
||||
(require rackunit)
|
||||
(check-true (judgment-holds
|
||||
(ordered?
|
||||
(B (R E (s O) E)
|
||||
(s (s (s O)))
|
||||
E)
|
||||
n_1 n_2)))
|
||||
(check-true (judgment-holds
|
||||
(rbtree (B (R E (s O) E)
|
||||
(s (s (s O)))
|
||||
E)
|
||||
n_1)))
|
||||
(check-true (judgment-holds
|
||||
(rbst (B (R E (s O) E)
|
||||
(s (s (s O)))
|
||||
E))))
|
||||
(check-true (judgment-holds
|
||||
(rbst (R (B E (s O) E)
|
||||
(s (s (s O)))
|
||||
(B E
|
||||
(s (s (s (s (s O)))))
|
||||
E)))))
|
||||
(check-false (judgment-holds
|
||||
(rbst (R (B E (s (s O)) E)
|
||||
(s O)
|
||||
(R E O E)))))
|
||||
)
|
||||
|
||||
(define (ins-preserves-rb-tree t)
|
||||
(or (not (judgment-holds (rb-tree ,t)))
|
||||
|
|
@ -221,50 +221,50 @@
|
|||
(insert (num->n ,n) ,t))))])))
|
||||
|
||||
(module+
|
||||
test
|
||||
(define (check-rbsts n)
|
||||
(for ([_ (in-range n)])
|
||||
(match (generate-term rbtrees
|
||||
#:satisfying
|
||||
(rbst t)
|
||||
8)
|
||||
[#f (void)]
|
||||
[`(rbst ,t)
|
||||
(check-not-false (or (ins-preserves-rb-tree t)
|
||||
(printf "~s\n" t)))])))
|
||||
|
||||
(define (check-rbst/rb-tree tries)
|
||||
(for ([_ tries])
|
||||
(match (generate-term rbtrees
|
||||
#:satisfying
|
||||
(rbst t)
|
||||
8)
|
||||
[#f (void)]
|
||||
[`(rbst ,t)
|
||||
(define res
|
||||
(judgment-holds
|
||||
(rb-tree ,t)))
|
||||
(unless res (displayln t))
|
||||
(check-not-false res)]))
|
||||
(for ([_ tries])
|
||||
(match (generate-term rbtrees
|
||||
#:satisfying
|
||||
(rb-tree t)
|
||||
8)
|
||||
[#f (void)]
|
||||
[`(rb-tree ,t)
|
||||
(define res
|
||||
(judgment-holds
|
||||
(rb-tree ,t)))
|
||||
(unless res (displayln t))
|
||||
(check-not-false res)])))
|
||||
)
|
||||
test
|
||||
(define (check-rbsts n)
|
||||
(for ([_ (in-range n)])
|
||||
(match (generate-term rbtrees
|
||||
#:satisfying
|
||||
(rbst t)
|
||||
8)
|
||||
[#f (void)]
|
||||
[`(rbst ,t)
|
||||
(check-not-false (or (ins-preserves-rb-tree t)
|
||||
(printf "~s\n" t)))])))
|
||||
|
||||
(define (check-rbst/rb-tree tries)
|
||||
(for ([_ tries])
|
||||
(match (generate-term rbtrees
|
||||
#:satisfying
|
||||
(rbst t)
|
||||
8)
|
||||
[#f (void)]
|
||||
[`(rbst ,t)
|
||||
(define res
|
||||
(judgment-holds
|
||||
(rb-tree ,t)))
|
||||
(unless res (displayln t))
|
||||
(check-not-false res)]))
|
||||
(for ([_ tries])
|
||||
(match (generate-term rbtrees
|
||||
#:satisfying
|
||||
(rb-tree t)
|
||||
8)
|
||||
[#f (void)]
|
||||
[`(rb-tree ,t)
|
||||
(define res
|
||||
(judgment-holds
|
||||
(rb-tree ,t)))
|
||||
(unless res (displayln t))
|
||||
(check-not-false res)])))
|
||||
)
|
||||
|
||||
(define (generate-M-term)
|
||||
(generate-term rbtrees t 5))
|
||||
|
||||
(define (generate-typed-term)
|
||||
(match (generate-term rbtrees
|
||||
(match (generate-term rbtrees
|
||||
#:satisfying
|
||||
(rb-tree t)
|
||||
5)
|
||||
|
|
@ -276,10 +276,10 @@
|
|||
(judgment-holds (rb-tree ,t)))
|
||||
|
||||
(define (typed-generator)
|
||||
(let ([g (redex-generator rbtrees
|
||||
(let ([g (redex-generator rbtrees
|
||||
(rb-tree t)
|
||||
5)])
|
||||
(λ ()
|
||||
(λ ()
|
||||
(match (g)
|
||||
[`(rb-tree ,t)
|
||||
t]
|
||||
|
|
@ -298,3 +298,22 @@
|
|||
(begin0
|
||||
(generate-term rbtrees t #:i-th index)
|
||||
(set! index (add1 index))))))
|
||||
|
||||
(define fixed
|
||||
(term
|
||||
(;; 1 and 2
|
||||
(B (R E (num->n 1) E)
|
||||
(num->n 3)
|
||||
E)
|
||||
;; 3
|
||||
(B
|
||||
;;; size should be 1, but in 3 it's 0
|
||||
(B
|
||||
;; size is 0
|
||||
(R E (num->n 1) E)
|
||||
(num->n 2)
|
||||
;; size is 0
|
||||
(R E (num->n 3) E))
|
||||
(num->n 5)
|
||||
;; size is 0
|
||||
(R E (num->n 10) E)))))
|
||||
|
|
|
|||
|
|
@ -33,7 +33,7 @@
|
|||
[("-f" "--file") fname "Run tests for a single file"
|
||||
(set! files (list fname))]
|
||||
#:multi
|
||||
[("-t" "--type") t "Generation type to run, one of: search, grammar, search-gen, search-gen-ref, search-gen-enum, search-gen-enum-ref, enum, ordered"
|
||||
[("-t" "--type") t "Generation type to run, one of: search, grammar, search-gen, search-gen-ref, search-gen-enum, search-gen-enum-ref, enum, ordered, fixed"
|
||||
(set! gen-types (cons (string->symbol t) gen-types))])
|
||||
|
||||
(define-runtime-path here ".")
|
||||
|
|
@ -67,33 +67,39 @@
|
|||
(set! worklist (cdr worklist))
|
||||
(semaphore-post work-sem)
|
||||
(define path (simplify-path (build-path here file)))
|
||||
(define output-name (string-append (first
|
||||
(regexp-split #rx"\\."
|
||||
(last (regexp-split #rx"/" file))))
|
||||
"-"
|
||||
(symbol->string type)
|
||||
"-results.rktd"))
|
||||
(define args (apply string-append
|
||||
(add-between (list (if verbose? "-v" "")
|
||||
(string-append "-m " (number->string minutes))
|
||||
(string-append "-o " output-name)
|
||||
(string-append "-t "
|
||||
(symbol->string type))
|
||||
(if (equal? type 'ordered) "-f" ""))
|
||||
" ")))
|
||||
(define command (apply string-append
|
||||
(add-between (list "racket" (path->string (build-path here "test-file.rkt"))
|
||||
args (path->string path)) " ")))
|
||||
(printf "running: ~s\n" command)
|
||||
(define output-name
|
||||
(string-append (first
|
||||
(regexp-split #rx"\\."
|
||||
(last (regexp-split #rx"/" file))))
|
||||
"-"
|
||||
(symbol->string type)
|
||||
"-results.rktd"))
|
||||
(define args
|
||||
(apply string-append
|
||||
(add-between (list (if verbose? "-v" "")
|
||||
(string-append "-m " (number->string minutes))
|
||||
(string-append "-o " output-name)
|
||||
(string-append "-t "
|
||||
(symbol->string type))
|
||||
(if (equal? type 'ordered) "-f" ""))
|
||||
" ")))
|
||||
(define command
|
||||
(apply string-append
|
||||
(add-between
|
||||
(list "racket" (path->string (build-path here "test-file.rkt"))
|
||||
args (path->string path)) " ")))
|
||||
(when verbose?
|
||||
(printf "running: ~s\n" command))
|
||||
(system command)
|
||||
(do-next)]))
|
||||
|
||||
(define (do-work)
|
||||
(printf "worklist:\n~a\n" (apply string-append
|
||||
(add-between (for/list ([w (in-list worklist)])
|
||||
(match-define (work f t) w)
|
||||
(string-append f ": " (symbol->string t)))
|
||||
", ")))
|
||||
(printf "worklist:\n~a\n"
|
||||
(apply string-append
|
||||
(add-between (for/list ([w (in-list worklist)])
|
||||
(match-define (work f t) w)
|
||||
(string-append f ": " (symbol->string t)))
|
||||
", ")))
|
||||
(for/list ([_ (in-range num-procs)])
|
||||
(thread do-next)))
|
||||
|
||||
|
|
@ -103,4 +109,4 @@
|
|||
(thread-wait t))
|
||||
|
||||
(printf "all tests finished\n")
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -269,11 +269,14 @@
|
|||
(v? term)
|
||||
(let ([red-res (apply-reduction-relation red term)]
|
||||
[t-type (type-check term)])
|
||||
;; xxx should this also be t-type IMPLIES?
|
||||
(and
|
||||
(= (length red-res) 1)
|
||||
(or
|
||||
(equal? (car red-res) "error")
|
||||
(equal? t-type (type-check (car red-res))))))))
|
||||
(let ([red-t (car red-res)])
|
||||
(or
|
||||
(equal? red-t "error")
|
||||
(let ([red-type (type-check red-t)])
|
||||
(equal? t-type red-type))))))))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term stlc M #:i-th (pick-an-index 0.0001)))
|
||||
|
|
@ -284,3 +287,36 @@
|
|||
(begin0
|
||||
(generate-term stlc M #:i-th index)
|
||||
(set! index (add1 index))))))
|
||||
|
||||
(define fixed
|
||||
(term
|
||||
(;; 1
|
||||
((λ (x int) x) 1)
|
||||
|
||||
;; 9
|
||||
((λ (x (list int)) (tl x)) ((cons 1) nil))
|
||||
|
||||
;; 2 -- xxx I don't think this is really an error because the (M
|
||||
;; N) case does everything that (c M) does since M can equal
|
||||
;; c. Otherwise the previous test case would work, because (tl x)
|
||||
;; would not be subst'd and it has no type
|
||||
|
||||
;; 3
|
||||
((λ (x int) ((λ (y int) y) x)) 1)
|
||||
|
||||
;; 4 -- xxx I don't think this is really an error because the
|
||||
;; normal λ rule always does renaming so this test below works
|
||||
;; fine and ends up with x1 in both places.
|
||||
|
||||
#;((λ (x int) ((λ (x (list int)) x) ((cons x) nil))) 1)
|
||||
|
||||
;; 5 & 6 --- xxx These diffs are bogus because they don't actually
|
||||
;; make a change to any of the program.
|
||||
|
||||
;; 7
|
||||
((λ (x int) (hd ((cons x) nil))) 1)
|
||||
|
||||
;; 8 -- xxx This isn't an error for the same reason 4 isn't.
|
||||
|
||||
)))
|
||||
|
||||
|
|
|
|||
|
|
@ -268,11 +268,14 @@
|
|||
(v? term)
|
||||
(let ([red-res (apply-reduction-relation red term)]
|
||||
[t-type (type-check term)])
|
||||
;; xxx should this also be t-type IMPLIES?
|
||||
(and
|
||||
(= (length red-res) 1)
|
||||
(or
|
||||
(equal? (car red-res) "error")
|
||||
(equal? t-type (type-check (car red-res))))))))
|
||||
(let ([red-t (car red-res)])
|
||||
(or
|
||||
(equal? red-t "error")
|
||||
(let ([red-type (type-check red-t)])
|
||||
(equal? t-type red-type))))))))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term stlc M #:i-th (pick-an-index 0.0001)))
|
||||
|
|
@ -283,3 +286,36 @@
|
|||
(begin0
|
||||
(generate-term stlc M #:i-th index)
|
||||
(set! index (add1 index))))))
|
||||
|
||||
(define fixed
|
||||
(term
|
||||
(;; 1
|
||||
((λ (x int) x) 1)
|
||||
|
||||
;; 9
|
||||
((λ (x (list int)) (tl x)) ((cons 1) nil))
|
||||
|
||||
;; 2 -- xxx I don't think this is really an error because the (M
|
||||
;; N) case does everything that (c M) does since M can equal
|
||||
;; c. Otherwise the previous test case would work, because (tl x)
|
||||
;; would not be subst'd and it has no type
|
||||
|
||||
;; 3
|
||||
((λ (x int) ((λ (y int) y) x)) 1)
|
||||
|
||||
;; 4 -- xxx I don't think this is really an error because the
|
||||
;; normal λ rule always does renaming so this test below works
|
||||
;; fine and ends up with x1 in both places.
|
||||
|
||||
#;((λ (x int) ((λ (x (list int)) x) ((cons x) nil))) 1)
|
||||
|
||||
;; 5 & 6 --- xxx These diffs are bogus because they don't actually
|
||||
;; make a change to any of the program.
|
||||
|
||||
;; 7
|
||||
((λ (x int) (hd ((cons x) nil))) 1)
|
||||
|
||||
;; 8 -- xxx This isn't an error for the same reason 4 isn't.
|
||||
|
||||
)))
|
||||
|
||||
|
|
|
|||
|
|
@ -269,11 +269,14 @@
|
|||
(v? term)
|
||||
(let ([red-res (apply-reduction-relation red term)]
|
||||
[t-type (type-check term)])
|
||||
;; xxx should this also be t-type IMPLIES?
|
||||
(and
|
||||
(= (length red-res) 1)
|
||||
(or
|
||||
(equal? (car red-res) "error")
|
||||
(equal? t-type (type-check (car red-res))))))))
|
||||
(let ([red-t (car red-res)])
|
||||
(or
|
||||
(equal? red-t "error")
|
||||
(let ([red-type (type-check red-t)])
|
||||
(equal? t-type red-type))))))))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term stlc M #:i-th (pick-an-index 0.0001)))
|
||||
|
|
@ -284,3 +287,36 @@
|
|||
(begin0
|
||||
(generate-term stlc M #:i-th index)
|
||||
(set! index (add1 index))))))
|
||||
|
||||
(define fixed
|
||||
(term
|
||||
(;; 1
|
||||
((λ (x int) x) 1)
|
||||
|
||||
;; 9
|
||||
((λ (x (list int)) (tl x)) ((cons 1) nil))
|
||||
|
||||
;; 2 -- xxx I don't think this is really an error because the (M
|
||||
;; N) case does everything that (c M) does since M can equal
|
||||
;; c. Otherwise the previous test case would work, because (tl x)
|
||||
;; would not be subst'd and it has no type
|
||||
|
||||
;; 3
|
||||
((λ (x int) ((λ (y int) y) x)) 1)
|
||||
|
||||
;; 4 -- xxx I don't think this is really an error because the
|
||||
;; normal λ rule always does renaming so this test below works
|
||||
;; fine and ends up with x1 in both places.
|
||||
|
||||
#;((λ (x int) ((λ (x (list int)) x) ((cons x) nil))) 1)
|
||||
|
||||
;; 5 & 6 --- xxx These diffs are bogus because they don't actually
|
||||
;; make a change to any of the program.
|
||||
|
||||
;; 7
|
||||
((λ (x int) (hd ((cons x) nil))) 1)
|
||||
|
||||
;; 8 -- xxx This isn't an error for the same reason 4 isn't.
|
||||
|
||||
)))
|
||||
|
||||
|
|
|
|||
|
|
@ -267,11 +267,14 @@
|
|||
(v? term)
|
||||
(let ([red-res (apply-reduction-relation red term)]
|
||||
[t-type (type-check term)])
|
||||
;; xxx should this also be t-type IMPLIES?
|
||||
(and
|
||||
(= (length red-res) 1)
|
||||
(or
|
||||
(equal? (car red-res) "error")
|
||||
(equal? t-type (type-check (car red-res))))))))
|
||||
(let ([red-t (car red-res)])
|
||||
(or
|
||||
(equal? red-t "error")
|
||||
(let ([red-type (type-check red-t)])
|
||||
(equal? t-type red-type))))))))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term stlc M #:i-th (pick-an-index 0.0001)))
|
||||
|
|
@ -282,3 +285,36 @@
|
|||
(begin0
|
||||
(generate-term stlc M #:i-th index)
|
||||
(set! index (add1 index))))))
|
||||
|
||||
(define fixed
|
||||
(term
|
||||
(;; 1
|
||||
((λ (x int) x) 1)
|
||||
|
||||
;; 9
|
||||
((λ (x (list int)) (tl x)) ((cons 1) nil))
|
||||
|
||||
;; 2 -- xxx I don't think this is really an error because the (M
|
||||
;; N) case does everything that (c M) does since M can equal
|
||||
;; c. Otherwise the previous test case would work, because (tl x)
|
||||
;; would not be subst'd and it has no type
|
||||
|
||||
;; 3
|
||||
((λ (x int) ((λ (y int) y) x)) 1)
|
||||
|
||||
;; 4 -- xxx I don't think this is really an error because the
|
||||
;; normal λ rule always does renaming so this test below works
|
||||
;; fine and ends up with x1 in both places.
|
||||
|
||||
#;((λ (x int) ((λ (x (list int)) x) ((cons x) nil))) 1)
|
||||
|
||||
;; 5 & 6 --- xxx These diffs are bogus because they don't actually
|
||||
;; make a change to any of the program.
|
||||
|
||||
;; 7
|
||||
((λ (x int) (hd ((cons x) nil))) 1)
|
||||
|
||||
;; 8 -- xxx This isn't an error for the same reason 4 isn't.
|
||||
|
||||
)))
|
||||
|
||||
|
|
|
|||
|
|
@ -269,11 +269,14 @@
|
|||
(v? term)
|
||||
(let ([red-res (apply-reduction-relation red term)]
|
||||
[t-type (type-check term)])
|
||||
;; xxx should this also be t-type IMPLIES?
|
||||
(and
|
||||
(= (length red-res) 1)
|
||||
(or
|
||||
(equal? (car red-res) "error")
|
||||
(equal? t-type (type-check (car red-res))))))))
|
||||
(let ([red-t (car red-res)])
|
||||
(or
|
||||
(equal? red-t "error")
|
||||
(let ([red-type (type-check red-t)])
|
||||
(equal? t-type red-type))))))))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term stlc M #:i-th (pick-an-index 0.0001)))
|
||||
|
|
@ -284,3 +287,36 @@
|
|||
(begin0
|
||||
(generate-term stlc M #:i-th index)
|
||||
(set! index (add1 index))))))
|
||||
|
||||
(define fixed
|
||||
(term
|
||||
(;; 1
|
||||
((λ (x int) x) 1)
|
||||
|
||||
;; 9
|
||||
((λ (x (list int)) (tl x)) ((cons 1) nil))
|
||||
|
||||
;; 2 -- xxx I don't think this is really an error because the (M
|
||||
;; N) case does everything that (c M) does since M can equal
|
||||
;; c. Otherwise the previous test case would work, because (tl x)
|
||||
;; would not be subst'd and it has no type
|
||||
|
||||
;; 3
|
||||
((λ (x int) ((λ (y int) y) x)) 1)
|
||||
|
||||
;; 4 -- xxx I don't think this is really an error because the
|
||||
;; normal λ rule always does renaming so this test below works
|
||||
;; fine and ends up with x1 in both places.
|
||||
|
||||
#;((λ (x int) ((λ (x (list int)) x) ((cons x) nil))) 1)
|
||||
|
||||
;; 5 & 6 --- xxx These diffs are bogus because they don't actually
|
||||
;; make a change to any of the program.
|
||||
|
||||
;; 7
|
||||
((λ (x int) (hd ((cons x) nil))) 1)
|
||||
|
||||
;; 8 -- xxx This isn't an error for the same reason 4 isn't.
|
||||
|
||||
)))
|
||||
|
||||
|
|
|
|||
|
|
@ -269,11 +269,14 @@
|
|||
(v? term)
|
||||
(let ([red-res (apply-reduction-relation red term)]
|
||||
[t-type (type-check term)])
|
||||
;; xxx should this also be t-type IMPLIES?
|
||||
(and
|
||||
(= (length red-res) 1)
|
||||
(or
|
||||
(equal? (car red-res) "error")
|
||||
(equal? t-type (type-check (car red-res))))))))
|
||||
(let ([red-t (car red-res)])
|
||||
(or
|
||||
(equal? red-t "error")
|
||||
(let ([red-type (type-check red-t)])
|
||||
(equal? t-type red-type))))))))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term stlc M #:i-th (pick-an-index 0.0001)))
|
||||
|
|
@ -284,3 +287,36 @@
|
|||
(begin0
|
||||
(generate-term stlc M #:i-th index)
|
||||
(set! index (add1 index))))))
|
||||
|
||||
(define fixed
|
||||
(term
|
||||
(;; 1
|
||||
((λ (x int) x) 1)
|
||||
|
||||
;; 9
|
||||
((λ (x (list int)) (tl x)) ((cons 1) nil))
|
||||
|
||||
;; 2 -- xxx I don't think this is really an error because the (M
|
||||
;; N) case does everything that (c M) does since M can equal
|
||||
;; c. Otherwise the previous test case would work, because (tl x)
|
||||
;; would not be subst'd and it has no type
|
||||
|
||||
;; 3
|
||||
((λ (x int) ((λ (y int) y) x)) 1)
|
||||
|
||||
;; 4 -- xxx I don't think this is really an error because the
|
||||
;; normal λ rule always does renaming so this test below works
|
||||
;; fine and ends up with x1 in both places.
|
||||
|
||||
#;((λ (x int) ((λ (x (list int)) x) ((cons x) nil))) 1)
|
||||
|
||||
;; 5 & 6 --- xxx These diffs are bogus because they don't actually
|
||||
;; make a change to any of the program.
|
||||
|
||||
;; 7
|
||||
((λ (x int) (hd ((cons x) nil))) 1)
|
||||
|
||||
;; 8 -- xxx This isn't an error for the same reason 4 isn't.
|
||||
|
||||
)))
|
||||
|
||||
|
|
|
|||
|
|
@ -269,11 +269,14 @@
|
|||
(v? term)
|
||||
(let ([red-res (apply-reduction-relation red term)]
|
||||
[t-type (type-check term)])
|
||||
;; xxx should this also be t-type IMPLIES?
|
||||
(and
|
||||
(= (length red-res) 1)
|
||||
(or
|
||||
(equal? (car red-res) "error")
|
||||
(equal? t-type (type-check (car red-res))))))))
|
||||
(let ([red-t (car red-res)])
|
||||
(or
|
||||
(equal? red-t "error")
|
||||
(let ([red-type (type-check red-t)])
|
||||
(equal? t-type red-type))))))))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term stlc M #:i-th (pick-an-index 0.0001)))
|
||||
|
|
@ -284,3 +287,36 @@
|
|||
(begin0
|
||||
(generate-term stlc M #:i-th index)
|
||||
(set! index (add1 index))))))
|
||||
|
||||
(define fixed
|
||||
(term
|
||||
(;; 1
|
||||
((λ (x int) x) 1)
|
||||
|
||||
;; 9
|
||||
((λ (x (list int)) (tl x)) ((cons 1) nil))
|
||||
|
||||
;; 2 -- xxx I don't think this is really an error because the (M
|
||||
;; N) case does everything that (c M) does since M can equal
|
||||
;; c. Otherwise the previous test case would work, because (tl x)
|
||||
;; would not be subst'd and it has no type
|
||||
|
||||
;; 3
|
||||
((λ (x int) ((λ (y int) y) x)) 1)
|
||||
|
||||
;; 4 -- xxx I don't think this is really an error because the
|
||||
;; normal λ rule always does renaming so this test below works
|
||||
;; fine and ends up with x1 in both places.
|
||||
|
||||
#;((λ (x int) ((λ (x (list int)) x) ((cons x) nil))) 1)
|
||||
|
||||
;; 5 & 6 --- xxx These diffs are bogus because they don't actually
|
||||
;; make a change to any of the program.
|
||||
|
||||
;; 7
|
||||
((λ (x int) (hd ((cons x) nil))) 1)
|
||||
|
||||
;; 8 -- xxx This isn't an error for the same reason 4 isn't.
|
||||
|
||||
)))
|
||||
|
||||
|
|
|
|||
|
|
@ -268,11 +268,14 @@
|
|||
(v? term)
|
||||
(let ([red-res (apply-reduction-relation red term)]
|
||||
[t-type (type-check term)])
|
||||
;; xxx should this also be t-type IMPLIES?
|
||||
(and
|
||||
(= (length red-res) 1)
|
||||
(or
|
||||
(equal? (car red-res) "error")
|
||||
(equal? t-type (type-check (car red-res))))))))
|
||||
(let ([red-t (car red-res)])
|
||||
(or
|
||||
(equal? red-t "error")
|
||||
(let ([red-type (type-check red-t)])
|
||||
(equal? t-type red-type))))))))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term stlc M #:i-th (pick-an-index 0.0001)))
|
||||
|
|
@ -283,3 +286,36 @@
|
|||
(begin0
|
||||
(generate-term stlc M #:i-th index)
|
||||
(set! index (add1 index))))))
|
||||
|
||||
(define fixed
|
||||
(term
|
||||
(;; 1
|
||||
((λ (x int) x) 1)
|
||||
|
||||
;; 9
|
||||
((λ (x (list int)) (tl x)) ((cons 1) nil))
|
||||
|
||||
;; 2 -- xxx I don't think this is really an error because the (M
|
||||
;; N) case does everything that (c M) does since M can equal
|
||||
;; c. Otherwise the previous test case would work, because (tl x)
|
||||
;; would not be subst'd and it has no type
|
||||
|
||||
;; 3
|
||||
((λ (x int) ((λ (y int) y) x)) 1)
|
||||
|
||||
;; 4 -- xxx I don't think this is really an error because the
|
||||
;; normal λ rule always does renaming so this test below works
|
||||
;; fine and ends up with x1 in both places.
|
||||
|
||||
#;((λ (x int) ((λ (x (list int)) x) ((cons x) nil))) 1)
|
||||
|
||||
;; 5 & 6 --- xxx These diffs are bogus because they don't actually
|
||||
;; make a change to any of the program.
|
||||
|
||||
;; 7
|
||||
((λ (x int) (hd ((cons x) nil))) 1)
|
||||
|
||||
;; 8 -- xxx This isn't an error for the same reason 4 isn't.
|
||||
|
||||
)))
|
||||
|
||||
|
|
|
|||
|
|
@ -269,11 +269,14 @@
|
|||
(v? term)
|
||||
(let ([red-res (apply-reduction-relation red term)]
|
||||
[t-type (type-check term)])
|
||||
;; xxx should this also be t-type IMPLIES?
|
||||
(and
|
||||
(= (length red-res) 1)
|
||||
(or
|
||||
(equal? (car red-res) "error")
|
||||
(equal? t-type (type-check (car red-res))))))))
|
||||
(let ([red-t (car red-res)])
|
||||
(or
|
||||
(equal? red-t "error")
|
||||
(let ([red-type (type-check red-t)])
|
||||
(equal? t-type red-type))))))))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term stlc M #:i-th (pick-an-index 0.0001)))
|
||||
|
|
@ -284,3 +287,36 @@
|
|||
(begin0
|
||||
(generate-term stlc M #:i-th index)
|
||||
(set! index (add1 index))))))
|
||||
|
||||
(define fixed
|
||||
(term
|
||||
(;; 1
|
||||
((λ (x int) x) 1)
|
||||
|
||||
;; 9
|
||||
((λ (x (list int)) (tl x)) ((cons 1) nil))
|
||||
|
||||
;; 2 -- xxx I don't think this is really an error because the (M
|
||||
;; N) case does everything that (c M) does since M can equal
|
||||
;; c. Otherwise the previous test case would work, because (tl x)
|
||||
;; would not be subst'd and it has no type
|
||||
|
||||
;; 3
|
||||
((λ (x int) ((λ (y int) y) x)) 1)
|
||||
|
||||
;; 4 -- xxx I don't think this is really an error because the
|
||||
;; normal λ rule always does renaming so this test below works
|
||||
;; fine and ends up with x1 in both places.
|
||||
|
||||
#;((λ (x int) ((λ (x (list int)) x) ((cons x) nil))) 1)
|
||||
|
||||
;; 5 & 6 --- xxx These diffs are bogus because they don't actually
|
||||
;; make a change to any of the program.
|
||||
|
||||
;; 7
|
||||
((λ (x int) (hd ((cons x) nil))) 1)
|
||||
|
||||
;; 8 -- xxx This isn't an error for the same reason 4 isn't.
|
||||
|
||||
)))
|
||||
|
||||
|
|
|
|||
|
|
@ -268,11 +268,14 @@
|
|||
(v? term)
|
||||
(let ([red-res (apply-reduction-relation red term)]
|
||||
[t-type (type-check term)])
|
||||
;; xxx should this also be t-type IMPLIES?
|
||||
(and
|
||||
(= (length red-res) 1)
|
||||
(or
|
||||
(equal? (car red-res) "error")
|
||||
(equal? t-type (type-check (car red-res))))))))
|
||||
(let ([red-t (car red-res)])
|
||||
(or
|
||||
(equal? red-t "error")
|
||||
(let ([red-type (type-check red-t)])
|
||||
(equal? t-type red-type))))))))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term stlc M #:i-th (pick-an-index 0.0001)))
|
||||
|
|
@ -283,3 +286,36 @@
|
|||
(begin0
|
||||
(generate-term stlc M #:i-th index)
|
||||
(set! index (add1 index))))))
|
||||
|
||||
(define fixed
|
||||
(term
|
||||
(;; 1
|
||||
((λ (x int) x) 1)
|
||||
|
||||
;; 9
|
||||
((λ (x (list int)) (tl x)) ((cons 1) nil))
|
||||
|
||||
;; 2 -- xxx I don't think this is really an error because the (M
|
||||
;; N) case does everything that (c M) does since M can equal
|
||||
;; c. Otherwise the previous test case would work, because (tl x)
|
||||
;; would not be subst'd and it has no type
|
||||
|
||||
;; 3
|
||||
((λ (x int) ((λ (y int) y) x)) 1)
|
||||
|
||||
;; 4 -- xxx I don't think this is really an error because the
|
||||
;; normal λ rule always does renaming so this test below works
|
||||
;; fine and ends up with x1 in both places.
|
||||
|
||||
#;((λ (x int) ((λ (x (list int)) x) ((cons x) nil))) 1)
|
||||
|
||||
;; 5 & 6 --- xxx These diffs are bogus because they don't actually
|
||||
;; make a change to any of the program.
|
||||
|
||||
;; 7
|
||||
((λ (x int) (hd ((cons x) nil))) 1)
|
||||
|
||||
;; 8 -- xxx This isn't an error for the same reason 4 isn't.
|
||||
|
||||
)))
|
||||
|
||||
|
|
|
|||
|
|
@ -244,6 +244,7 @@
|
|||
(v? term)
|
||||
(let ([red-res (apply-reduction-relation red term)]
|
||||
[t-type (type-check term)])
|
||||
;; xxx shouldn't this be t-type IMPLIES this?
|
||||
(and
|
||||
(= (length red-res) 1)
|
||||
(or
|
||||
|
|
@ -258,4 +259,20 @@
|
|||
(λ ()
|
||||
(begin0
|
||||
(generate-term stlc M #:i-th index)
|
||||
(set! index (add1 index))))))
|
||||
(set! index (add1 index))))))
|
||||
|
||||
(define fixed
|
||||
(term
|
||||
(;; 2
|
||||
((cons 1) 2)
|
||||
;; 3
|
||||
((λ (x int) (hd x))
|
||||
7)
|
||||
;; 10
|
||||
((λ (x (list int)) (hd x))
|
||||
7)
|
||||
;; 5, 6, 7, 8, 9
|
||||
((λ (x int) (hd x))
|
||||
((cons 1) nil))
|
||||
;; 4
|
||||
(hd ((cons ((cons 1) nil)) nil)))))
|
||||
|
|
|
|||
|
|
@ -244,6 +244,7 @@
|
|||
(v? term)
|
||||
(let ([red-res (apply-reduction-relation red term)]
|
||||
[t-type (type-check term)])
|
||||
;; xxx shouldn't this be t-type IMPLIES this?
|
||||
(and
|
||||
(= (length red-res) 1)
|
||||
(or
|
||||
|
|
@ -258,4 +259,20 @@
|
|||
(λ ()
|
||||
(begin0
|
||||
(generate-term stlc M #:i-th index)
|
||||
(set! index (add1 index))))))
|
||||
(set! index (add1 index))))))
|
||||
|
||||
(define fixed
|
||||
(term
|
||||
(;; 2
|
||||
((cons 1) 2)
|
||||
;; 3
|
||||
((λ (x int) (hd x))
|
||||
7)
|
||||
;; 10
|
||||
((λ (x (list int)) (hd x))
|
||||
7)
|
||||
;; 5, 6, 7, 8, 9
|
||||
((λ (x int) (hd x))
|
||||
((cons 1) nil))
|
||||
;; 4
|
||||
(hd ((cons ((cons 1) nil)) nil)))))
|
||||
|
|
|
|||
|
|
@ -245,6 +245,7 @@
|
|||
(v? term)
|
||||
(let ([red-res (apply-reduction-relation red term)]
|
||||
[t-type (type-check term)])
|
||||
;; xxx shouldn't this be t-type IMPLIES this?
|
||||
(and
|
||||
(= (length red-res) 1)
|
||||
(or
|
||||
|
|
@ -259,4 +260,20 @@
|
|||
(λ ()
|
||||
(begin0
|
||||
(generate-term stlc M #:i-th index)
|
||||
(set! index (add1 index))))))
|
||||
(set! index (add1 index))))))
|
||||
|
||||
(define fixed
|
||||
(term
|
||||
(;; 2
|
||||
((cons 1) 2)
|
||||
;; 3
|
||||
((λ (x int) (hd x))
|
||||
7)
|
||||
;; 10
|
||||
((λ (x (list int)) (hd x))
|
||||
7)
|
||||
;; 5, 6, 7, 8, 9
|
||||
((λ (x int) (hd x))
|
||||
((cons 1) nil))
|
||||
;; 4
|
||||
(hd ((cons ((cons 1) nil)) nil)))))
|
||||
|
|
|
|||
|
|
@ -245,6 +245,7 @@
|
|||
(v? term)
|
||||
(let ([red-res (apply-reduction-relation red term)]
|
||||
[t-type (type-check term)])
|
||||
;; xxx shouldn't this be t-type IMPLIES this?
|
||||
(and
|
||||
(= (length red-res) 1)
|
||||
(or
|
||||
|
|
@ -259,4 +260,20 @@
|
|||
(λ ()
|
||||
(begin0
|
||||
(generate-term stlc M #:i-th index)
|
||||
(set! index (add1 index))))))
|
||||
(set! index (add1 index))))))
|
||||
|
||||
(define fixed
|
||||
(term
|
||||
(;; 2
|
||||
((cons 1) 2)
|
||||
;; 3
|
||||
((λ (x int) (hd x))
|
||||
7)
|
||||
;; 10
|
||||
((λ (x (list int)) (hd x))
|
||||
7)
|
||||
;; 5, 6, 7, 8, 9
|
||||
((λ (x int) (hd x))
|
||||
((cons 1) nil))
|
||||
;; 4
|
||||
(hd ((cons ((cons 1) nil)) nil)))))
|
||||
|
|
|
|||
|
|
@ -244,6 +244,7 @@
|
|||
(v? term)
|
||||
(let ([red-res (apply-reduction-relation red term)]
|
||||
[t-type (type-check term)])
|
||||
;; xxx shouldn't this be t-type IMPLIES this?
|
||||
(and
|
||||
(= (length red-res) 1)
|
||||
(or
|
||||
|
|
@ -258,4 +259,20 @@
|
|||
(λ ()
|
||||
(begin0
|
||||
(generate-term stlc M #:i-th index)
|
||||
(set! index (add1 index))))))
|
||||
(set! index (add1 index))))))
|
||||
|
||||
(define fixed
|
||||
(term
|
||||
(;; 2
|
||||
((cons 1) 2)
|
||||
;; 3
|
||||
((λ (x int) (hd x))
|
||||
7)
|
||||
;; 10
|
||||
((λ (x (list int)) (hd x))
|
||||
7)
|
||||
;; 5, 6, 7, 8, 9
|
||||
((λ (x int) (hd x))
|
||||
((cons 1) nil))
|
||||
;; 4
|
||||
(hd ((cons ((cons 1) nil)) nil)))))
|
||||
|
|
|
|||
|
|
@ -244,6 +244,7 @@
|
|||
(v? term)
|
||||
(let ([red-res (apply-reduction-relation red term)]
|
||||
[t-type (type-check term)])
|
||||
;; xxx shouldn't this be t-type IMPLIES this?
|
||||
(and
|
||||
(= (length red-res) 1)
|
||||
(or
|
||||
|
|
@ -258,4 +259,20 @@
|
|||
(λ ()
|
||||
(begin0
|
||||
(generate-term stlc M #:i-th index)
|
||||
(set! index (add1 index))))))
|
||||
(set! index (add1 index))))))
|
||||
|
||||
(define fixed
|
||||
(term
|
||||
(;; 2
|
||||
((cons 1) 2)
|
||||
;; 3
|
||||
((λ (x int) (hd x))
|
||||
7)
|
||||
;; 10
|
||||
((λ (x (list int)) (hd x))
|
||||
7)
|
||||
;; 5, 6, 7, 8, 9
|
||||
((λ (x int) (hd x))
|
||||
((cons 1) nil))
|
||||
;; 4
|
||||
(hd ((cons ((cons 1) nil)) nil)))))
|
||||
|
|
|
|||
|
|
@ -243,6 +243,7 @@
|
|||
(v? term)
|
||||
(let ([red-res (apply-reduction-relation red term)]
|
||||
[t-type (type-check term)])
|
||||
;; xxx shouldn't this be t-type IMPLIES this?
|
||||
(and
|
||||
(= (length red-res) 1)
|
||||
(or
|
||||
|
|
@ -257,4 +258,20 @@
|
|||
(λ ()
|
||||
(begin0
|
||||
(generate-term stlc M #:i-th index)
|
||||
(set! index (add1 index))))))
|
||||
(set! index (add1 index))))))
|
||||
|
||||
(define fixed
|
||||
(term
|
||||
(;; 2
|
||||
((cons 1) 2)
|
||||
;; 3
|
||||
((λ (x int) (hd x))
|
||||
7)
|
||||
;; 10
|
||||
((λ (x (list int)) (hd x))
|
||||
7)
|
||||
;; 5, 6, 7, 8, 9
|
||||
((λ (x int) (hd x))
|
||||
((cons 1) nil))
|
||||
;; 4
|
||||
(hd ((cons ((cons 1) nil)) nil)))))
|
||||
|
|
|
|||
|
|
@ -244,6 +244,7 @@
|
|||
(v? term)
|
||||
(let ([red-res (apply-reduction-relation red term)]
|
||||
[t-type (type-check term)])
|
||||
;; xxx shouldn't this be t-type IMPLIES this?
|
||||
(and
|
||||
(= (length red-res) 1)
|
||||
(or
|
||||
|
|
@ -258,4 +259,20 @@
|
|||
(λ ()
|
||||
(begin0
|
||||
(generate-term stlc M #:i-th index)
|
||||
(set! index (add1 index))))))
|
||||
(set! index (add1 index))))))
|
||||
|
||||
(define fixed
|
||||
(term
|
||||
(;; 2
|
||||
((cons 1) 2)
|
||||
;; 3
|
||||
((λ (x int) (hd x))
|
||||
7)
|
||||
;; 10
|
||||
((λ (x (list int)) (hd x))
|
||||
7)
|
||||
;; 5, 6, 7, 8, 9
|
||||
((λ (x int) (hd x))
|
||||
((cons 1) nil))
|
||||
;; 4
|
||||
(hd ((cons ((cons 1) nil)) nil)))))
|
||||
|
|
|
|||
|
|
@ -244,6 +244,7 @@
|
|||
(v? term)
|
||||
(let ([red-res (apply-reduction-relation red term)]
|
||||
[t-type (type-check term)])
|
||||
;; xxx shouldn't this be t-type IMPLIES this?
|
||||
(and
|
||||
(= (length red-res) 1)
|
||||
(or
|
||||
|
|
@ -258,4 +259,20 @@
|
|||
(λ ()
|
||||
(begin0
|
||||
(generate-term stlc M #:i-th index)
|
||||
(set! index (add1 index))))))
|
||||
(set! index (add1 index))))))
|
||||
|
||||
(define fixed
|
||||
(term
|
||||
(;; 2
|
||||
((cons 1) 2)
|
||||
;; 3
|
||||
((λ (x int) (hd x))
|
||||
7)
|
||||
;; 10
|
||||
((λ (x (list int)) (hd x))
|
||||
7)
|
||||
;; 5, 6, 7, 8, 9
|
||||
((λ (x int) (hd x))
|
||||
((cons 1) nil))
|
||||
;; 4
|
||||
(hd ((cons ((cons 1) nil)) nil)))))
|
||||
|
|
|
|||
|
|
@ -245,6 +245,7 @@
|
|||
(v? term)
|
||||
(let ([red-res (apply-reduction-relation red term)]
|
||||
[t-type (type-check term)])
|
||||
;; xxx shouldn't this be t-type IMPLIES this?
|
||||
(and
|
||||
(= (length red-res) 1)
|
||||
(or
|
||||
|
|
@ -259,4 +260,20 @@
|
|||
(λ ()
|
||||
(begin0
|
||||
(generate-term stlc M #:i-th index)
|
||||
(set! index (add1 index))))))
|
||||
(set! index (add1 index))))))
|
||||
|
||||
(define fixed
|
||||
(term
|
||||
(;; 2
|
||||
((cons 1) 2)
|
||||
;; 3
|
||||
((λ (x int) (hd x))
|
||||
7)
|
||||
;; 10
|
||||
((λ (x (list int)) (hd x))
|
||||
7)
|
||||
;; 5, 6, 7, 8, 9
|
||||
((λ (x int) (hd x))
|
||||
((cons 1) nil))
|
||||
;; 4
|
||||
(hd ((cons ((cons 1) nil)) nil)))))
|
||||
|
|
|
|||
|
|
@ -18,7 +18,7 @@
|
|||
|
||||
(define all-types '(search grammar search-gen search-gen-ref
|
||||
search-gen-enum search-gen-enum-ref
|
||||
enum ordered))
|
||||
enum ordered fixed))
|
||||
(define types '())
|
||||
|
||||
(define (set-type! arg)
|
||||
|
|
@ -40,7 +40,7 @@
|
|||
[("-f" "--first-only") "Find the first counterexample only"
|
||||
(set! first-only #t)]
|
||||
#:multi
|
||||
[("-t" "--type") t "Generation type to run, one of: search, grammar, search-gen, search-gen-ref, search-gen-enum, search-gen-enum-ref, enum, ordered"
|
||||
[("-t" "--type") t "Generation type to run, one of: search, grammar, search-gen, search-gen-ref, search-gen-enum, search-gen-enum-ref, enum, ordered, fixed"
|
||||
(set-type! t)]
|
||||
#:args filenames
|
||||
(match filenames
|
||||
|
|
@ -174,6 +174,7 @@
|
|||
(define typed-generator (dynamic-require fpath 'typed-generator))
|
||||
(define gen-enum (dynamic-require fpath 'generate-enum-term))
|
||||
(define ordered-generator (dynamic-require fpath 'ordered-enum-generator))
|
||||
(define fixed (dynamic-require fpath 'fixed))
|
||||
(define err (dynamic-require fpath 'the-error))
|
||||
(printf "\n-------------------------------------------------------------------\n")
|
||||
(printf "~a has the error: ~a\n\n" fpath err)
|
||||
|
|
@ -185,6 +186,13 @@
|
|||
(and (tc t)
|
||||
t)))
|
||||
(cond
|
||||
[(equal? gen-type 'fixed)
|
||||
(define some-failed?
|
||||
(for/or ([t (in-list fixed)])
|
||||
(define ok? (check t))
|
||||
(not ok?)))
|
||||
(unless some-failed?
|
||||
(error 'fixed "Expected some term to fail, but didn't find one in ~a" fixed))]
|
||||
[(equal? gen-type 'grammar)
|
||||
(run/spawn-generations fpath verbose? no-errs? (λ () (gen-and-type gen-term))
|
||||
check seconds gen-type)]
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user