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

Makes let-rec verification match the implementation

Browse Source
This commit is contained in:
Casey Klein 2010-06-24 14:20:34 -05:00
parent bc511912a4
commit f786f24ac5
2 changed files with 5 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
collects/redex/examples/racket-machine/verification-test.rkt
View File

@ -390,6 +390,10 @@
(negate bytecode-ok?)
'(let-void 1 (branch #f (let-rec ((lam () (0) 'x)) 'y) (loc-noclr 0))))
(test-predicate
(negate bytecode-ok?)
'(let-void 1 (let-rec ((lam () () 'x)) 'y)))
;; ignored? properly maintained
(test-predicate
(negate bytecode-ok?)

2
collects/redex/examples/racket-machine/verification.rkt
View File

@ -140,7 +140,7 @@
(side-condition (< (term n_p) (term n_l)))]
; let-rec
[(verify (let-rec ((name l (lam ((name v val) ...) (n_0 ...) e_0)) ...) e) (ṽ_0 ... ṽ_n ...) n_l b γ η f)
[(verify (let-rec ((name l (lam ((name v val) ...) (n_0 n_1 ...) e_0)) ...) e) (ṽ_0 ... ṽ_n ...) n_l b γ η f)
(verify e s_1 n_l b γ η f)
(where n ,(length (term (l ...))))
(side-condition (= (length (term (ṽ_0 ...))) (term n)))