fixed things up so that everything is at least compiling now
svn: r10980
This commit is contained in:
Robby Findler
parent
ba4b0b6301
commit
86c7c808d4
|
|
@ -1,6 +1,5 @@
|
||||||
(module arithmetic mzscheme
|
#lang scheme
|
||||||
(require (planet robby/redex:5/reduction-semantics)
|
(require redex)
|
||||||
(planet robby/redex:5/gui))
|
|
||||||
|
|
||||||
(define-language lang
|
(define-language lang
|
||||||
(e (binop e e)
|
(e (binop e e)
|
||||||
|
|
@ -39,4 +38,4 @@
|
||||||
[(--> (in-hole e-ctxt_1 a) (in-hole e-ctxt_1 b))
|
[(--> (in-hole e-ctxt_1 a) (in-hole e-ctxt_1 b))
|
||||||
(c--> a b)]))
|
(c--> a b)]))
|
||||||
|
|
||||||
(traces reductions (term (- (* (sqrt 36) (/ 1 2)) (+ 1 2)))))
|
(traces reductions (term (- (* (sqrt 36) (/ 1 2)) (+ 1 2))))
|
||||||
File diff suppressed because it is too large
Load Diff
|
|
@ -1,57 +1,56 @@
|
||||||
(module church mzscheme
|
#lang scheme
|
||||||
(require (planet robby/redex:5/reduction-semantics)
|
(require redex)
|
||||||
(planet robby/redex:5/gui))
|
|
||||||
|
|
||||||
(reduction-steps-cutoff 100)
|
(reduction-steps-cutoff 100)
|
||||||
|
|
||||||
(define-language lang
|
(define-language lang
|
||||||
(e (lambda (x) e)
|
(e (lambda (x) e)
|
||||||
(let (x e) e)
|
(let (x e) e)
|
||||||
(app e e)
|
(app e e)
|
||||||
(+ e e)
|
(+ e e)
|
||||||
number
|
number
|
||||||
x)
|
x)
|
||||||
(e-ctxt (lambda (x) e-ctxt)
|
(e-ctxt (lambda (x) e-ctxt)
|
||||||
a-ctxt)
|
a-ctxt)
|
||||||
(a-ctxt (let (x a-ctxt) e)
|
(a-ctxt (let (x a-ctxt) e)
|
||||||
(app a-ctxt e)
|
(app a-ctxt e)
|
||||||
(app x a-ctxt)
|
(app x a-ctxt)
|
||||||
hole)
|
hole)
|
||||||
(v (lambda (x) e)
|
(v (lambda (x) e)
|
||||||
x)
|
x)
|
||||||
(x variable))
|
(x variable))
|
||||||
|
|
||||||
(define reductions
|
(define reductions
|
||||||
(reduction-relation
|
(reduction-relation
|
||||||
lang
|
lang
|
||||||
(--> (in-hole e-ctxt_1 (app (lambda (x_1) e_body) e_arg))
|
(--> (in-hole e-ctxt_1 (app (lambda (x_1) e_body) e_arg))
|
||||||
(in-hole e-ctxt_1 (subst (x_1 e_arg e_body))))
|
(in-hole e-ctxt_1 (subst (x_1 e_arg e_body))))
|
||||||
(--> (in-hole e-ctxt_1 (let (x_1 v_1) e_1))
|
(--> (in-hole e-ctxt_1 (let (x_1 v_1) e_1))
|
||||||
(in-hole e-ctxt_1 (subst (x_1 v_1 e_1))))))
|
(in-hole e-ctxt_1 (subst (x_1 v_1 e_1))))))
|
||||||
|
|
||||||
(define-metafunction subst
|
(define-metafunction subst
|
||||||
lang
|
lang
|
||||||
[(x_1 e_1 (lambda (x_1) e_2)) (lambda (x_1) e_2)]
|
[(x_1 e_1 (lambda (x_1) e_2)) (lambda (x_1) e_2)]
|
||||||
[(x_1 e_1 (lambda (x_2) e_2))
|
[(x_1 e_1 (lambda (x_2) e_2))
|
||||||
,(term-let ((x_new (variable-not-in (term e_1) (term x_2))))
|
,(term-let ((x_new (variable-not-in (term e_1) (term x_2))))
|
||||||
(term (lambda (x_new) (subst (x_1 e_1 (subst (x_2 x_new e_2)))))))]
|
(term (lambda (x_new) (subst (x_1 e_1 (subst (x_2 x_new e_2)))))))]
|
||||||
[(x_1 e_1 (let (x_1 e_2) e_3)) (let (x_1 (subst (x_1 e_1 e_2))) e_3)]
|
[(x_1 e_1 (let (x_1 e_2) e_3)) (let (x_1 (subst (x_1 e_1 e_2))) e_3)]
|
||||||
[(x_1 e_1 (let (x_2 e_2) e_3))
|
[(x_1 e_1 (let (x_2 e_2) e_3))
|
||||||
,(term-let ((x_new (variable-not-in (term e_1) (term x_2))))
|
,(term-let ((x_new (variable-not-in (term e_1) (term x_2))))
|
||||||
(term (let (x_2 (subst (x_1 e_1 e_2))) (subst (x_1 e_1 (subst (x_2 x_new e_3)))))))]
|
(term (let (x_2 (subst (x_1 e_1 e_2))) (subst (x_1 e_1 (subst (x_2 x_new e_3)))))))]
|
||||||
[(x_1 e_1 x_1) e_1]
|
[(x_1 e_1 x_1) e_1]
|
||||||
[(x_1 e_1 x_2) x_2]
|
[(x_1 e_1 x_2) x_2]
|
||||||
[(x_1 e_1 (app e_2 e_3)) (app (subst (x_1 e_1 e_2))
|
[(x_1 e_1 (app e_2 e_3)) (app (subst (x_1 e_1 e_2))
|
||||||
(subst (x_1 e_1 e_3)))]
|
(subst (x_1 e_1 e_3)))]
|
||||||
[(x_1 e_1 (+ e_2 e_3)) (+ (subst (x_1 e_1 e_2))
|
[(x_1 e_1 (+ e_2 e_3)) (+ (subst (x_1 e_1 e_2))
|
||||||
(subst (x_1 e_1 e_3)))]
|
(subst (x_1 e_1 e_3)))]
|
||||||
[(x_1 e_1 number_1) number_1])
|
[(x_1 e_1 number_1) number_1])
|
||||||
|
|
||||||
(traces lang reductions
|
(traces lang reductions
|
||||||
'(let (plus (lambda (m)
|
'(let (plus (lambda (m)
|
||||||
(lambda (n)
|
(lambda (n)
|
||||||
(lambda (s)
|
(lambda (s)
|
||||||
(lambda (z)
|
(lambda (z)
|
||||||
(app (app m s) (app (app n s) z)))))))
|
(app (app m s) (app (app n s) z)))))))
|
||||||
(let (two (lambda (s) (lambda (z) (app s (app s z)))))
|
(let (two (lambda (s) (lambda (z) (app s (app s z)))))
|
||||||
(app (app plus two) two)))))
|
(app (app plus two) two))))
|
||||||
|
|
@ -1,90 +1,91 @@
|
||||||
|
#lang scheme
|
||||||
|
|
||||||
;"one point basis"
|
;"one point basis"
|
||||||
;"formal aspects of computing"
|
;"formal aspects of computing"
|
||||||
|
|
||||||
(module combinators mzscheme
|
(require redex)
|
||||||
(require (planet robby/redex:5/reduction-semantics)
|
|
||||||
(planet robby/redex:5/gui))
|
|
||||||
|
|
||||||
(initial-font-size 12)
|
(initial-font-size 12)
|
||||||
(reduction-steps-cutoff 100)
|
(reduction-steps-cutoff 100)
|
||||||
(initial-char-width 80)
|
(initial-char-width 80)
|
||||||
|
|
||||||
(define-language lang
|
(define-language lang
|
||||||
(e (e e)
|
(e (e e)
|
||||||
comb
|
comb
|
||||||
abs1
|
abs1
|
||||||
abs2
|
abs2
|
||||||
abs3)
|
abs3)
|
||||||
(e-ctxt (e e-ctxt)
|
(e-ctxt (e e-ctxt)
|
||||||
(e-ctxt e)
|
(e-ctxt e)
|
||||||
hole)
|
hole)
|
||||||
(comb i
|
(comb i
|
||||||
j
|
j
|
||||||
b
|
b
|
||||||
c
|
c
|
||||||
c*
|
c*
|
||||||
w))
|
w))
|
||||||
|
|
||||||
(define ij-relation
|
(define ij-relation
|
||||||
(reduction-relation
|
(reduction-relation
|
||||||
lang
|
lang
|
||||||
(--> (in-hole e-ctxt_1 (i e_1))
|
(--> (in-hole e-ctxt_1 (i e_1))
|
||||||
(in-hole e-ctxt_1 e_1))
|
(in-hole e-ctxt_1 e_1))
|
||||||
(--> (in-hole e-ctxt_1 ((((j e_a) e_b) e_c) e_d))
|
(--> (in-hole e-ctxt_1 ((((j e_a) e_b) e_c) e_d))
|
||||||
(in-hole e-ctxt_1 ((e_a e_b) ((e_a e_d) e_c))))))
|
(in-hole e-ctxt_1 ((e_a e_b) ((e_a e_d) e_c))))))
|
||||||
|
|
||||||
(define relation
|
(define relation
|
||||||
(union-reduction-relations
|
(union-reduction-relations
|
||||||
ij-relation
|
ij-relation
|
||||||
(reduction-relation
|
(reduction-relation
|
||||||
lang
|
lang
|
||||||
(--> (in-hole e-ctxt_1 (((b e_m) e_n) e_l))
|
(--> (in-hole e-ctxt_1 (((b e_m) e_n) e_l))
|
||||||
(in-hole e-ctxt_1 (e_m (e_n e_l))))
|
(in-hole e-ctxt_1 (e_m (e_n e_l))))
|
||||||
(--> (in-hole e-ctxt_1 (((c e_m) e_n) e_l))
|
(--> (in-hole e-ctxt_1 (((c e_m) e_n) e_l))
|
||||||
(in-hole e-ctxt_1 ((e_m e_l) e_n)))
|
(in-hole e-ctxt_1 ((e_m e_l) e_n)))
|
||||||
(--> (in-hole e-ctxt_1 ((c* e_a) e_b))
|
(--> (in-hole e-ctxt_1 ((c* e_a) e_b))
|
||||||
(in-hole e-ctxt_1 (e_b e_a)))
|
(in-hole e-ctxt_1 (e_b e_a)))
|
||||||
(--> (in-hole e-ctxt_1 ((w e_a) e_b))
|
(--> (in-hole e-ctxt_1 ((w e_a) e_b))
|
||||||
(in-hole e-ctxt_1 ((e_a e_b) e_b))))))
|
(in-hole e-ctxt_1 ((e_a e_b) e_b))))))
|
||||||
|
|
||||||
|
|
||||||
(define c* `((j i) i))
|
(define c* `((j i) i))
|
||||||
(define (make-c c*) `(((j ,c*) (j ,c*)) (j ,c*)))
|
(define (make-c c*) `(((j ,c*) (j ,c*)) (j ,c*)))
|
||||||
(define (make-b c) `((,c ((j i) ,c)) (j i)))
|
(define (make-b c) `((,c ((j i) ,c)) (j i)))
|
||||||
(define (make-w b c c*) `(,c ((,c ((,b ,c) ((,c ((,b j) ,c*)) ,c*))) ,c*)))
|
(define (make-w b c c*) `(,c ((,c ((,b ,c) ((,c ((,b j) ,c*)) ,c*))) ,c*)))
|
||||||
(define (make-s b c w) `((,b ((,b (,b ,w)) ,c)) (,b ,b)))
|
(define (make-s b c w) `((,b ((,b (,b ,w)) ,c)) (,b ,b)))
|
||||||
|
|
||||||
(traces/multiple lang
|
(traces lang
|
||||||
relation
|
relation
|
||||||
(list
|
(list
|
||||||
`((,c* abs1) abs2)
|
`((,c* abs1) abs2)
|
||||||
`(((,(make-c 'c*) abs1) abs2) abs3)
|
`(((,(make-c 'c*) abs1) abs2) abs3)
|
||||||
`(((,(make-b 'c) abs1) abs2) abs3)
|
`(((,(make-b 'c) abs1) abs2) abs3)
|
||||||
`((,(make-w 'b 'c 'c*) abs1) abs2)
|
`((,(make-w 'b 'c 'c*) abs1) abs2)
|
||||||
`(((,(make-s 'b 'c 'w) abs1) abs2) abs3)))
|
`(((,(make-s 'b 'c 'w) abs1) abs2) abs3))
|
||||||
|
#:multiple #t)
|
||||||
|
|
||||||
(require (lib "pretty.ss"))
|
(require (lib "pretty.ss"))
|
||||||
#;
|
#;
|
||||||
(let loop ([t (make-s (make-b (make-c c*))
|
(let loop ([t (make-s (make-b (make-c c*))
|
||||||
|
(make-c c*)
|
||||||
|
(make-w (make-b (make-c c*))
|
||||||
|
(make-c c*)
|
||||||
|
c*))]
|
||||||
|
[i 0])
|
||||||
|
(when (zero? (modulo i 100))
|
||||||
|
(display i)
|
||||||
|
(display " ")
|
||||||
|
(flush-output))
|
||||||
|
(let ([next (apply-reduction-relation ij-relation t)])
|
||||||
|
(if (null? next)
|
||||||
|
(begin (newline)
|
||||||
|
(pretty-print t))
|
||||||
|
(loop (car next) (+ i 1)))))
|
||||||
|
|
||||||
|
#;
|
||||||
|
(traces lang ij-relation
|
||||||
|
(make-s (make-b (make-c c*))
|
||||||
|
(make-c c*)
|
||||||
|
(make-w (make-b (make-c c*))
|
||||||
(make-c c*)
|
(make-c c*)
|
||||||
(make-w (make-b (make-c c*))
|
c*)))
|
||||||
(make-c c*)
|
|
||||||
c*))]
|
|
||||||
[i 0])
|
|
||||||
(when (zero? (modulo i 100))
|
|
||||||
(display i)
|
|
||||||
(display " ")
|
|
||||||
(flush-output))
|
|
||||||
(let ([next (apply-reduction-relation ij-relation t)])
|
|
||||||
(if (null? next)
|
|
||||||
(begin (newline)
|
|
||||||
(pretty-print t))
|
|
||||||
(loop (car next) (+ i 1)))))
|
|
||||||
|
|
||||||
#;
|
|
||||||
(traces lang ij-relation
|
|
||||||
(make-s (make-b (make-c c*))
|
|
||||||
(make-c c*)
|
|
||||||
(make-w (make-b (make-c c*))
|
|
||||||
(make-c c*)
|
|
||||||
c*))))
|
|
||||||
|
|
@ -1,18 +1,17 @@
|
||||||
(module compatible-closure mzscheme
|
#lang scheme
|
||||||
(require (planet robby/redex:5/reduction-semantics)
|
(require redex)
|
||||||
(planet robby/redex:5/gui))
|
|
||||||
|
|
||||||
(define-language grammar
|
(define-language grammar
|
||||||
(B t
|
(B t
|
||||||
f
|
f
|
||||||
(B * B)))
|
(B * B)))
|
||||||
|
|
||||||
(define r
|
(define r
|
||||||
(reduction-relation
|
(reduction-relation
|
||||||
grammar
|
grammar
|
||||||
(--> (f * B_1) B_1 false) ; [a]
|
(--> (f * B_1) B_1 false) ; [a]
|
||||||
(--> (t * B_1) t true))) ; [b]
|
(--> (t * B_1) t true))) ; [b]
|
||||||
|
|
||||||
(define ->r (compatible-closure r grammar B))
|
(define ->r (compatible-closure r grammar B))
|
||||||
|
|
||||||
(traces grammar ->r '((f * f) * (t * f))))
|
(traces grammar ->r '((f * f) * (t * f)))
|
||||||
|
|
|
||||||
|
|
@ -1,67 +0,0 @@
|
||||||
(module eta mzscheme
|
|
||||||
(require (planet robby/redex:5/reduction-semantics)
|
|
||||||
(planet robby/redex:5/gui)
|
|
||||||
(planet robby/redex:5/subst))
|
|
||||||
|
|
||||||
(reduction-steps-cutoff 100)
|
|
||||||
|
|
||||||
(define-language lang
|
|
||||||
(e (e e)
|
|
||||||
x
|
|
||||||
(+ e e)
|
|
||||||
v)
|
|
||||||
(c (v c)
|
|
||||||
(c e)
|
|
||||||
(+ v c)
|
|
||||||
(+ c e)
|
|
||||||
hole)
|
|
||||||
(v (lambda (x) e)
|
|
||||||
number)
|
|
||||||
(x (variable-except lambda +)))
|
|
||||||
|
|
||||||
(define reductions
|
|
||||||
(reduction-relation
|
|
||||||
lang
|
|
||||||
(c=> ((lambda (variable_x) e_body) v_arg)
|
|
||||||
,(lc-subst (term variable_x) (term v_arg) (term e_body)))
|
|
||||||
(c=> (+ number_1 number_2)
|
|
||||||
,(+ (term number_1) (term number_2)))
|
|
||||||
(c=> (side-condition (lambda (variable_x) (e_fun variable_x))
|
|
||||||
(equal? (term e_fun) (lc-subst (term variable_x) 1234 (term e_fun))))
|
|
||||||
e_fun)
|
|
||||||
|
|
||||||
(--> (in-hole c (number_n v_arg))
|
|
||||||
,(format "procedure application: expected procedure, given: ~a; arguments were: ~a"
|
|
||||||
(term number_n)
|
|
||||||
(term v_arg)))
|
|
||||||
(--> (in-hole c (+ (name non-num (lambda (variable) e)) (name arg2 v)))
|
|
||||||
,(format "+: expects type <number> as 1st argument, given: ~s; other arguments were: ~s"
|
|
||||||
(term non-num) (term arg2)))
|
|
||||||
(--> (in-hole c (+ (name arg1 v) (name non-num (lambda (variable) e))))
|
|
||||||
,(format "+: expects type <number> as 2nd argument, given: ~s; other arguments were: ~s"
|
|
||||||
(term arg1) (term non-num)))
|
|
||||||
|
|
||||||
where
|
|
||||||
|
|
||||||
[(c=> x y) (--> (in-hole c_1 x) (in-hole c_1 y))]))
|
|
||||||
|
|
||||||
(define lc-subst
|
|
||||||
(subst
|
|
||||||
[(? symbol?) (variable)]
|
|
||||||
[(? number?) (constant)]
|
|
||||||
[`(lambda (,x) ,b)
|
|
||||||
(all-vars (list x))
|
|
||||||
(build (lambda (vars body) `(lambda (,(car vars)) ,body)))
|
|
||||||
(subterm (list x) b)]
|
|
||||||
[`(+ ,n2 ,n1)
|
|
||||||
(all-vars '())
|
|
||||||
(build (lambda (vars n1 n2) `(+ ,n1 ,n1)))
|
|
||||||
(subterm '() n1)
|
|
||||||
(subterm '() n2)]
|
|
||||||
[`(,f ,x)
|
|
||||||
(all-vars '())
|
|
||||||
(build (lambda (vars f x) `(,f ,x)))
|
|
||||||
(subterm '() f)
|
|
||||||
(subterm '() x)]))
|
|
||||||
|
|
||||||
(traces lang reductions '(+ (lambda (x) ((+ 1 2) x)) 1)))
|
|
||||||
|
|
@ -1,254 +0,0 @@
|
||||||
(module iswim mzscheme
|
|
||||||
(require (planet robby/redex:5/reduction-semantics)
|
|
||||||
(planet robby/redex:5/subst)
|
|
||||||
(lib "contract.ss"))
|
|
||||||
|
|
||||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
|
||||||
;; Expression grammar:
|
|
||||||
|
|
||||||
(define-language iswim-grammar
|
|
||||||
(M (M M)
|
|
||||||
(o1 M)
|
|
||||||
(o2 M M)
|
|
||||||
V
|
|
||||||
("letcc" X M)
|
|
||||||
("cc" M M))
|
|
||||||
(V X
|
|
||||||
("lam" variable M)
|
|
||||||
b
|
|
||||||
("[" M "]"))
|
|
||||||
(X variable)
|
|
||||||
(b number)
|
|
||||||
(o1 "add1" "sub1" "iszero")
|
|
||||||
(o2 "+" "-" "*" "^")
|
|
||||||
(on o1 o2)
|
|
||||||
|
|
||||||
;; Evaluation contexts:
|
|
||||||
(E hole
|
|
||||||
(E M)
|
|
||||||
(V E)
|
|
||||||
(o1 E)
|
|
||||||
(o2 E M)
|
|
||||||
(o2 V E)
|
|
||||||
("cc" E M)
|
|
||||||
("cc" V E))
|
|
||||||
|
|
||||||
;; Continuations (CK machine):
|
|
||||||
(k "mt"
|
|
||||||
("fun" V k)
|
|
||||||
("arg" M k)
|
|
||||||
("narg" (V ... on) (M ...) k))
|
|
||||||
|
|
||||||
;; Environments and closures (CEK):
|
|
||||||
(env ((X = vcl) ...))
|
|
||||||
(cl (M : env))
|
|
||||||
(vcl (V- : env))
|
|
||||||
|
|
||||||
;; Values that are not variables:
|
|
||||||
(V- ("lam" variable M)
|
|
||||||
b)
|
|
||||||
|
|
||||||
;; Continuations with closures (CEK):
|
|
||||||
(k- "mt"
|
|
||||||
("fun" vcl k-)
|
|
||||||
("arg" cl k-)
|
|
||||||
("narg" (vcl ... on) (cl ...) k-)))
|
|
||||||
|
|
||||||
(define M? (redex-match iswim-grammar M))
|
|
||||||
(define V? (redex-match iswim-grammar V))
|
|
||||||
(define o1? (redex-match iswim-grammar o1))
|
|
||||||
(define o2? (redex-match iswim-grammar o2))
|
|
||||||
(define on? (redex-match iswim-grammar on))
|
|
||||||
(define k? (redex-match iswim-grammar k))
|
|
||||||
|
|
||||||
(define env? (redex-match iswim-grammar env))
|
|
||||||
(define cl? (redex-match iswim-grammar cl))
|
|
||||||
(define vcl? (redex-match iswim-grammar vcl))
|
|
||||||
(define k-? (redex-match iswim-grammar k-))
|
|
||||||
|
|
||||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
|
||||||
;; Substitution:
|
|
||||||
|
|
||||||
;; The subst form makes implemention of capture-avoiding
|
|
||||||
;; easier. We just have to describe how variables bind
|
|
||||||
;; in our language's forms.
|
|
||||||
|
|
||||||
(define iswim-subst/backwards
|
|
||||||
(subst
|
|
||||||
[(? symbol?) (variable)]
|
|
||||||
[(? number?) (constant)]
|
|
||||||
[`("lam" ,X ,M)
|
|
||||||
(all-vars (list X))
|
|
||||||
(build (lambda (X-list M) `("lam" ,(car X-list) ,M)))
|
|
||||||
(subterm (list X) M)]
|
|
||||||
[`(,(and o (or "add1" "sub1" "iszero")) ,M1)
|
|
||||||
(all-vars '())
|
|
||||||
(build (lambda (vars M1) `(,o ,M1)))
|
|
||||||
(subterm '() M1)]
|
|
||||||
[`(,(and o (or "+" "-" "*" "^")) ,M1 ,M2)
|
|
||||||
(all-vars '())
|
|
||||||
(build (lambda (vars M1 M2) `(,o ,M1 ,M2)))
|
|
||||||
(subterm '() M1)
|
|
||||||
(subterm '() M2)]
|
|
||||||
[`(,M1 ,M2)
|
|
||||||
(all-vars '())
|
|
||||||
(build (lambda (empty-list M1 M2) `(,M1 ,M2)))
|
|
||||||
(subterm '() M1)
|
|
||||||
(subterm '() M2)]
|
|
||||||
[`("letcc" ,X ,M)
|
|
||||||
(all-vars (list X))
|
|
||||||
(build (lambda (X-list M) `("letcc" ,(car X-list) ,M)))
|
|
||||||
(subterm (list X) M)]
|
|
||||||
[`("cc" ,M1 ,M2)
|
|
||||||
(all-vars '())
|
|
||||||
(build (lambda (vars M1 M2) `("cc" ,M1 ,M2)))
|
|
||||||
(subterm '() M1)
|
|
||||||
(subterm '() M2)]
|
|
||||||
[`("[" ,E "]")
|
|
||||||
(all-vars '())
|
|
||||||
(build (lambda (vars) `("[" ,E "]")))]))
|
|
||||||
|
|
||||||
|
|
||||||
;; the argument order for the subst-generated function
|
|
||||||
;; doesn't match the order in the notes:
|
|
||||||
(define (iswim-subst M Xr Mr)
|
|
||||||
(iswim-subst/backwards Xr Mr M))
|
|
||||||
|
|
||||||
(define empty-env '())
|
|
||||||
|
|
||||||
;; Environment lookup
|
|
||||||
(define (env-lookup env X)
|
|
||||||
(let ([m (assq X env)])
|
|
||||||
(and m (caddr m))))
|
|
||||||
|
|
||||||
;; Environment extension
|
|
||||||
(define (env-extend env X vcl)
|
|
||||||
(cons (list X '= vcl) env))
|
|
||||||
|
|
||||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
|
||||||
;; Reductions:
|
|
||||||
|
|
||||||
;; beta_v reduction
|
|
||||||
(define beta_v
|
|
||||||
(reduction-relation
|
|
||||||
iswim-grammar
|
|
||||||
(--> (("lam" X_1 M_1) V_1)
|
|
||||||
,(iswim-subst (term M_1) (term X_1) (term V_1)))))
|
|
||||||
|
|
||||||
(define delta
|
|
||||||
(reduction-relation
|
|
||||||
iswim-grammar
|
|
||||||
(--> ("add1" b_1) ,(add1 (term b_1)))
|
|
||||||
(--> ("sub1" b_1) ,(sub1 (term b_1)))
|
|
||||||
(--> ("iszero" b_1)
|
|
||||||
,(if (zero? (term b_1))
|
|
||||||
(term ("lam" x ("lam" y x)))
|
|
||||||
(term ("lam" x ("lam" y y)))))
|
|
||||||
(--> ("+" b_1 b_2) ,(+ (term b_1) (term b_2)))
|
|
||||||
(--> ("-" b_1 b_2) ,(- (term b_1) (term b_2)))
|
|
||||||
(--> ("*" b_1 b_2) ,(* (term b_1) (term b_2)))
|
|
||||||
(--> ("^" b_1 b_2) ,(expt (term b_1) (term b_2)))))
|
|
||||||
|
|
||||||
;; ->v
|
|
||||||
(define ->v (compatible-closure (union-reduction-relations beta_v delta)
|
|
||||||
iswim-grammar
|
|
||||||
M))
|
|
||||||
|
|
||||||
;; :->v
|
|
||||||
(define :->v (context-closure (union-reduction-relations beta_v delta)
|
|
||||||
iswim-grammar
|
|
||||||
E))
|
|
||||||
|
|
||||||
;; :->v+letcc
|
|
||||||
(define :->v+letcc
|
|
||||||
(union-reduction-relations
|
|
||||||
:->v
|
|
||||||
(reduction-relation
|
|
||||||
iswim-grammar
|
|
||||||
|
|
||||||
;; letcc rule:
|
|
||||||
(--> (in-hole E_1 ("letcc" X_1 M_1))
|
|
||||||
(in-hole E_1 ,(iswim-subst (term M_1)
|
|
||||||
(term X_1)
|
|
||||||
`("[" (in-hole E_1 ||) "]"))))
|
|
||||||
|
|
||||||
;; cc rule:
|
|
||||||
(--> (in-hole E ("cc" ("[" (in-hole E_2 ||) "]") V_1))
|
|
||||||
(in-hole E_2 V_1)))))
|
|
||||||
|
|
||||||
|
|
||||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
|
||||||
;; Helpers:
|
|
||||||
|
|
||||||
(define (delta*n on Vs)
|
|
||||||
(let ([l (apply-reduction-relation delta `(,on ,@Vs))])
|
|
||||||
(if (null? l)
|
|
||||||
#f
|
|
||||||
(car l))))
|
|
||||||
|
|
||||||
(define (delta*1 o1 V)
|
|
||||||
(delta*n o1 (list V)))
|
|
||||||
|
|
||||||
(define (delta*2 o2 V1 V2)
|
|
||||||
(delta*n o2 (list V1 V2)))
|
|
||||||
|
|
||||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
|
||||||
;; Abbreviations:
|
|
||||||
|
|
||||||
(define (if0 test then else)
|
|
||||||
(let ([X (variable-not-in `(,then ,else) 'X)])
|
|
||||||
`(((("iszero" ,test) ("lam" ,X ,then)) ("lam" ,X ,else)) 77)))
|
|
||||||
|
|
||||||
(define true '("lam" x ("lam" y x)))
|
|
||||||
(define false '("lam" x ("lam" y y)))
|
|
||||||
(define boolean-not `("lam" x ((x ,false) ,true)))
|
|
||||||
|
|
||||||
(define mkpair '("lam" x ("lam" y ("lam" s ((s x) y)))))
|
|
||||||
(define fst '("lam" p (p ("lam" x ("lam" y x)))))
|
|
||||||
(define snd '("lam" p (p ("lam" x ("lam" y y)))))
|
|
||||||
|
|
||||||
(define Y_v '("lam" f ("lam" x
|
|
||||||
((("lam" g (f ("lam" x ((g g) x))))
|
|
||||||
("lam" g (f ("lam" x ((g g) x)))))
|
|
||||||
x))))
|
|
||||||
|
|
||||||
(define mksum `("lam" s
|
|
||||||
("lam" x
|
|
||||||
,(if0 'x 0 '("+" x (s ("sub1" x)))))))
|
|
||||||
(define sum `(,Y_v ,mksum))
|
|
||||||
|
|
||||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
|
||||||
;; Exports:
|
|
||||||
|
|
||||||
(provide iswim-grammar)
|
|
||||||
|
|
||||||
(provide/contract (M? (any/c . -> . any/c))
|
|
||||||
(V? (any/c . -> . any/c))
|
|
||||||
(o1? (any/c . -> . any/c))
|
|
||||||
(o2? (any/c . -> . any/c))
|
|
||||||
(on? (any/c . -> . any/c))
|
|
||||||
(k? (any/c . -> . any/c))
|
|
||||||
(env? (any/c . -> . any/c))
|
|
||||||
(cl? (any/c . -> . any/c))
|
|
||||||
(vcl? (any/c . -> . any/c))
|
|
||||||
(iswim-subst (M? symbol? M? . -> . M?))
|
|
||||||
(env-lookup (env? symbol? . -> . (union false/c vcl?)))
|
|
||||||
(env-extend (env? symbol? vcl? . -> . env?))
|
|
||||||
(empty-env env?)
|
|
||||||
(beta_v reduction-relation?)
|
|
||||||
(delta reduction-relation?)
|
|
||||||
(delta*1 (o1? V? . -> . (union false/c V?)))
|
|
||||||
(delta*2 (o2? V? V? . -> . (union false/c V?)))
|
|
||||||
(delta*n (on? (listof V?) . -> . (union false/c V?)))
|
|
||||||
(->v reduction-relation?)
|
|
||||||
(:->v reduction-relation?)
|
|
||||||
(:->v+letcc reduction-relation?)
|
|
||||||
(if0 (M? M? M? . -> . M?))
|
|
||||||
(true M?)
|
|
||||||
(false M?)
|
|
||||||
(boolean-not M?)
|
|
||||||
(mkpair M?)
|
|
||||||
(fst M?)
|
|
||||||
(snd M?)
|
|
||||||
(Y_v M?)
|
|
||||||
(sum M?)))
|
|
||||||
|
|
@ -1,155 +1,130 @@
|
||||||
(module letrec mzscheme
|
#lang scheme
|
||||||
(require (planet robby/redex:5/reduction-semantics)
|
|
||||||
(planet robby/redex:5/gui)
|
|
||||||
(planet robby/redex:5/subst)
|
|
||||||
(lib "list.ss"))
|
|
||||||
|
|
||||||
(reduction-steps-cutoff 20)
|
#|
|
||||||
|
|
||||||
(define-language lang
|
BUG: letrec & let are not handled properly by substitution
|
||||||
(p ((store (x v) ...) e))
|
|
||||||
(e (set! x e)
|
|
||||||
(let ((x e)) e)
|
|
||||||
(letrec ((x e)) e)
|
|
||||||
(begin e e ...)
|
|
||||||
(e e)
|
|
||||||
x
|
|
||||||
v)
|
|
||||||
(v (lambda (x) e)
|
|
||||||
number)
|
|
||||||
(x variable)
|
|
||||||
(pc ((store (x v) ...) ec))
|
|
||||||
(ec (ec e)
|
|
||||||
(v ec)
|
|
||||||
(set! variable ec)
|
|
||||||
(let ((x ec)) e)
|
|
||||||
(begin ec e e ...)
|
|
||||||
hole))
|
|
||||||
|
|
||||||
(define substitute
|
|#
|
||||||
(subst
|
|
||||||
[(? symbol?) (variable)]
|
|
||||||
[(? number?) (constant)]
|
|
||||||
[`(lambda (,x) ,b)
|
|
||||||
(all-vars (list x))
|
|
||||||
(build (lambda (vars body) `(lambda (,(car vars)) ,body)))
|
|
||||||
(subterm (list x) b)]
|
|
||||||
[`(set! ,x ,e)
|
|
||||||
(all-vars '())
|
|
||||||
(build (lambda (vars name body) `(set! ,name ,body)))
|
|
||||||
(subterm '() x)
|
|
||||||
(subterm '() e)]
|
|
||||||
[`(let ((,x ,e1)) ,e2)
|
|
||||||
(all-vars (list x))
|
|
||||||
(build (lambda (vars letval body) `(let ((,(car vars) ,letval)) ,body)))
|
|
||||||
(subterm '() e1)
|
|
||||||
(subterm (list x) e2)]
|
|
||||||
[`(letrec ((,x ,e1)) ,e2)
|
|
||||||
(all-vars (list x))
|
|
||||||
(build (lambda (vars letval body) `(letrec ((,(car vars) ,letval)) ,body)))
|
|
||||||
(subterm (list x) e1)
|
|
||||||
(subterm (list x) e2)]
|
|
||||||
[`(begin ,@(es ...))
|
|
||||||
(all-vars (list))
|
|
||||||
(build (lambda (vars . rest) `(begin ,@rest)))
|
|
||||||
(subterms '() es)]
|
|
||||||
[`(,f ,x)
|
|
||||||
(all-vars '())
|
|
||||||
(build (lambda (vars f x) `(,f ,x)))
|
|
||||||
(subterm '() f)
|
|
||||||
(subterm '() x)]))
|
|
||||||
|
|
||||||
;; collect : term -> term
|
(require redex "subst.ss")
|
||||||
;; performs a garbage collection on the term `p'
|
|
||||||
(define (collect p)
|
|
||||||
(define (find-unused vars p)
|
|
||||||
(filter (λ (var) (unused? var p))
|
|
||||||
vars))
|
|
||||||
|
|
||||||
(define (unused? var p)
|
(reduction-steps-cutoff 20)
|
||||||
(let ([rhss (map cadr (cdar p))]
|
|
||||||
[body (cadr p)])
|
|
||||||
(and (not (free-in? var body))
|
|
||||||
(andmap (λ (rhs) (not (free-in? var rhs)))
|
|
||||||
rhss))))
|
|
||||||
|
|
||||||
(define (free-in? var body)
|
(define-language lang
|
||||||
(not (equal? (substitute var (gensym) body)
|
(p ((store (x v) ...) e))
|
||||||
body)))
|
(e (set! x e)
|
||||||
|
(let ((x e)) e)
|
||||||
|
(letrec ((x e)) e)
|
||||||
|
(begin e e ...)
|
||||||
|
(e e)
|
||||||
|
x
|
||||||
|
v)
|
||||||
|
(v (lambda (x) e)
|
||||||
|
number)
|
||||||
|
(x variable)
|
||||||
|
(pc ((store (x v) ...) ec))
|
||||||
|
(ec (ec e)
|
||||||
|
(v ec)
|
||||||
|
(set! variable ec)
|
||||||
|
(let ((x ec)) e)
|
||||||
|
(begin ec e e ...)
|
||||||
|
hole))
|
||||||
|
|
||||||
(define (remove-unused vars p)
|
;; collect : term -> term
|
||||||
`((store ,@(filter (λ (binding) (not (memq (car binding) vars)))
|
;; performs a garbage collection on the term `p'
|
||||||
(cdar p)))
|
(define (collect p)
|
||||||
,(cadr p)))
|
(define (substitute var exp body)
|
||||||
|
(term-let ((var var)
|
||||||
|
(exp exp)
|
||||||
|
(body body))
|
||||||
|
(term (subst (var exp body)))))
|
||||||
|
|
||||||
(let* ([vars (map car (cdar p))]
|
(define (find-unused vars p)
|
||||||
[unused (find-unused vars p)])
|
(filter (λ (var) (unused? var p))
|
||||||
(cond
|
vars))
|
||||||
[(null? unused) p]
|
|
||||||
[else
|
|
||||||
(collect (remove-unused unused p))])))
|
|
||||||
|
|
||||||
(define reductions
|
(define (unused? var p)
|
||||||
(reduction-relation
|
(let ([rhss (map cadr (cdar p))]
|
||||||
lang
|
[body (cadr p)])
|
||||||
(==> (in-hole pc_1 (begin v e_1 e_2 ...))
|
(and (not (free-in? var body))
|
||||||
(in-hole pc_1 (begin e_1 e_2 ...))
|
(andmap (λ (rhs) (not (free-in? var rhs)))
|
||||||
begin\ many)
|
rhss))))
|
||||||
|
|
||||||
(==> (in-hole pc_1 (begin e_1))
|
(define (free-in? var body)
|
||||||
(in-hole pc_1 e_1)
|
(not (equal? (substitute var (gensym) body)
|
||||||
begin\ one)
|
body)))
|
||||||
|
|
||||||
(==> ((store (x_before v_before) ...
|
(define (remove-unused vars p)
|
||||||
(x_i v_i)
|
`((store ,@(filter (λ (binding) (not (memq (car binding) vars)))
|
||||||
(x_after v_after) ...)
|
(cdar p)))
|
||||||
(in-hole ec_1 x_i))
|
,(cadr p)))
|
||||||
((store
|
|
||||||
(x_before v_before) ...
|
|
||||||
(x_i v_i)
|
|
||||||
(x_after v_after) ...)
|
|
||||||
(in-hole ec_1 v_i))
|
|
||||||
deref)
|
|
||||||
|
|
||||||
(==> ((store (x_before v_before) ...
|
(let* ([vars (map car (cdar p))]
|
||||||
(x_i v)
|
[unused (find-unused vars p)])
|
||||||
(x_after v_after) ...)
|
(cond
|
||||||
(in-hole ec_1 (set! x_i v_new)))
|
[(null? unused) p]
|
||||||
((store (x_before v_before) ...
|
[else
|
||||||
(x_i v_new)
|
(collect (remove-unused unused p))])))
|
||||||
(x_after v_after) ...)
|
|
||||||
(in-hole ec_1 v_new))
|
|
||||||
set!)
|
|
||||||
|
|
||||||
(==> (in-hole pc_1 ((lambda (x_1) e_1) v_1))
|
(define reductions
|
||||||
(in-hole pc_1
|
(reduction-relation
|
||||||
,(substitute (term x_1) (term v_1) (term e_1)))
|
lang
|
||||||
βv)
|
(==> (in-hole pc_1 (begin v e_1 e_2 ...))
|
||||||
|
(in-hole pc_1 (begin e_1 e_2 ...))
|
||||||
|
begin\ many)
|
||||||
|
|
||||||
(==> ((store (name the-store any) ...)
|
(==> (in-hole pc_1 (begin e_1))
|
||||||
(in-hole ec_1 (let ((x_1 v_1)) e_1)))
|
(in-hole pc_1 e_1)
|
||||||
,(let ((new-x (variable-not-in (term (the-store ...)) (term x_1))))
|
begin\ one)
|
||||||
(term
|
|
||||||
((store the-store ... (,new-x v_1))
|
|
||||||
(in-hole ec_1
|
|
||||||
,(substitute (term x_1) new-x (term e_1))))))
|
|
||||||
let)
|
|
||||||
|
|
||||||
(==> (in-hole pc_1 (letrec ((x_1 e_1)) e_2))
|
(==> ((store (x_before v_before) ...
|
||||||
(in-hole pc_1 (let ((x_1 0)) (begin (set! x_1 e_1) e_2)))
|
(x_i v_i)
|
||||||
letrec)
|
(x_after v_after) ...)
|
||||||
|
(in-hole ec_1 x_i))
|
||||||
|
((store
|
||||||
|
(x_before v_before) ...
|
||||||
|
(x_i v_i)
|
||||||
|
(x_after v_after) ...)
|
||||||
|
(in-hole ec_1 v_i))
|
||||||
|
deref)
|
||||||
|
|
||||||
where
|
(==> ((store (x_before v_before) ...
|
||||||
[(==> a b) (--> a ,(collect (term b)))]))
|
(x_i v)
|
||||||
|
(x_after v_after) ...)
|
||||||
|
(in-hole ec_1 (set! x_i v_new)))
|
||||||
|
((store (x_before v_before) ...
|
||||||
|
(x_i v_new)
|
||||||
|
(x_after v_after) ...)
|
||||||
|
(in-hole ec_1 v_new))
|
||||||
|
set!)
|
||||||
|
|
||||||
(define (run e) (traces lang reductions `((store) ,e)))
|
(==> (in-hole pc_1 ((lambda (x_1) e_1) v_1))
|
||||||
|
(in-hole pc_1 (subst (x_1 v_1 e_1)))
|
||||||
|
βv)
|
||||||
|
|
||||||
(run '(letrec ((f (lambda (x)
|
(==> ((store (name the-store any) ...)
|
||||||
(letrec ((y (f 1)))
|
(in-hole ec_1 (let ((x_1 v_1)) e_1)))
|
||||||
2))))
|
,(let ((new-x (variable-not-in (term (the-store ...)) (term x_1))))
|
||||||
(f 3)))
|
(term
|
||||||
|
((store the-store ... (,new-x v_1))
|
||||||
|
(in-hole ec_1 (subst (x_1 ,new-x e_1))))))
|
||||||
|
let)
|
||||||
|
|
||||||
(run '(letrec ((f (lambda (x)
|
(==> (in-hole pc_1 (letrec ((x_1 e_1)) e_2))
|
||||||
(letrec ((y 1))
|
(in-hole pc_1 (let ((x_1 0)) (begin (set! x_1 e_1) e_2)))
|
||||||
(f 1)))))
|
letrec)
|
||||||
(f 3))))
|
|
||||||
|
with
|
||||||
|
[(--> a ,(collect (term b))) (==> a b)]))
|
||||||
|
|
||||||
|
(define (run e) (traces lang reductions `((store) ,e)))
|
||||||
|
|
||||||
|
(run '(letrec ((f (lambda (x)
|
||||||
|
(letrec ((y (f 1)))
|
||||||
|
2))))
|
||||||
|
(f 3)))
|
||||||
|
|
||||||
|
(run '(letrec ((f (lambda (x)
|
||||||
|
(letrec ((y 1))
|
||||||
|
(f 1)))))
|
||||||
|
(f 3)))
|
||||||
|
|
|
||||||
|
|
@ -1,60 +1,36 @@
|
||||||
(module omega mzscheme
|
#lang scheme
|
||||||
(require (planet robby/redex:5/reduction-semantics)
|
(require redex "subst.ss")
|
||||||
(planet robby/redex:5/subst)
|
|
||||||
(planet robby/redex:5/gui))
|
|
||||||
|
|
||||||
(reduction-steps-cutoff 10)
|
(reduction-steps-cutoff 10)
|
||||||
|
|
||||||
(define-language lang
|
(define-language lang
|
||||||
(e (e e)
|
(e (e e)
|
||||||
(abort e)
|
(abort e)
|
||||||
x
|
x
|
||||||
v)
|
v)
|
||||||
(c (v c)
|
(c (v c)
|
||||||
(c e)
|
(c e)
|
||||||
hole)
|
hole)
|
||||||
(v call/cc
|
(v call/cc
|
||||||
number
|
number
|
||||||
(lambda (x) e))
|
(lambda (x) e))
|
||||||
|
|
||||||
(x (variable-except lambda call/cc abort)))
|
(x (variable-except lambda call/cc abort)))
|
||||||
|
|
||||||
(define reductions
|
(define reductions
|
||||||
(reduction-relation
|
(reduction-relation
|
||||||
lang
|
lang
|
||||||
(--> (in-hole c_1 (call/cc v_arg))
|
(--> (in-hole c_1 (call/cc v_arg))
|
||||||
,(term-let ([v (variable-not-in (term c_1) 'x)])
|
,(term-let ([v (variable-not-in (term c_1) 'x)])
|
||||||
(term (in-hole c_1 (v_arg (lambda (v) (abort (in-hole c_1 v)))))))
|
(term (in-hole c_1 (v_arg (lambda (v) (abort (in-hole c_1 v)))))))
|
||||||
call/cc)
|
call/cc)
|
||||||
(--> (in-hole c (abort e_1))
|
(--> (in-hole c (abort e_1))
|
||||||
e_1
|
e_1
|
||||||
abort)
|
abort)
|
||||||
(--> (in-hole c_1 ((lambda (variable_x) e_body) v_arg))
|
(--> (in-hole c_1 ((lambda (variable_x) e_body) v_arg))
|
||||||
(in-hole c_1 ,(lc-subst (term variable_x) (term v_arg) (term e_body)))
|
(in-hole c_1 (subst (variable_x v_arg e_body)))
|
||||||
βv)))
|
βv)))
|
||||||
|
|
||||||
(define lc-subst
|
(traces lang reductions '((lambda (x) (x x)) (lambda (x) (x x))))
|
||||||
(plt-subst
|
(traces lang reductions '((call/cc call/cc) (call/cc call/cc)))
|
||||||
['abort (constant)]
|
(traces lang reductions '((lambda (x) ((call/cc call/cc) x)) (call/cc call/cc)))
|
||||||
['call/cc (constant)]
|
|
||||||
[(? symbol?) (variable)]
|
|
||||||
[(? number?) (constant)]
|
|
||||||
[`(lambda (,x) ,b)
|
|
||||||
(all-vars (list x))
|
|
||||||
(build (lambda (vars body) `(lambda (,(car vars)) ,body)))
|
|
||||||
(subterm (list x) b)]
|
|
||||||
[`(call/cc ,v)
|
|
||||||
(all-vars '())
|
|
||||||
(build (lambda (vars arg) `(call/cc ,arg)))
|
|
||||||
(subterm '() v)]
|
|
||||||
[`(,f ,x)
|
|
||||||
(all-vars '())
|
|
||||||
(build (lambda (vars f x) `(,f ,x)))
|
|
||||||
(subterm '() f)
|
|
||||||
(subterm '() x)]))
|
|
||||||
|
|
||||||
|
|
||||||
(traces lang reductions '((lambda (x) (x x)) (lambda (x) (x x))))
|
|
||||||
(traces lang reductions '((call/cc call/cc) (call/cc call/cc)))
|
|
||||||
(traces lang reductions '((lambda (x) ((call/cc call/cc) x)) (call/cc call/cc)))
|
|
||||||
)
|
|
||||||
|
|
|
||||||
|
|
@ -1,169 +1,168 @@
|
||||||
|
#lang scheme
|
||||||
|
(require redex)
|
||||||
|
|
||||||
#|
|
#|
|
||||||
|
|
||||||
semaphores make things much more predictable...
|
semaphores make things much more predictable...
|
||||||
|
|
||||||
|#
|
|#
|
||||||
|
|
||||||
(module semaphores mzscheme
|
(reduction-steps-cutoff 100)
|
||||||
(require (planet robby/redex:5/reduction-semantics)
|
|
||||||
(planet robby/redex:5/gui))
|
|
||||||
|
|
||||||
(reduction-steps-cutoff 100)
|
(define-language lang
|
||||||
|
(p ((store (variable v) ...)
|
||||||
|
(semas (variable sema-count) ...)
|
||||||
|
(threads e ...)))
|
||||||
|
(sema-count number
|
||||||
|
none)
|
||||||
|
(e (set! variable e)
|
||||||
|
(begin e ...)
|
||||||
|
(semaphore variable)
|
||||||
|
(semaphore-wait e)
|
||||||
|
(semaphore-post e)
|
||||||
|
(lambda (variable) e)
|
||||||
|
(e e)
|
||||||
|
variable
|
||||||
|
(list e ...)
|
||||||
|
(cons e e)
|
||||||
|
number
|
||||||
|
(void))
|
||||||
|
(p-ctxt ((store (variable v) ...)
|
||||||
|
(semas (variable sema-count) ...)
|
||||||
|
(threads e ... e-ctxt e ...)))
|
||||||
|
(e-ctxt (e-ctxt e)
|
||||||
|
(v e-ctxt)
|
||||||
|
(cons e-ctxt e)
|
||||||
|
(cons v e-ctxt)
|
||||||
|
(list v ... e-ctxt e ...)
|
||||||
|
(set! variable e-ctxt)
|
||||||
|
(begin e-ctxt e ...)
|
||||||
|
(semaphore-wait e-ctxt)
|
||||||
|
(semaphore-post e-ctxt)
|
||||||
|
hole)
|
||||||
|
(v (semaphore variable)
|
||||||
|
(lambda (variable) e)
|
||||||
|
(list v ...)
|
||||||
|
number
|
||||||
|
(void)))
|
||||||
|
|
||||||
(define-language lang
|
(define reductions
|
||||||
(p ((store (variable v) ...)
|
(reduction-relation
|
||||||
(semas (variable sema-count) ...)
|
lang
|
||||||
(threads e ...)))
|
(--> (in-hole (name c p-ctxt) (begin v e_1 e_2 e_rest ...))
|
||||||
(sema-count number
|
(in-hole c (begin e_1 e_2 e_rest ...)))
|
||||||
none)
|
(--> (in-hole (name c p-ctxt) (cons v_1 (list v_2s ...)))
|
||||||
(e (set! variable e)
|
(in-hole c (list v_1 v_2s ...)))
|
||||||
(begin e ...)
|
(--> (in-hole (name c p-ctxt) (begin v e_1))
|
||||||
(semaphore variable)
|
(in-hole c e_1))
|
||||||
(semaphore-wait e)
|
(--> (in-hole (name c p-ctxt) (begin v_1))
|
||||||
(semaphore-post e)
|
(in-hole c v_1))
|
||||||
(lambda (variable) e)
|
(--> ((store
|
||||||
(e e)
|
(variable_before v_before) ...
|
||||||
variable
|
((name x variable) (name v v))
|
||||||
(list e ...)
|
(variable_after v_after) ...)
|
||||||
(cons e e)
|
(name semas any)
|
||||||
number
|
(threads
|
||||||
(void))
|
e_before ...
|
||||||
(p-ctxt ((store (variable v) ...)
|
(in-hole (name c e-ctxt) (name x variable))
|
||||||
(semas (variable sema-count) ...)
|
e_after ...))
|
||||||
(threads e ... e-ctxt e ...)))
|
((store
|
||||||
(e-ctxt (e-ctxt e)
|
(variable_before v_before) ...
|
||||||
(v e-ctxt)
|
(x v)
|
||||||
(cons e-ctxt e)
|
(variable_after v_after) ...)
|
||||||
(cons v e-ctxt)
|
semas
|
||||||
(list v ... e-ctxt e ...)
|
(threads
|
||||||
(set! variable e-ctxt)
|
e_before ...
|
||||||
(begin e-ctxt e ...)
|
(in-hole c v)
|
||||||
(semaphore-wait e-ctxt)
|
e_after ...)))
|
||||||
(semaphore-post e-ctxt)
|
(--> ((store (variable_before v_before) ...
|
||||||
hole)
|
(variable_i v)
|
||||||
(v (semaphore variable)
|
(variable_after v_after) ...)
|
||||||
(lambda (variable) e)
|
(name semas any)
|
||||||
(list v ...)
|
(threads
|
||||||
number
|
e_before ...
|
||||||
(void)))
|
(in-hole (name c e-ctxt) (set! variable_i v_new))
|
||||||
|
e_after ...))
|
||||||
(define reductions
|
((store (variable_before v_before) ...
|
||||||
(reduction-relation
|
(variable_i v_new)
|
||||||
lang
|
(variable_after v_after) ...)
|
||||||
(--> (in-hole (name c p-ctxt) (begin v e_1 e_2 e_rest ...))
|
semas
|
||||||
(in-hole c (begin e_1 e_2 e_rest ...)))
|
(threads
|
||||||
(--> (in-hole (name c p-ctxt) (cons v_1 (list v_2s ...)))
|
e_before ...
|
||||||
(in-hole c (list v_1 v_2s ...)))
|
(in-hole c (void))
|
||||||
(--> (in-hole (name c p-ctxt) (begin v e_1))
|
e_after ...)))
|
||||||
(in-hole c e_1))
|
(--> ((name store any)
|
||||||
(--> (in-hole (name c p-ctxt) (begin v_1))
|
(semas
|
||||||
(in-hole c v_1))
|
(variable_before v_before) ...
|
||||||
(--> ((store
|
(variable_sema number_n)
|
||||||
(variable_before v_before) ...
|
(variable_after v_after) ...)
|
||||||
((name x variable) (name v v))
|
(threads
|
||||||
(variable_after v_after) ...)
|
e_before ...
|
||||||
(name semas any)
|
(in-hole (name c e-ctxt) (semaphore-wait (semaphore variable_sema)))
|
||||||
(threads
|
e_after ...))
|
||||||
e_before ...
|
(store
|
||||||
(in-hole (name c e-ctxt) (name x variable))
|
(semas
|
||||||
e_after ...))
|
(variable_before v_before) ...
|
||||||
((store
|
(variable_sema ,(if (= (term number_n) 1)
|
||||||
(variable_before v_before) ...
|
(term none)
|
||||||
(x v)
|
(- (term number_n) 1)))
|
||||||
(variable_after v_after) ...)
|
|
||||||
semas
|
|
||||||
(threads
|
|
||||||
e_before ...
|
|
||||||
(in-hole c v)
|
|
||||||
e_after ...)))
|
|
||||||
(--> ((store (variable_before v_before) ...
|
|
||||||
(variable_i v)
|
|
||||||
(variable_after v_after) ...)
|
(variable_after v_after) ...)
|
||||||
(name semas any)
|
(threads
|
||||||
(threads
|
e_before ...
|
||||||
e_before ...
|
(in-hole c (void))
|
||||||
(in-hole (name c e-ctxt) (set! variable_i v_new))
|
e_after ...)))
|
||||||
e_after ...))
|
(--> ((name store any)
|
||||||
((store (variable_before v_before) ...
|
(semas
|
||||||
(variable_i v_new)
|
(variable_before v_before) ...
|
||||||
|
(variable_sema number_n)
|
||||||
|
(variable_after v_after) ...)
|
||||||
|
(threads
|
||||||
|
e_before ...
|
||||||
|
(in-hole (name c e-ctxt) (semaphore-post (semaphore variable_sema)))
|
||||||
|
e_after ...))
|
||||||
|
(store
|
||||||
|
(semas
|
||||||
|
(variable_before v_before) ...
|
||||||
|
(variable_sema ,(+ (term number_n) 1))
|
||||||
(variable_after v_after) ...)
|
(variable_after v_after) ...)
|
||||||
semas
|
(threads
|
||||||
(threads
|
e_before ...
|
||||||
e_before ...
|
(in-hole c (void))
|
||||||
(in-hole c (void))
|
e_after ...)))
|
||||||
e_after ...)))
|
|
||||||
(--> ((name store any)
|
|
||||||
(semas
|
|
||||||
(variable_before v_before) ...
|
|
||||||
(variable_sema number_n)
|
|
||||||
(variable_after v_after) ...)
|
|
||||||
(threads
|
|
||||||
e_before ...
|
|
||||||
(in-hole (name c e-ctxt) (semaphore-wait (semaphore variable_sema)))
|
|
||||||
e_after ...))
|
|
||||||
(store
|
|
||||||
(semas
|
|
||||||
(variable_before v_before) ...
|
|
||||||
(variable_sema ,(if (= (term number_n) 1)
|
|
||||||
(term none)
|
|
||||||
(- (term number_n) 1)))
|
|
||||||
(variable_after v_after) ...)
|
|
||||||
(threads
|
|
||||||
e_before ...
|
|
||||||
(in-hole c (void))
|
|
||||||
e_after ...)))
|
|
||||||
(--> ((name store any)
|
|
||||||
(semas
|
|
||||||
(variable_before v_before) ...
|
|
||||||
(variable_sema number_n)
|
|
||||||
(variable_after v_after) ...)
|
|
||||||
(threads
|
|
||||||
e_before ...
|
|
||||||
(in-hole (name c e-ctxt) (semaphore-post (semaphore variable_sema)))
|
|
||||||
e_after ...))
|
|
||||||
(store
|
|
||||||
(semas
|
|
||||||
(variable_before v_before) ...
|
|
||||||
(variable_sema ,(+ (term number_n) 1))
|
|
||||||
(variable_after v_after) ...)
|
|
||||||
(threads
|
|
||||||
e_before ...
|
|
||||||
(in-hole c (void))
|
|
||||||
e_after ...)))
|
|
||||||
|
|
||||||
(--> ((name store any)
|
(--> ((name store any)
|
||||||
(semas
|
(semas
|
||||||
(variable_before v_before) ...
|
(variable_before v_before) ...
|
||||||
(variable_sema none)
|
(variable_sema none)
|
||||||
(variable_after v_after) ...)
|
(variable_after v_after) ...)
|
||||||
(threads
|
(threads
|
||||||
e_before ...
|
e_before ...
|
||||||
(in-hole (name c e-ctxt) (semaphore-post (semaphore variable_sema)))
|
(in-hole (name c e-ctxt) (semaphore-post (semaphore variable_sema)))
|
||||||
e_after ...))
|
e_after ...))
|
||||||
(store
|
(store
|
||||||
(semas
|
(semas
|
||||||
(variable_before v_before) ...
|
(variable_before v_before) ...
|
||||||
(variable_sema 1)
|
(variable_sema 1)
|
||||||
(variable_after v_after) ...)
|
(variable_after v_after) ...)
|
||||||
(threads
|
(threads
|
||||||
e_before ...
|
e_before ...
|
||||||
(in-hole c (void))
|
(in-hole c (void))
|
||||||
e_after ...)))))
|
e_after ...)))))
|
||||||
|
|
||||||
(stepper lang
|
(stepper lang
|
||||||
reductions
|
reductions
|
||||||
`((store (y (list)))
|
`((store (y (list)))
|
||||||
(semas)
|
(semas)
|
||||||
(threads (set! y (cons 1 y))
|
(threads (set! y (cons 1 y))
|
||||||
(set! y (cons 2 y)))))
|
(set! y (cons 2 y)))))
|
||||||
|
|
||||||
(stepper lang
|
(stepper lang
|
||||||
reductions
|
reductions
|
||||||
`((store (y (list)))
|
`((store (y (list)))
|
||||||
(semas (x 1))
|
(semas (x 1))
|
||||||
(threads (begin (semaphore-wait (semaphore x))
|
(threads (begin (semaphore-wait (semaphore x))
|
||||||
(set! y (cons 1 y))
|
(set! y (cons 1 y))
|
||||||
(semaphore-post (semaphore x)))
|
(semaphore-post (semaphore x)))
|
||||||
(begin (semaphore-wait (semaphore x))
|
(begin (semaphore-wait (semaphore x))
|
||||||
(set! y (cons 2 y))
|
(set! y (cons 2 y))
|
||||||
(semaphore-post (semaphore x)))))))
|
(semaphore-post (semaphore x))))))
|
||||||
|
|
@ -1,92 +1,71 @@
|
||||||
(module subject-reduction mzscheme
|
#lang scheme
|
||||||
(require (planet robby/redex:5/reduction-semantics)
|
(require redex)
|
||||||
(planet robby/redex:5/gui)
|
|
||||||
(planet robby/redex:5/subst)
|
|
||||||
(lib "plt-match.ss"))
|
|
||||||
|
|
||||||
(reduction-steps-cutoff 10)
|
(reduction-steps-cutoff 10)
|
||||||
|
|
||||||
(define-language lang
|
(define-language lang
|
||||||
(e (e e)
|
(e (e e)
|
||||||
(abort e)
|
(abort e)
|
||||||
x
|
x
|
||||||
v)
|
v)
|
||||||
(x (variable-except lambda call/cc abort))
|
(x (variable-except lambda call/cc abort))
|
||||||
(c (v c)
|
(c (v c)
|
||||||
(c e)
|
(c e)
|
||||||
hole)
|
hole)
|
||||||
(v call/cc
|
(v call/cc
|
||||||
number
|
number
|
||||||
(lambda (x t) e))
|
(lambda (x t) e))
|
||||||
(t num
|
(t num
|
||||||
(t -> t)))
|
(t -> t)))
|
||||||
|
|
||||||
(define reductions
|
(define reductions
|
||||||
(reduction-relation
|
(reduction-relation
|
||||||
lang
|
lang
|
||||||
(--> (in-hole c_1 (call/cc v_arg))
|
(--> (in-hole c_1 (call/cc v_arg))
|
||||||
,(term-let ([v (variable-not-in (term c_1) 'x)])
|
,(term-let ([v (variable-not-in (term c_1) 'x)])
|
||||||
(term
|
(term
|
||||||
(in-hole c_1 (v_arg (lambda (v) (abort (in-hole c_1 v)))))))
|
(in-hole c_1 (v_arg (lambda (v) (abort (in-hole c_1 v)))))))
|
||||||
call/cc)
|
call/cc)
|
||||||
(--> (in-hole c (abort e_1))
|
(--> (in-hole c (abort e_1))
|
||||||
e_1
|
e_1
|
||||||
abort)
|
abort)
|
||||||
|
|
||||||
;; this rules calls subst with the wrong arguments, which is caught by the example below.
|
;; this rules calls subst with the wrong arguments, which is caught by the example below.
|
||||||
(--> (in-hole c_1 ((lambda (x_format t_1) e_body) v_actual))
|
(--> (in-hole c_1 ((lambda (x_format t_1) e_body) v_actual))
|
||||||
(in-hole c_1 ,(lc-subst (term x_format) (term e_body) (term v_actual)))
|
(in-hole c_1 (subst x_format v_actual e_body))
|
||||||
βv)))
|
βv)))
|
||||||
|
|
||||||
(define lc-subst
|
(define (type-check term)
|
||||||
(plt-subst
|
(let/ec k
|
||||||
[(? symbol?) (variable)]
|
(let loop ([term term]
|
||||||
[(? number?) (constant)]
|
[env '()])
|
||||||
[`(lambda (,x ,t) ,b)
|
(match term
|
||||||
(all-vars (list x))
|
[(? symbol?)
|
||||||
(build (lambda (vars body) `(lambda (,(car vars) ,t) ,body)))
|
(let ([l (assoc term env)])
|
||||||
(subterm (list x) b)]
|
(if l
|
||||||
[`(call/cc ,v)
|
(cdr l)
|
||||||
(all-vars '())
|
(k #f)))]
|
||||||
(build (lambda (vars arg) `(call/cc ,arg)))
|
[(? number?) 'num]
|
||||||
(subterm '() v)]
|
[`(lambda (,x ,t) ,b)
|
||||||
[`(,f ,x)
|
(let ([body (loop b (cons (cons x t) env))])
|
||||||
(all-vars '())
|
`(,t -> ,body))]
|
||||||
(build (lambda (vars f x) `(,f ,x)))
|
[`(,e1 ,e2)
|
||||||
(subterm '() f)
|
(let ([t1 (loop e1 env)]
|
||||||
(subterm '() x)]))
|
[t2 (loop e2 env)])
|
||||||
|
(match t1
|
||||||
|
[`(,td -> ,tr)
|
||||||
|
(if (equal? td t2)
|
||||||
|
tr
|
||||||
|
(k #f))]
|
||||||
|
[else (k #f)]))]))))
|
||||||
|
|
||||||
(define (type-check term)
|
(define (pred term1)
|
||||||
(let/ec k
|
(let ([t1 (type-check term1)])
|
||||||
(let loop ([term term]
|
(lambda (term2)
|
||||||
[env '()])
|
(and t1
|
||||||
(match term
|
(equal? (type-check term2) t1)))))
|
||||||
[(? symbol?)
|
|
||||||
(let ([l (assoc term env)])
|
|
||||||
(if l
|
|
||||||
(cdr l)
|
|
||||||
(k #f)))]
|
|
||||||
[(? number?) 'num]
|
|
||||||
[`(lambda (,x ,t) ,b)
|
|
||||||
(let ([body (loop b (cons (cons x t) env))])
|
|
||||||
`(,t -> ,body))]
|
|
||||||
[`(,e1 ,e2)
|
|
||||||
(let ([t1 (loop e1 env)]
|
|
||||||
[t2 (loop e2 env)])
|
|
||||||
(match t1
|
|
||||||
[`(,td -> ,tr)
|
|
||||||
(if (equal? td t2)
|
|
||||||
tr
|
|
||||||
(k #f))]
|
|
||||||
[else (k #f)]))]))))
|
|
||||||
|
|
||||||
(define (pred term1)
|
(define (show term)
|
||||||
(let ([t1 (type-check term1)])
|
(traces reductions term #:pred (pred term)))
|
||||||
(lambda (term2)
|
|
||||||
(and t1
|
|
||||||
(equal? (type-check term2) t1)))))
|
|
||||||
|
|
||||||
(define (show term)
|
(show '((lambda (x (num -> num)) 1) ((lambda (x (num -> num)) x) (lambda (x num) x))))
|
||||||
(traces/pred lang reductions (list term) (pred term)))
|
|
||||||
|
|
||||||
(show '((lambda (x (num -> num)) 1) ((lambda (x (num -> num)) x) (lambda (x num) x)))))
|
|
||||||
74
collects/redex/examples/subst.ss
Normal file
74
collects/redex/examples/subst.ss
Normal file
|
|
@ -0,0 +1,74 @@
|
||||||
|
#lang scheme
|
||||||
|
(require redex)
|
||||||
|
(provide subst subst-n)
|
||||||
|
|
||||||
|
(define-language subst-lang
|
||||||
|
(x variable))
|
||||||
|
|
||||||
|
(define-metafunction subst-n
|
||||||
|
subst-lang
|
||||||
|
[((x_1 any_1) (x_2 any_2) ... any_3)
|
||||||
|
(subst (x_1 any_1 (subst-n ((x_2 any_2) ... any_3))))]
|
||||||
|
[(any_3) any_3])
|
||||||
|
|
||||||
|
(define-metafunction subst
|
||||||
|
subst-lang
|
||||||
|
;; 1. x_1 bound, so don't continue in λ body
|
||||||
|
[(x_1 any_1 (λ (x_2 ... x_1 x_3 ...) any_2))
|
||||||
|
(λ (x_2 ... x_1 x_3 ...) any_2)
|
||||||
|
(side-condition (not (member (term x_1) (term (x_2 ...)))))]
|
||||||
|
;; 2. general purpose capture avoiding case
|
||||||
|
[(x_1 any_1 (λ (x_2 ...) any_2))
|
||||||
|
,(term-let ([(x_new ...)
|
||||||
|
(variables-not-in (term (x_1 any_1 any_2))
|
||||||
|
(term (x_2 ...)))])
|
||||||
|
(term
|
||||||
|
(λ (x_new ...)
|
||||||
|
(subst (x_1 any_1 (subst-vars ((x_2 x_new) ... any_2)))))))]
|
||||||
|
;; 3. replace x_1 with e_1
|
||||||
|
[(x_1 any_1 x_1) any_1]
|
||||||
|
;; 4. x_1 and x_2 are different, so don't replace
|
||||||
|
[(x_1 any_1 x_2) x_2]
|
||||||
|
;; the last two cases cover all other expression forms
|
||||||
|
[(x_1 any_1 (any_2 ...))
|
||||||
|
((subst (x_1 any_1 any_2)) ...)]
|
||||||
|
[(x_1 any_1 any_2) any_2])
|
||||||
|
|
||||||
|
(define-metafunction subst-vars
|
||||||
|
subst-lang
|
||||||
|
[((x_1 any_1) x_1) any_1]
|
||||||
|
[((x_1 any_1) (any_2 ...)) ((subst-vars ((x_1 any_1) any_2)) ...)]
|
||||||
|
[((x_1 any_1) any_2) any_2]
|
||||||
|
[((x_1 any_1) (x_2 any_2) ... any_3)
|
||||||
|
(subst-vars ((x_1 any_1) (subst-vars ((x_2 any_2) ... any_3))))]
|
||||||
|
[(any) any])
|
||||||
|
|
||||||
|
(begin
|
||||||
|
(test-equal (term (subst (x y x))) (term y))
|
||||||
|
(test-equal (term (subst (x y z))) (term z))
|
||||||
|
(test-equal (term (subst (x y (x (y z))))) (term (y (y z))))
|
||||||
|
(test-equal (term (subst (x y ((λ (x) x) ((λ (y1) y1) (λ (x) z))))))
|
||||||
|
(term ((λ (x) x) ((λ (y2) y2) (λ (x) z)))))
|
||||||
|
(test-equal (term (subst (x y (if0 (+ 1 x) x x))))
|
||||||
|
(term (if0 (+ 1 y) y y)))
|
||||||
|
(test-equal (term (subst (x (λ (z) y) (λ (y) x))))
|
||||||
|
(term (λ (y1) (λ (z) y))))
|
||||||
|
(test-equal (term (subst (x 1 (λ (y) x))))
|
||||||
|
(term (λ (y) 1)))
|
||||||
|
(test-equal (term (subst (x y (λ (y) x))))
|
||||||
|
(term (λ (y1) y)))
|
||||||
|
(test-equal (term (subst (x (λ (y) y) (λ (z) (z2 z)))))
|
||||||
|
(term (λ (z1) (z2 z1))))
|
||||||
|
(test-equal (term (subst (x (λ (z) z) (λ (z) (z1 z)))))
|
||||||
|
(term (λ (z2) (z1 z2))))
|
||||||
|
(test-equal (term (subst (x z (λ (z) (z1 z)))))
|
||||||
|
(term (λ (z2) (z1 z2))))
|
||||||
|
(test-equal (term (subst (x3 5 (λ (x2) x2))))
|
||||||
|
(term (λ (x1) x1)))
|
||||||
|
(test-equal (term (subst (z * (λ (z x) 1))))
|
||||||
|
(term (λ (z x) 1)))
|
||||||
|
(test-equal (term (subst (q (λ (x) z) (λ (z x) q))))
|
||||||
|
(term (λ (z1 x1) (λ (x) z))))
|
||||||
|
(test-equal (term (subst (x 1 (λ (x x) x))))
|
||||||
|
(term (λ (x x) x)))
|
||||||
|
(test-results))
|
||||||
|
|
@ -1,117 +1,86 @@
|
||||||
(module threads mzscheme
|
#lang scheme
|
||||||
(require (planet robby/redex:5/reduction-semantics)
|
(require redex)
|
||||||
(planet robby/redex:5/subst)
|
|
||||||
(planet robby/redex:5/gui)
|
|
||||||
(lib "plt-match.ss"))
|
|
||||||
|
|
||||||
(reduction-steps-cutoff 100)
|
(reduction-steps-cutoff 100)
|
||||||
|
|
||||||
(define-language threads
|
(define-language threads
|
||||||
(p ((store (x v) ...) (threads e ...)))
|
(p ((store (x v) ...) (threads e ...)))
|
||||||
(e (set! x e)
|
(e (set! x e)
|
||||||
(let ((x e)) e)
|
(let ((x e)) e)
|
||||||
(e e)
|
(e e)
|
||||||
x
|
x
|
||||||
v
|
v
|
||||||
(+ e e))
|
(+ e e))
|
||||||
(v (lambda (x) e)
|
(v (lambda (x) e)
|
||||||
number)
|
number)
|
||||||
(x variable)
|
(x variable)
|
||||||
(pc ((store (x v) ...) tc))
|
(pc ((store (x v) ...) tc))
|
||||||
(tc (threads e ... ec e ...))
|
(tc (threads e ... ec e ...))
|
||||||
(ec (ec e) (v ec) (set! variable ec) (let ((x ec)) e) (+ ec e) (+ v ec) hole))
|
(ec (ec e) (v ec) (set! variable ec) (let ((x ec)) e) (+ ec e) (+ v ec) hole))
|
||||||
|
|
||||||
(define reductions
|
(define reductions
|
||||||
(reduction-relation
|
(reduction-relation
|
||||||
threads
|
threads
|
||||||
(--> (in-hole pc_1 (+ number_1 number_2))
|
(--> (in-hole pc_1 (+ number_1 number_2))
|
||||||
(in-hole pc_1 ,(+ (term number_1) (term number_2)))
|
(in-hole pc_1 ,(+ (term number_1) (term number_2)))
|
||||||
sum)
|
sum)
|
||||||
|
|
||||||
(--> ((store
|
(--> ((store
|
||||||
(name befores (x v)) ...
|
(name befores (x v)) ...
|
||||||
(x_i v_i)
|
(x_i v_i)
|
||||||
(name afters (x v)) ...)
|
(name afters (x v)) ...)
|
||||||
(in-hole tc_1 x_i))
|
(in-hole tc_1 x_i))
|
||||||
((store
|
((store
|
||||||
befores ...
|
befores ...
|
||||||
(x_i v_i)
|
(x_i v_i)
|
||||||
afters ...)
|
afters ...)
|
||||||
(in-hole tc_1 v_i))
|
(in-hole tc_1 v_i))
|
||||||
deref)
|
deref)
|
||||||
|
|
||||||
(--> ((store (x_1 v_1) ... (x_i v) (x_2 v_2) ...)
|
(--> ((store (x_1 v_1) ... (x_i v) (x_2 v_2) ...)
|
||||||
(in-hole tc_1 (set! x_i v_new)))
|
(in-hole tc_1 (set! x_i v_new)))
|
||||||
((store (x_1 v_1) ... (x_i v_new) (x_2 v_2) ...)
|
((store (x_1 v_1) ... (x_i v_new) (x_2 v_2) ...)
|
||||||
(in-hole tc_1 v_new))
|
(in-hole tc_1 v_new))
|
||||||
set!)
|
set!)
|
||||||
|
|
||||||
(--> (in-hole pc_1 ((lambda (x_1) e_1) v_1))
|
(--> (in-hole pc_1 ((lambda (x_1) e_1) v_1))
|
||||||
(in-hole pc_1 ,(substitute (term x_1) (term v_1) (term e_1)))
|
(in-hole pc_1 ,(substitute (term x_1) (term v_1) (term e_1)))
|
||||||
app)
|
app)
|
||||||
|
|
||||||
(--> ((store (name the-store any) ...)
|
(--> ((store (name the-store any) ...)
|
||||||
(in-hole tc_1 (let ((x_1 v_1)) e_1)))
|
(in-hole tc_1 (let ((x_1 v_1)) e_1)))
|
||||||
(term-let ((new-x (variable-not-in (term (the-store ...)) (term x_1))))
|
(term-let ((new-x (variable-not-in (term (the-store ...)) (term x_1))))
|
||||||
(term
|
(term
|
||||||
((store the-store ... (new-x v_1))
|
((store the-store ... (new-x v_1))
|
||||||
(in-hole tc_1 ,(substitute (term x_1) (term new-x) (term e_1))))))
|
(in-hole tc_1 ,(substitute (term x_1) (term new-x) (term e_1))))))
|
||||||
let)))
|
let)))
|
||||||
|
|
||||||
(define substitute
|
(define (substitute . x) (error 'substitute "~s" x))
|
||||||
(plt-subst
|
|
||||||
[(? symbol?) (variable)]
|
|
||||||
[(? number?) (constant)]
|
|
||||||
[`(lambda (,x) ,b)
|
|
||||||
(all-vars (list x))
|
|
||||||
(build (lambda (vars body) `(lambda (,(car vars)) ,body)))
|
|
||||||
(subterm (list x) b)]
|
|
||||||
[`(set! ,x ,e)
|
|
||||||
(all-vars '())
|
|
||||||
(build (lambda (vars name body) `(set! ,name ,body)))
|
|
||||||
(subterm '() x)
|
|
||||||
(subterm '() e)]
|
|
||||||
[`(let ((,x ,e1)) ,e2)
|
|
||||||
(all-vars (list x))
|
|
||||||
(build (lambda (vars letval body) `(let ((,(car vars) ,letval)) ,body)))
|
|
||||||
(subterm '() e1)
|
|
||||||
(subterm (list x) e2)]
|
|
||||||
[`(+ ,e1 ,e2)
|
|
||||||
(all-vars '())
|
|
||||||
(build (lambda (vars e1 e2) `(+ ,e1 ,e2)))
|
|
||||||
(subterm '() e1)
|
|
||||||
(subterm '() e2)]
|
|
||||||
[`(,f ,x)
|
|
||||||
(all-vars '())
|
|
||||||
(build (lambda (vars f x) `(,f ,x)))
|
|
||||||
(subterm '() f)
|
|
||||||
(subterm '() x)]))
|
|
||||||
|
|
||||||
(define (run es) (traces threads reductions `((store) (threads ,@es))))
|
(define (run es) (traces threads reductions `((store) (threads ,@es))))
|
||||||
(provide run)
|
(provide run)
|
||||||
|
|
||||||
(define (count x)
|
(define (count x)
|
||||||
(match x
|
(match x
|
||||||
[`(set! ,x ,e) (+ 1 (count e))]
|
[`(set! ,x ,e) (+ 1 (count e))]
|
||||||
[(? symbol?) 1]
|
[(? symbol?) 1]
|
||||||
[(? number?) 0]
|
[(? number?) 0]
|
||||||
[`(+ ,e1 ,e2) (+ 1 (count e1) (count e2))]))
|
[`(+ ,e1 ,e2) (+ 1 (count e1) (count e2))]))
|
||||||
|
|
||||||
;; use a pretty-printer that just summaizes the terms, showing the depth of each thread.
|
;; use a pretty-printer that just summaizes the terms, showing the depth of each thread.
|
||||||
(traces threads reductions
|
(traces reductions
|
||||||
'((store (x 1))
|
'((store (x 1))
|
||||||
(threads
|
(threads
|
||||||
(set! x (+ x -1))
|
(set! x (+ x -1))
|
||||||
(set! x (+ x 1))))
|
(set! x (+ x 1))))
|
||||||
|
|
||||||
(lambda (exp)
|
(lambda (exp)
|
||||||
(match exp
|
(match exp
|
||||||
[`((store (x ,x)) (threads ,t1 ,t2))
|
[`((store (x ,x)) (threads ,t1 ,t2))
|
||||||
(format "~a ~a ~a" x (count t1) (count t2))])))
|
(format "~a ~a ~a" x (count t1) (count t2))])))
|
||||||
|
|
||||||
(parameterize ([initial-char-width 16])
|
(parameterize ([initial-char-width 16])
|
||||||
(stepper threads reductions '((store) (threads
|
(stepper threads reductions '((store) (threads
|
||||||
(+ 1 1)
|
(+ 1 1)
|
||||||
(+ 1 1)
|
(+ 1 1)
|
||||||
(+ 1 1)))))
|
(+ 1 1)))))
|
||||||
)
|
|
||||||
|
|
|
||||||
|
|
@ -1,87 +1,69 @@
|
||||||
(module types mzscheme
|
#lang scheme
|
||||||
(require (planet robby/redex:5/reduction-semantics)
|
(require redex
|
||||||
(planet robby/redex:5/subst)
|
"subst.ss")
|
||||||
(planet robby/redex:5/gui))
|
|
||||||
|
|
||||||
(reduction-steps-cutoff 10)
|
(reduction-steps-cutoff 10)
|
||||||
|
|
||||||
(define-language lang
|
(define-language lang
|
||||||
(e (e e)
|
(e (e e)
|
||||||
x
|
x
|
||||||
number
|
number
|
||||||
(lambda (x t) e)
|
(lambda (x t) e)
|
||||||
(if e e e)
|
(if e e e)
|
||||||
(= e e)
|
(= e e)
|
||||||
(-> e e)
|
(-> e e)
|
||||||
num
|
num
|
||||||
bool)
|
bool)
|
||||||
(c (t c)
|
(c (t c)
|
||||||
(c e)
|
(c e)
|
||||||
(-> t c)
|
(-> t c)
|
||||||
(-> c e)
|
(-> c e)
|
||||||
(= t c)
|
(= t c)
|
||||||
(= c e)
|
(= c e)
|
||||||
(if c e e)
|
(if c e e)
|
||||||
(if t c e)
|
(if t c e)
|
||||||
(if t t c)
|
(if t t c)
|
||||||
hole)
|
hole)
|
||||||
(x (variable-except lambda -> if =))
|
(x (variable-except lambda -> if =))
|
||||||
(t num bool (-> t t)))
|
(t num bool (-> t t)))
|
||||||
|
|
||||||
(define reductions
|
(define reductions
|
||||||
(reduction-relation
|
(reduction-relation
|
||||||
lang
|
lang
|
||||||
(r--> number num)
|
(r--> number num)
|
||||||
|
|
||||||
(r--> (lambda (x_1 t_1) e_body)
|
(r--> (lambda (x_1 t_1) e_body)
|
||||||
(-> t_1 ,(lc-subst (term x_1)
|
(-> t_1 (subst (x_1 t_1 e_body))))
|
||||||
(term t_1)
|
|
||||||
(term e_body))))
|
|
||||||
|
|
||||||
(r--> ((-> t_1 t_2) t_1) t_2)
|
(r--> ((-> t_1 t_2) t_1) t_2)
|
||||||
|
|
||||||
(e--> (side-condition ((-> t_1 t) t_2)
|
(e--> (side-condition ((-> t_1 t) t_2)
|
||||||
(not (equal? (term t_1) (term t_2))))
|
(not (equal? (term t_1) (term t_2))))
|
||||||
,(format "app: domain error ~s and ~s" (term t_1) (term t_2)))
|
,(format "app: domain error ~s and ~s" (term t_1) (term t_2)))
|
||||||
|
|
||||||
(e--> (num t_1)
|
(e--> (num t_1)
|
||||||
,(format "app: non function error ~s" (term t_1)))
|
,(format "app: non function error ~s" (term t_1)))
|
||||||
|
|
||||||
(r--> (if bool t_1 t_1) t_1)
|
(r--> (if bool t_1 t_1) t_1)
|
||||||
(e--> (side-condition (if bool t_1 t_2)
|
(e--> (side-condition (if bool t_1 t_2)
|
||||||
(not (equal? (term t_1) (term t_2))))
|
(not (equal? (term t_1) (term t_2))))
|
||||||
,(format "if: then and else clause mismatch ~s and ~s" (term t_1) (term t_2)))
|
,(format "if: then and else clause mismatch ~s and ~s" (term t_1) (term t_2)))
|
||||||
(e--> (side-condition (if t_1 t t)
|
(e--> (side-condition (if t_1 t t)
|
||||||
(not (equal? (term t_1) 'bool)))
|
(not (equal? (term t_1) 'bool)))
|
||||||
,(format "if: test not boolean ~s" (term t_1)))
|
,(format "if: test not boolean ~s" (term t_1)))
|
||||||
|
|
||||||
(r--> (= num num) bool)
|
(r--> (= num num) bool)
|
||||||
(e--> (side-condition (= t_1 t_2)
|
(e--> (side-condition (= t_1 t_2)
|
||||||
(or (not (equal? (term t_1) 'num))
|
(or (not (equal? (term t_1) 'num))
|
||||||
(not (equal? (term t_2) 'num))))
|
(not (equal? (term t_2) 'num))))
|
||||||
,(format "=: not comparing numbers ~s and ~s" (term t_1) (term t_2)))
|
,(format "=: not comparing numbers ~s and ~s" (term t_1) (term t_2)))
|
||||||
|
|
||||||
where
|
with
|
||||||
|
|
||||||
[(r--> a b) (--> (in-hole c_1 a) (in-hole c_1 b))]
|
[(--> (in-hole c_1 a) (in-hole c_1 b)) (r--> a b)]
|
||||||
[(e--> a b) (--> (in-hole c a) b)]))
|
[(--> (in-hole c a) b) (e--> a b)]))
|
||||||
|
|
||||||
(define lc-subst
|
(traces reductions
|
||||||
(subst
|
'((lambda (x num) (lambda (y num) (if (= x y) 0 x))) 1))
|
||||||
[(? symbol?) (variable)]
|
(traces reductions
|
||||||
[(? number?) (constant)]
|
'((lambda (x num) (lambda (y num) (if (= x y) 0 (lambda (x num) x)))) 1))
|
||||||
[`(lambda (,x ,t) ,b)
|
|
||||||
(all-vars (list x))
|
|
||||||
(build (lambda (vars body) `(lambda (,(car vars) ,t) ,body)))
|
|
||||||
(subterm (list x) b)]
|
|
||||||
[`(,f ,@(xs ...))
|
|
||||||
(all-vars '())
|
|
||||||
(build (lambda (vars f . xs) `(,f ,@xs)))
|
|
||||||
(subterm '() f)
|
|
||||||
(subterms '() xs)]))
|
|
||||||
|
|
||||||
(traces lang reductions
|
|
||||||
'((lambda (x num) (lambda (y num) (if (= x y) 0 x))) 1))
|
|
||||||
(traces lang reductions
|
|
||||||
'((lambda (x num) (lambda (y num) (if (= x y) 0 (lambda (x num) x)))) 1))
|
|
||||||
)
|
|
||||||
|
|
|
||||||
|
|
@ -8,64 +8,62 @@ In the other window, you expect to see the currently unreducted terms in green a
|
||||||
|
|
||||||
|#
|
|#
|
||||||
|
|
||||||
(module color-test mzscheme
|
#lang scheme/gui
|
||||||
(require "../reduction-semantics.ss"
|
|
||||||
"../gui.ss"
|
|
||||||
(lib "mred.ss" "mred")
|
|
||||||
(lib "class.ss"))
|
|
||||||
|
|
||||||
(reduction-steps-cutoff 1)
|
(require "../reduction-semantics.ss"
|
||||||
|
"../gui.ss")
|
||||||
|
|
||||||
(let ()
|
(reduction-steps-cutoff 1)
|
||||||
|
|
||||||
(define (get-range term-node)
|
(let ()
|
||||||
(let loop ([node term-node])
|
|
||||||
(let ([parents (term-node-parents node)])
|
|
||||||
(cond
|
|
||||||
[(null? parents) (list node)]
|
|
||||||
[else (cons node (loop (car parents)))]))))
|
|
||||||
|
|
||||||
(define (color-range-pred sexp term-node)
|
(define (get-range term-node)
|
||||||
(let* ([parents (get-range term-node)]
|
(let loop ([node term-node])
|
||||||
[max-val (car (term-node-expr (car parents)))])
|
(let ([parents (term-node-parents node)])
|
||||||
(for-each
|
(cond
|
||||||
(λ (node)
|
[(null? parents) (list node)]
|
||||||
(let ([val (car (term-node-expr node))])
|
[else (cons node (loop (car parents)))]))))
|
||||||
(term-node-set-color! node
|
|
||||||
(make-object color%
|
|
||||||
(floor (- 255 (* val (/ 255 max-val))))
|
|
||||||
0
|
|
||||||
(floor (* val (/ 255 max-val)))))))
|
|
||||||
parents)))
|
|
||||||
|
|
||||||
(define-language empty-language)
|
(define (color-range-pred sexp term-node)
|
||||||
|
(let* ([parents (get-range term-node)]
|
||||||
|
[max-val (car (term-node-expr (car parents)))])
|
||||||
|
(for-each
|
||||||
|
(λ (node)
|
||||||
|
(let ([val (car (term-node-expr node))])
|
||||||
|
(term-node-set-color! node
|
||||||
|
(make-object color%
|
||||||
|
(floor (- 255 (* val (/ 255 max-val))))
|
||||||
|
0
|
||||||
|
(floor (* val (/ 255 max-val)))))))
|
||||||
|
parents)))
|
||||||
|
|
||||||
(traces/pred empty-language
|
(define-language empty-language)
|
||||||
(reduction-relation
|
|
||||||
empty-language
|
|
||||||
(--> (number_1 word)
|
|
||||||
(,(+ (term number_1) 1) word)
|
|
||||||
inc))
|
|
||||||
(list '(1 word))
|
|
||||||
color-range-pred))
|
|
||||||
|
|
||||||
(let ()
|
(traces
|
||||||
(define-language empty-language)
|
(reduction-relation
|
||||||
|
empty-language
|
||||||
|
(--> (number_1 word)
|
||||||
|
(,(+ (term number_1) 1) word)
|
||||||
|
inc))
|
||||||
|
'(1 word)
|
||||||
|
#:pred color-range-pred))
|
||||||
|
|
||||||
(define (last-color-pred sexp term-node)
|
(let ()
|
||||||
(term-node-set-color! term-node
|
(define-language empty-language)
|
||||||
(if (null? (term-node-children term-node))
|
|
||||||
"green"
|
|
||||||
"white")))
|
|
||||||
|
|
||||||
(traces/pred empty-language
|
(define (last-color-pred sexp term-node)
|
||||||
(reduction-relation
|
(term-node-set-color! term-node
|
||||||
empty-language
|
(if (null? (term-node-children term-node))
|
||||||
(--> (number_1 word)
|
"green"
|
||||||
(,(+ (term number_1) 1) word)
|
"white")))
|
||||||
inc)
|
|
||||||
(--> (number_1 word)
|
(traces (reduction-relation
|
||||||
(,(* (term number_1) 2) word)
|
empty-language
|
||||||
dup))
|
(--> (number_1 word)
|
||||||
(list '(1 word))
|
(,(+ (term number_1) 1) word)
|
||||||
last-color-pred)))
|
inc)
|
||||||
|
(--> (number_1 word)
|
||||||
|
(,(* (term number_1) 2) word)
|
||||||
|
dup))
|
||||||
|
'(1 word)
|
||||||
|
#:pred last-color-pred))
|
||||||
|
|
@ -1,60 +0,0 @@
|
||||||
(module schemeunit-test mzscheme
|
|
||||||
(require "../schemeunit.ss"
|
|
||||||
(all-except "../reduction-semantics.ss" check)
|
|
||||||
(planet "text-ui.ss" ("schematics" "schemeunit.plt" 2))
|
|
||||||
(planet "test.ss" ("schematics" "schemeunit.plt" 2)))
|
|
||||||
|
|
||||||
(define-language lang
|
|
||||||
(e number (+ e e) (choose e e))
|
|
||||||
(ec hole (+ e ec) (+ ec e))
|
|
||||||
(v number true false))
|
|
||||||
|
|
||||||
(define reductions
|
|
||||||
(reduction-relation
|
|
||||||
lang
|
|
||||||
(--> (in-hole ec_1 (+ number_1 number_2))
|
|
||||||
(in-hole ec_1 ,(+ (term number_1) (term number_2))))
|
|
||||||
(--> (in-hole ec_1 (choose e_1 e_2))
|
|
||||||
(in-hole ec_1 e_1))
|
|
||||||
(--> (in-hole ec_1 (choose e_1 e_2))
|
|
||||||
(in-hole ec_1 e_2))))
|
|
||||||
|
|
||||||
(define tests-passed 0)
|
|
||||||
|
|
||||||
(define (try-it check in out key/vals)
|
|
||||||
(let ([sp (open-output-string)])
|
|
||||||
(parameterize ([current-output-port sp])
|
|
||||||
(test/text-ui (test-case "X" (check reductions in out))))
|
|
||||||
(let ([s (get-output-string sp)])
|
|
||||||
(for-each
|
|
||||||
(λ (key/val)
|
|
||||||
(let* ([key (car key/val)]
|
|
||||||
[val (cadr key/val)]
|
|
||||||
[m (regexp-match (format "\n~a: ([^\n]*)\n" key) s)])
|
|
||||||
(unless m
|
|
||||||
(error 'try-it "didn't find key ~s in ~s" key s))
|
|
||||||
(unless (if (regexp? val)
|
|
||||||
(regexp-match val (cadr m))
|
|
||||||
(equal? val (cadr m)))
|
|
||||||
(error 'try-in "didn't match key ~s, expected ~s got ~s" key val (cadr m)))))
|
|
||||||
key/vals)))
|
|
||||||
(set! tests-passed (+ tests-passed 1)))
|
|
||||||
|
|
||||||
(try-it check-reduces
|
|
||||||
'(choose 1 2)
|
|
||||||
1
|
|
||||||
'((multiple-results "(2 1)")))
|
|
||||||
|
|
||||||
(try-it check-reduces
|
|
||||||
'(+ 1 2)
|
|
||||||
1
|
|
||||||
'((expected "1")
|
|
||||||
(actual "3")))
|
|
||||||
|
|
||||||
(try-it check-reduces/multiple
|
|
||||||
'(+ (choose 3 4) 1)
|
|
||||||
'(4 6)
|
|
||||||
'((expecteds "(4 6)")
|
|
||||||
(actuals #rx"[(][45] [54][)]")))
|
|
||||||
|
|
||||||
(printf "schemeunit-tests: all ~a tests passed.\n" tests-passed))
|
|
||||||
|
|
@ -1,125 +0,0 @@
|
||||||
(module subst-test mzscheme
|
|
||||||
(require "../subst.ss"
|
|
||||||
(lib "match.ss"))
|
|
||||||
|
|
||||||
(define (lc-subst1 var val exp) (subst/proc var val exp lc-separate))
|
|
||||||
(define (lc-free-vars exp) (free-vars/memoize (make-hash-table) exp lc-separate))
|
|
||||||
(define (lc-rename old-name new-name exp) (alpha-rename old-name new-name exp lc-separate))
|
|
||||||
|
|
||||||
(define lc-subst2
|
|
||||||
(subst
|
|
||||||
[`(lambda ,vars ,body)
|
|
||||||
(all-vars vars)
|
|
||||||
(build (lambda (vars body) `(lambda ,vars ,body)))
|
|
||||||
(subterm vars body)]
|
|
||||||
[`(let (,l-var ,exp) ,body)
|
|
||||||
(all-vars (list l-var))
|
|
||||||
(build (lambda (l-vars exp body) `(let (,@l-vars ,exp) ,body)))
|
|
||||||
(subterm '() exp)
|
|
||||||
(subterm (list l-var) body)]
|
|
||||||
[(? symbol?) (variable)]
|
|
||||||
[(? number?) (constant)]
|
|
||||||
[`(,fun ,@(args ...))
|
|
||||||
(all-vars '())
|
|
||||||
(build (lambda (vars fun . args) `(,fun ,@args)))
|
|
||||||
(subterm '() fun)
|
|
||||||
(subterms '() args)]))
|
|
||||||
|
|
||||||
(define (lc-separate exp constant variable combine sub-piece)
|
|
||||||
(match exp
|
|
||||||
[`(lambda ,vars ,body)
|
|
||||||
(combine (lambda (vars body) `(lambda ,vars ,body))
|
|
||||||
vars
|
|
||||||
(sub-piece vars body))]
|
|
||||||
[`(let (,l-var ,exp) ,body)
|
|
||||||
(combine (lambda (l-vars exp body) `(let (,(car l-vars) ,exp) ,body))
|
|
||||||
(list l-var)
|
|
||||||
(sub-piece '() exp)
|
|
||||||
(sub-piece (list l-var) body))]
|
|
||||||
[(? symbol?) (variable (lambda (x) x) exp)]
|
|
||||||
[(? number?) (constant exp)]
|
|
||||||
[`(,fun ,@(args ...))
|
|
||||||
(apply
|
|
||||||
combine
|
|
||||||
(lambda (variables fun . args) `(,fun ,@args))
|
|
||||||
'()
|
|
||||||
(append
|
|
||||||
(list (sub-piece '() fun))
|
|
||||||
(map (lambda (x) (sub-piece '() x)) args)))]))
|
|
||||||
|
|
||||||
(define test-cases 0)
|
|
||||||
(define failed-tests? #f)
|
|
||||||
|
|
||||||
(define-syntax (test stx)
|
|
||||||
(syntax-case stx ()
|
|
||||||
[(_ test-exp expected)
|
|
||||||
(syntax (test test-exp expected equal?))]
|
|
||||||
[(_ test-exp expected same?)
|
|
||||||
(syntax
|
|
||||||
(let ([actual test-exp]
|
|
||||||
[expected-v expected])
|
|
||||||
;(printf "testing: ~s\n" (syntax-object->datum #'test-exp))
|
|
||||||
(set! test-cases (+ test-cases 1))
|
|
||||||
(unless (same? actual expected-v)
|
|
||||||
(set! failed-tests? #t)
|
|
||||||
(printf " test: ~s\n expected: ~s\n got: ~s\n"
|
|
||||||
(syntax-object->datum #'test-exp)
|
|
||||||
expected-v
|
|
||||||
actual))))]))
|
|
||||||
|
|
||||||
(define (set-equal? xs ys)
|
|
||||||
(and (andmap (lambda (x) (memq x ys)) xs)
|
|
||||||
(andmap (lambda (y) (memq y xs)) ys)))
|
|
||||||
|
|
||||||
(define (lc-tests)
|
|
||||||
(tests lc-free-vars lc-subst1 lc-rename)
|
|
||||||
(tests #f lc-subst2 #f))
|
|
||||||
|
|
||||||
(define (tests free-vars subst rename)
|
|
||||||
(when free-vars
|
|
||||||
(test (free-vars 'x) '(x) set-equal?)
|
|
||||||
(test (free-vars '(lambda (x) x)) '() set-equal?)
|
|
||||||
(test (free-vars '(lambda (x) y)) '(y) set-equal?)
|
|
||||||
(test (free-vars '(let (x 1) x)) '() set-equal?)
|
|
||||||
(test (free-vars '(let (x 1) y)) '(y) set-equal?)
|
|
||||||
(test (free-vars '(let (x x) y)) '(y x) set-equal?)
|
|
||||||
(test (free-vars '(let (x 1) (y y))) '(y) set-equal?)
|
|
||||||
(test (free-vars '(lambda (y) (y y))) '() set-equal?))
|
|
||||||
|
|
||||||
(when rename
|
|
||||||
(test (rename 'x 'y 'x) 'x)
|
|
||||||
(test (rename 'x 'y '(lambda (x) x)) '(lambda (y) y)))
|
|
||||||
|
|
||||||
(test (subst 'x 1 'x) 1)
|
|
||||||
(test (subst 'x 1 'y) 'y)
|
|
||||||
(test (subst 'x 1 '(lambda (x) x)) '(lambda (x) x))
|
|
||||||
(test (subst 'x 1 '(lambda (y) x)) '(lambda (y) 1))
|
|
||||||
(test (subst 'x 'y '(lambda (y) x)) '(lambda (y@) y))
|
|
||||||
(test (subst 'x 'y '(lambda (y) (x y))) '(lambda (y@) (y y@)))
|
|
||||||
(test (subst 'x 'y '(let (x 1) 1)) '(let (x 1) 1))
|
|
||||||
(test (subst 'x 'y '(let (x 1) x)) '(let (x 1) x))
|
|
||||||
(test (subst 'x 'y '(let (x 1) y)) '(let (x 1) y))
|
|
||||||
(test (subst 'x 'y '(let (y 1) (x y))) '(let (y@ 1) (y y@)))
|
|
||||||
(test (subst 'q '(lambda (x) y) '(lambda (y) y)) '(lambda (y) y))
|
|
||||||
(test (subst 'q '(lambda (x) y) '(let ([y q]) y)) '(let ([y (lambda (x) y)]) y))
|
|
||||||
(test (subst 'p '1 '(let (t 2) ((p t) t)))
|
|
||||||
'(let (t 2) ((1 t) t)))
|
|
||||||
(test (subst 'p '(lambda (s) s)
|
|
||||||
'(let (t (lambda (s) s)) ((p t) t)))
|
|
||||||
'(let (t (lambda (s) s)) (((lambda (s) s) t) t)))
|
|
||||||
(test (subst 'p
|
|
||||||
'(lambda (s) (s s))
|
|
||||||
'(let (t (lambda (s) s))
|
|
||||||
p))
|
|
||||||
'(let (t (lambda (s) s))
|
|
||||||
(lambda (s) (s s))))
|
|
||||||
|
|
||||||
(test (subst 's
|
|
||||||
'(lambda (z) (s z))
|
|
||||||
'(lambda (s) (lambda (z) (s z))))
|
|
||||||
'(lambda (s) (lambda (z) (s z))))
|
|
||||||
|
|
||||||
(test (subst 's
|
|
||||||
'(lambda (s) (lambda (z) (s z)))
|
|
||||||
'(lambda (z) (s z)))
|
|
||||||
'(lambda (z) ((lambda (s) (lambda (z) (s z))) z)))))
|
|
||||||
Loading…
Reference in New Issue
Block a user