From 3abb14a63e0052705db8d824d9e728dfdac234ce Mon Sep 17 00:00:00 2001 From: Robby Findler Date: Fri, 21 Mar 2014 23:21:42 -0500 Subject: [PATCH] fix property to actually use Kleene equality (instead of comparing the output of standard reduction) --- .../redex/examples/benchmark/stlc-sub/1.diff | 2 +- .../redex/examples/benchmark/stlc-sub/2.diff | 4 ++-- .../redex/examples/benchmark/stlc-sub/3.diff | 2 +- .../redex/examples/benchmark/stlc-sub/4.diff | 2 +- .../redex/examples/benchmark/stlc-sub/5.diff | 4 ++-- .../redex/examples/benchmark/stlc-sub/6.diff | 6 +++--- .../redex/examples/benchmark/stlc-sub/7.diff | 8 ++++---- .../redex/examples/benchmark/stlc-sub/8.diff | 6 +++--- .../redex/examples/benchmark/stlc-sub/9.diff | 6 +++--- .../examples/benchmark/stlc-sub/stlc-sub-1.rkt | 11 ++++++++++- .../examples/benchmark/stlc-sub/stlc-sub-2.rkt | 11 ++++++++++- .../examples/benchmark/stlc-sub/stlc-sub-3.rkt | 11 ++++++++++- .../examples/benchmark/stlc-sub/stlc-sub-4.rkt | 11 ++++++++++- .../examples/benchmark/stlc-sub/stlc-sub-5.rkt | 13 +++++++++++-- .../examples/benchmark/stlc-sub/stlc-sub-6.rkt | 9 +++++++++ .../examples/benchmark/stlc-sub/stlc-sub-7.rkt | 9 +++++++++ .../examples/benchmark/stlc-sub/stlc-sub-8.rkt | 9 +++++++++ .../examples/benchmark/stlc-sub/stlc-sub-9.rkt | 9 +++++++++ .../examples/benchmark/stlc-sub/stlc-sub-base.rkt | 11 ++++++++++- 19 files changed, 117 insertions(+), 27 deletions(-) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/1.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/1.diff index 3afc1e4438..c5891bf246 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/1.diff +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/1.diff @@ -5,7 +5,7 @@ 106,107d105 < [(subst x x M_x) < M_x] -298a297,300 +307a306,309 > (define small-counter-example > (term ((λ (x int) x) 1))) > (test-equal (check small-counter-example) #f) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/2.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/2.diff index 9ffb86fad4..7c7a8baf90 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/2.diff +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/2.diff @@ -6,9 +6,9 @@ < (λ (x_new τ) (subst (replace M y x_new) x M_x)) --- > (λ (x_new τ) (subst (replace M x_new y) x M_x)) -147a148 +156a157 > -298a300,303 +307a309,312 > (define small-counter-example > (term ((λ (x int) (λ (y int) y)) 1))) > (test-equal (check small-counter-example) #f) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/3.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/3.diff index 1afda48b8f..50cbce2067 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/3.diff +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/3.diff @@ -6,7 +6,7 @@ < ((subst M x M_x) (subst N x M_x))] --- > ((subst N x M_x) (subst M x M_x))] -297a298,301 +306a307,310 > > (define small-counter-example > (term ((λ (x int) (+ 1)) 1))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/4.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/4.diff index 2d83b3abf5..ed5909ec1d 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/4.diff +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/4.diff @@ -6,7 +6,7 @@ < (where x_new ,(variable-not-in (term (x y M)) --- > (where x_new ,(variable-not-in (term M) -298a299,302 +307a308,311 > (define small-counter-example > (term ((λ (z int) (((λ (y1 int) (λ (y int) y)) z) 1)) 0))) > (test-equal (check small-counter-example) #f) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/5.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/5.diff index 72d3c27d71..ddf3e79e4f 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/5.diff +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/5.diff @@ -6,8 +6,8 @@ < [(subst x x M_x) --- > [(subst x y M_x) -298a299,302 +307a308,311 > (define small-counter-example -> (term (λ (x int) ((λ (x int) x) x)))) +> (term ((λ (x int) (λ (y (list int)) (hd y))) 1))) > (test-equal (check small-counter-example) #f) > diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/6.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/6.diff index 4bc719bca4..59e5bfc0ac 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/6.diff +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/6.diff @@ -5,7 +5,7 @@ 106,107d105 < [(subst x x M_x) < M_x] -272,294c270,281 +281,303c279,290 < ;; rewrite all βv redexes already in the term < ;; (but not any new ones that might appear) < (define-metafunction stlc @@ -25,7 +25,7 @@ < (and (equal? N-type M-type) < (let ([a1 (Eval M)] [a2 (Eval N)]) < (and (not (string? a1)) (not (string? a2)) -< (equal? a1 a2) +< (equal? (term (answer ,a1)) (term (answer ,a2))) < (or (equal? a1 'error) < (and (equal? (type-check a1) M-type) < (equal? (type-check a2) M-type))))))))))) @@ -42,7 +42,7 @@ > (or (equal? red-t "error") > (let ([red-type (type-check red-t)]) > (equal? t-type red-type)))))))))) -298a286,289 +307a295,298 > (define small-counter-example > (term ((λ (x int) x) 1))) > (test-equal (check small-counter-example) #f) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/7.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/7.diff index fbe927b69e..2615be0cba 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/7.diff +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/7.diff @@ -6,9 +6,9 @@ < (λ (x_new τ) (subst (replace M y x_new) x M_x)) --- > (λ (x_new τ) (subst (replace M x_new y) x M_x)) -147a148 +156a157 > -272,294c273,284 +281,303c282,293 < ;; rewrite all βv redexes already in the term < ;; (but not any new ones that might appear) < (define-metafunction stlc @@ -28,7 +28,7 @@ < (and (equal? N-type M-type) < (let ([a1 (Eval M)] [a2 (Eval N)]) < (and (not (string? a1)) (not (string? a2)) -< (equal? a1 a2) +< (equal? (term (answer ,a1)) (term (answer ,a2))) < (or (equal? a1 'error) < (and (equal? (type-check a1) M-type) < (equal? (type-check a2) M-type))))))))))) @@ -45,7 +45,7 @@ > (or (equal? red-t "error") > (let ([red-type (type-check red-t)]) > (equal? t-type red-type)))))))))) -298a289,292 +307a298,301 > (define small-counter-example > (term ((λ (x int) (λ (y int) y)) 1))) > (test-equal (check small-counter-example) #f) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/8.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/8.diff index ad67de0435..f3b540db85 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/8.diff +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/8.diff @@ -6,7 +6,7 @@ < ((subst M x M_x) (subst N x M_x))] --- > ((subst N x M_x) (subst M x M_x))] -272,294c272,283 +281,303c281,292 < ;; rewrite all βv redexes already in the term < ;; (but not any new ones that might appear) < (define-metafunction stlc @@ -26,7 +26,7 @@ < (and (equal? N-type M-type) < (let ([a1 (Eval M)] [a2 (Eval N)]) < (and (not (string? a1)) (not (string? a2)) -< (equal? a1 a2) +< (equal? (term (answer ,a1)) (term (answer ,a2))) < (or (equal? a1 'error) < (and (equal? (type-check a1) M-type) < (equal? (type-check a2) M-type))))))))))) @@ -43,7 +43,7 @@ > (or (equal? red-t "error") > (let ([red-type (type-check red-t)]) > (equal? t-type red-type)))))))))) -297a287,290 +306a296,299 > > (define small-counter-example > (term ((λ (x int) (+ 1)) 1))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/9.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/9.diff index 5fa3b595ec..f18451b12c 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/9.diff +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/9.diff @@ -6,7 +6,7 @@ < [(subst x x M_x) --- > [(subst x y M_x) -272,294c272,283 +281,303c281,292 < ;; rewrite all βv redexes already in the term < ;; (but not any new ones that might appear) < (define-metafunction stlc @@ -26,7 +26,7 @@ < (and (equal? N-type M-type) < (let ([a1 (Eval M)] [a2 (Eval N)]) < (and (not (string? a1)) (not (string? a2)) -< (equal? a1 a2) +< (equal? (term (answer ,a1)) (term (answer ,a2))) < (or (equal? a1 'error) < (and (equal? (type-check a1) M-type) < (equal? (type-check a2) M-type))))))))))) @@ -43,7 +43,7 @@ > (or (equal? red-t "error") > (let ([red-type (type-check red-t)]) > (equal? t-type red-type)))))))))) -298a288,291 +307a297,300 > (define small-counter-example > (term ((λ (a (list int)) (λ (x int) x)) nil))) > (test-equal (check small-counter-example) #f) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-1.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-1.rkt index 48654353ba..1bf07508fb 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-1.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-1.rkt @@ -143,6 +143,15 @@ [else (error 'Eval "argument doesn't typecheck: ~s" M)])) +(define-metafunction stlc + answer : any -> any + [(answer (λ (x τ) M)) λ] + [(answer c) c] + [(answer (cons v)) λ] + [(answer ((cons v_1) v_2)) cons] + [(answer (+ v)) λ] + [(answer error) error]) + (define x? (redex-match stlc x)) (define v? (redex-match? stlc v)) @@ -286,7 +295,7 @@ (and (equal? N-type M-type) (let ([a1 (Eval M)] [a2 (Eval N)]) (and (not (string? a1)) (not (string? a2)) - (equal? a1 a2) + (equal? (term (answer ,a1)) (term (answer ,a2))) (or (equal? a1 'error) (and (equal? (type-check a1) M-type) (equal? (type-check a2) M-type))))))))))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-2.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-2.rkt index c3e73edcc2..7c5ee23c84 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-2.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-2.rkt @@ -145,6 +145,15 @@ [else (error 'Eval "argument doesn't typecheck: ~s" M)])) +(define-metafunction stlc + answer : any -> any + [(answer (λ (x τ) M)) λ] + [(answer c) c] + [(answer (cons v)) λ] + [(answer ((cons v_1) v_2)) cons] + [(answer (+ v)) λ] + [(answer error) error]) + (define x? (redex-match stlc x)) @@ -289,7 +298,7 @@ (and (equal? N-type M-type) (let ([a1 (Eval M)] [a2 (Eval N)]) (and (not (string? a1)) (not (string? a2)) - (equal? a1 a2) + (equal? (term (answer ,a1)) (term (answer ,a2))) (or (equal? a1 'error) (and (equal? (type-check a1) M-type) (equal? (type-check a2) M-type))))))))))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-3.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-3.rkt index f6b9c8be9e..ca46184a00 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-3.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-3.rkt @@ -145,6 +145,15 @@ [else (error 'Eval "argument doesn't typecheck: ~s" M)])) +(define-metafunction stlc + answer : any -> any + [(answer (λ (x τ) M)) λ] + [(answer c) c] + [(answer (cons v)) λ] + [(answer ((cons v_1) v_2)) cons] + [(answer (+ v)) λ] + [(answer error) error]) + (define x? (redex-match stlc x)) (define v? (redex-match? stlc v)) @@ -288,7 +297,7 @@ (and (equal? N-type M-type) (let ([a1 (Eval M)] [a2 (Eval N)]) (and (not (string? a1)) (not (string? a2)) - (equal? a1 a2) + (equal? (term (answer ,a1)) (term (answer ,a2))) (or (equal? a1 'error) (and (equal? (type-check a1) M-type) (equal? (type-check a2) M-type))))))))))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-4.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-4.rkt index d15f0348d1..fc5ace3754 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-4.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-4.rkt @@ -145,6 +145,15 @@ [else (error 'Eval "argument doesn't typecheck: ~s" M)])) +(define-metafunction stlc + answer : any -> any + [(answer (λ (x τ) M)) λ] + [(answer c) c] + [(answer (cons v)) λ] + [(answer ((cons v_1) v_2)) cons] + [(answer (+ v)) λ] + [(answer error) error]) + (define x? (redex-match stlc x)) (define v? (redex-match? stlc v)) @@ -288,7 +297,7 @@ (and (equal? N-type M-type) (let ([a1 (Eval M)] [a2 (Eval N)]) (and (not (string? a1)) (not (string? a2)) - (equal? a1 a2) + (equal? (term (answer ,a1)) (term (answer ,a2))) (or (equal? a1 'error) (and (equal? (type-check a1) M-type) (equal? (type-check a2) M-type))))))))))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-5.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-5.rkt index af9ec23c93..c5430ec671 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-5.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-5.rkt @@ -145,6 +145,15 @@ [else (error 'Eval "argument doesn't typecheck: ~s" M)])) +(define-metafunction stlc + answer : any -> any + [(answer (λ (x τ) M)) λ] + [(answer c) c] + [(answer (cons v)) λ] + [(answer ((cons v_1) v_2)) cons] + [(answer (+ v)) λ] + [(answer error) error]) + (define x? (redex-match stlc x)) (define v? (redex-match? stlc v)) @@ -288,7 +297,7 @@ (and (equal? N-type M-type) (let ([a1 (Eval M)] [a2 (Eval N)]) (and (not (string? a1)) (not (string? a2)) - (equal? a1 a2) + (equal? (term (answer ,a1)) (term (answer ,a2))) (or (equal? a1 'error) (and (equal? (type-check a1) M-type) (equal? (type-check a2) M-type))))))))))) @@ -297,7 +306,7 @@ (generate-term stlc M #:i-th (pick-an-index 0.035))) (define small-counter-example - (term (λ (x int) ((λ (x int) x) x)))) + (term ((λ (x int) (λ (y (list int)) (hd y))) 1))) (test-equal (check small-counter-example) #f) (define (ordered-enum-generator) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-6.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-6.rkt index f4d204ee96..dccc1a074e 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-6.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-6.rkt @@ -143,6 +143,15 @@ [else (error 'Eval "argument doesn't typecheck: ~s" M)])) +(define-metafunction stlc + answer : any -> any + [(answer (λ (x τ) M)) λ] + [(answer c) c] + [(answer (cons v)) λ] + [(answer ((cons v_1) v_2)) cons] + [(answer (+ v)) λ] + [(answer error) error]) + (define x? (redex-match stlc x)) (define v? (redex-match? stlc v)) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-7.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-7.rkt index 267191fb9e..765e724f4a 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-7.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-7.rkt @@ -145,6 +145,15 @@ [else (error 'Eval "argument doesn't typecheck: ~s" M)])) +(define-metafunction stlc + answer : any -> any + [(answer (λ (x τ) M)) λ] + [(answer c) c] + [(answer (cons v)) λ] + [(answer ((cons v_1) v_2)) cons] + [(answer (+ v)) λ] + [(answer error) error]) + (define x? (redex-match stlc x)) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-8.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-8.rkt index 3defe6114d..29886a7882 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-8.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-8.rkt @@ -145,6 +145,15 @@ [else (error 'Eval "argument doesn't typecheck: ~s" M)])) +(define-metafunction stlc + answer : any -> any + [(answer (λ (x τ) M)) λ] + [(answer c) c] + [(answer (cons v)) λ] + [(answer ((cons v_1) v_2)) cons] + [(answer (+ v)) λ] + [(answer error) error]) + (define x? (redex-match stlc x)) (define v? (redex-match? stlc v)) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-9.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-9.rkt index 8e2934c4d0..aa4562ff22 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-9.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-9.rkt @@ -145,6 +145,15 @@ [else (error 'Eval "argument doesn't typecheck: ~s" M)])) +(define-metafunction stlc + answer : any -> any + [(answer (λ (x τ) M)) λ] + [(answer c) c] + [(answer (cons v)) λ] + [(answer ((cons v_1) v_2)) cons] + [(answer (+ v)) λ] + [(answer error) error]) + (define x? (redex-match stlc x)) (define v? (redex-match? stlc v)) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-base.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-base.rkt index 0c6df2ed9f..a5941bd9b9 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-base.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-base.rkt @@ -145,6 +145,15 @@ [else (error 'Eval "argument doesn't typecheck: ~s" M)])) +(define-metafunction stlc + answer : any -> any + [(answer (λ (x τ) M)) λ] + [(answer c) c] + [(answer (cons v)) λ] + [(answer ((cons v_1) v_2)) cons] + [(answer (+ v)) λ] + [(answer error) error]) + (define x? (redex-match stlc x)) (define v? (redex-match? stlc v)) @@ -288,7 +297,7 @@ (and (equal? N-type M-type) (let ([a1 (Eval M)] [a2 (Eval N)]) (and (not (string? a1)) (not (string? a2)) - (equal? a1 a2) + (equal? (term (answer ,a1)) (term (answer ,a2))) (or (equal? a1 'error) (and (equal? (type-check a1) M-type) (equal? (type-check a2) M-type)))))))))))