From bc511912a48b2b138057060017744b8c5f2daf7c Mon Sep 17 00:00:00 2001 From: Casey Klein Date: Wed, 23 Jun 2010 14:14:14 -0500 Subject: [PATCH] Makes `let-one' verification match VM --- .../redex/examples/racket-machine/verification-test.rkt | 4 ++++ collects/redex/examples/racket-machine/verification.rkt | 7 +++---- 2 files changed, 7 insertions(+), 4 deletions(-) diff --git a/collects/redex/examples/racket-machine/verification-test.rkt b/collects/redex/examples/racket-machine/verification-test.rkt index 06b32bfc72..e241407237 100644 --- a/collects/redex/examples/racket-machine/verification-test.rkt +++ b/collects/redex/examples/racket-machine/verification-test.rkt @@ -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? diff --git a/collects/redex/examples/racket-machine/verification.rkt b/collects/redex/examples/racket-machine/verification.rkt index 89aeca13d4..6c55d629e4 100644 --- a/collects/redex/examples/racket-machine/verification.rkt +++ b/collects/redex/examples/racket-machine/verification.rkt @@ -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)