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

remove the "variable not a prefix" side-condition from the r6rs model

Browse Source
This commit is contained in:
Robby Findler 2014-05-24 17:01:35 -05:00
parent 747b5cd46e
commit 5c2c3c65ff
2 changed files with 130 additions and 128 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
pkgs/redex-pkgs/redex-examples/redex/examples/r6rs/r6rs-tests.rkt
View File

@ -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)

241
pkgs/redex-pkgs/redex-examples/redex/examples/r6rs/r6rs.rkt
View File

@ -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*))