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

adjust benchmark so that the 'check' functions are required to be

Browse Source 
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
This commit is contained in:
Robby Findler 2014-03-30 17:24:02 -05:00
parent a9d8158133
commit c7c95b8906
9 changed files with 11 additions and 18 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/list-machine-1.rkt
View File

@ -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

2
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/list-machine-2.rkt
View File

@ -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

2
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/list-machine-3.rkt
View File

@ -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

2
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/list-machine-base.rkt
View File

@ -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

2
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/rbtrees-1.rkt
View File

@ -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)))

2
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/rbtrees-2.rkt
View File

@ -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)))

2
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/rbtrees-3.rkt
View File

@ -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)))

2
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/rbtrees-base.rkt
View File

@ -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)))

13
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/test-file.rkt
View File

@ -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)