Adds a Redex version of Jay's continuation mark transformation
This commit is contained in:
Casey Klein
parent
0e169cfbb7
commit
3250ff846c
|
|
@ -1243,7 +1243,7 @@ path/s is either such a string or a list of them.
|
|||
"collects/redex/tests/matcher-test.rkt" drdr:command-line (mzc *)
|
||||
"collects/redex/tests/pict-test.rkt" drdr:command-line (mzc *)
|
||||
"collects/redex/tests/rg-test.rkt" drdr:command-line (mzc *)
|
||||
"collects/redex/tests/run-tests.rkt" drdr:command-line (gracket-text * "--examples" "--no-bitmaps") drdr:timeout 300
|
||||
"collects/redex/tests/run-tests.rkt" drdr:command-line (gracket-text * "--examples" "--no-bitmaps") drdr:timeout 360
|
||||
"collects/redex/tests/term-test.rkt" drdr:command-line (mzc *)
|
||||
"collects/redex/tests/tl-test.rkt" drdr:command-line (mzc *)
|
||||
"collects/repo-time-stamp" responsible (eli)
|
||||
|
|
|
|||
|
|
@ -18,6 +18,10 @@ to demonstrate various different uses of PLT Redex:
|
|||
closure. Also, one of the first examples from Matthias
|
||||
Felleisen and Matthew Flatt's monograph
|
||||
|
||||
cont-mark-transform: the continuation mark transformation from
|
||||
McCarthy's ICFP '09 paper “Automatically RESTful Web Applications
|
||||
Or, Marking Modular Serializable Continuations"
|
||||
|
||||
contracts.rkt: A core contract calculus, including blame,
|
||||
with function contracts, (eager) pair contracts,
|
||||
and a few numeric predicates
|
||||
|
|
|
|||
296
collects/redex/examples/cont-mark-transform/CMT-test.rkt
Normal file
296
collects/redex/examples/cont-mark-transform/CMT-test.rkt
Normal file
|
|
@ -0,0 +1,296 @@
|
|||
#lang racket
|
||||
|
||||
(require "CMT.rkt"
|
||||
"SL-syntax.rkt"
|
||||
"SL-semantics.rkt"
|
||||
"TL-syntax.rkt"
|
||||
"TL-semantics.rkt"
|
||||
"common.rkt"
|
||||
"test-util.rkt"
|
||||
redex)
|
||||
|
||||
(define-syntax (test-translation stx)
|
||||
(syntax-case stx ()
|
||||
[(_ expr)
|
||||
#`(with-handlers ([exn:fail?
|
||||
(λ (exn)
|
||||
#,(syntax/loc stx
|
||||
(test-equal (exn-message exn) "")))])
|
||||
(let ([e (term expr)])
|
||||
(let ([v ((make-eval -->SL (redex-match SL v))
|
||||
(term (∅ / ,e)))]
|
||||
[u ((make-eval -->TL (redex-match TL v))
|
||||
(term (∅ / (translate ,e))))])
|
||||
#,(syntax/loc stx (test-equal u v)))))]))
|
||||
|
||||
(test-translation
|
||||
((λ (x) ("S" x))
|
||||
(call/cc (λ (k) (k ("Z"))))))
|
||||
|
||||
; two marks with the same key on the same frame
|
||||
(test-translation
|
||||
((λ (x) x)
|
||||
(w-c-m ("a") ("1")
|
||||
(w-c-m ("a") ("2")
|
||||
(c-c-m [("a")])))))
|
||||
|
||||
; mark reapplied to the reconstituted continuation
|
||||
(test-translation
|
||||
(w-c-m ("a") ("1")
|
||||
(w-c-m ("a") ("2")
|
||||
((λ (x) (x))
|
||||
(call/cc (λ (k) (k (λ () (c-c-m [("a")])))))))))
|
||||
|
||||
; variables as keys/values in w-c-ms in context
|
||||
(test-translation
|
||||
((λ (x y z)
|
||||
(w-c-m x y
|
||||
(w-c-m x z
|
||||
((λ (x) (x))
|
||||
(call/cc (λ (k) (k (λ () (c-c-m [x])))))))))
|
||||
("a") ("1") ("2")))
|
||||
|
||||
; transforms a context that includes variables in application frame
|
||||
(test-translation
|
||||
((λ (f)
|
||||
(f (w-c-m ("a") ("1")
|
||||
((call/cc (λ (k) (k (λ () (c-c-m [("a")])))))))))
|
||||
(λ (x) x)))
|
||||
|
||||
; transformation within installed continuation marks
|
||||
(test-translation
|
||||
(w-c-m ("a") (λ () (call/cc (λ (k) (k (λ () (c-c-m [("a")]))))))
|
||||
((λ (frames)
|
||||
(match frames
|
||||
[("cons" cms _)
|
||||
(match cms
|
||||
[("cons" cm _)
|
||||
(match cm
|
||||
[("cons" _ t)
|
||||
((t))])])]))
|
||||
(c-c-m [("a")]))))
|
||||
|
||||
; a continuation, in a values-only position, that contains
|
||||
; multiple frames, each with continuation marks
|
||||
(test-translation
|
||||
(letrec ([(ref k) (κ ((λ (x) ("outer" x))
|
||||
(w-c-m ("a") ("1")
|
||||
(w-c-m ("b") ("2")
|
||||
((λ (x) ("inner" x))
|
||||
(w-c-m ("a") ("3")
|
||||
(w-c-m ("b") ("4")
|
||||
(hole))))))))])
|
||||
((λ (x) ("skipped" x))
|
||||
((ref k) (λ () (c-c-m [("a") ("b")]))))))
|
||||
|
||||
; produces a call to map-set where one argument is a (K x).
|
||||
(test-translation
|
||||
(λ (x) (w-c-m ("k" x) ("l") (x))))
|
||||
|
||||
; application and match translation redexes allow variables
|
||||
; in datatype instances
|
||||
(test-translation
|
||||
(λ (x) (x ("k" x))))
|
||||
(test-translation
|
||||
(λ (x) (match ("k" x) [("k" x) x])))
|
||||
|
||||
; w-c-m translation redex with non-w body
|
||||
(test-translation
|
||||
(λ (x)
|
||||
(w-c-m ("a") ("b")
|
||||
("c" x))))
|
||||
|
||||
; continuation value in continuation mark of a continuation value
|
||||
(test-translation
|
||||
((λ (x) ("skipped" x))
|
||||
((κ (w-c-m ("a") (κ ((λ (x) ("wrapped" x)) hole))
|
||||
((λ (x) ("skipped" x))
|
||||
(hole))))
|
||||
(λ ()
|
||||
((λ (ms)
|
||||
(match ms
|
||||
[("cons" f _)
|
||||
(match f
|
||||
[("cons" m _)
|
||||
(match m
|
||||
[("cons" _ k)
|
||||
(k ("a"))])])]))
|
||||
(c-c-m [("a")]))))))
|
||||
|
||||
(test-->>
|
||||
-->TL
|
||||
#:cycles-ok
|
||||
(term
|
||||
(∅
|
||||
/
|
||||
(translate
|
||||
((λ (t) (t t))
|
||||
(call/cc (λ (x) (call/cc x))))))))
|
||||
|
||||
(test-translation
|
||||
((λ (bh)
|
||||
((λ (x y) ("pair" x y))
|
||||
bh
|
||||
(λ (x) x)))
|
||||
(letrec ([(ref bh) (ref bh)]) (ref bh))))
|
||||
|
||||
(test-TL-result
|
||||
(make-store [reverse ,TL-reverse])
|
||||
(,TL-equal? ("1") ("1"))
|
||||
("true"))
|
||||
|
||||
(test-TL-result
|
||||
(make-store [reverse ,TL-reverse])
|
||||
(,TL-equal? ("1") ("2"))
|
||||
("false"))
|
||||
|
||||
(test-TL-result
|
||||
(make-store [reverse ,TL-reverse])
|
||||
(w-c-m ("1") ("whatever") (,TL-equal? ("1") ("1")))
|
||||
("true"))
|
||||
|
||||
(test-TL-result
|
||||
(make-store [equal? ,TL-equal?] [reverse ,TL-reverse] [map-set ,map-set])
|
||||
((ref map-set) ("nil") ("1") ("a"))
|
||||
("cons" ("cons" ("1") ("a")) ("nil")))
|
||||
|
||||
(test-TL-result
|
||||
(make-store [equal? ,TL-equal?] [reverse ,TL-reverse] [map-set ,map-set])
|
||||
((ref map-set) ("cons" ("cons" ("1") ("a"))
|
||||
("cons" ("cons" ("2") ("b"))
|
||||
("nil")))
|
||||
("2") ("c"))
|
||||
("cons" ("cons" ("1") ("a"))
|
||||
("cons" ("cons" ("2") ("c"))
|
||||
("nil"))))
|
||||
|
||||
(test-TL-result
|
||||
(make-store [c-w-i-c-m ,c-w-i-c-m] [reverse ,TL-reverse])
|
||||
(w-c-m ("a") ("1")
|
||||
((λ (x) x)
|
||||
((ref c-w-i-c-m) ("a") (λ (x) x) ("2"))))
|
||||
("2"))
|
||||
|
||||
(test-TL-result
|
||||
(make-store [c-w-i-c-m ,c-w-i-c-m] [reverse ,TL-reverse])
|
||||
(w-c-m ("a") ("1")
|
||||
((ref c-w-i-c-m) ("a") (λ (x) ("b" x)) ("dontcare")))
|
||||
("b" ("1")))
|
||||
|
||||
(test-TL-result
|
||||
(make-store [restore-marks ,restore-marks])
|
||||
((ref restore-marks)
|
||||
("cons" ("cons" ("a") ("1"))
|
||||
("cons" ("cons" ("b") ("2"))
|
||||
("nil")))
|
||||
(λ () (c-c-m [("a") ("b")])))
|
||||
("cons"
|
||||
("cons" ("cons" ("b") ("2"))
|
||||
("cons" ("cons" ("a") ("1"))
|
||||
("nil")))
|
||||
("nil")))
|
||||
|
||||
;; Variables and Values
|
||||
(test-equal (term (CMT/a z)) (term z))
|
||||
(test-equal (term (CMT/a (ref foo))) (term (ref foo)))
|
||||
(test-equal (term (CMT/a (λ (x) z))) (term (λ (x) z)))
|
||||
|
||||
(define TL-empty-cont
|
||||
(term (λ (x)
|
||||
(abort
|
||||
((ref resume)
|
||||
("cons"
|
||||
("cons" ("cons" ("diamond") ("nil"))
|
||||
("nil"))
|
||||
("nil"))
|
||||
x)))))
|
||||
(test-equal (term (CMT/a (κ hole))) TL-empty-cont)
|
||||
|
||||
(test-equal
|
||||
(term (CMT/a (κ ((ref f) (ref y) hole))))
|
||||
(term (λ (x1)
|
||||
(abort
|
||||
((ref resume)
|
||||
("cons"
|
||||
("cons" ("cons" ("diamond") ("nil"))
|
||||
("nil"))
|
||||
("cons"
|
||||
("cons" ("cons" ("diamond") ("nil"))
|
||||
("cons"
|
||||
("cons" ("square") (λ (x) ((ref f) (ref y) x)))
|
||||
("nil")))
|
||||
("nil")))
|
||||
x1)))))
|
||||
|
||||
(test-equal (term (CMT/a ("nil"))) (term ("nil")))
|
||||
(test-equal (term (CMT/a ("cons" x ("nil")))) (term ("cons" x ("nil"))))
|
||||
|
||||
(test-equal
|
||||
(term (CMT/a ("cons" (κ hole) ("nil"))))
|
||||
(term ("cons" ,TL-empty-cont ("nil"))))
|
||||
|
||||
;; Redexes
|
||||
(test-equal (term (CMT/r (f x y))) (term (f x y)))
|
||||
(test-equal
|
||||
(term (CMT/r (f x (κ hole))))
|
||||
(term (f x ,TL-empty-cont)))
|
||||
|
||||
(test-equal (term (CMT/r (letrec ([(ref x) ("nil")]) z)))
|
||||
(term (letrec ([(ref x) ("nil")]) z)))
|
||||
|
||||
(test-equal
|
||||
(term (CMT/r (letrec ([(ref x) (κ hole)])
|
||||
(κ hole))))
|
||||
(term (letrec ([(ref x) ,TL-empty-cont])
|
||||
,TL-empty-cont)))
|
||||
|
||||
(test-equal (term (CMT/r (call/cc f)))
|
||||
(term (f ((ref kont/ms) (c-c-m [("square") ("diamond")])))))
|
||||
|
||||
(test-equal (term (CMT/r (match (κ hole) [("nil") (κ hole)])))
|
||||
(term (match ,TL-empty-cont
|
||||
[("nil") ,TL-empty-cont])))
|
||||
|
||||
;; Contexts
|
||||
(test-equal (term (CMT/T hole)) (term hole))
|
||||
|
||||
(test-equal (term (CMT/T ((ref f) (ref y) hole)))
|
||||
(term ((λ (x) ((ref f) (ref y) x))
|
||||
(w-c-m ("square") (λ (x) ((ref f) (ref y) x))
|
||||
hole))))
|
||||
|
||||
;; Compositions + Whole Programs
|
||||
(test-equal
|
||||
(term (CMT ((ref f) (ref y) (call/cc (λ (k) (k z))))))
|
||||
(term
|
||||
((λ (x) ((ref f) (ref y) x))
|
||||
(w-c-m ("square") (λ (x) ((ref f) (ref y) x))
|
||||
((λ (k) (k z))
|
||||
((ref kont/ms) (c-c-m [("square") ("diamond")])))))))
|
||||
|
||||
;; Sub-units of big test
|
||||
(test-equal (term (CMT ((ref +) ,(num 1) tmp)))
|
||||
(term ((ref +) ,(num 1) tmp)))
|
||||
|
||||
;;; Running the resulting programs
|
||||
(define (CMT--> sl-version expected-ans)
|
||||
(define tl-version
|
||||
(term (translate ,sl-version)))
|
||||
(test-TL-result
|
||||
(make-store [= ,=-impl]
|
||||
[+ ,+-impl]
|
||||
[- ,--impl]
|
||||
[* ,*-impl]
|
||||
[if ,if-impl])
|
||||
,tl-version
|
||||
,expected-ans))
|
||||
|
||||
(CMT--> `(call/cc (λ (k)
|
||||
((λ (tmp) ((ref +) ,(num 2) tmp))
|
||||
(k ,(num 3)))))
|
||||
(num 3))
|
||||
(CMT--> `((λ (tmp) ((ref +) ,(num 1) tmp))
|
||||
(call/cc (λ (k)
|
||||
((λ (tmp) ((ref +) ,(num 2) tmp))
|
||||
(k ,(num 3))))))
|
||||
(num 4))
|
||||
232
collects/redex/examples/cont-mark-transform/CMT.rkt
Normal file
232
collects/redex/examples/cont-mark-transform/CMT.rkt
Normal file
|
|
@ -0,0 +1,232 @@
|
|||
#lang racket
|
||||
|
||||
(require "SL-syntax.rkt"
|
||||
"SL-semantics.rkt"
|
||||
"TL-syntax.rkt"
|
||||
redex)
|
||||
|
||||
(provide CMT translate
|
||||
TL-equal? TL-reverse
|
||||
map-set c-w-i-c-m
|
||||
restore-marks resume
|
||||
CMT/a CMT/r CMT/T)
|
||||
|
||||
(define-metafunction SL
|
||||
[(CMT a) (CMT/a a)]
|
||||
[(CMT (in-hole T r))
|
||||
(in-hole (CMT/T T) (CMT/r r))])
|
||||
|
||||
(define-metafunction SL
|
||||
[(CMT/a x) x]
|
||||
[(CMT/a σ) σ]
|
||||
[(CMT/a (λ (x ...) e))
|
||||
(λ (x ...) (CMT e))]
|
||||
[(CMT/a (κ E))
|
||||
(λ (x) (abort ((ref resume) v x)))
|
||||
(where v (resume-marks E))
|
||||
(where x ,(variable-not-in (term v) (term x)))]
|
||||
[(CMT/a (K a ...))
|
||||
(K (CMT/a a) ...)])
|
||||
|
||||
(define-metafunction SL
|
||||
[(CMT/r (a ...))
|
||||
((CMT/a a) ...)]
|
||||
[(CMT/r (letrec ([σ w] ...) e))
|
||||
(letrec ([σ (CMT/a w)] ...) (CMT e))]
|
||||
[(CMT/r (w-c-m a ...))
|
||||
(w-c-m (CMT/a a) ...)]
|
||||
[(CMT/r (c-c-m [a ...]))
|
||||
(c-c-m [(CMT/a a) ...])]
|
||||
[(CMT/r (match a l ...))
|
||||
(match (CMT/a a) (CMT/r l) ...)]
|
||||
[(CMT/r [(K x ...) e])
|
||||
[(K x ...) (CMT e)]]
|
||||
[(CMT/r (abort e))
|
||||
(abort (CMT e))]
|
||||
[(CMT/r (call/cc w))
|
||||
((CMT/a w) ((ref kont/ms) (c-c-m [("square") ("diamond")])))])
|
||||
|
||||
(define-metafunction SL
|
||||
[(CMT/T hole) hole]
|
||||
[(CMT/T (a ... T))
|
||||
(v_K (w-c-m ("square") v_K (CMT/T T)))
|
||||
(where (a_* ...) ((CMT/a a) ...))
|
||||
(where x ,(variable-not-in (term (a_* ...)) (term x)))
|
||||
(where v_K (λ (x) (a_* ... x)))]
|
||||
[(CMT/T (w-c-m a_1 a_2 T))
|
||||
(w-c-m a_1* a_2*
|
||||
((ref c-w-i-c-m)
|
||||
("diamond")
|
||||
(λ (x_cms)
|
||||
((λ (x_cms’)
|
||||
(w-c-m ("diamond") x_cms’ any_T))
|
||||
((ref map-set) x_cms a_1* a_2*)))
|
||||
("nil")))
|
||||
(where any_T (CMT/T T)) ; w-c-m case does not produce a T
|
||||
(where a_1* (CMT/a a_1))
|
||||
(where a_2* (CMT/a a_2))
|
||||
(where (x_cms x_cms’) ,(variables-not-in (term (any_T a_1* a_2*)) '(cms cms’)))])
|
||||
|
||||
(define-metafunction SL
|
||||
[(resume-marks E)
|
||||
(resume-marks E #f ("nil"))]
|
||||
|
||||
[(resume-marks hole k a_m)
|
||||
("cons" (frame-marks k a_m) ("nil"))]
|
||||
[(resume-marks (w-c-m a_1 a_2 T) k a_m)
|
||||
(resume-marks T k ("cons" ("cons" (CMT a_1) (CMT a_2)) a_m))]
|
||||
[(resume-marks (a ... T) k a_m)
|
||||
("cons" (frame-marks k a_m)
|
||||
(resume-marks T (λ (x) (a_* ... x)) ("nil")))
|
||||
(where (a_* ...) ((CMT a) ...))
|
||||
(where x ,(variable-not-in (term (a_* ...)) (term x)))])
|
||||
|
||||
(define-metafunction SL
|
||||
[(frame-marks #f a_m)
|
||||
("cons" ("cons" ("diamond") (reverse-marks a_m))
|
||||
("nil"))]
|
||||
[(frame-marks v_k a_m)
|
||||
("cons" ("cons" ("diamond") (reverse-marks a_m))
|
||||
("cons" ("cons" ("square") v_k)
|
||||
("nil")))])
|
||||
|
||||
(define-metafunction SL
|
||||
[(reverse-marks a)
|
||||
(reverse-marks a ("nil"))]
|
||||
[(reverse-marks ("nil") a) a]
|
||||
[(reverse-marks ("cons" a_1 a_2) a_3)
|
||||
(reverse-marks a_2 ("cons" a_1 a_3))])
|
||||
|
||||
(define-metafunction SL
|
||||
translate : e_1 -> (side-condition e_2 (TL-e? (term e_2)))
|
||||
[(translate e)
|
||||
(letrec ([(ref resume) ,resume]
|
||||
[(ref restore-marks) ,restore-marks]
|
||||
[(ref c-w-i-c-m) ,c-w-i-c-m]
|
||||
[(ref map-set) ,map-set]
|
||||
[(ref kont/ms) ,kont/ms]
|
||||
[(ref equal?) ,TL-equal?]
|
||||
[(ref reverse) ,TL-reverse])
|
||||
(CMT e))])
|
||||
(define TL-e? (redex-match TL e))
|
||||
|
||||
(define kont/ms
|
||||
(term
|
||||
(λ (m)
|
||||
(λ (x)
|
||||
(abort ((ref resume) m x))))))
|
||||
|
||||
(define c-w-i-c-m
|
||||
(term
|
||||
(λ (k proc default-v)
|
||||
((λ (cms)
|
||||
((λ (reversed)
|
||||
(proc
|
||||
(match reversed
|
||||
[("cons" _ rest)
|
||||
(match rest
|
||||
[("cons" frame _)
|
||||
(match frame
|
||||
[("nil") default-v]
|
||||
[("cons" mark _)
|
||||
(match mark
|
||||
[("cons" _ value) value])])])])))
|
||||
((ref reverse) cms ("nil"))))
|
||||
(c-c-m [k])))))
|
||||
|
||||
(define map-set
|
||||
(term
|
||||
(λ (map k v)
|
||||
(match map
|
||||
[("nil") ("cons" ("cons" k v) ("nil"))]
|
||||
[("cons" pair rest)
|
||||
(match pair
|
||||
[("cons" k’ v’)
|
||||
((λ (eq)
|
||||
(match eq
|
||||
[("true")
|
||||
("cons" ("cons" k v) rest)]
|
||||
[("false")
|
||||
((λ (rest’) ("cons" pair rest’))
|
||||
((ref map-set) rest k v))]))
|
||||
((ref equal?) k k’))])]))))
|
||||
|
||||
(define restore-marks
|
||||
(term
|
||||
(λ (cms thnk)
|
||||
(match cms
|
||||
[("nil") (thnk)]
|
||||
[("cons" cm cms)
|
||||
(match cm
|
||||
[("cons" m v)
|
||||
(w-c-m m v
|
||||
((ref restore-marks) cms thnk))])]))))
|
||||
|
||||
(define resume
|
||||
(term
|
||||
(λ (l v)
|
||||
(match l
|
||||
[("nil") v]
|
||||
[("cons" ms l)
|
||||
(match ms
|
||||
[("nil") ((ref resume) l v)]
|
||||
[("cons" m ms)
|
||||
(match m
|
||||
[("cons" j u)
|
||||
(match j
|
||||
[("square")
|
||||
(match ms
|
||||
[("nil")
|
||||
(u (w-c-m ("square") u
|
||||
((ref resume) l v)))]
|
||||
; How do you get a frame with both marks where square appears first?
|
||||
; All frames not introduced by "runtime" calls are marked first with
|
||||
; square (thus reported after any diamond mark), and `resume' seems
|
||||
; to restore this invariant. Use randomized testing to investigate.
|
||||
[("cons" cms-mark _)
|
||||
(match cms-mark
|
||||
[("cons" _ cms)
|
||||
(u (w-c-m ("square") u
|
||||
((ref restore-marks)
|
||||
cms
|
||||
(λ ()
|
||||
(w-c-m ("diamond") cms ((ref resume) l v))))))])])]
|
||||
[("diamond")
|
||||
(match ms
|
||||
[("nil")
|
||||
((ref restore-marks)
|
||||
u
|
||||
(λ () (w-c-m ("diamond") u ((ref resume) l v))))]
|
||||
[("cons" kont-mark _)
|
||||
(match kont-mark
|
||||
[("cons" _ k)
|
||||
(k (w-c-m ("square") k
|
||||
((ref restore-marks)
|
||||
u
|
||||
(λ ()
|
||||
(w-c-m ("diamond") u ((ref resume) l v))))))])])])])])]))))
|
||||
|
||||
(define TL-equal?
|
||||
(term
|
||||
(λ (x y)
|
||||
((λ (cms)
|
||||
((λ (reversed)
|
||||
(match reversed
|
||||
[("cons" frame _)
|
||||
(match frame
|
||||
[("cons" _ rest)
|
||||
(match rest
|
||||
[("nil") ("true")]
|
||||
[("cons" _ __) ("false")])])]))
|
||||
((ref reverse) cms ("nil"))))
|
||||
(w-c-m x ("")
|
||||
(w-c-m y ("")
|
||||
(c-c-m [x y])))))))
|
||||
|
||||
(define TL-reverse
|
||||
(term
|
||||
(λ (xs onto)
|
||||
(match xs
|
||||
[("nil") onto]
|
||||
[("cons" x xs’)
|
||||
((ref reverse) xs’ ("cons" x onto))]))))
|
||||
|
|
@ -0,0 +1,376 @@
|
|||
#lang racket
|
||||
|
||||
(require "SL-syntax.rkt"
|
||||
"SL-semantics.rkt"
|
||||
"common.rkt"
|
||||
"test-util.rkt"
|
||||
redex)
|
||||
|
||||
(test-SL-result
|
||||
∅
|
||||
((λ (x) ("S" x)) ("Z"))
|
||||
("S" ("Z")))
|
||||
|
||||
(test-SL-stuck ∅ ((λ (x) ("S" x)) ("Z") ("Z")))
|
||||
|
||||
(test-SL-result
|
||||
∅
|
||||
(match ("a" ("1"))
|
||||
[("a" x) x]
|
||||
[("b" y) y])
|
||||
("1"))
|
||||
|
||||
(test-SL-result
|
||||
∅
|
||||
(match ("b" ("1"))
|
||||
[("a" x) x]
|
||||
[("b" y) y])
|
||||
("1"))
|
||||
|
||||
(test-SL-stuck
|
||||
∅
|
||||
(match ("a" ("1"))
|
||||
[("a" x) x]
|
||||
[("a" y) y]))
|
||||
|
||||
(test-SL-result
|
||||
∅
|
||||
(letrec ([(ref build-list)
|
||||
(λ (n f)
|
||||
(match n
|
||||
[("Z") ("nil")]
|
||||
[("S" m)
|
||||
((λ (x)
|
||||
((λ (xs) ("cons" x xs))
|
||||
((ref build-list) m f)))
|
||||
(f m))]))])
|
||||
((ref build-list) ("S" ("S" ("S" ("Z")))) (λ (i) ("S" i))))
|
||||
("cons" ("S" ("S" ("S" ("Z"))))
|
||||
("cons" ("S" ("S" ("Z")))
|
||||
("cons" ("S" ("Z"))
|
||||
("nil")))))
|
||||
|
||||
(test-SL-result
|
||||
∅
|
||||
((λ (clobber)
|
||||
((λ (a)
|
||||
((λ (b) (a))
|
||||
(clobber ("b"))))
|
||||
(clobber ("a"))))
|
||||
(λ (x)
|
||||
(letrec ([(ref y) (λ () x)])
|
||||
(ref y))))
|
||||
("b"))
|
||||
|
||||
(test-SL-result
|
||||
∅
|
||||
(letrec ([(ref x) ("S" ("Z"))])
|
||||
(match (ref x)
|
||||
[("Z") ("a")]
|
||||
[("S" _) ("b")]))
|
||||
("b"))
|
||||
|
||||
(test-SL-result
|
||||
∅
|
||||
(w-c-m ("a") ("1")
|
||||
((λ (x) x)
|
||||
(w-c-m ("a") ("2")
|
||||
(c-c-m [("a")]))))
|
||||
("cons"
|
||||
("cons" ("cons" ("a") ("1")) ("nil"))
|
||||
("cons" ("cons" ("cons" ("a") ("2")) ("nil"))
|
||||
("nil"))))
|
||||
|
||||
(test-SL-result
|
||||
∅
|
||||
(w-c-m ("a") ("1")
|
||||
(w-c-m ("b") ("2")
|
||||
(c-c-m [("a") ("b")])))
|
||||
("cons" ("cons" ("cons" ("b") ("2"))
|
||||
("cons" ("cons" ("a") ("1")) ("nil")))
|
||||
("nil")))
|
||||
|
||||
(test-SL-result
|
||||
∅
|
||||
(w-c-m ("a") ("1")
|
||||
(w-c-m ("b") ("2")
|
||||
(c-c-m [("b") ("a")])))
|
||||
("cons" ("cons" ("cons" ("b") ("2"))
|
||||
("cons" ("cons" ("a") ("1")) ("nil")))
|
||||
("nil")))
|
||||
|
||||
(test-SL-result
|
||||
∅
|
||||
(w-c-m ("a") ("1")
|
||||
(c-c-m [("b") ("a")]))
|
||||
("cons" ("cons" ("cons" ("a") ("1")) ("nil"))
|
||||
("nil")))
|
||||
|
||||
(test-SL-result
|
||||
∅
|
||||
(w-c-m ("a") ("1")
|
||||
((λ (x) x)
|
||||
((λ (x) x)
|
||||
((λ (x) x)
|
||||
(w-c-m ("a") ("2")
|
||||
(w-c-m ("b") ("1")
|
||||
(c-c-m [("a") ("b")])))))))
|
||||
("cons"
|
||||
("cons" ("cons" ("a") ("1")) ("nil"))
|
||||
("cons" ("nil")
|
||||
("cons" ("nil")
|
||||
("cons"
|
||||
("cons"
|
||||
("cons" ("b") ("1"))
|
||||
("cons" ("cons" ("a") ("2"))
|
||||
("nil")))
|
||||
("nil"))))))
|
||||
|
||||
(test-SL-result
|
||||
∅
|
||||
(w-c-m ("a") ("1")
|
||||
((λ (x) x)
|
||||
(c-c-m [("a")])))
|
||||
("cons"
|
||||
("cons" ("cons" ("a") ("1")) ("nil"))
|
||||
("cons" ("nil") ("nil"))))
|
||||
|
||||
(test-SL-result
|
||||
∅
|
||||
((λ (_)
|
||||
((λ (x) (x x))
|
||||
(λ (x) (x x))))
|
||||
(abort ("Z")))
|
||||
("Z"))
|
||||
|
||||
(test-SL-result
|
||||
∅
|
||||
((λ (x)
|
||||
(match x
|
||||
[("Z") ("a")]
|
||||
[("S" _) ("b")]))
|
||||
(call/cc
|
||||
(λ (k)
|
||||
((λ (_)
|
||||
((λ (x) (x x))
|
||||
(λ (x) (x x))))
|
||||
(k ("Z"))))))
|
||||
("a"))
|
||||
|
||||
(test-SL-result
|
||||
∅
|
||||
((λ (x) ("S" ("S" x)))
|
||||
(letrec ([(ref k) (κ ((λ (x) ("S" x)) hole))])
|
||||
((ref k) ("Z"))))
|
||||
("S" ("Z")))
|
||||
|
||||
(test-SL-result
|
||||
∅
|
||||
((λ (x)
|
||||
(match ("b" x)
|
||||
[("b" x) x]))
|
||||
("a"))
|
||||
("a"))
|
||||
|
||||
(test-->>
|
||||
-->SL
|
||||
#:cycles-ok
|
||||
(term
|
||||
(∅
|
||||
/
|
||||
((λ (t) (t t))
|
||||
(call/cc (λ (x) (call/cc x)))))))
|
||||
|
||||
;; fact
|
||||
(define fact-impl
|
||||
`(λ (n)
|
||||
,(:if `((ref =) n ,(num 0))
|
||||
(:let 'marks '(c-c-m [("fact")])
|
||||
'(abort marks))
|
||||
`(w-c-m ("fact") n
|
||||
,(:let 'sub1-fact
|
||||
(:let 'sub1 `((ref -) n ,(num 1))
|
||||
`((ref fact) sub1))
|
||||
`((ref *) n sub1-fact))))))
|
||||
(define fact-tr-impl
|
||||
`(λ (n a)
|
||||
,(:if `((ref =) n ,(num 0))
|
||||
(:let 'marks '(c-c-m [("fact")])
|
||||
'(abort marks))
|
||||
`(w-c-m ("fact") n
|
||||
,(:let 'sub1 `((ref -) n ,(num 1))
|
||||
(:let 'multa `((ref *) n a)
|
||||
`((ref fact-tr) sub1 multa)))))))
|
||||
(define (test-fact n)
|
||||
(test-SL-result
|
||||
∅
|
||||
,(with-arith
|
||||
`(letrec ([(ref fact) ,fact-impl])
|
||||
((ref fact) ,(num n))))
|
||||
,(lst (append (build-list n (λ (i) (term ("cons" ("cons" ("fact") ,(num (- n i))) ("nil")))))
|
||||
(list (term ("nil")) ; frame computing 1 * fact(0)
|
||||
(term ("nil"))))))) ; frame that names c-c-m result
|
||||
(define (test-fact-tr n)
|
||||
(test-SL-result
|
||||
∅
|
||||
,(with-arith
|
||||
`(letrec ([(ref fact-tr) ,fact-tr-impl])
|
||||
((ref fact-tr) ,(num n) ,(num 1))))
|
||||
,(lst (list (term ("cons" ("cons" ("fact") ,(num 1)) ("nil")))
|
||||
(term ("nil")))))) ; frame that names c-c-m result
|
||||
(for ([i (in-range 1 4)]) (test-fact i))
|
||||
(for ([i (in-range 1 4)]) (test-fact-tr i))
|
||||
|
||||
;;; Values
|
||||
(test-->> -->SL
|
||||
'(∅ / (λ (x) x))
|
||||
'(∅ / (λ (x) x)))
|
||||
(test-->> -->SL
|
||||
'(∅ / ("nil"))
|
||||
'(∅ / ("nil")))
|
||||
(test-->> -->SL
|
||||
'(∅ / ("S" ("0")))
|
||||
'(∅ / ("S" ("0"))))
|
||||
(test-->> -->SL
|
||||
'(∅ / (ref x))
|
||||
'(∅ / (ref x)))
|
||||
|
||||
;;; Applications
|
||||
(test-->> -->SL
|
||||
'(∅ / ((λ (x) x) ("nil")))
|
||||
'(∅ / ("nil")))
|
||||
|
||||
;;; Store applications
|
||||
(test-->> -->SL
|
||||
'((∅ [(ref x) ↦ (λ (x) ("nil"))])
|
||||
/
|
||||
((ref x) ("0")))
|
||||
'((∅ [(ref x) ↦ (λ (x) ("nil"))])
|
||||
/
|
||||
("nil")))
|
||||
|
||||
;;; Letrec
|
||||
(test-->> -->SL
|
||||
'(∅ / (letrec ([(ref x) (λ (x) ("nil"))])
|
||||
("foo")))
|
||||
'((∅ [(ref x) ↦ (λ (x) ("nil"))])
|
||||
/
|
||||
("foo")))
|
||||
(test-->> -->SL
|
||||
'(∅ / (letrec ([(ref x) (λ (x) ("nil"))])
|
||||
((ref x) ("0"))))
|
||||
'((∅ [(ref x) ↦ (λ (x) ("nil"))])
|
||||
/
|
||||
("nil")))
|
||||
|
||||
;;; match
|
||||
(test-->> -->SL
|
||||
'(∅ / (match ("S" ("0"))
|
||||
[("S" n) n]
|
||||
[("0") ("0")]))
|
||||
'(∅ / ("0")))
|
||||
(test-->> -->SL
|
||||
'(∅ / (match ("S" ("0"))
|
||||
[("0") ("0")]
|
||||
[("S" n) n]))
|
||||
'(∅ / ("0")))
|
||||
|
||||
; Store match
|
||||
(test-->> -->SL
|
||||
'(∅ / (letrec ([(ref x) ("S" ("0"))])
|
||||
(match (ref x)
|
||||
[("S" n) n]
|
||||
[("0") ("0")])))
|
||||
'((∅ [(ref x) ↦ ("S" ("0"))])
|
||||
/
|
||||
("0")))
|
||||
|
||||
;; w-c-m
|
||||
(test-->> -->SL
|
||||
`(∅ / (w-c-m ("k") ,(num 1) ,(num 2)))
|
||||
`(∅ / ,(num 2)))
|
||||
(test-->> -->SL
|
||||
`(∅ / (w-c-m ("k") ,(num 1) (w-c-m ("k") ,(num 3) ,(num 2))))
|
||||
`(∅ / ,(num 2)))
|
||||
(test-->> -->SL
|
||||
`(∅ / (w-c-m ("k") ,(num 1) ((λ (x) x) ,(num 2))))
|
||||
`(∅ / ,(num 2)))
|
||||
|
||||
;; c-c-m
|
||||
(test-->> -->SL
|
||||
`(∅ / (c-c-m [("k")]))
|
||||
`(∅ / ("cons" ("nil") ("nil"))))
|
||||
(test-->> -->SL
|
||||
`(∅ / (w-c-m ("k") ,(num 1) (c-c-m [("k")])))
|
||||
`(∅ / ("cons" ("cons" ("cons" ("k") ,(num 1)) ("nil")) ("nil"))))
|
||||
(test-->> -->SL
|
||||
`(∅ / (w-c-m ("k") ,(num 1) (w-c-m ("k") ,(num 2) (c-c-m [("k")]))))
|
||||
`(∅ / ("cons" ("cons" ("cons" ("k") ,(num 2)) ("nil")) ("nil"))))
|
||||
(test-->> -->SL
|
||||
`(∅ / (w-c-m ("k") ,(num 1) ((λ (x) x) (w-c-m ("k") ,(num 2) (c-c-m [("k")])))))
|
||||
`(∅ / ("cons" ("cons" ("cons" ("k") ,(num 1)) ("nil"))
|
||||
("cons" ("cons" ("cons" ("k") ,(num 2)) ("nil"))
|
||||
("nil")))))
|
||||
|
||||
(test-->> -->SL
|
||||
`(∅ / (w-c-m ("k1") ,(num 1) (c-c-m [("k1") ("k2")])))
|
||||
`(∅ / ("cons" ("cons" ("cons" ("k1") ,(num 1)) ("nil")) ("nil"))))
|
||||
(test-->> -->SL
|
||||
`(∅ / (w-c-m ("k1") ,(num 1) (w-c-m ("k2") ,(num 2) (c-c-m [("k1") ("k2")]))))
|
||||
`(∅ / ("cons" ("cons" ("cons" ("k2") ,(num 2))
|
||||
("cons" ("cons" ("k1") ,(num 1))
|
||||
("nil")))
|
||||
("nil"))))
|
||||
|
||||
;; abort
|
||||
(test-->> -->SL
|
||||
`(∅ / (abort ,(num 2)))
|
||||
`(∅ / ,(num 2)))
|
||||
(test-->> -->SL
|
||||
`(∅ / ((λ (x) x) (abort ,(num 2))))
|
||||
`(∅ / ,(num 2)))
|
||||
|
||||
;; arith
|
||||
(test-->> -->SL
|
||||
`(∅ / ,(:let 'x (num 1) 'x))
|
||||
`(∅ / ,(num 1)))
|
||||
(test-SL-result ∅ ,(with-arith (num 1)) ,(num 1))
|
||||
(test-SL-result ∅ ,(with-arith `((ref +) ,(num 1) ,(num 1))) ,(num 2))
|
||||
(test-SL-result ∅ ,(with-arith `((ref *) ,(num 2) ,(num 2))) ,(num 4))
|
||||
(test-SL-result ∅ ,(with-arith `((ref =) ,(num 2) ,(num 2))) ("#t"))
|
||||
(test-SL-result ∅ ,(with-arith `((ref =) ,(num 2) ,(num 3))) ("#f"))
|
||||
(test-SL-result ∅ ,(with-arith `((ref -) ,(num 3) ,(num 2))) ,(num 1))
|
||||
(test-SL-result ∅ ,(with-arith (:if '("#t") (num 1) (num 2))) ,(num 1))
|
||||
(test-SL-result ∅ ,(with-arith (:if '("#f") (num 1) (num 2))) ,(num 2))
|
||||
|
||||
;; call/cc
|
||||
(test-->> -->SL
|
||||
`(∅ / (call/cc (λ (k) (k ("v")))))
|
||||
`(∅ / ("v")))
|
||||
(test-->> -->SL
|
||||
`(∅ / (call/cc (λ (k)
|
||||
((λ (x) ("x"))
|
||||
(k ("v"))))))
|
||||
`(∅ / ("v")))
|
||||
|
||||
;; call/cc + w-c-m
|
||||
(test-->> -->SL
|
||||
`(∅ / (w-c-m ("k") ("v1")
|
||||
((λ (f) (f ("unit")))
|
||||
(call/cc (λ (k)
|
||||
(w-c-m ("k") ("v2")
|
||||
(k (λ (x) (c-c-m [("k")])))))))))
|
||||
`(∅ / ("cons" ("cons" ("cons" ("k") ("v1")) ("nil")) ("nil"))))
|
||||
|
||||
(test-->> -->SL
|
||||
`(∅ / (w-c-m ("k") ("v1")
|
||||
((λ (f) (f ("unit")))
|
||||
(call/cc (λ (k)
|
||||
(w-c-m ("k") ("v2")
|
||||
((λ (cms)
|
||||
(k (λ (x) cms)))
|
||||
(c-c-m [("k")]))))))))
|
||||
`(∅ / ("cons" ("cons" ("cons" ("k") ("v1")) ("nil"))
|
||||
("cons" ("cons" ("cons" ("k") ("v2")) ("nil"))
|
||||
("cons" ("nil")
|
||||
("nil"))))))
|
||||
126
collects/redex/examples/cont-mark-transform/SL-semantics.rkt
Normal file
126
collects/redex/examples/cont-mark-transform/SL-semantics.rkt
Normal file
|
|
@ -0,0 +1,126 @@
|
|||
#lang racket
|
||||
|
||||
(require "SL-syntax.rkt"
|
||||
redex)
|
||||
(provide -->SL χ)
|
||||
|
||||
(define -->SL
|
||||
(reduction-relation
|
||||
SL #:domain (Σ / e)
|
||||
(--> (Σ / (in-hole E ((λ (x ..._1) e) v ..._1)))
|
||||
(Σ / (in-hole E (subst-n (x v) ... e)))
|
||||
"1")
|
||||
(--> (Σ / (in-hole E (match (K v ...) l ...)))
|
||||
(Σ / (in-hole E (subst-n (x v) ... e)))
|
||||
; The match must be unique, according to Fig. 5
|
||||
(where ([(K x ...) e]) (matches (K v ...) l ...))
|
||||
"2")
|
||||
(--> (Σ / (in-hole E (letrec ([σ v] ...) e)))
|
||||
((store-set Σ [σ ↦ v] ...) / (in-hole E e))
|
||||
"3")
|
||||
(--> (Σ / (in-hole E (σ v ...)))
|
||||
(Σ / (in-hole E (subst-n (x v) ... e)))
|
||||
(where (λ (x ...) e) (store-lookup Σ σ))
|
||||
(side-condition (= (length (term (v ...))) (length (term (x ...)))))
|
||||
"4")
|
||||
(--> (Σ / (in-hole E_1 (σ v)))
|
||||
(Σ / (in-hole E_2 v))
|
||||
(where (κ E_2) (store-lookup Σ σ))
|
||||
"4’")
|
||||
(--> (Σ / (in-hole E (match σ l ...)))
|
||||
(Σ / (in-hole E (match (store-lookup Σ σ) l ...)))
|
||||
"5")
|
||||
(--> (Σ / (in-hole E (w-c-m v_k v_1
|
||||
(in-hole C (w-c-m v_k v_2 e)))))
|
||||
(Σ / (in-hole E (w-c-m v_k v_2 (in-hole C e))))
|
||||
(side-condition (term (no-dup-keys C (v_k))))
|
||||
"6")
|
||||
(--> (Σ / (in-hole E (w-c-m v_k v_1 v_2)))
|
||||
(Σ / (in-hole E v_2))
|
||||
"7")
|
||||
(--> (Σ / (in-hole E (c-c-m [v ...])))
|
||||
(Σ / (in-hole E (χ (v ...) E ("nil"))))
|
||||
"8")
|
||||
(--> (Σ / (in-hole E (abort e)))
|
||||
(Σ / e)
|
||||
"9")
|
||||
(--> (Σ / (in-hole E (call/cc v)))
|
||||
(Σ / (in-hole E (v (κ E))))
|
||||
"*")
|
||||
(--> (Σ / (in-hole E_1 ((κ E_2) v)))
|
||||
(Σ / (in-hole E_2 v))
|
||||
"#")))
|
||||
|
||||
(define-metafunction SL
|
||||
[(matches (K v ...)) ()]
|
||||
[(matches
|
||||
(K v ..._1)
|
||||
[(K x ..._1) e]
|
||||
l ...)
|
||||
([(K x ...) e] l_i ...)
|
||||
(where (l_i ...) (matches (K v ...) l ...))]
|
||||
[(matches
|
||||
(K v ..._1)
|
||||
l_0 l_1 ...)
|
||||
(l_i ...)
|
||||
(where (l_i ...) (matches (K v ...) l_1 ...))])
|
||||
|
||||
(define-metafunction SL
|
||||
[(store-set Σ) Σ]
|
||||
[(store-set Σ [σ_0 ↦ v_0] [σ_1 ↦ v_1] ...)
|
||||
(store-set (Σ [σ_0 ↦ v_0]) [σ_1 ↦ v_1] ...)])
|
||||
|
||||
(define-metafunction SL
|
||||
[(store-lookup (Σ [σ ↦ v]) σ) v]
|
||||
[(store-lookup (Σ [σ_1 ↦ v]) σ_2)
|
||||
(store-lookup Σ σ_2)])
|
||||
|
||||
(define-metafunction SL
|
||||
[(χ (v_0 ...) E)
|
||||
(χ (v_0 ...) E ("nil"))]
|
||||
[(χ (v_0 ...) hole v_l) ("cons" v_l ("nil"))]
|
||||
[(χ (v_0 ...) (v_i ... E) v_l)
|
||||
("cons" v_l (χ (v_0 ...) E ("nil")))]
|
||||
[(χ (v_0 ... v_k v_k+1 ...) (w-c-m v_k v_v E) v_l)
|
||||
(χ (v_0 ... v_k v_k+1 ...) E ("cons" ("cons" v_k v_v) v_l))]
|
||||
[(χ (v_0 ...) (w-c-m v_k v_v E) v_l)
|
||||
(χ (v_0 ...) E v_l)])
|
||||
|
||||
(define-metafunction SL
|
||||
[(subst-n (x_1 any_1) (x_2 any_2) ... any_3)
|
||||
(subst x_1 any_1 (subst-n (x_2 any_2) ... any_3))]
|
||||
[(subst-n any_3) any_3])
|
||||
|
||||
(define-metafunction SL
|
||||
;; x_1 bound, so don't continue in body
|
||||
[(subst x_1 any_1 (λ (x_2 ... x_1 x_3 ...) any_2))
|
||||
(λ (x_2 ... x_1 x_3 ...) any_2)]
|
||||
;; general purpose capture avoiding case
|
||||
[(subst x_1 any_1 (λ (x_2 ...) any_2))
|
||||
(λ (x_new ...) (subst x_1 any_1 (subst-vars (x_2 x_new) ... any_2)))
|
||||
(where (x_new ...) ,(variables-not-in (term (x_1 any_1 any_2)) (term (x_2 ...))))]
|
||||
;; replace x_1 with e_1
|
||||
[(subst x_1 any_1 x_1) any_1]
|
||||
;; x_1 and x_2 are different, so don't replace
|
||||
[(subst x_1 any_1 x_2) x_2]
|
||||
;; match
|
||||
[(subst x_1 any_1 (match a [(K_0 x_0 ...) e_0] ...))
|
||||
(match (subst x_1 any_1 a)
|
||||
[(K_0 x_0’ ...) e_0’]
|
||||
...)
|
||||
(where
|
||||
((λ (x_0’ ...) e_0’) ...)
|
||||
((subst x_1 any_1 (λ (x_0 ...) e_0)) ...))]
|
||||
;; ref
|
||||
[(subst x any σ) σ]
|
||||
;; the last cases cover all other expressions
|
||||
[(subst x_1 any_1 (any_2 ...)) ((subst x_1 any_1 any_2) ...)]
|
||||
[(subst x_1 any_1 any_2) any_2])
|
||||
|
||||
(define-metafunction SL
|
||||
[(subst-vars (x_1 any_1) x_1) any_1]
|
||||
[(subst-vars (x_1 any_1) (any_2 ...)) ((subst-vars (x_1 any_1) any_2) ...)]
|
||||
[(subst-vars (x_1 any_1) any_2) any_2]
|
||||
[(subst-vars (x_1 any_1) (x_2 any_2) ... any_3)
|
||||
(subst-vars (x_1 any_1) (subst-vars (x_2 any_2) ... any_3))]
|
||||
[(subst-vars any) any])
|
||||
44
collects/redex/examples/cont-mark-transform/SL-syntax.rkt
Normal file
44
collects/redex/examples/cont-mark-transform/SL-syntax.rkt
Normal file
|
|
@ -0,0 +1,44 @@
|
|||
#lang racket
|
||||
|
||||
(require "TL-syntax.rkt"
|
||||
redex)
|
||||
(provide SL no-dup-keys)
|
||||
|
||||
(define-extended-language SL TL
|
||||
(e ....
|
||||
(call/cc w))
|
||||
(v ....
|
||||
(κ (hide-hole E)))
|
||||
|
||||
(D (w-c-m v v D)
|
||||
hole
|
||||
(v ... D))
|
||||
(E (side-condition D_1 (term (no-dup-keys D_1 ()))))
|
||||
|
||||
; used in the marks collapsing rule (6)
|
||||
(C (w-c-m v v C)
|
||||
hole)
|
||||
|
||||
; used in translation
|
||||
(r (a ...)
|
||||
(letrec ([σ w] ...) e)
|
||||
(w-c-m a a a)
|
||||
(c-c-m [a ...])
|
||||
(match a l ...)
|
||||
(abort e)
|
||||
(call/cc e))
|
||||
(T (w-c-m a a T)
|
||||
hole
|
||||
(a ... T))
|
||||
(k v
|
||||
#f))
|
||||
|
||||
(define-metafunction SL
|
||||
[(no-dup-keys hole (v ...))
|
||||
#t]
|
||||
[(no-dup-keys (w-c-m v_i v D) (v_0 ... v_i v_i+1 ...))
|
||||
#f]
|
||||
[(no-dup-keys (w-c-m v_i v D) (v_0 ...))
|
||||
(no-dup-keys D (v_i v_0 ...))]
|
||||
[(no-dup-keys (v ... D) (v_0 ...))
|
||||
(no-dup-keys D ())])
|
||||
|
|
@ -0,0 +1,21 @@
|
|||
#lang racket
|
||||
|
||||
(require "TL-semantics.rkt"
|
||||
"common.rkt"
|
||||
redex)
|
||||
|
||||
(test-TL-result
|
||||
∅
|
||||
((λ (x) x) (λ (x) x))
|
||||
(λ (x) x))
|
||||
|
||||
(test-TL-stuck
|
||||
∅
|
||||
(call/cc (λ (x) x)))
|
||||
|
||||
(test-predicate
|
||||
(curry regexp-match? #rx"not defined")
|
||||
(with-handlers ([exn:fail? exn-message])
|
||||
(apply-reduction-relation
|
||||
-->TL
|
||||
(term (∅ / ((κ hole) (λ (x) x)))))))
|
||||
19
collects/redex/examples/cont-mark-transform/TL-semantics.rkt
Normal file
19
collects/redex/examples/cont-mark-transform/TL-semantics.rkt
Normal file
|
|
@ -0,0 +1,19 @@
|
|||
#lang racket
|
||||
|
||||
(require "TL-syntax.rkt"
|
||||
"SL-syntax.rkt"
|
||||
"SL-semantics.rkt"
|
||||
redex)
|
||||
|
||||
(provide -->TL)
|
||||
|
||||
(define -->TL
|
||||
(extend-reduction-relation
|
||||
-->SL SL #:domain (Σ / (side-condition e_1 (TL-expr? (term e_1))))
|
||||
(--> any any
|
||||
(side-condition #f)
|
||||
"*")
|
||||
(--> any any
|
||||
(side-condition #f)
|
||||
"#")))
|
||||
(define TL-expr? (redex-match TL e))
|
||||
30
collects/redex/examples/cont-mark-transform/TL-syntax.rkt
Normal file
30
collects/redex/examples/cont-mark-transform/TL-syntax.rkt
Normal file
|
|
@ -0,0 +1,30 @@
|
|||
#lang racket
|
||||
|
||||
(require redex)
|
||||
(provide TL)
|
||||
|
||||
(define-language TL
|
||||
(e a
|
||||
(a ... e)
|
||||
(letrec ([σ v] ...) e)
|
||||
(w-c-m a a e)
|
||||
(c-c-m [a ...])
|
||||
(match a l ...)
|
||||
(abort e))
|
||||
|
||||
(l [(K x ...) e])
|
||||
(a w
|
||||
(K a ...))
|
||||
(w v
|
||||
x)
|
||||
(v (λ (x ...) e)
|
||||
(K v ...)
|
||||
σ)
|
||||
|
||||
(x variable-not-otherwise-mentioned)
|
||||
(σ (ref variable))
|
||||
|
||||
(Σ ∅
|
||||
(Σ [σ ↦ v]))
|
||||
|
||||
(K string))
|
||||
5
collects/redex/examples/cont-mark-transform/all-test.rkt
Normal file
5
collects/redex/examples/cont-mark-transform/all-test.rkt
Normal file
|
|
@ -0,0 +1,5 @@
|
|||
#lang racket
|
||||
|
||||
(require "TL-semantics-test.rkt"
|
||||
"SL-semantics-test.rkt"
|
||||
"CMT-test.rkt")
|
||||
78
collects/redex/examples/cont-mark-transform/common.rkt
Normal file
78
collects/redex/examples/cont-mark-transform/common.rkt
Normal file
|
|
@ -0,0 +1,78 @@
|
|||
#lang racket
|
||||
|
||||
(require "SL-syntax.rkt" "SL-semantics.rkt"
|
||||
"TL-syntax.rkt" "TL-semantics.rkt"
|
||||
redex)
|
||||
|
||||
(define ((make-eval --> value?) program)
|
||||
(match (unique-normal-form program -->)
|
||||
[(and state `(,_ / ,expr))
|
||||
(if (value? expr)
|
||||
(term (answer ,expr))
|
||||
(raise (eval-undefined "stuck" (current-continuation-marks) program state)))]))
|
||||
(define-struct (eval-undefined exn:fail) (input stuck-state))
|
||||
(provide make-eval
|
||||
(struct-out eval-undefined))
|
||||
|
||||
(define-metafunction SL
|
||||
[(answer (λ (x ...) e))
|
||||
procedure]
|
||||
[(answer (K v ...))
|
||||
(K (answer v) ...)]
|
||||
[(answer σ)
|
||||
reference]
|
||||
[(answer (κ E))
|
||||
procedure])
|
||||
|
||||
(define (unique-normal-form t R)
|
||||
(match (let ([nfs '()]
|
||||
[seen (set)])
|
||||
(let recur ([u t] [s (max-normalization-steps)])
|
||||
(when (negative? s)
|
||||
(raise (normalization-timeout "too many steps" (current-continuation-marks))))
|
||||
(unless (set-member? seen u)
|
||||
(set! seen (set-add seen u))
|
||||
(match (apply-reduction-relation R u)
|
||||
[(list) (set! nfs (cons u nfs))]
|
||||
[vs (for ([v vs]) (recur v (sub1 s)))])))
|
||||
nfs)
|
||||
[(list u) u]
|
||||
[(list) (raise (normalization-timeout "no normal forms" (current-continuation-marks)))]
|
||||
[_ (error 'unique-normal-form "distinct normal forms")]))
|
||||
(define max-normalization-steps (make-parameter +inf.0))
|
||||
(define-struct (normalization-timeout exn:fail) ())
|
||||
(provide max-normalization-steps
|
||||
(struct-out normalization-timeout))
|
||||
|
||||
(define-syntax (test-result stx)
|
||||
(syntax-case stx ()
|
||||
[(_ R Σ e v)
|
||||
#`(match (unique-normal-form (term (Σ / e)) R)
|
||||
[`(,_ / ,u)
|
||||
#,(syntax/loc stx (test-equal u (term v)))])]))
|
||||
|
||||
(define-syntax (test-stuck stx)
|
||||
(syntax-case stx ()
|
||||
[(_ R v? Σ e)
|
||||
#`(match (unique-normal-form (term (Σ / e)) R)
|
||||
[`(,_ / ,r)
|
||||
#,(syntax/loc stx (test-predicate (negate v?) r))])]))
|
||||
|
||||
(define-syntax-rule (define-test-forms language relation test-result-id test-stuck-id)
|
||||
(begin
|
||||
(define value? (redex-match language v))
|
||||
(define-syntax-rule (test-result-id . args)
|
||||
(test-result relation . args))
|
||||
(define-syntax-rule (test-stuck-id . args)
|
||||
(test-stuck relation value? . args))
|
||||
(provide test-result-id test-stuck-id)))
|
||||
|
||||
(define-test-forms SL -->SL test-SL-result test-SL-stuck)
|
||||
(define-test-forms TL -->TL test-TL-result test-TL-stuck)
|
||||
|
||||
(define-metafunction SL
|
||||
[(make-store) ∅]
|
||||
[(make-store [any_1 any_2] any_3 ...)
|
||||
((make-store any_3 ...)
|
||||
[(ref any_1) ↦ any_2])])
|
||||
(provide make-store)
|
||||
232
collects/redex/examples/cont-mark-transform/randomized-tests.rkt
Normal file
232
collects/redex/examples/cont-mark-transform/randomized-tests.rkt
Normal file
|
|
@ -0,0 +1,232 @@
|
|||
#lang racket
|
||||
|
||||
(require "SL-syntax.rkt" "SL-semantics.rkt"
|
||||
"TL-syntax.rkt" "TL-semantics.rkt"
|
||||
"CMT.rkt"
|
||||
"common.rkt"
|
||||
redex)
|
||||
(provide main same-result?)
|
||||
|
||||
(define (main . args)
|
||||
(define seed (add1 (random (sub1 (expt 2 31)))))
|
||||
(define unique-decomp-tests #f)
|
||||
(define CMT-range-all-tests #f)
|
||||
(define CMT-range-rules-tests #f)
|
||||
(define same-result-all-tests #f)
|
||||
(define same-result-rules-tests #f)
|
||||
|
||||
(command-line
|
||||
#:argv args
|
||||
#:once-each
|
||||
["--seed"
|
||||
n
|
||||
"Seed PRG with n"
|
||||
(set! seed (string->number n))]
|
||||
["--unique-decomposition"
|
||||
n
|
||||
"Test unique decomposition of n expressions"
|
||||
(set! unique-decomp-tests (string->number n))]
|
||||
["--CMT-range"
|
||||
n
|
||||
("Test that CMT produces a TL expression for n expressions,"
|
||||
"chosen from SL's e non-terminal")
|
||||
(set! CMT-range-all-tests (string->number n))]
|
||||
["--CMT-range-rules"
|
||||
n
|
||||
("Test that CMT produces a TL expression for n expressions,"
|
||||
"chosen from the left-hand sides of -->SL")
|
||||
(set! CMT-range-rules-tests (string->number n))]
|
||||
["--same-result"
|
||||
n
|
||||
("Test that translation preserves meaning for n expression,"
|
||||
"chosen from SL's e non-terminal")
|
||||
(set! same-result-all-tests (string->number n))]
|
||||
["--same-result-rules"
|
||||
n
|
||||
("Test that translation preserves meaning for n expression,"
|
||||
"chosen from SL's e non-terminal")
|
||||
(set! same-result-rules-tests (string->number n))])
|
||||
|
||||
(printf "Random seed: ~s\n" seed)
|
||||
|
||||
(when unique-decomp-tests
|
||||
(test-unique-decomposition unique-decomp-tests))
|
||||
(when CMT-range-all-tests
|
||||
(test-CMT-range CMT-range-all-tests))
|
||||
(when CMT-range-rules-tests
|
||||
(test-CMT-range/rules CMT-range-rules-tests))
|
||||
(when same-result-all-tests
|
||||
(test-same-result same-result-all-tests))
|
||||
(when same-result-rules-tests
|
||||
(test-same-result/rules same-result-rules-tests)))
|
||||
|
||||
;; Unique decomposition
|
||||
(define (test-unique-decomposition attempts)
|
||||
(redex-check SL e (uniquely-decomposes? (term e)) #:attempts attempts))
|
||||
|
||||
(define uniquely-decomposes?
|
||||
(let ([a? (redex-match SL a)]
|
||||
[decompositions (redex-match SL (in-hole T r))])
|
||||
(λ (e)
|
||||
(or (a? e)
|
||||
(match (decompositions e)
|
||||
[(list _) #t]
|
||||
[_ #f])))))
|
||||
|
||||
;; CMT produces TL expressions
|
||||
(define (test-CMT-range attempts)
|
||||
(test-translation CMT-produces-TL?
|
||||
#:attempts attempts))
|
||||
|
||||
(define (test-CMT-range/rules attempts)
|
||||
(test-translation CMT-produces-TL?
|
||||
#:attempts attempts
|
||||
#:source -->SL/no-side-conds))
|
||||
|
||||
(define CMT-produces-TL?
|
||||
(let ([TL-e? (redex-match TL e)])
|
||||
(λ (e)
|
||||
(TL-e? (term (CMT ,e))))))
|
||||
|
||||
;; Translated programs have the same result
|
||||
(define (test-same-result attempts)
|
||||
(test-translation same-result?
|
||||
#:attempts attempts))
|
||||
|
||||
(define (test-same-result/rules attempts)
|
||||
(test-translation same-result?
|
||||
#:attempts attempts
|
||||
#:source -->SL/no-side-conds))
|
||||
|
||||
(define (same-result? expr)
|
||||
(let/ec return
|
||||
(define SL-result
|
||||
(with-handlers ([normalization-timeout? return]
|
||||
[eval-undefined? return])
|
||||
(parameterize ([max-normalization-steps 1000])
|
||||
(SL-eval (term (∅ / ,expr))))))
|
||||
(define TL-result
|
||||
(TL-eval (term (∅ / (translate ,expr)))))
|
||||
(or (equal? SL-result TL-result)
|
||||
(compares-incomparable-keys? expr))))
|
||||
|
||||
(define SL-eval
|
||||
(make-eval -->SL (redex-match SL v)))
|
||||
(define TL-eval
|
||||
(make-eval -->TL (redex-match TL v)))
|
||||
|
||||
;; Utilities
|
||||
(define-syntax-rule (test-translation predicate . kw-args)
|
||||
(redex-check SL-gen (Σ / e)
|
||||
(predicate (term e))
|
||||
#:prepare close-program . kw-args))
|
||||
|
||||
(define-extended-language SL-gen SL
|
||||
(σ (ref (variable-except resume restore-marks c-w-i-c-m map-set kont/ms equal? last)))
|
||||
(K (side-condition string_1 (not (member (term string_1) '("square" "diamond")))))
|
||||
|
||||
(K-tree (K K-tree ...)))
|
||||
|
||||
(define -->SL/no-side-conds
|
||||
; Disables side-conditions on some rules.
|
||||
(extend-reduction-relation
|
||||
-->SL SL
|
||||
(--> (Σ / (in-hole E (match (K v ...) l ...))) any "2")
|
||||
(--> (Σ / (in-hole E (σ v ...))) any "4")
|
||||
(--> (Σ / (in-hole E_1 (σ v))) any "4’")))
|
||||
|
||||
(define close-program
|
||||
(match-lambda
|
||||
[`(,Σ / ,e)
|
||||
`(,Σ / ,(close-expr e))]))
|
||||
|
||||
(define close-expr
|
||||
(let ([var? (redex-match SL x)]
|
||||
[val? (redex-match SL v)])
|
||||
(λ (expr)
|
||||
; 1. Considers refs to be bound only within the binding letrec.
|
||||
; 2. Avoids adding duplicate mark to an existing frame, since
|
||||
; doing so (a) can make a continuation value syntactically invalid
|
||||
; and (b) can change the reduction rule that applies
|
||||
(let recur ([expr expr] [vars (set)] [refs (set)] [keys (set)])
|
||||
(match expr
|
||||
[(? var?)
|
||||
(if (set-empty? vars)
|
||||
(if (set-empty? refs)
|
||||
(random-constant)
|
||||
`(ref ,(random-element refs)))
|
||||
(if (set-member? vars expr)
|
||||
expr
|
||||
(random-element vars)))]
|
||||
[`(ref ,σ)
|
||||
(if (set-empty? refs)
|
||||
(random-constant)
|
||||
(if (set-member? refs σ)
|
||||
expr
|
||||
`(ref ,(random-element refs))))]
|
||||
[`(w-c-m ,k ,v ,e)
|
||||
(define k’
|
||||
(if (val? k)
|
||||
k
|
||||
(let retry ([candidate (recur k vars refs keys)]
|
||||
[retries 0])
|
||||
(when (> retries 3)
|
||||
(error 'close "too many"))
|
||||
(if (set-member? keys candidate)
|
||||
(retry (list (first (random-constant)) candidate)
|
||||
(add1 retries))
|
||||
candidate))))
|
||||
(define ext-keys
|
||||
(if (val? k’)
|
||||
(set-add keys k’)
|
||||
keys))
|
||||
`(w-c-m ,k’ ,(recur v vars refs (set))
|
||||
,(recur e vars refs ext-keys))]
|
||||
[`(letrec ([(ref ,σs) ,es] ...) ,e)
|
||||
(define ext-refs (extend refs σs))
|
||||
`(letrec ,(for/list ([e es] [σ σs])
|
||||
`[(ref ,σ) ,(recur e vars ext-refs (set))])
|
||||
,(recur e vars ext-refs (set)))]
|
||||
[`(match ,e [(,ks ,xss ...) ,es] ...)
|
||||
(define ext-vars (extend vars (apply append xss)))
|
||||
`(match ,(recur e vars refs (set))
|
||||
,@(for/list ([xs xss] [e es] [k ks])
|
||||
`[(,k ,@xs) ,(recur e ext-vars refs (set))]))]
|
||||
[`(λ ,xs ,e)
|
||||
(define ext-vars (extend vars xs))
|
||||
`(λ ,xs ,(recur e ext-vars refs (set)))]
|
||||
[(? list?)
|
||||
(map (λ (e) (recur e vars refs (set))) expr)]
|
||||
[_ expr])))))
|
||||
|
||||
(define (extend s xs)
|
||||
(for/fold ([s s]) ([x xs])
|
||||
(set-add s x)))
|
||||
|
||||
(define random-constant
|
||||
(let ([generate-K-tree (generate-term SL-gen K-tree)])
|
||||
(λ () (generate-K-tree (random 3)))))
|
||||
|
||||
(define (random-element xs)
|
||||
(list-ref (set-map xs values) (random (set-count xs))))
|
||||
|
||||
(define (compares-incomparable-keys? expr)
|
||||
(define procedure? (redex-match SL (λ (x ...) e)))
|
||||
(define continuation? (redex-match SL (κ E)))
|
||||
(let/ec return
|
||||
(apply-reduction-relation*
|
||||
(extend-reduction-relation
|
||||
-->SL SL
|
||||
(--> (Σ / (in-hole E (c-c-m [v ...])))
|
||||
,(if (andmap comparable? (term (v ...)))
|
||||
(term (Σ / (in-hole E (χ (v ...) E ("nil")))))
|
||||
(return #t))
|
||||
"8"))
|
||||
`(∅ / ,expr))
|
||||
#f))
|
||||
|
||||
(define comparable?
|
||||
(let ()
|
||||
(define-extended-language SL’ SL
|
||||
(c σ (K c ...)))
|
||||
(redex-match SL’ c)))
|
||||
84
collects/redex/examples/cont-mark-transform/test-util.rkt
Normal file
84
collects/redex/examples/cont-mark-transform/test-util.rkt
Normal file
|
|
@ -0,0 +1,84 @@
|
|||
#lang racket
|
||||
|
||||
(require "common.rkt" redex)
|
||||
(provide (all-defined-out))
|
||||
|
||||
(define (num n)
|
||||
(if (zero? n)
|
||||
`("0")
|
||||
`("S" ,(num (sub1 n)))))
|
||||
|
||||
(define (lst l)
|
||||
(if (empty? l)
|
||||
`("nil")
|
||||
`("cons" ,(first l) ,(lst (rest l)))))
|
||||
|
||||
(define (:let name named-expr body)
|
||||
`((λ (,name) ,body)
|
||||
,named-expr))
|
||||
|
||||
(define =-impl
|
||||
`(λ (x y)
|
||||
(match x
|
||||
[("0")
|
||||
(match y
|
||||
[("0") ("#t")]
|
||||
[("S" yn) ("#f")])]
|
||||
[("S" xn)
|
||||
(match y
|
||||
[("0") ("#f")]
|
||||
[("S" yn) ((ref =) xn yn)])])))
|
||||
|
||||
(define +-impl
|
||||
`(λ (x y)
|
||||
(match x
|
||||
[("0") y]
|
||||
[("S" xn)
|
||||
,(:let 'in '((ref +) xn y)
|
||||
'("S" in))])))
|
||||
|
||||
(define --impl
|
||||
`(λ (n m)
|
||||
(match n
|
||||
[("0") n]
|
||||
[("S" k)
|
||||
(match m
|
||||
[("0") n]
|
||||
[("S" l) ((ref -) k l)])])))
|
||||
|
||||
(define *-impl
|
||||
`(λ (n m)
|
||||
(match n
|
||||
[("0") ("0")]
|
||||
[("S" p) ,(:let 'tmp '((ref *) p m)
|
||||
'((ref +) m tmp))])))
|
||||
|
||||
(define if-impl
|
||||
`(λ (cond true false)
|
||||
(match cond
|
||||
[("#t") (true)]
|
||||
[("#f") (false)])))
|
||||
|
||||
(define (with-arith e)
|
||||
`(letrec
|
||||
([(ref =) ,=-impl]
|
||||
[(ref +) ,+-impl]
|
||||
[(ref -) ,--impl]
|
||||
[(ref *) ,*-impl]
|
||||
[(ref if) ,if-impl])
|
||||
,e))
|
||||
|
||||
(define arith-store
|
||||
(term
|
||||
(make-store [= ,=-impl]
|
||||
[+ ,+-impl]
|
||||
[- ,--impl]
|
||||
[* ,*-impl]
|
||||
[if ,if-impl])))
|
||||
|
||||
(define (:if cond true false)
|
||||
(:let 'cond-val cond
|
||||
`((ref if)
|
||||
cond-val
|
||||
(λ () ,true)
|
||||
(λ () ,false))))
|
||||
|
|
@ -32,6 +32,7 @@
|
|||
"../examples/racket-machine/reduction-test.ss"
|
||||
"../examples/racket-machine/verification-test.ss"
|
||||
"../examples/delim-cont/test.rkt"
|
||||
"../examples/cont-mark-transform/all-test.rkt"
|
||||
("../examples/r6rs/r6rs-tests.ss" main))
|
||||
'())))
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user