From 33fa2f86541c3e8524a5aa273c148d74b923a52e Mon Sep 17 00:00:00 2001 From: Robby Findler Date: Sun, 30 Mar 2014 10:15:55 -0500 Subject: [PATCH] adjust let-poly check functions so they count exns as failure, but only for the bugs that are expected to show up that way --- .../redex/examples/benchmark/let-poly/5.diff | 32 ++++++++++++++++--- .../redex/examples/benchmark/let-poly/6.diff | 32 ++++++++++++++++--- .../benchmark/let-poly/let-poly-5.rkt | 29 ++++++++--------- .../benchmark/let-poly/let-poly-6.rkt | 29 ++++++++--------- 4 files changed, 84 insertions(+), 38 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 86bf20179a..4db83d294d 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 @@ -10,9 +10,33 @@ > (τ (eliminate-τ x τ σ) (eliminate-G x τ G))] > [(eliminate-G x τ (y σ G)) > (y (eliminate-τ x τ σ) (eliminate-G x τ G))]) -571a574,578 +560,571c562,577 +< (let ([t-type (type-check M)]) +< (implies +< t-type +< (let loop ([Σ+M `(· ,M)]) +< (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)) +< (let ([red-res (apply-reduction-relation red Σ+M)]) +< (and (= (length red-res) 1) +< (let ([red-t (car red-res)]) +< (or (equal? red-t "error") +< (loop red-t)))))))))))) +--- +> (with-handlers ([exn:fail? (λ (x) #f)]) +> (let ([t-type (type-check M)]) +> (implies +> t-type +> (let loop ([Σ+M `(· ,M)]) +> (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)) +> (let ([red-res (apply-reduction-relation red Σ+M)]) +> (and (= (length red-res) 1) +> (let ([red-t (car red-res)]) +> (or (equal? red-t "error") +> (loop red-t))))))))))))) > > (define small-counter-example (term (cons 1))) -> (test-equal (with-handlers ([exn:fail? (λ (x) #f)]) -> (check small-counter-example)) -> #f) +> (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 773d1a12f9..d08c608bf6 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 @@ -6,9 +6,33 @@ < [(∨ boolean_1 boolean_2) #t]) --- > [(∨ boolean boolean) #t]) -571a572,576 +560,571c560,575 +< (let ([t-type (type-check M)]) +< (implies +< t-type +< (let loop ([Σ+M `(· ,M)]) +< (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)) +< (let ([red-res (apply-reduction-relation red Σ+M)]) +< (and (= (length red-res) 1) +< (let ([red-t (car red-res)]) +< (or (equal? red-t "error") +< (loop red-t)))))))))))) +--- +> (with-handlers ([exn:fail? (λ (x) #f)]) +> (let ([t-type (type-check M)]) +> (implies +> t-type +> (let loop ([Σ+M `(· ,M)]) +> (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)) +> (let ([red-res (apply-reduction-relation red Σ+M)]) +> (and (= (length red-res) 1) +> (let ([red-t (car red-res)]) +> (or (equal? red-t "error") +> (loop red-t))))))))))))) > > (define small-counter-example (term ((λ x x) 1))) -> (test-equal (with-handlers ([exn:fail? (λ (x) #f)]) -> (check small-counter-example)) -> #f) +> (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 3d556cae25..42154de5fc 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 @@ -559,20 +559,19 @@ from the given term. (define (check M) (or (not M) - (let ([t-type (type-check M)]) - (implies - t-type - (let loop ([Σ+M `(· ,M)]) - (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)) - (let ([red-res (apply-reduction-relation red Σ+M)]) - (and (= (length red-res) 1) - (let ([red-t (car red-res)]) - (or (equal? red-t "error") - (loop red-t)))))))))))) + (with-handlers ([exn:fail? (λ (x) #f)]) + (let ([t-type (type-check M)]) + (implies + t-type + (let loop ([Σ+M `(· ,M)]) + (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)) + (let ([red-res (apply-reduction-relation red Σ+M)]) + (and (= (length red-res) 1) + (let ([red-t (car red-res)]) + (or (equal? red-t "error") + (loop red-t))))))))))))) (define small-counter-example (term (cons 1))) -(test-equal (with-handlers ([exn:fail? (λ (x) #f)]) - (check small-counter-example)) - #f) +(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 8d95d50428..01b7ad3591 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 @@ -557,20 +557,19 @@ from the given term. (define (check M) (or (not M) - (let ([t-type (type-check M)]) - (implies - t-type - (let loop ([Σ+M `(· ,M)]) - (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)) - (let ([red-res (apply-reduction-relation red Σ+M)]) - (and (= (length red-res) 1) - (let ([red-t (car red-res)]) - (or (equal? red-t "error") - (loop red-t)))))))))))) + (with-handlers ([exn:fail? (λ (x) #f)]) + (let ([t-type (type-check M)]) + (implies + t-type + (let loop ([Σ+M `(· ,M)]) + (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)) + (let ([red-res (apply-reduction-relation red Σ+M)]) + (and (= (length red-res) 1) + (let ([red-t (car red-res)]) + (or (equal? red-t "error") + (loop red-t))))))))))))) (define small-counter-example (term ((λ x x) 1))) -(test-equal (with-handlers ([exn:fail? (λ (x) #f)]) - (check small-counter-example)) - #f) +(test-equal (check small-counter-example) #f)