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

fix rvm ordered generation to not do test every time

Browse Source
This commit is contained in:
Burke Fetscher 2014-03-22 19:22:37 -05:00
parent ac1d7ea19e
commit da158e6d95
14 changed files with 38 additions and 54 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/14.diff
View File

@ -16,8 +16,7 @@
> ;; bug 14
> [(closure-intact? (box-nc ṽ_1 ...) (imm ṽ_2 ...))
> (closure-intact? (ṽ_1 ...) (ṽ_2 ...))]
475a481,489
>
480a486,493
> (define small-counter-example
> '(let-one 'x
> (application (proc-const (val val) (loc 0))

4
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/15.diff
View File

@ -13,8 +13,7 @@
< `(case-lam ,@(map (curry recur depth #f) ls))]
---
> `(case-lam ,@(map (curry recur depth #t) ls))]
475a478,485
>
480a483,490
> (define small-counter-example
> '(let-one 42
> (boxenv 0
@ -22,3 +21,4 @@
> (loc-box 1)))))
>
> (test-equal (check small-counter-example) #f)
>

5
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/2.diff
View File

@ -3,8 +3,7 @@
---
> ;; bug 2
> #;(side-condition (< (term n_0) (term n_h)))]
475a477,487
>
480a482,492
> (define small-counter-example
> '(proc-const (val)
> (branch (loc 0)
@ -15,4 +14,4 @@
> void)))
>
> (test-equal (check small-counter-example) #f)
\ No newline at end of file
>

3
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/3.diff
View File

@ -14,8 +14,7 @@
< (where (s_1 γ_1 η_1) (verify* (e_0 e_1 ...) (abs-push n not s) n_l* #f γ η))
---
> (where (s_1 γ_1 η_1) (verify* (e_0 e_1 ...) (abs-push n uninit s) n_l* #f γ η))
475a476,484
>
480a481,488
> (define small-counter-example
> '(application
> (proc-const (val val) (branch (loc-noclr 0) 'a 'b))

5
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/4.diff
View File

@ -7,12 +7,9 @@
---
> ;; bug 4
> #;(side-condition (< (term n_p) (term n_l)))]
475a477,484
>
480a482,486
> (define small-counter-example
> '(let-one 'x
> (branch #f (boxenv 0 'y) (loc-box 0))))
>
> (test-equal (check small-counter-example) #f)
>
>

4
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/5.diff
View File

@ -7,8 +7,7 @@
---
> ;;bug 5
> ;;(side-condition (<= (term n) (term n_l)))
475a477,486
>
480a482,489
> (define small-counter-example
> '(let-void 1
> (branch #f
@ -17,4 +16,3 @@
>
> (test-equal (check small-counter-example) #f)
>
>

5
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/6.diff
View File

@ -3,12 +3,11 @@
---
> ;; bug 6
> #;(side-condition (term (AND (lam-verified? l s ?) ...)))]
475a477,483
>
480a482,488
> (define small-counter-example
> '(application
> (case-lam (lam (val) () (loc-noclr 34)))
> 'x))
>
> (test-equal (check small-counter-example) #f)
\ No newline at end of file
>

9
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-14.rkt
View File

@ -478,6 +478,10 @@
(define (ordered-enum-generator)
(let ([index 0])
(λ ()
(begin0
(fix (generate-term bytecode e #:i-th index))
(set! index (add1 index))))))
(define small-counter-example
'(let-one 'x
@ -487,9 +491,4 @@
(test-equal (check small-counter-example) #f)
(λ ()
(begin0
(fix (generate-term bytecode e #:i-th index))
(set! index (add1 index))))))
(define fixed '())

8
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-15.rkt
View File

@ -475,6 +475,10 @@
(define (ordered-enum-generator)
(let ([index 0])
(λ ()
(begin0
(fix (generate-term bytecode e #:i-th index))
(set! index (add1 index))))))
(define small-counter-example
'(let-one 42
@ -483,9 +487,5 @@
(loc-box 1)))))
(test-equal (check small-counter-example) #f)
(λ ()
(begin0
(fix (generate-term bytecode e #:i-th index))
(set! index (add1 index))))))
(define fixed '())

8
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-2.rkt
View File

@ -474,6 +474,10 @@
(define (ordered-enum-generator)
(let ([index 0])
(λ ()
(begin0
(fix (generate-term bytecode e #:i-th index))
(set! index (add1 index))))))
(define small-counter-example
'(proc-const (val)
@ -485,9 +489,5 @@
void)))
(test-equal (check small-counter-example) #f)
(λ ()
(begin0
(fix (generate-term bytecode e #:i-th index))
(set! index (add1 index))))))
(define fixed '())

9
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-3.rkt
View File

@ -473,6 +473,10 @@
(define (ordered-enum-generator)
(let ([index 0])
(λ ()
(begin0
(fix (generate-term bytecode e #:i-th index))
(set! index (add1 index))))))
(define small-counter-example
'(application
@ -482,9 +486,4 @@
(test-equal (check small-counter-example) #f)
(λ ()
(begin0
(fix (generate-term bytecode e #:i-th index))
(set! index (add1 index))))))
(define fixed '())

11
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-4.rkt
View File

@ -474,17 +474,14 @@
(define (ordered-enum-generator)
(let ([index 0])
(λ ()
(begin0
(fix (generate-term bytecode e #:i-th index))
(set! index (add1 index))))))
(define small-counter-example
'(let-one 'x
(branch #f (boxenv 0 'y) (loc-box 0))))
(test-equal (check small-counter-example) #f)
(λ ()
(begin0
(fix (generate-term bytecode e #:i-th index))
(set! index (add1 index))))))
(define fixed '())

10
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-5.rkt
View File

@ -474,6 +474,10 @@
(define (ordered-enum-generator)
(let ([index 0])
(λ ()
(begin0
(fix (generate-term bytecode e #:i-th index))
(set! index (add1 index))))))
(define small-counter-example
'(let-void 1
@ -483,10 +487,4 @@
(test-equal (check small-counter-example) #f)
(λ ()
(begin0
(fix (generate-term bytecode e #:i-th index))
(set! index (add1 index))))))
(define fixed '())

8
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-6.rkt
View File

@ -474,6 +474,10 @@
(define (ordered-enum-generator)
(let ([index 0])
(λ ()
(begin0
(fix (generate-term bytecode e #:i-th index))
(set! index (add1 index))))))
(define small-counter-example
'(application
@ -481,9 +485,5 @@
'x))
(test-equal (check small-counter-example) #f)
(λ ()
(begin0
(fix (generate-term bytecode e #:i-th index))
(set! index (add1 index))))))
(define fixed '())