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

Fixes substitution bugs

Browse Source
This commit is contained in:
Casey Klein 2010-11-25 13:44:06 -06:00
parent d927bc117e
commit b616ac3cd4
2 changed files with 18 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
collects/redex/examples/delim-cont/meta.rkt
View File

@ -14,7 +14,7 @@
[(subst x_1 x_2 (λ (x_3 ...) e_1)) ; shortcut; x_1 != any x_3
(λ (x_3 ...) (subst x_1 x_2 e_1))]
[(subst x_1 e_1 (λ (x_2 ...) e_2)) ; x_1 != any x_2
,(term-let ([(x_new ...) (variables-not-in (term e_1) (term (x_2 ...)))])
,(term-let ([(x_new ...) (variables-not-in (term (x_1 e_1 e_2)) (term (x_2 ...)))])
(term (λ (x_new ...)
(subst x_1 e_1 (subst* (x_2 ...) (x_new ...) e_2)))))]
[(subst x_1 e_1 x_1) e_1]

19
collects/redex/examples/delim-cont/test.rkt
View File

@ -35,6 +35,21 @@
;; Basic ----------------------------------------
(define (basic-tests)
(test "(λx.e)[y←v] ≠ λy.(e[x←y][y←v])"
'(<>
([k 4]) []
(((λ (k1) (λ (k) k))
(λ () k))
0))
'(<> ([k 4]) [] 0))
(test "(λx.e)[y←v] ≠ λz.(e[x←z][y←v]) if z ∈ FV(e)"
'(<>
([k2 5])
()
(((λ (k1) (λ (k) k2))
(λ () k))
0))
'(<> ([k2 5]) [] 5))
(test "basic dw"
'(<>
() []
@ -995,7 +1010,7 @@
(λ (x) x)))))
hole))
100)
(λ (x) x)))))
(λ (x1) x1)))))
(test "similar way to get stuck, but using the pre thunk"
'(<>
([output (list)]
@ -1059,7 +1074,7 @@
hole))
100)
0)
(λ (x) x)))))
(λ (x1) x1)))))
(test "loop"
'(<>
([counter (list 4 3 2 1 0)])