diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/.gitignore b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/.gitignore new file mode 100644 index 0000000000..1aa2c6f859 --- /dev/null +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/.gitignore @@ -0,0 +1,2 @@ +*.orig +/*.rktd diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/delim-cont-1.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/delim-cont-1.rkt index d05527ef2f..d57f048c93 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/delim-cont-1.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/delim-cont-1.rkt @@ -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) + ))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/delim-cont-2.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/delim-cont-2.rkt index 4ddcf329ab..3a9177688e 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/delim-cont-2.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/delim-cont-2.rkt @@ -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) + ))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/delim-cont-3.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/delim-cont-3.rkt index 521af9cd40..7d8c8a67f7 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/delim-cont-3.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/delim-cont-3.rkt @@ -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) + ))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/delim-cont-base.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/delim-cont-base.rkt index 93a8f478a4..65794d72d6 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/delim-cont-base.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/delim-cont-base.rkt @@ -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) + ))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/list-machine-1.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/list-machine-1.rkt index cb433e9deb..252b854477 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/list-machine-1.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/list-machine-1.rkt @@ -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))))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/list-machine-2.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/list-machine-2.rkt index 45e4dd8d78..30ab220074 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/list-machine-2.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/list-machine-2.rkt @@ -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))))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/list-machine-3.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/list-machine-3.rkt index dc3f39aa62..cb5dd99ff4 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/list-machine-3.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/list-machine-3.rkt @@ -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))))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/list-machine-base.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/list-machine-base.rkt index 52e1397880..f1d8221bc3 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/list-machine-base.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/list-machine-base.rkt @@ -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))))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-10.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-10.rkt index f7c15ddcc9..572ed74d8c 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-10.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-10.rkt @@ -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])) + + ))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-2.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-2.rkt index eac830027e..11818409ed 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-2.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-2.rkt @@ -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])) + + ))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-3.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-3.rkt index ac66e902e2..8effebdef4 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-3.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-3.rkt @@ -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])) + + ))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-4.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-4.rkt index 4ed2a404f0..2ef34a53e4 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-4.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-4.rkt @@ -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])) + + ))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-5.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-5.rkt index b728025588..e6d7f0ccc5 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-5.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-5.rkt @@ -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])) + + ))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-6.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-6.rkt index 63eeecc84a..95105eb362 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-6.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-6.rkt @@ -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])) + + ))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-7.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-7.rkt index 8549119199..b581320dfd 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-7.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-7.rkt @@ -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])) + + ))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-8.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-8.rkt index 2dccacbe64..f84e98dd99 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-8.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-8.rkt @@ -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])) + + ))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-9.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-9.rkt index b0aaea1db2..b554f7e786 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-9.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-9.rkt @@ -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])) + + ))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-base.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-base.rkt index 0e091a778c..be6cf0dcc2 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-base.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-base.rkt @@ -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])) + + ))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/rbtrees-1.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/rbtrees-1.rkt index 509c927df3..63f6ffc968 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/rbtrees-1.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/rbtrees-1.rkt @@ -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))))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/rbtrees-2.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/rbtrees-2.rkt index b9b81c9009..2f119b6a2b 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/rbtrees-2.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/rbtrees-2.rkt @@ -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))))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/rbtrees-3.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/rbtrees-3.rkt index 8ed6275477..80c9a7fe1e 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/rbtrees-3.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/rbtrees-3.rkt @@ -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))))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/rbtrees-base.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/rbtrees-base.rkt index dd80dd872b..9a443f1884 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/rbtrees-base.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/rbtrees-base.rkt @@ -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))))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/run-muts.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/run-muts.rkt index ebc7f189d1..42054408fa 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/run-muts.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/run-muts.rkt @@ -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") - \ No newline at end of file + diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-1.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-1.rkt index 24d40c2615..0fc29e5a04 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-1.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-1.rkt @@ -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. + + ))) + diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-2.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-2.rkt index ef954c1879..d3301d3dff 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-2.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-2.rkt @@ -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. + + ))) + diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-3.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-3.rkt index 4b0f552ceb..bbcc3211fe 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-3.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-3.rkt @@ -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. + + ))) + diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-4.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-4.rkt index da48df93a6..a6b02af375 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-4.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-4.rkt @@ -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. + + ))) + diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-5.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-5.rkt index b29f14f942..5ae59042a2 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-5.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-5.rkt @@ -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. + + ))) + diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-6.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-6.rkt index 5f6024d52a..08be36d3f4 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-6.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-6.rkt @@ -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. + + ))) + diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-7.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-7.rkt index ee6a640d39..b2eeb91d89 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-7.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-7.rkt @@ -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. + + ))) + diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-8.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-8.rkt index 4e79d0f34f..b4522ee5ef 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-8.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-8.rkt @@ -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. + + ))) + diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-9.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-9.rkt index b0e80cc09c..4b34887a69 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-9.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-9.rkt @@ -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. + + ))) + diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-base.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-base.rkt index 6809f135ba..e8744360b7 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-base.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-base.rkt @@ -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. + + ))) + diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-10.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-10.rkt index 29b914580d..c940da175e 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-10.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-10.rkt @@ -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)))))) \ No newline at end of file + (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))))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-2.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-2.rkt index 78a513eccd..13f0e6afa4 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-2.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-2.rkt @@ -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)))))) \ No newline at end of file + (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))))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-3.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-3.rkt index eeaba61278..661e9b0b1f 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-3.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-3.rkt @@ -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)))))) \ No newline at end of file + (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))))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-4.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-4.rkt index 40d827796f..dc10d2e32a 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-4.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-4.rkt @@ -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)))))) \ No newline at end of file + (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))))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-5.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-5.rkt index 396c7b6016..ba02a3c960 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-5.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-5.rkt @@ -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)))))) \ No newline at end of file + (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))))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-6.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-6.rkt index 7a2d22b3a0..ca6e4d85c4 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-6.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-6.rkt @@ -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)))))) \ No newline at end of file + (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))))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-7.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-7.rkt index 425af3b610..9bbf08d565 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-7.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-7.rkt @@ -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)))))) \ No newline at end of file + (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))))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-8.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-8.rkt index 106aa9f123..ee843474c0 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-8.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-8.rkt @@ -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)))))) \ No newline at end of file + (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))))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-9.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-9.rkt index 976d04494a..69a31f0014 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-9.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-9.rkt @@ -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)))))) \ No newline at end of file + (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))))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-base.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-base.rkt index 5084abe4b6..d790961584 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-base.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-base.rkt @@ -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)))))) \ No newline at end of file + (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))))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/test-file.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/test-file.rkt index 5fd27fe5bf..920f33b572 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/test-file.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/test-file.rkt @@ -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)]