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

add small counter examples to list machine

Browse Source 
Also include test cases that show that the counter
examples type check
This commit is contained in:
Robby Findler 2014-03-21 16:26:04 -05:00
parent bd3aaa0ff7
commit 29fe17729b
6 changed files with 45 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/1.diff
View File

@ -26,3 +26,11 @@
< [(:lookup-Γ Γ v_0 τ_0) (:lookup-Γ Γ v_1 τ_1)
---
> [(:lookup-Γ Γ v_0 τ_0) (:lookup-Γ Γ v_0 τ_1)
449a454,460
>
> (define small-counter-example
> (term (l0 : (begin (cons v0 Z v0) halt) end)))
> (test-equal (check small-counter-example) #f)
> (test-equal (judgment-holds (check-program ,small-counter-example
> (l0 : (v0 : nil empty) empty)))
> #t)

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

@ -30,3 +30,11 @@
> ;; 20 is a small number, but some terms can get exponentially large
> (or stopped
> (empty? closure)
449a454,460
>
> (define small-counter-example
> (term (l0 : (begin (cons v0 v0 v0) halt) end)))
> (test-equal (check small-counter-example) #f)
> (test-equal (judgment-holds (check-program ,small-counter-example
> (l0 : (v0 : nil empty) empty)))
> #t)

8
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/3.diff
View File

@ -6,3 +6,11 @@
< (p r_2 ι)
---
> (p r ι)
449a450,456
>
> (define small-counter-example
> (term (l0 : (begin (cons v0 v0 v0) (begin (fetch-field v0 1 v0) halt)) end)))
> (test-equal (check small-counter-example) #f)
> (test-equal (judgment-holds (check-program ,small-counter-example
> (l0 : (v0 : nil empty) empty)))
> #t)

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

@ -451,3 +451,10 @@
halt))
(loop : (jump loop)
end)))))
(define small-counter-example
(term (l0 : (begin (cons v0 Z v0) halt) end)))
(test-equal (check small-counter-example) #f)
(test-equal (judgment-holds (check-program ,small-counter-example
(l0 : (v0 : nil empty) empty)))
#t)

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

@ -451,3 +451,10 @@
halt))
(loop : (jump loop)
end)))))
(define small-counter-example
(term (l0 : (begin (cons v0 v0 v0) halt) end)))
(test-equal (check small-counter-example) #f)
(test-equal (judgment-holds (check-program ,small-counter-example
(l0 : (v0 : nil empty) empty)))
#t)

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

@ -447,3 +447,10 @@
halt))
(loop : (jump loop)
end)))))
(define small-counter-example
(term (l0 : (begin (cons v0 v0 v0) (begin (fetch-field v0 1 v0) halt)) end)))
(test-equal (check small-counter-example) #f)
(test-equal (judgment-holds (check-program ,small-counter-example
(l0 : (v0 : nil empty) empty)))
#t)