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

Redex: fix a small bug in the list-machine example

Browse Source
This commit is contained in:
Burke Fetscher 2013-05-16 17:39:25 -05:00
parent a8d981230c
commit d001abc5dd
2 changed files with 7 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
collects/redex/examples/list-machine/list-machine-typing.rkt
View File

@ -92,7 +92,7 @@
[(:lookup Γ v (listcons τ)) (:set Γ v_2 (list τ) Γ_2) [(:lookup Γ v (listcons τ)) (:set Γ v_2 (list τ) Γ_2)
----- -----
(check-instr Π Γ (fetch-field v 1 v_2) Γ_2)] (check-instr Π Γ (fetch-field v 1 v_2) Γ_2)]
[(:lookup Γ v_0 τ_0) (:lookup Γ v_0 τ_1) [(:lookup Γ v_0 τ_0) (:lookup Γ v_1 τ_1)
(⊔ (list τ_0) τ_1 (list τ)) (:set Γ v (listcons τ) Γ_2) (⊔ (list τ_0) τ_1 (list τ)) (:set Γ v (listcons τ) Γ_2)
----- -----
(check-instr Π Γ (cons v_0 v_1 v) Γ_2)]) (check-instr Π Γ (cons v_0 v_1 v) Γ_2)])

6
collects/redex/examples/list-machine/test.rkt
View File

@ -132,6 +132,12 @@
(y : (list (list nil)) (y : (list (list nil))
(z : (listcons (list nil)) (z : (listcons (list nil))
empty)))))) empty))))))
(test-equal (judgment-holds (check-instr
(l0 : (v0 : nil empty) empty)
(v0 : nil empty)
(cons v0 x f)
Γ))
#f)
(test-equal (judgment-holds (check-block empty empty halt)) #t) (test-equal (judgment-holds (check-block empty empty halt)) #t)
(test-equal (judgment-holds (check-block empty (test-equal (judgment-holds (check-block empty