suzanne.soy/racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

fix let-poly's check function so it always terminates

Browse Source
This commit is contained in:
Robby Findler 2014-03-30 21:15:39 -05:00
parent d33e6e635b
commit eb1fbc8bcf
10 changed files with 40 additions and 40 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/5.diff
View File

@ -14,7 +14,7 @@
< (let ([t-type (type-check M)]) < (let ([t-type (type-check M)])
< (implies < (implies
< t-type < 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))) < (define new-type (type-check (list-ref Σ+M 1) (list-ref Σ+M 0)))
< (and (consistent-with? t-type new-type) < (and (consistent-with? t-type new-type)
< (or (v? (list-ref Σ+M 1)) < (or (v? (list-ref Σ+M 1))
@ -22,13 +22,13 @@
< (and (= (length red-res) 1) < (and (= (length red-res) 1)
< (let ([red-t (car red-res)]) < (let ([red-t (car red-res)])
< (or (equal? red-t "error") < (or (equal? red-t "error")
< (loop red-t)))))))))))) < (zero? n) (loop red-t (- n 1)))))))))))))
--- ---
> (with-handlers ([exn:fail? (λ (x) #f)]) > (with-handlers ([exn:fail? (λ (x) #f)])
> (let ([t-type (type-check M)]) > (let ([t-type (type-check M)])
> (implies > (implies
> t-type > 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))) > (define new-type (type-check (list-ref Σ+M 1) (list-ref Σ+M 0)))
> (and (consistent-with? t-type new-type) > (and (consistent-with? t-type new-type)
> (or (v? (list-ref Σ+M 1)) > (or (v? (list-ref Σ+M 1))
@ -36,7 +36,7 @@
> (and (= (length red-res) 1) > (and (= (length red-res) 1)
> (let ([red-t (car red-res)]) > (let ([red-t (car red-res)])
> (or (equal? red-t "error") > (or (equal? red-t "error")
> (loop red-t))))))))))))) > (zero? n) (loop red-t (- n 1))))))))))))))
> >
> (define small-counter-example (term (cons 1))) > (define small-counter-example (term (cons 1)))
> (test-equal (check small-counter-example) #f) > (test-equal (check small-counter-example) #f)

8
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/6.diff
View File

@ -10,7 +10,7 @@
< (let ([t-type (type-check M)]) < (let ([t-type (type-check M)])
< (implies < (implies
< t-type < 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))) < (define new-type (type-check (list-ref Σ+M 1) (list-ref Σ+M 0)))
< (and (consistent-with? t-type new-type) < (and (consistent-with? t-type new-type)
< (or (v? (list-ref Σ+M 1)) < (or (v? (list-ref Σ+M 1))
@ -18,13 +18,13 @@
< (and (= (length red-res) 1) < (and (= (length red-res) 1)
< (let ([red-t (car red-res)]) < (let ([red-t (car red-res)])
< (or (equal? red-t "error") < (or (equal? red-t "error")
< (loop red-t)))))))))))) < (zero? n) (loop red-t (- n 1)))))))))))))
--- ---
> (with-handlers ([exn:fail? (λ (x) #f)]) > (with-handlers ([exn:fail? (λ (x) #f)])
> (let ([t-type (type-check M)]) > (let ([t-type (type-check M)])
> (implies > (implies
> t-type > 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))) > (define new-type (type-check (list-ref Σ+M 1) (list-ref Σ+M 0)))
> (and (consistent-with? t-type new-type) > (and (consistent-with? t-type new-type)
> (or (v? (list-ref Σ+M 1)) > (or (v? (list-ref Σ+M 1))
@ -32,7 +32,7 @@
> (and (= (length red-res) 1) > (and (= (length red-res) 1)
> (let ([red-t (car red-res)]) > (let ([red-t (car red-res)])
> (or (equal? red-t "error") > (or (equal? red-t "error")
> (loop red-t))))))))))))) > (zero? n) (loop red-t (- n 1))))))))))))))
> >
> (define small-counter-example (term ((λ x x) 1))) > (define small-counter-example (term ((λ x x) 1)))
> (test-equal (check small-counter-example) #f) > (test-equal (check small-counter-example) #f)

8
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-1.rkt
View File

@ -550,8 +550,8 @@ Generators
#| #|
Check to see if a combination of preservation Check to see if a combination of preservation
and progress holds for every single term reachable and progress holds for the first 100 terms
from the given term. reachable from the given term.
|# |#
@ -560,7 +560,7 @@ from the given term.
(let ([t-type (type-check M)]) (let ([t-type (type-check M)])
(implies (implies
t-type 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))) (define new-type (type-check (list-ref Σ+M 1) (list-ref Σ+M 0)))
(and (consistent-with? t-type new-type) (and (consistent-with? t-type new-type)
(or (v? (list-ref Σ+M 1)) (or (v? (list-ref Σ+M 1))
@ -568,7 +568,7 @@ from the given term.
(and (= (length red-res) 1) (and (= (length red-res) 1)
(let ([red-t (car red-res)]) (let ([red-t (car red-res)])
(or (equal? red-t "error") (or (equal? red-t "error")
(loop red-t)))))))))))) (zero? n) (loop red-t (- n 1)))))))))))))
(define small-counter-example '(hd ((λ x x) 1))) (define small-counter-example '(hd ((λ x x) 1)))
(test-equal (check small-counter-example) #f) (test-equal (check small-counter-example) #f)

8
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-2.rkt
View File

@ -545,8 +545,8 @@ Generators
#| #|
Check to see if a combination of preservation Check to see if a combination of preservation
and progress holds for every single term reachable and progress holds for the first 100 terms
from the given term. reachable from the given term.
|# |#
@ -555,7 +555,7 @@ from the given term.
(let ([t-type (type-check M)]) (let ([t-type (type-check M)])
(implies (implies
t-type 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))) (define new-type (type-check (list-ref Σ+M 1) (list-ref Σ+M 0)))
(and (consistent-with? t-type new-type) (and (consistent-with? t-type new-type)
(or (v? (list-ref Σ+M 1)) (or (v? (list-ref Σ+M 1))
@ -563,7 +563,7 @@ from the given term.
(and (= (length red-res) 1) (and (= (length red-res) 1)
(let ([red-t (car red-res)]) (let ([red-t (car red-res)])
(or (equal? red-t "error") (or (equal? red-t "error")
(loop red-t)))))))))))) (zero? n) (loop red-t (- n 1)))))))))))))
(define small-counter-example '(let ([x (new nil)]) (define small-counter-example '(let ([x (new nil)])
((λ ignore ((λ ignore

8
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-3.rkt
View File

@ -550,8 +550,8 @@ Generators
#| #|
Check to see if a combination of preservation Check to see if a combination of preservation
and progress holds for every single term reachable and progress holds for the first 100 terms
from the given term. reachable from the given term.
|# |#
@ -560,7 +560,7 @@ from the given term.
(let ([t-type (type-check M)]) (let ([t-type (type-check M)])
(implies (implies
t-type 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))) (define new-type (type-check (list-ref Σ+M 1) (list-ref Σ+M 0)))
(and (consistent-with? t-type new-type) (and (consistent-with? t-type new-type)
(or (v? (list-ref Σ+M 1)) (or (v? (list-ref Σ+M 1))
@ -568,7 +568,7 @@ from the given term.
(and (= (length red-res) 1) (and (= (length red-res) 1)
(let ([red-t (car red-res)]) (let ([red-t (car red-res)])
(or (equal? red-t "error") (or (equal? red-t "error")
(loop red-t)))))))))))) (zero? n) (loop red-t (- n 1)))))))))))))
(define small-counter-example (term (1 cons))) (define small-counter-example (term (1 cons)))
(test-equal (check small-counter-example) #f) (test-equal (check small-counter-example) #f)

8
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-4.rkt
View File

@ -552,8 +552,8 @@ Generators
#| #|
Check to see if a combination of preservation Check to see if a combination of preservation
and progress holds for every single term reachable and progress holds for the first 100 terms
from the given term. reachable from the given term.
|# |#
@ -562,7 +562,7 @@ from the given term.
(let ([t-type (type-check M)]) (let ([t-type (type-check M)])
(implies (implies
t-type 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))) (define new-type (type-check (list-ref Σ+M 1) (list-ref Σ+M 0)))
(and (consistent-with? t-type new-type) (and (consistent-with? t-type new-type)
(or (v? (list-ref Σ+M 1)) (or (v? (list-ref Σ+M 1))
@ -570,7 +570,7 @@ from the given term.
(and (= (length red-res) 1) (and (= (length red-res) 1)
(let ([red-t (car red-res)]) (let ([red-t (car red-res)])
(or (equal? red-t "error") (or (equal? red-t "error")
(loop red-t)))))))))))) (zero? n) (loop red-t (- n 1)))))))))))))
(define small-counter-example (term ((λ x (x x)) hd))) (define small-counter-example (term ((λ x (x x)) hd)))
(test-equal (check small-counter-example) #f) (test-equal (check small-counter-example) #f)

8
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-5.rkt
View File

@ -552,8 +552,8 @@ Generators
#| #|
Check to see if a combination of preservation Check to see if a combination of preservation
and progress holds for every single term reachable and progress holds for the first 100 terms
from the given term. reachable from the given term.
|# |#
@ -563,7 +563,7 @@ from the given term.
(let ([t-type (type-check M)]) (let ([t-type (type-check M)])
(implies (implies
t-type 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))) (define new-type (type-check (list-ref Σ+M 1) (list-ref Σ+M 0)))
(and (consistent-with? t-type new-type) (and (consistent-with? t-type new-type)
(or (v? (list-ref Σ+M 1)) (or (v? (list-ref Σ+M 1))
@ -571,7 +571,7 @@ from the given term.
(and (= (length red-res) 1) (and (= (length red-res) 1)
(let ([red-t (car red-res)]) (let ([red-t (car red-res)])
(or (equal? red-t "error") (or (equal? red-t "error")
(loop red-t))))))))))))) (zero? n) (loop red-t (- n 1))))))))))))))
(define small-counter-example (term (cons 1))) (define small-counter-example (term (cons 1)))
(test-equal (check small-counter-example) #f) (test-equal (check small-counter-example) #f)

8
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-6.rkt
View File

@ -550,8 +550,8 @@ Generators
#| #|
Check to see if a combination of preservation Check to see if a combination of preservation
and progress holds for every single term reachable and progress holds for the first 100 terms
from the given term. reachable from the given term.
|# |#
@ -561,7 +561,7 @@ from the given term.
(let ([t-type (type-check M)]) (let ([t-type (type-check M)])
(implies (implies
t-type 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))) (define new-type (type-check (list-ref Σ+M 1) (list-ref Σ+M 0)))
(and (consistent-with? t-type new-type) (and (consistent-with? t-type new-type)
(or (v? (list-ref Σ+M 1)) (or (v? (list-ref Σ+M 1))
@ -569,7 +569,7 @@ from the given term.
(and (= (length red-res) 1) (and (= (length red-res) 1)
(let ([red-t (car red-res)]) (let ([red-t (car red-res)])
(or (equal? red-t "error") (or (equal? red-t "error")
(loop red-t))))))))))))) (zero? n) (loop red-t (- n 1))))))))))))))
(define small-counter-example (term ((λ x x) 1))) (define small-counter-example (term ((λ x x) 1)))
(test-equal (check small-counter-example) #f) (test-equal (check small-counter-example) #f)

8
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-7.rkt
View File

@ -551,8 +551,8 @@ Generators
#| #|
Check to see if a combination of preservation Check to see if a combination of preservation
and progress holds for every single term reachable and progress holds for the first 100 terms
from the given term. reachable from the given term.
|# |#
@ -561,7 +561,7 @@ from the given term.
(let ([t-type (type-check M)]) (let ([t-type (type-check M)])
(implies (implies
t-type 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))) (define new-type (type-check (list-ref Σ+M 1) (list-ref Σ+M 0)))
(and (consistent-with? t-type new-type) (and (consistent-with? t-type new-type)
(or (v? (list-ref Σ+M 1)) (or (v? (list-ref Σ+M 1))
@ -569,7 +569,7 @@ from the given term.
(and (= (length red-res) 1) (and (= (length red-res) 1)
(let ([red-t (car red-res)]) (let ([red-t (car red-res)])
(or (equal? red-t "error") (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)))) (define small-counter-example (term (let ((x (λ y y))) (x x))))
(test-equal (check small-counter-example) #f) (test-equal (check small-counter-example) #f)

8
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-base.rkt
View File

@ -550,8 +550,8 @@ Generators
#| #|
Check to see if a combination of preservation Check to see if a combination of preservation
and progress holds for every single term reachable and progress holds for the first 100 terms
from the given term. reachable from the given term.
|# |#
@ -560,7 +560,7 @@ from the given term.
(let ([t-type (type-check M)]) (let ([t-type (type-check M)])
(implies (implies
t-type 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))) (define new-type (type-check (list-ref Σ+M 1) (list-ref Σ+M 0)))
(and (consistent-with? t-type new-type) (and (consistent-with? t-type new-type)
(or (v? (list-ref Σ+M 1)) (or (v? (list-ref Σ+M 1))
@ -568,4 +568,4 @@ from the given term.
(and (= (length red-res) 1) (and (= (length red-res) 1)
(let ([red-t (car red-res)]) (let ([red-t (car red-res)])
(or (equal? red-t "error") (or (equal? red-t "error")
(loop red-t)))))))))))) (zero? n) (loop red-t (- n 1)))))))))))))