From c7c95b8906ec180a8414aae86bb02e0672a0dd3d Mon Sep 17 00:00:00 2001 From: Robby Findler Date: Sun, 30 Mar 2014 17:24:02 -0500 Subject: [PATCH] adjust benchmark so that the 'check' functions are required to be self-contained (and then don't call type-check anymore from the benchmark scripts) this fixes a problem in the let-poly models, since some of the bugs there cause the type-checker to raise an error --- .../benchmark/list-machine/list-machine-1.rkt | 2 +- .../benchmark/list-machine/list-machine-2.rkt | 2 +- .../benchmark/list-machine/list-machine-3.rkt | 2 +- .../benchmark/list-machine/list-machine-base.rkt | 2 +- .../redex/examples/benchmark/rbtrees/rbtrees-1.rkt | 2 +- .../redex/examples/benchmark/rbtrees/rbtrees-2.rkt | 2 +- .../redex/examples/benchmark/rbtrees/rbtrees-3.rkt | 2 +- .../examples/benchmark/rbtrees/rbtrees-base.rkt | 2 +- .../redex/examples/benchmark/test-file.rkt | 13 +++---------- 9 files changed, 11 insertions(+), 18 deletions(-) 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 b12ea614dc..54a9a1ddcb 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 @@ -134,7 +134,7 @@ (define (check p) (or (not p) - (check-progress p))) + (implies (type-check p) (check-progress p)))) (define-metafunction list-machine different : any any -> any 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 56a25a9b6d..be0844ba2b 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 @@ -134,7 +134,7 @@ (define (check p) (or (not p) - (check-progress p))) + (implies (type-check p) (check-progress p)))) (define-metafunction list-machine different : any any -> any 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 fa948aaef3..4c2cbbb025 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 @@ -130,7 +130,7 @@ (define (check p) (or (not p) - (check-progress p))) + (implies (type-check p) (check-progress p)))) (define-metafunction list-machine different : any any -> any 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 3c7f13976f..6f3a9ffcd9 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 @@ -130,7 +130,7 @@ (define (check p) (or (not p) - (check-progress p))) + (implies (type-check p) (check-progress p)))) (define-metafunction list-machine different : any any -> any 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 f345efc3a3..83715d33ff 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 @@ -287,7 +287,7 @@ (define (check t) (or (not t) - (ins-preserves-rb-tree t))) + (implies (type-check t) (ins-preserves-rb-tree t)))) (define (generate-enum-term) (generate-term rbtrees t #:i-th (pick-an-index 0.25))) 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 3673bb8bf7..7fda3e7ed9 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 @@ -285,7 +285,7 @@ (define (check t) (or (not t) - (ins-preserves-rb-tree t))) + (implies (type-check t) (ins-preserves-rb-tree t)))) (define (generate-enum-term) (generate-term rbtrees t #:i-th (pick-an-index 0.25))) 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 5d6134943c..ab87bd5a50 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 @@ -287,7 +287,7 @@ (define (check t) (or (not t) - (ins-preserves-rb-tree t))) + (implies (type-check t) (ins-preserves-rb-tree t)))) (define (generate-enum-term) (generate-term rbtrees t #:i-th (pick-an-index 0.25))) 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 5a3a9622a8..19d4bebdc7 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 @@ -287,7 +287,7 @@ (define (check t) (or (not t) - (ins-preserves-rb-tree t))) + (implies (type-check t) (ins-preserves-rb-tree t)))) (define (generate-enum-term) (generate-term rbtrees t #:i-th (pick-an-index 0.25))) 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 10a16ec42f..e88550f138 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 @@ -186,11 +186,6 @@ (printf "~a has the error: ~a\n\n" fpath err) (printf "Running ~a....\n" fpath) (printf "Using generator: ~s\n" gen-type) - (define (gen-and-type gen) - (λ () - (define t (gen)) - (and (tc t) - t))) (cond [(equal? gen-type 'fixed) (define small-counter-example @@ -206,15 +201,13 @@ (error 'fixed "Expected ~e to fail on check, but it didn't" small-counter-example))] [(equal? gen-type 'grammar) - (run/spawn-generations fpath verbose? no-errs? (λ () (gen-and-type gen-term)) + (run/spawn-generations fpath verbose? no-errs? (λ () gen-term) check seconds gen-type)] [(equal? gen-type 'enum) - (run/spawn-generations fpath verbose? no-errs? (λ () (gen-and-type gen-enum)) + (run/spawn-generations fpath verbose? no-errs? (λ () gen-enum) check seconds gen-type)] [(equal? gen-type 'ordered) - (run/spawn-generations fpath verbose? no-errs? (λ () - (define g (ordered-generator)) - (gen-and-type g)) + (run/spawn-generations fpath verbose? no-errs? (λ () (ordered-generator)) check seconds gen-type)] [(equal? gen-type 'search) (run/spawn-generations fpath verbose? no-errs? (λ () gen-typed-term)