From da158e6d952dcb9b530a93019395e2d4d42cff3b Mon Sep 17 00:00:00 2001 From: Burke Fetscher Date: Sat, 22 Mar 2014 19:22:37 -0500 Subject: [PATCH] fix rvm ordered generation to not do test every time --- .../redex/examples/benchmark/rvm/14.diff | 3 +-- .../redex/examples/benchmark/rvm/15.diff | 4 ++-- .../redex/examples/benchmark/rvm/2.diff | 5 ++--- .../redex/examples/benchmark/rvm/3.diff | 3 +-- .../redex/examples/benchmark/rvm/4.diff | 5 +---- .../redex/examples/benchmark/rvm/5.diff | 4 +--- .../redex/examples/benchmark/rvm/6.diff | 5 ++--- .../redex/examples/benchmark/rvm/verification-14.rkt | 9 ++++----- .../redex/examples/benchmark/rvm/verification-15.rkt | 8 ++++---- .../redex/examples/benchmark/rvm/verification-2.rkt | 8 ++++---- .../redex/examples/benchmark/rvm/verification-3.rkt | 9 ++++----- .../redex/examples/benchmark/rvm/verification-4.rkt | 11 ++++------- .../redex/examples/benchmark/rvm/verification-5.rkt | 10 ++++------ .../redex/examples/benchmark/rvm/verification-6.rkt | 8 ++++---- 14 files changed, 38 insertions(+), 54 deletions(-) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/14.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/14.diff index aa65fdf53b..6d63097529 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/14.diff +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/14.diff @@ -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)) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/15.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/15.diff index c012b7089b..d147409970 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/15.diff +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/15.diff @@ -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) +> diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/2.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/2.diff index e75e3841be..eced4bfcf1 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/2.diff +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/2.diff @@ -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 +> diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/3.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/3.diff index 53f6ec2229..b61dc85f56 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/3.diff +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/3.diff @@ -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)) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/4.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/4.diff index 84f429049a..813ab61e5d 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/4.diff +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/4.diff @@ -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) -> -> diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/5.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/5.diff index 80597b9ae4..8753ce38e8 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/5.diff +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/5.diff @@ -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) > -> diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/6.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/6.diff index 79ba6ed2d8..246adfd756 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/6.diff +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/6.diff @@ -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 +> diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-14.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-14.rkt index 3f48bf8ee6..132aae8dbd 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-14.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-14.rkt @@ -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 '()) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-15.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-15.rkt index ede5f120ce..ab4c8f988f 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-15.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-15.rkt @@ -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 '()) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-2.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-2.rkt index 64128124aa..2328e08707 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-2.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-2.rkt @@ -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 '()) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-3.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-3.rkt index 99a5c76c76..041d60f417 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-3.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-3.rkt @@ -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 '()) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-4.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-4.rkt index 4425a866ab..3ada4193bf 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-4.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-4.rkt @@ -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 '()) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-5.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-5.rkt index 33b4e21eca..9098c2bf73 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-5.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-5.rkt @@ -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 '()) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-6.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-6.rkt index 8975e56f87..12af4369e1 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-6.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-6.rkt @@ -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 '())