diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/10.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/10.diff index e86376aec3..23bcc13828 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/10.diff +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/10.diff @@ -2,17 +2,9 @@ < (define the-error "no error") --- > (define the-error "app rule the range of the function is matched to the argument") -8d7 -< racket/contract -9a9 -> racket/contract 58c58 < (typeof Γ M_2 σ) --- > (typeof Γ M_2 σ_2) 232d231 < -249c248 -< (= (length red-res) 1) ---- -> (= (length red-res) 1) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/2.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/2.diff index 0f1cb447ce..d024180321 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/2.diff +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/2.diff @@ -7,7 +7,3 @@ < ((cons v) v)) --- > (cons v)) -249c248 -< (= (length red-res) 1) ---- -> (= (length red-res) 1) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/3.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/3.diff index f95109aa74..1932a76597 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/3.diff +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/3.diff @@ -2,15 +2,7 @@ < (define the-error "no error") --- > (define the-error "the order of the types in the function position of application has been swapped") -8d7 -< racket/contract -9a9 -> racket/contract 57c57 < [(typeof Γ M (σ → σ_2)) --- > [(typeof Γ M (σ_2 → σ)) -249c249 -< (= (length red-res) 1) ---- -> (= (length red-res) 1) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/4.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/4.diff index 3f471d9554..1cebcca1f5 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/4.diff +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/4.diff @@ -2,15 +2,7 @@ < (define the-error "no error") --- > (define the-error "the type of cons is incorrect") -8d7 -< racket/contract -9a9 -> racket/contract 67c67 < (int → ((list int) → (list int)))] --- > (int → ((list int) → int))] -249c249 -< (= (length red-res) 1) ---- -> (= (length red-res) 1) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/5.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/5.diff index 8d7df681bf..dd35b1299c 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/5.diff +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/5.diff @@ -2,17 +2,9 @@ < (define the-error "no error") --- > (define the-error "the tail reduction returns the wrong value") -8d7 -< racket/contract -9a9 -> racket/contract 92c92 < (in-hole E v_2) --- > (in-hole E v_1) 232d231 < -249c248 -< (= (length red-res) 1) ---- -> (= (length red-res) 1) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/6.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/6.diff index cb47557f2a..c978fe3fba 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/6.diff +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/6.diff @@ -2,17 +2,9 @@ < (define the-error "no error") --- > (define the-error "hd reduction acts on partially applied cons") -8d7 -< racket/contract -9a9 -> racket/contract 88c88 < (--> (in-hole E (hd ((cons v_1) v_2))) --- > (--> (in-hole E (hd (cons v_1))) 232d231 < -249c248 -< (= (length red-res) 1) ---- -> (= (length red-res) 1) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/7.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/7.diff index 56b9367f2f..5df0c31c62 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/7.diff +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/7.diff @@ -2,10 +2,6 @@ < (define the-error "no error") --- > (define the-error "evaluation isn't allowed on the rhs of applications") -8d7 -< racket/contract -9a9 -> racket/contract 36,37c36 < (E M) < (v E))) @@ -13,7 +9,3 @@ > (E M))) 232d230 < -249c247 -< (= (length red-res) 1) ---- -> (= (length red-res) 1) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/8.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/8.diff index f92bbbd4b4..d18e4f37b9 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/8.diff +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/8.diff @@ -2,17 +2,9 @@ < (define the-error "no error") --- > (define the-error "lookup always returns int") -8d7 -< racket/contract -9a9 -> racket/contract 76c76 < σ] --- > int] 232d231 < -249c248 -< (= (length red-res) 1) ---- -> (= (length red-res) 1) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/9.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/9.diff index 691e083eeb..99aaad3984 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/9.diff +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/9.diff @@ -2,17 +2,9 @@ < (define the-error "no error") --- > (define the-error "variables aren't required to match in lookup") -8d7 -< racket/contract -9a9 -> racket/contract 75c75 < [(lookup (x σ Γ) x) --- > [(lookup (x σ Γ) x_2) 232d231 < -249c248 -< (= (length red-res) 1) ---- -> (= (length red-res) 1) 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 c940da175e..6194c5ae97 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 @@ -264,15 +264,21 @@ (define fixed (term (;; 2 - ((cons 1) 2) + ((cons 1) nil) ;; 3 - ((λ (x int) (hd x)) + ((λ (x (list int)) 1) 7) + ;; 4 (if we hadn't changed number->v in cons) + (cons ((cons 0) nil)) + ;; 5 + (tl ((cons 1) nil)) + ;; 6 + (hd ((cons 1) nil)) + ;; 7 + ((λ (x int) x) (hd ((cons 1) nil))) + ;; 8 + ((λ (x (list int)) (cons x)) nil) + ;; 9 + ((λ (x int) (λ (y (list int)) x)) 1) ;; 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))))) + (hd 0)))) 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 13f0e6afa4..b48aa96393 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 @@ -5,8 +5,8 @@ (require redex/reduction-semantics (only-in redex/private/generate-term pick-an-index) racket/list - racket/contract racket/match + racket/contract "tut-subst.rkt") (provide (all-defined-out)) @@ -264,15 +264,21 @@ (define fixed (term (;; 2 - ((cons 1) 2) + ((cons 1) nil) ;; 3 - ((λ (x int) (hd x)) + ((λ (x (list int)) 1) 7) + ;; 4 (if we hadn't changed number->v in cons) + (cons ((cons 0) nil)) + ;; 5 + (tl ((cons 1) nil)) + ;; 6 + (hd ((cons 1) nil)) + ;; 7 + ((λ (x int) x) (hd ((cons 1) nil))) + ;; 8 + ((λ (x (list int)) (cons x)) nil) + ;; 9 + ((λ (x int) (λ (y (list int)) x)) 1) ;; 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))))) + (hd 0)))) 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 661e9b0b1f..5615fa769f 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 @@ -265,15 +265,21 @@ (define fixed (term (;; 2 - ((cons 1) 2) + ((cons 1) nil) ;; 3 - ((λ (x int) (hd x)) + ((λ (x (list int)) 1) 7) + ;; 4 (if we hadn't changed number->v in cons) + (cons ((cons 0) nil)) + ;; 5 + (tl ((cons 1) nil)) + ;; 6 + (hd ((cons 1) nil)) + ;; 7 + ((λ (x int) x) (hd ((cons 1) nil))) + ;; 8 + ((λ (x (list int)) (cons x)) nil) + ;; 9 + ((λ (x int) (λ (y (list int)) x)) 1) ;; 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))))) + (hd 0)))) 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 dc10d2e32a..06e5de57dd 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 @@ -265,15 +265,21 @@ (define fixed (term (;; 2 - ((cons 1) 2) + ((cons 1) nil) ;; 3 - ((λ (x int) (hd x)) + ((λ (x (list int)) 1) 7) + ;; 4 (if we hadn't changed number->v in cons) + (cons ((cons 0) nil)) + ;; 5 + (tl ((cons 1) nil)) + ;; 6 + (hd ((cons 1) nil)) + ;; 7 + ((λ (x int) x) (hd ((cons 1) nil))) + ;; 8 + ((λ (x (list int)) (cons x)) nil) + ;; 9 + ((λ (x int) (λ (y (list int)) x)) 1) ;; 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))))) + (hd 0)))) 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 ba02a3c960..10bfba6605 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 @@ -264,15 +264,21 @@ (define fixed (term (;; 2 - ((cons 1) 2) + ((cons 1) nil) ;; 3 - ((λ (x int) (hd x)) + ((λ (x (list int)) 1) 7) + ;; 4 (if we hadn't changed number->v in cons) + (cons ((cons 0) nil)) + ;; 5 + (tl ((cons 1) nil)) + ;; 6 + (hd ((cons 1) nil)) + ;; 7 + ((λ (x int) x) (hd ((cons 1) nil))) + ;; 8 + ((λ (x (list int)) (cons x)) nil) + ;; 9 + ((λ (x int) (λ (y (list int)) x)) 1) ;; 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))))) + (hd 0)))) 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 ca6e4d85c4..7e7d7d1be3 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 @@ -264,15 +264,21 @@ (define fixed (term (;; 2 - ((cons 1) 2) + ((cons 1) nil) ;; 3 - ((λ (x int) (hd x)) + ((λ (x (list int)) 1) 7) + ;; 4 (if we hadn't changed number->v in cons) + (cons ((cons 0) nil)) + ;; 5 + (tl ((cons 1) nil)) + ;; 6 + (hd ((cons 1) nil)) + ;; 7 + ((λ (x int) x) (hd ((cons 1) nil))) + ;; 8 + ((λ (x (list int)) (cons x)) nil) + ;; 9 + ((λ (x int) (λ (y (list int)) x)) 1) ;; 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))))) + (hd 0)))) 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 9bbf08d565..9360bee92f 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 @@ -263,15 +263,21 @@ (define fixed (term (;; 2 - ((cons 1) 2) + ((cons 1) nil) ;; 3 - ((λ (x int) (hd x)) + ((λ (x (list int)) 1) 7) + ;; 4 (if we hadn't changed number->v in cons) + (cons ((cons 0) nil)) + ;; 5 + (tl ((cons 1) nil)) + ;; 6 + (hd ((cons 1) nil)) + ;; 7 + ((λ (x int) x) (hd ((cons 1) nil))) + ;; 8 + ((λ (x (list int)) (cons x)) nil) + ;; 9 + ((λ (x int) (λ (y (list int)) x)) 1) ;; 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))))) + (hd 0)))) 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 ee843474c0..8ee7b2cf14 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 @@ -264,15 +264,21 @@ (define fixed (term (;; 2 - ((cons 1) 2) + ((cons 1) nil) ;; 3 - ((λ (x int) (hd x)) + ((λ (x (list int)) 1) 7) + ;; 4 (if we hadn't changed number->v in cons) + (cons ((cons 0) nil)) + ;; 5 + (tl ((cons 1) nil)) + ;; 6 + (hd ((cons 1) nil)) + ;; 7 + ((λ (x int) x) (hd ((cons 1) nil))) + ;; 8 + ((λ (x (list int)) (cons x)) nil) + ;; 9 + ((λ (x int) (λ (y (list int)) x)) 1) ;; 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))))) + (hd 0)))) 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 69a31f0014..6aaf98f71c 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 @@ -264,15 +264,21 @@ (define fixed (term (;; 2 - ((cons 1) 2) + ((cons 1) nil) ;; 3 - ((λ (x int) (hd x)) + ((λ (x (list int)) 1) 7) + ;; 4 (if we hadn't changed number->v in cons) + (cons ((cons 0) nil)) + ;; 5 + (tl ((cons 1) nil)) + ;; 6 + (hd ((cons 1) nil)) + ;; 7 + ((λ (x int) x) (hd ((cons 1) nil))) + ;; 8 + ((λ (x (list int)) (cons x)) nil) + ;; 9 + ((λ (x int) (λ (y (list int)) x)) 1) ;; 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))))) + (hd 0)))) 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 d790961584..b62eeaeb1c 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 @@ -5,8 +5,8 @@ (require redex/reduction-semantics (only-in redex/private/generate-term pick-an-index) racket/list - racket/contract racket/match + racket/contract "tut-subst.rkt") (provide (all-defined-out)) @@ -247,7 +247,7 @@ [t-type (type-check term)]) ;; xxx shouldn't this be t-type IMPLIES this? (and - (= (length red-res) 1) + (= (length red-res) 1) (or (equal? (car red-res) "error") (equal? t-type (type-check (car red-res)))))))) @@ -265,15 +265,21 @@ (define fixed (term (;; 2 - ((cons 1) 2) + ((cons 1) nil) ;; 3 - ((λ (x int) (hd x)) + ((λ (x (list int)) 1) 7) + ;; 4 (if we hadn't changed number->v in cons) + (cons ((cons 0) nil)) + ;; 5 + (tl ((cons 1) nil)) + ;; 6 + (hd ((cons 1) nil)) + ;; 7 + ((λ (x int) x) (hd ((cons 1) nil))) + ;; 8 + ((λ (x (list int)) (cons x)) nil) + ;; 9 + ((λ (x int) (λ (y (list int)) x)) 1) ;; 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))))) + (hd 0)))) 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 920f33b572..e86db5285b 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 @@ -189,7 +189,7 @@ [(equal? gen-type 'fixed) (define some-failed? (for/or ([t (in-list fixed)]) - (define ok? (check t)) + (define ok? (check (and (tc t) t))) (not ok?))) (unless some-failed? (error 'fixed "Expected some term to fail, but didn't find one in ~a" fixed))] @@ -240,13 +240,14 @@ (for ([gen-type (in-list types)]) (test-file filename verbose #f gen-type (* minutes 60)))) -(call-with-output-file output-file - (λ (out) - (write - (apply append - (for/list ([(type times) (in-hash results)]) - (apply append - (for/list ([t times]) - (list filename type t))))) +(unless (member 'fixed types) + (call-with-output-file output-file + (λ (out) + (write + (apply append + (for/list ([(type times) (in-hash results)]) + (apply append + (for/list ([t times]) + (list filename type t))))) out)) - #:exists 'replace) + #:exists 'replace))