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

Makes `let-one' verification match VM

Browse Source
This commit is contained in:
Casey Klein 2010-06-23 14:14:14 -05:00
parent 514f4e2e4b
commit bc511912a4
2 changed files with 7 additions and 4 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

@ -77,6 +77,10 @@
(negate bytecode-ok?)
'(let-one (loc 0) 'z))
(test-predicate
(negate bytecode-ok?)
'(let-one (install-value 0 'x 'y) 'z))
;; application
(test-predicate
bytecode-ok?

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

@ -67,10 +67,9 @@
; let-one
[(verify (let-one e_r e_b) (ṽ_1 ...) n_l b γ η f)
(verify e_b (imm ṽ_1* ...) ,(add1 (term n_l)) b γ η (shift 1 f))
(where (s_1 γ_1 η_1) (verify e_r (uninit ṽ_1 ...) ,(add1 (term n_l)) #f γ η ∅))
(side-condition (term (valid? s_1)))
;; MRF: the Racket implementation checks that s_1 starts with uninit
(where (ṽ_1* ...) (trim s_1 (ṽ_1 ...)))]
(where s_0 (uninit ṽ_1 ...))
(where (s_1 γ_1 η_1) (verify e_r s_0 ,(add1 (term n_l)) #f γ η ∅))
(where (uninit ṽ_1* ...) (trim s_1 s_0))]
; seq
[(verify (seq e_0 ... e_n) s n_l b γ η f)