From f786f24ac5a95679b46ce506503a966b21f42e4e Mon Sep 17 00:00:00 2001 From: Casey Klein Date: Thu, 24 Jun 2010 14:20:34 -0500 Subject: [PATCH] Makes let-rec verification match the implementation --- collects/redex/examples/racket-machine/verification-test.rkt | 4 ++++ collects/redex/examples/racket-machine/verification.rkt | 2 +- 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/collects/redex/examples/racket-machine/verification-test.rkt b/collects/redex/examples/racket-machine/verification-test.rkt index e241407237..347fddeb03 100644 --- a/collects/redex/examples/racket-machine/verification-test.rkt +++ b/collects/redex/examples/racket-machine/verification-test.rkt @@ -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?) diff --git a/collects/redex/examples/racket-machine/verification.rkt b/collects/redex/examples/racket-machine/verification.rkt index 6c55d629e4..ffebd96855 100644 --- a/collects/redex/examples/racket-machine/verification.rkt +++ b/collects/redex/examples/racket-machine/verification.rkt @@ -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)))