From eb1fbc8bcf9212126dc9e70fac1fe7343a8c6b0c Mon Sep 17 00:00:00 2001 From: Robby Findler Date: Sun, 30 Mar 2014 21:15:39 -0500 Subject: [PATCH] fix let-poly's check function so it always terminates --- .../redex/examples/benchmark/let-poly/5.diff | 8 ++++---- .../redex/examples/benchmark/let-poly/6.diff | 8 ++++---- .../redex/examples/benchmark/let-poly/let-poly-1.rkt | 8 ++++---- .../redex/examples/benchmark/let-poly/let-poly-2.rkt | 8 ++++---- .../redex/examples/benchmark/let-poly/let-poly-3.rkt | 8 ++++---- .../redex/examples/benchmark/let-poly/let-poly-4.rkt | 8 ++++---- .../redex/examples/benchmark/let-poly/let-poly-5.rkt | 8 ++++---- .../redex/examples/benchmark/let-poly/let-poly-6.rkt | 8 ++++---- .../redex/examples/benchmark/let-poly/let-poly-7.rkt | 8 ++++---- .../redex/examples/benchmark/let-poly/let-poly-base.rkt | 8 ++++---- 10 files changed, 40 insertions(+), 40 deletions(-) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/5.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/5.diff index 4db83d294d..9fb29dc23d 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/5.diff +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/5.diff @@ -14,7 +14,7 @@ < (let ([t-type (type-check M)]) < (implies < t-type -< (let loop ([Σ+M `(· ,M)]) +< (let loop ([Σ+M `(· ,M)] [n 100]) < (define new-type (type-check (list-ref Σ+M 1) (list-ref Σ+M 0))) < (and (consistent-with? t-type new-type) < (or (v? (list-ref Σ+M 1)) @@ -22,13 +22,13 @@ < (and (= (length red-res) 1) < (let ([red-t (car red-res)]) < (or (equal? red-t "error") -< (loop red-t)))))))))))) +< (zero? n) (loop red-t (- n 1))))))))))))) --- > (with-handlers ([exn:fail? (λ (x) #f)]) > (let ([t-type (type-check M)]) > (implies > t-type -> (let loop ([Σ+M `(· ,M)]) +> (let loop ([Σ+M `(· ,M)] [n 100]) > (define new-type (type-check (list-ref Σ+M 1) (list-ref Σ+M 0))) > (and (consistent-with? t-type new-type) > (or (v? (list-ref Σ+M 1)) @@ -36,7 +36,7 @@ > (and (= (length red-res) 1) > (let ([red-t (car red-res)]) > (or (equal? red-t "error") -> (loop red-t))))))))))))) +> (zero? n) (loop red-t (- n 1)))))))))))))) > > (define small-counter-example (term (cons 1))) > (test-equal (check small-counter-example) #f) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/6.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/6.diff index d08c608bf6..51deff07c3 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/6.diff +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/6.diff @@ -10,7 +10,7 @@ < (let ([t-type (type-check M)]) < (implies < t-type -< (let loop ([Σ+M `(· ,M)]) +< (let loop ([Σ+M `(· ,M)] [n 100]) < (define new-type (type-check (list-ref Σ+M 1) (list-ref Σ+M 0))) < (and (consistent-with? t-type new-type) < (or (v? (list-ref Σ+M 1)) @@ -18,13 +18,13 @@ < (and (= (length red-res) 1) < (let ([red-t (car red-res)]) < (or (equal? red-t "error") -< (loop red-t)))))))))))) +< (zero? n) (loop red-t (- n 1))))))))))))) --- > (with-handlers ([exn:fail? (λ (x) #f)]) > (let ([t-type (type-check M)]) > (implies > t-type -> (let loop ([Σ+M `(· ,M)]) +> (let loop ([Σ+M `(· ,M)] [n 100]) > (define new-type (type-check (list-ref Σ+M 1) (list-ref Σ+M 0))) > (and (consistent-with? t-type new-type) > (or (v? (list-ref Σ+M 1)) @@ -32,7 +32,7 @@ > (and (= (length red-res) 1) > (let ([red-t (car red-res)]) > (or (equal? red-t "error") -> (loop red-t))))))))))))) +> (zero? n) (loop red-t (- n 1)))))))))))))) > > (define small-counter-example (term ((λ x x) 1))) > (test-equal (check small-counter-example) #f) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-1.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-1.rkt index c0511f8ac9..94c907bef5 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-1.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-1.rkt @@ -550,8 +550,8 @@ Generators #| Check to see if a combination of preservation -and progress holds for every single term reachable -from the given term. +and progress holds for the first 100 terms +reachable from the given term. |# @@ -560,7 +560,7 @@ from the given term. (let ([t-type (type-check M)]) (implies t-type - (let loop ([Σ+M `(· ,M)]) + (let loop ([Σ+M `(· ,M)] [n 100]) (define new-type (type-check (list-ref Σ+M 1) (list-ref Σ+M 0))) (and (consistent-with? t-type new-type) (or (v? (list-ref Σ+M 1)) @@ -568,7 +568,7 @@ from the given term. (and (= (length red-res) 1) (let ([red-t (car red-res)]) (or (equal? red-t "error") - (loop red-t)))))))))))) + (zero? n) (loop red-t (- n 1))))))))))))) (define small-counter-example '(hd ((λ x x) 1))) (test-equal (check small-counter-example) #f) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-2.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-2.rkt index 48412165c2..5bfd58a2fc 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-2.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-2.rkt @@ -545,8 +545,8 @@ Generators #| Check to see if a combination of preservation -and progress holds for every single term reachable -from the given term. +and progress holds for the first 100 terms +reachable from the given term. |# @@ -555,7 +555,7 @@ from the given term. (let ([t-type (type-check M)]) (implies t-type - (let loop ([Σ+M `(· ,M)]) + (let loop ([Σ+M `(· ,M)] [n 100]) (define new-type (type-check (list-ref Σ+M 1) (list-ref Σ+M 0))) (and (consistent-with? t-type new-type) (or (v? (list-ref Σ+M 1)) @@ -563,7 +563,7 @@ from the given term. (and (= (length red-res) 1) (let ([red-t (car red-res)]) (or (equal? red-t "error") - (loop red-t)))))))))))) + (zero? n) (loop red-t (- n 1))))))))))))) (define small-counter-example '(let ([x (new nil)]) ((λ ignore diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-3.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-3.rkt index 5dd8f9843c..79b4465f87 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-3.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-3.rkt @@ -550,8 +550,8 @@ Generators #| Check to see if a combination of preservation -and progress holds for every single term reachable -from the given term. +and progress holds for the first 100 terms +reachable from the given term. |# @@ -560,7 +560,7 @@ from the given term. (let ([t-type (type-check M)]) (implies t-type - (let loop ([Σ+M `(· ,M)]) + (let loop ([Σ+M `(· ,M)] [n 100]) (define new-type (type-check (list-ref Σ+M 1) (list-ref Σ+M 0))) (and (consistent-with? t-type new-type) (or (v? (list-ref Σ+M 1)) @@ -568,7 +568,7 @@ from the given term. (and (= (length red-res) 1) (let ([red-t (car red-res)]) (or (equal? red-t "error") - (loop red-t)))))))))))) + (zero? n) (loop red-t (- n 1))))))))))))) (define small-counter-example (term (1 cons))) (test-equal (check small-counter-example) #f) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-4.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-4.rkt index 4bc27ba6e3..7f1c1e32fd 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-4.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-4.rkt @@ -552,8 +552,8 @@ Generators #| Check to see if a combination of preservation -and progress holds for every single term reachable -from the given term. +and progress holds for the first 100 terms +reachable from the given term. |# @@ -562,7 +562,7 @@ from the given term. (let ([t-type (type-check M)]) (implies t-type - (let loop ([Σ+M `(· ,M)]) + (let loop ([Σ+M `(· ,M)] [n 100]) (define new-type (type-check (list-ref Σ+M 1) (list-ref Σ+M 0))) (and (consistent-with? t-type new-type) (or (v? (list-ref Σ+M 1)) @@ -570,7 +570,7 @@ from the given term. (and (= (length red-res) 1) (let ([red-t (car red-res)]) (or (equal? red-t "error") - (loop red-t)))))))))))) + (zero? n) (loop red-t (- n 1))))))))))))) (define small-counter-example (term ((λ x (x x)) hd))) (test-equal (check small-counter-example) #f) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-5.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-5.rkt index 42154de5fc..03d4ebf1cc 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-5.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-5.rkt @@ -552,8 +552,8 @@ Generators #| Check to see if a combination of preservation -and progress holds for every single term reachable -from the given term. +and progress holds for the first 100 terms +reachable from the given term. |# @@ -563,7 +563,7 @@ from the given term. (let ([t-type (type-check M)]) (implies t-type - (let loop ([Σ+M `(· ,M)]) + (let loop ([Σ+M `(· ,M)] [n 100]) (define new-type (type-check (list-ref Σ+M 1) (list-ref Σ+M 0))) (and (consistent-with? t-type new-type) (or (v? (list-ref Σ+M 1)) @@ -571,7 +571,7 @@ from the given term. (and (= (length red-res) 1) (let ([red-t (car red-res)]) (or (equal? red-t "error") - (loop red-t))))))))))))) + (zero? n) (loop red-t (- n 1)))))))))))))) (define small-counter-example (term (cons 1))) (test-equal (check small-counter-example) #f) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-6.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-6.rkt index 01b7ad3591..00af04e21a 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-6.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-6.rkt @@ -550,8 +550,8 @@ Generators #| Check to see if a combination of preservation -and progress holds for every single term reachable -from the given term. +and progress holds for the first 100 terms +reachable from the given term. |# @@ -561,7 +561,7 @@ from the given term. (let ([t-type (type-check M)]) (implies t-type - (let loop ([Σ+M `(· ,M)]) + (let loop ([Σ+M `(· ,M)] [n 100]) (define new-type (type-check (list-ref Σ+M 1) (list-ref Σ+M 0))) (and (consistent-with? t-type new-type) (or (v? (list-ref Σ+M 1)) @@ -569,7 +569,7 @@ from the given term. (and (= (length red-res) 1) (let ([red-t (car red-res)]) (or (equal? red-t "error") - (loop red-t))))))))))))) + (zero? n) (loop red-t (- n 1)))))))))))))) (define small-counter-example (term ((λ x x) 1))) (test-equal (check small-counter-example) #f) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-7.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-7.rkt index 37209baafb..f954be062a 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-7.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-7.rkt @@ -551,8 +551,8 @@ Generators #| Check to see if a combination of preservation -and progress holds for every single term reachable -from the given term. +and progress holds for the first 100 terms +reachable from the given term. |# @@ -561,7 +561,7 @@ from the given term. (let ([t-type (type-check M)]) (implies t-type - (let loop ([Σ+M `(· ,M)]) + (let loop ([Σ+M `(· ,M)] [n 100]) (define new-type (type-check (list-ref Σ+M 1) (list-ref Σ+M 0))) (and (consistent-with? t-type new-type) (or (v? (list-ref Σ+M 1)) @@ -569,7 +569,7 @@ from the given term. (and (= (length red-res) 1) (let ([red-t (car red-res)]) (or (equal? red-t "error") - (loop red-t)))))))))))) + (zero? n) (loop red-t (- n 1))))))))))))) (define small-counter-example (term (let ((x (λ y y))) (x x)))) (test-equal (check small-counter-example) #f) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-base.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-base.rkt index 7c4de66bb2..906e521b6a 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-base.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-base.rkt @@ -550,8 +550,8 @@ Generators #| Check to see if a combination of preservation -and progress holds for every single term reachable -from the given term. +and progress holds for the first 100 terms +reachable from the given term. |# @@ -560,7 +560,7 @@ from the given term. (let ([t-type (type-check M)]) (implies t-type - (let loop ([Σ+M `(· ,M)]) + (let loop ([Σ+M `(· ,M)] [n 100]) (define new-type (type-check (list-ref Σ+M 1) (list-ref Σ+M 0))) (and (consistent-with? t-type new-type) (or (v? (list-ref Σ+M 1)) @@ -568,4 +568,4 @@ from the given term. (and (= (length red-res) 1) (let ([red-t (car red-res)]) (or (equal? red-t "error") - (loop red-t)))))))))))) + (zero? n) (loop red-t (- n 1)))))))))))))