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

fix property to actually use Kleene equality (instead

Browse Source 
of comparing the output of standard reduction)
This commit is contained in:
Robby Findler 2014-03-21 23:21:42 -05:00
parent 29fe17729b
commit 3abb14a63e
19 changed files with 117 additions and 27 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/1.diff
View File

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

4
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/2.diff
View File

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

2
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/3.diff
View File

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

2
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/4.diff
View File

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

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

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

6
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/6.diff
View File

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

8
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/7.diff
View File

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

6
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/8.diff
View File

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

6
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/9.diff
View File

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

11
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-1.rkt
View File

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

11
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-2.rkt
View File

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

11
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-3.rkt
View File

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

11
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-4.rkt
View File

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

13
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-5.rkt
View File

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

9
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-6.rkt
View File

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

9
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-7.rkt
View File

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

9
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-8.rkt
View File

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

9
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-9.rkt
View File

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

11
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-base.rkt
View File

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