diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/r6rs/r6rs-tests.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/r6rs/r6rs-tests.rkt index 14d1f20c24..621aa14fcf 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/r6rs/r6rs-tests.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/r6rs/r6rs-tests.rkt @@ -91,15 +91,14 @@ [`(unknown ,str) actual] [`(uncaught-exception ,v) actual] [`(store ,xs ...) - (let loop ([actual actual]) - (subst-:-vars actual))] + (subst-:-vars actual)] [_ (error 'rewrite-actual "unknown actual ~s\n" actual)])) (define (subst-:-vars exp) (match exp [`(store ,str ,exps ...) - (let* ([pp-var? (λ (x) (regexp-match #rx"^[qmi]p" (format "~a" (car x))))] + (let* ([pp-var? (λ (x) (regexp-match #rx"^([(]-)?[qmi]p" (format "~a" (car x))))] [pp-bindings (filter pp-var? str)] [with-out-pp (fp-sub pp-bindings `(store ,(filter (λ (x) (not (pp-var? x))) str) ,@exps))] [with-out-app-vars (remove-unassigned-app-vars with-out-pp)] @@ -108,7 +107,11 @@ [`(unknown ,string) string] [_ (error 'subst-:-vars "unknown exp ~s" exp)])) -(define (is-ri-var? x) (regexp-match #rx"^ri" (symbol->string x))) +(define (is-ri-var? x) + (or (and (symbol? x) (regexp-match #rx"^r" (symbol->string x))) + (and (pair? x) + (symbol? (car x)) + (regexp-match #rx"^-i" (symbol->string (car x)))))) (define (remove-unused-ri-vars exp) (match exp @@ -116,7 +119,7 @@ (let ([ri-vars (filter is-ri-var? (map car str))] [str-without-ri-binders (filter (λ (binding) (not (is-ri-var? (car binding)))) str)]) - `(store ,(filter (λ (binding) + `(store ,(filter (λ (binding) (cond [(is-ri-var? (car binding)) (not (not-in (car binding) (cons str-without-ri-binders exps)))] @@ -139,12 +142,12 @@ (cond [(pair? e) (and (not-in var (car e)) (not-in var (cdr e)))] - [else (not (eq? var e))])) + [else (not (equal? var e))])) (define (appears-in-set? x e) (let loop ([e e]) (match e - [`(set! ,x2 ,e2) (or (eq? x x2) + [`(set! ,x2 ,e2) (or (equal? x x2) (loop e2))] [else (and (list? e) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/r6rs/r6rs.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/r6rs/r6rs.rkt index fcb8e5ec88..f9d686f06d 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/r6rs/r6rs.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/r6rs/r6rs.rkt @@ -78,38 +78,37 @@ ; pair pointers, both mutable and immutable (pp ip mp) - (ip (variable-prefix ip)) - (mp (variable-prefix mp)) + (ip (-ip x)) + (mp (-mp x)) (sym (variable-except dot)) - (x (side-condition - (name var_none - (variable-except - dot ; the . in dotted pairs - lambda if loc set! ; core syntax names - quote - begin begin0 - - null ; non-function values - unspecified - pair closure - - error ; signal an error - - letrec letrec* l! reinit - - procedure? condition? - cons consi pair? null? car cdr ; list functions - set-car! set-cdr! list - + - * / ; math functions - call/cc throw dw dynamic-wind ; call/cc functions - values call-with-values ; values functions - apply eqv? - - with-exception-handler handlers - raise-continuable raise make-cond)) - (not (pp? (term var_none))))) + (x (variable-except + dot ; the . in dotted pairs + lambda if loc set! ; core syntax names + quote + begin begin0 + + null ; non-function values + unspecified + pair closure + + error ; signal an error + + letrec letrec* l! reinit + + procedure? condition? + cons consi pair? null? car cdr ; list functions + set-car! set-cdr! list + + - * / ; math functions + call/cc throw dw dynamic-wind ; call/cc functions + values call-with-values ; values functions + apply eqv? + + with-exception-handler handlers + raise-continuable raise make-cond + -ip -mp)) + (cansub x pp) (n number) @@ -255,14 +254,14 @@ "6listn") (--> (store (sf_1 ...) (in-hole E_1 (cons v_1 v_2))) - (store (sf_1 ... (mp (cons v_1 v_2))) (in-hole E_1 mp)) + (store (sf_1 ... ((-mp x) (cons v_1 v_2))) (in-hole E_1 (-mp x))) "6cons" - (fresh mp)) + (fresh x)) (--> (store (sf_1 ...) (in-hole E_1 (consi v_1 v_2))) - (store (sf_1 ... (ip (cons v_1 v_2))) (in-hole E_1 ip)) + (store (sf_1 ... ((-ip x) (cons v_1 v_2))) (in-hole E_1 (-ip x))) "6consi" - (fresh ip)) + (fresh x)) ;; car (--> (store (sf_1 ... (pp_i (cons v_1 v_2)) sf_2 ...) (in-hole E_1 (car pp_i))) @@ -806,115 +805,115 @@ Underspecification)) (define-metafunction lang - + ;; variable cases - [(r6rs-subst-one (variable_1 e_1 variable_1)) e_1] - [(r6rs-subst-one (variable_1 e_1 variable_2)) variable_2] + [(r6rs-subst-one (cansub_1 e_1 cansub_1)) e_1] + [(r6rs-subst-one (cansub_1 e_1 cansub_2)) cansub_2] ;; dont substitute inside quoted expressions - [(r6rs-subst-one (variable_1 e_1 'any_1)) 'any_1] + [(r6rs-subst-one (cansub_1 e_1 'any_1)) 'any_1] ;; when the lambda/letrec binds the variable, stop stubstituting - [(r6rs-subst-one (variable_1 e (lambda (variable_2 ... variable_1 variable_3 ...) e_2 e_3 ...))) - (lambda (variable_2 ... variable_1 variable_3 ...) e_2 e_3 ...) - (side-condition (not (memq (term variable_1) (term (variable_2 ...)))))] - [(r6rs-subst-one (variable_1 e (lambda (variable_2 ... dot variable_1) e_2 e_3 ...))) - (lambda (variable_2 ... dot variable_1) e_2 e_3 ...)] - [(r6rs-subst-one (variable_1 e (lambda (variable_2 ... variable_1 variable_3 ... dot variable_4) e_2 e_3 ...))) - (lambda (variable_2 ... variable_1 variable_3 ... dot variable_4) e_2 e_3 ...) - (side-condition (not (memq (term variable_1) (term (variable_2 ...)))))] - [(r6rs-subst-one (variable_1 e (lambda variable_1 e_2 e_3 ...))) - (lambda variable_1 e_2 e_3 ...)] - [(r6rs-subst-one (variable_1 e (letrec ([variable_2 e_2] ... [variable_1 e_1] [variable_3 e_3] ...) e_4 e_5 ...))) - (letrec ([variable_2 e_2] ... [variable_1 e_1] [variable_3 e_3] ...) e_4 e_5 ...) - (side-condition (not (memq (term variable_1) (term (variable_2 ...)))))] - [(r6rs-subst-one (variable_1 e (letrec* ([variable_2 e_2] ... [variable_1 e_1] [variable_3 e_3] ...) e_4 e_5 ...))) - (letrec* ([variable_2 e_2] ... [variable_1 e_1] [variable_3 e_3] ...) e_4 e_5 ...) - (side-condition (not (memq (term variable_1) (term (variable_2 ...)))))] + [(r6rs-subst-one (cansub_1 e (lambda (cansub_2 ... cansub_1 cansub_3 ...) e_2 e_3 ...))) + (lambda (cansub_2 ... cansub_1 cansub_3 ...) e_2 e_3 ...) + (side-condition (not (memq (term cansub_1) (term (cansub_2 ...)))))] + [(r6rs-subst-one (cansub_1 e (lambda (cansub_2 ... dot cansub_1) e_2 e_3 ...))) + (lambda (cansub_2 ... dot cansub_1) e_2 e_3 ...)] + [(r6rs-subst-one (cansub_1 e (lambda (cansub_2 ... cansub_1 cansub_3 ... dot cansub_4) e_2 e_3 ...))) + (lambda (cansub_2 ... cansub_1 cansub_3 ... dot cansub_4) e_2 e_3 ...) + (side-condition (not (memq (term cansub_1) (term (cansub_2 ...)))))] + [(r6rs-subst-one (cansub_1 e (lambda cansub_1 e_2 e_3 ...))) + (lambda cansub_1 e_2 e_3 ...)] + [(r6rs-subst-one (cansub_1 e (letrec ([cansub_2 e_2] ... [cansub_1 e_1] [cansub_3 e_3] ...) e_4 e_5 ...))) + (letrec ([cansub_2 e_2] ... [cansub_1 e_1] [cansub_3 e_3] ...) e_4 e_5 ...) + (side-condition (not (memq (term cansub_1) (term (cansub_2 ...)))))] + [(r6rs-subst-one (cansub_1 e (letrec* ([cansub_2 e_2] ... [cansub_1 e_1] [cansub_3 e_3] ...) e_4 e_5 ...))) + (letrec* ([cansub_2 e_2] ... [cansub_1 e_1] [cansub_3 e_3] ...) e_4 e_5 ...) + (side-condition (not (memq (term cansub_1) (term (cansub_2 ...)))))] ;; next 3 cases: we know no capture can occur, so we just recur - [(r6rs-subst-one (variable_1 e_1 (lambda (variable_2 ...) e_2 e_3 ...))) - (lambda (variable_2 ...) - (r6rs-subst-one (variable_1 e_1 e_2)) - (r6rs-subst-one (variable_1 e_1 e_3)) ...) + [(r6rs-subst-one (cansub_1 e_1 (lambda (cansub_2 ...) e_2 e_3 ...))) + (lambda (cansub_2 ...) + (r6rs-subst-one (cansub_1 e_1 e_2)) + (r6rs-subst-one (cansub_1 e_1 e_3)) ...) (side-condition (andmap (λ (x) (equal? (variable-not-in (term e_1) x) x)) - (term (variable_2 ...))))] - [(r6rs-subst-one (variable_1 e_1 (lambda (variable_2 ... dot variable_3) e_2 e_3 ...))) - (lambda (variable_2 ...) - (r6rs-subst-one (variable_1 e_1 e_2)) - (r6rs-subst-one (variable_1 e_1 e_3)) ...) + (term (cansub_2 ...))))] + [(r6rs-subst-one (cansub_1 e_1 (lambda (cansub_2 ... dot cansub_3) e_2 e_3 ...))) + (lambda (cansub_2 ...) + (r6rs-subst-one (cansub_1 e_1 e_2)) + (r6rs-subst-one (cansub_1 e_1 e_3)) ...) (side-condition (andmap (λ (x) (equal? (variable-not-in (term e_1) x) x)) - (term (variable_2 ... variable_3))))] - [(r6rs-subst-one (variable_1 e_1 (lambda variable_2 e_2 e_3 ...))) - (lambda variable_2 - (r6rs-subst-one (variable_1 e_1 e_2)) - (r6rs-subst-one (variable_1 e_1 e_3)) ...) - (side-condition (equal? (variable-not-in (term e_1) (term variable_2)) - (term variable_2)))] - [(r6rs-subst-one (variable_1 e_1 (letrec ([variable_2 e_2] ...) e_3 e_4 ...))) - (letrec ([variable_2 (r6rs-subst-one (variable_1 e_1 e_2))] ...) - (r6rs-subst-one (variable_1 e_1 e_3)) - (r6rs-subst-one (variable_1 e_1 e_4)) ...) + (term (cansub_2 ... cansub_3))))] + [(r6rs-subst-one (cansub_1 e_1 (lambda cansub_2 e_2 e_3 ...))) + (lambda cansub_2 + (r6rs-subst-one (cansub_1 e_1 e_2)) + (r6rs-subst-one (cansub_1 e_1 e_3)) ...) + (side-condition (equal? (variable-not-in (term e_1) (term cansub_2)) + (term cansub_2)))] + [(r6rs-subst-one (cansub_1 e_1 (letrec ([cansub_2 e_2] ...) e_3 e_4 ...))) + (letrec ([cansub_2 (r6rs-subst-one (cansub_1 e_1 e_2))] ...) + (r6rs-subst-one (cansub_1 e_1 e_3)) + (r6rs-subst-one (cansub_1 e_1 e_4)) ...) (side-condition (andmap (λ (x) (equal? (variable-not-in (term e_1) x) x)) - (term (variable_2 ...))))] - [(r6rs-subst-one (variable_1 e_1 (letrec* ([variable_2 e_2] ...) e_3 e_4 ...))) - (letrec* ([variable_2 (r6rs-subst-one (variable_1 e_1 e_2))] ...) - (r6rs-subst-one (variable_1 e_1 e_3)) - (r6rs-subst-one (variable_1 e_1 e_4)) ...) + (term (cansub_2 ...))))] + [(r6rs-subst-one (cansub_1 e_1 (letrec* ([cansub_2 e_2] ...) e_3 e_4 ...))) + (letrec* ([cansub_2 (r6rs-subst-one (cansub_1 e_1 e_2))] ...) + (r6rs-subst-one (cansub_1 e_1 e_3)) + (r6rs-subst-one (cansub_1 e_1 e_4)) ...) (side-condition (andmap (λ (x) (equal? (variable-not-in (term e_1) x) x)) - (term (variable_2 ...))))] + (term (cansub_2 ...))))] ;; capture avoiding cases - [(r6rs-subst-one (variable_1 e_1 (lambda (variable_2 ... dot variable_3) e_2 e_3 ...))) - ,(term-let ([(variable_new ... variable_new_dot) (variables-not-in (term (variable_1 e_1 e_2 e_3 ...)) - (term (variable_2 ... variable_3)))]) - (term (lambda (variable_new ... dot variable_new_dot) - (r6rs-subst-one (variable_1 + [(r6rs-subst-one (cansub_1 e_1 (lambda (cansub_2 ... dot cansub_3) e_2 e_3 ...))) + ,(term-let ([(cansub_new ... cansub_new_dot) (variables-not-in (term (cansub_1 e_1 e_2 e_3 ...)) + (term (cansub_2 ... cansub_3)))]) + (term (lambda (cansub_new ... dot cansub_new_dot) + (r6rs-subst-one (cansub_1 e_1 - (r6rs-subst-many ((variable_2 variable_new) ... (variable_3 variable_new_dot) e_2)))) - (r6rs-subst-one (variable_1 + (r6rs-subst-many ((cansub_2 cansub_new) ... (cansub_3 cansub_new_dot) e_2)))) + (r6rs-subst-one (cansub_1 e_1 - (r6rs-subst-many ((variable_2 variable_new) ... (variable_3 variable_new_dot) e_3)))) + (r6rs-subst-many ((cansub_2 cansub_new) ... (cansub_3 cansub_new_dot) e_3)))) ...)))] - [(r6rs-subst-one (variable_1 e_1 (lambda (variable_2 ...) e_2 e_3 ...))) - ,(term-let ([(variable_new ...) (variables-not-in (term (variable_1 e_1 e_2 e_3 ...)) - (term (variable_2 ...)))]) - (term (lambda (variable_new ...) - (r6rs-subst-one (variable_1 e_1 (r6rs-subst-many ((variable_2 variable_new) ... e_2)))) - (r6rs-subst-one (variable_1 e_1 (r6rs-subst-many ((variable_2 variable_new) ... e_3)))) ...)))] - [(r6rs-subst-one (variable_1 e_1 (lambda variable_2 e_2 e_3 ...))) - ,(term-let ([variable_new (variable-not-in (term (variable_1 e_1 e_2 e_3 ...)) - (term variable_2))]) - (term (lambda variable_new - (r6rs-subst-one (variable_1 e_1 (r6rs-subst-one (variable_2 variable_new e_2)))) - (r6rs-subst-one (variable_1 e_1 (r6rs-subst-one (variable_2 variable_new e_3)))) ...)))] - [(r6rs-subst-one (variable_1 e_1 (letrec ([variable_2 e_2] ...) e_3 e_4 ...))) - ,(term-let ([(variable_new ...) (variables-not-in (term (variable_1 e_1 e_2 ... e_3 e_4 ...)) - (term (variable_2 ...)))]) - (term (letrec ([variable_new (r6rs-subst-one - (variable_1 - e_1 - (r6rs-subst-many ((variable_2 variable_new) ... e_2))))] ...) - (r6rs-subst-one (variable_1 e_1 (r6rs-subst-many ((variable_2 variable_new) ... e_3)))) - (r6rs-subst-one (variable_1 e_1 (r6rs-subst-many ((variable_2 variable_new) ... e_4)))) ...)))] - [(r6rs-subst-one (variable_1 e_1 (letrec* ([variable_2 e_2] ...) e_3 e_4 ...))) - ,(term-let ([(variable_new ...) (variables-not-in (term (variable_1 e_1 e_2 ... e_3 e_4 ...)) - (term (variable_2 ...)))]) - (term (letrec* ([variable_new (r6rs-subst-one - (variable_1 - e_1 - (r6rs-subst-many ((variable_2 variable_new) ... e_2))))] ...) - (r6rs-subst-one (variable_1 e_1 (r6rs-subst-many ((variable_2 variable_new) ... e_3)))) - (r6rs-subst-one (variable_1 e_1 (r6rs-subst-many ((variable_2 variable_new) ... e_4)))) ...)))] + [(r6rs-subst-one (cansub_1 e_1 (lambda (cansub_2 ...) e_2 e_3 ...))) + ,(term-let ([(cansub_new ...) (variables-not-in (term (cansub_1 e_1 e_2 e_3 ...)) + (term (cansub_2 ...)))]) + (term (lambda (cansub_new ...) + (r6rs-subst-one (cansub_1 e_1 (r6rs-subst-many ((cansub_2 cansub_new) ... e_2)))) + (r6rs-subst-one (cansub_1 e_1 (r6rs-subst-many ((cansub_2 cansub_new) ... e_3)))) ...)))] + [(r6rs-subst-one (cansub_1 e_1 (lambda cansub_2 e_2 e_3 ...))) + ,(term-let ([cansub_new (variable-not-in (term (cansub_1 e_1 e_2 e_3 ...)) + (term cansub_2))]) + (term (lambda cansub_new + (r6rs-subst-one (cansub_1 e_1 (r6rs-subst-one (cansub_2 cansub_new e_2)))) + (r6rs-subst-one (cansub_1 e_1 (r6rs-subst-one (cansub_2 cansub_new e_3)))) ...)))] + [(r6rs-subst-one (cansub_1 e_1 (letrec ([cansub_2 e_2] ...) e_3 e_4 ...))) + ,(term-let ([(cansub_new ...) (variables-not-in (term (cansub_1 e_1 e_2 ... e_3 e_4 ...)) + (term (cansub_2 ...)))]) + (term (letrec ([cansub_new (r6rs-subst-one + (cansub_1 + e_1 + (r6rs-subst-many ((cansub_2 cansub_new) ... e_2))))] ...) + (r6rs-subst-one (cansub_1 e_1 (r6rs-subst-many ((cansub_2 cansub_new) ... e_3)))) + (r6rs-subst-one (cansub_1 e_1 (r6rs-subst-many ((cansub_2 cansub_new) ... e_4)))) ...)))] + [(r6rs-subst-one (cansub_1 e_1 (letrec* ([cansub_2 e_2] ...) e_3 e_4 ...))) + ,(term-let ([(cansub_new ...) (variables-not-in (term (cansub_1 e_1 e_2 ... e_3 e_4 ...)) + (term (cansub_2 ...)))]) + (term (letrec* ([cansub_new (r6rs-subst-one + (cansub_1 + e_1 + (r6rs-subst-many ((cansub_2 cansub_new) ... e_2))))] ...) + (r6rs-subst-one (cansub_1 e_1 (r6rs-subst-many ((cansub_2 cansub_new) ... e_3)))) + (r6rs-subst-one (cansub_1 e_1 (r6rs-subst-many ((cansub_2 cansub_new) ... e_4)))) ...)))] ;; last two cases cover all other expressions -- they don't have any variables, ;; so we don't care about their structure. - [(r6rs-subst-one (variable_1 e_1 (any_1 ...))) ((r6rs-subst-one (variable_1 e_1 any_1)) ...)] - [(r6rs-subst-one (variable_1 e_1 any_1)) any_1]) + [(r6rs-subst-one (cansub_1 e_1 (any_1 ...))) ((r6rs-subst-one (cansub_1 e_1 any_1)) ...)] + [(r6rs-subst-one (cansub_1 e_1 any_1)) any_1]) (define-metafunction lang - [(r6rs-subst-many ((variable_1 e_1) (variable_2 e_2) ... e_3)) - (r6rs-subst-one (variable_1 e_1 (r6rs-subst-many ((variable_2 e_2) ... e_3))))] + [(r6rs-subst-many ((cansub_1 e_1) (cansub_2 e_2) ... e_3)) + (r6rs-subst-one (cansub_1 e_1 (r6rs-subst-many ((cansub_2 e_2) ... e_3))))] [(r6rs-subst-many (e_1)) e_1]) (metafunction-type observable (-> a* r*))