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

added optionaldomain specifications to reduction-relations

Browse Source 
svn: r13913
This commit is contained in:
Robby Findler 2009-03-03 16:27:09 +00:00
parent 164171be11
commit 8704fe05b2
5 changed files with 220 additions and 52 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
collects/redex/private/matcher.ss
View File

@ -612,7 +612,7 @@ before the pattern compiler is invoked.
(mtch-context match)
(mtch-hole match)))))
;; compile-pattern : compiled-lang pattern boolean (listof sym) -> compiled-pattern
;; compile-pattern : compiled-lang pattern boolean -> compiled-pattern
(define (compile-pattern clang pattern bind-names?)
(let-values ([(pattern has-hole?) (compile-pattern/cross? clang pattern #t bind-names?)])
(make-compiled-pattern pattern)))

103
collects/redex/private/reduction-semantics.ss
View File

@ -126,21 +126,25 @@
lang
(map
(λ (make-proc)
(λ (lang)
(let ([f (make-proc lang)])
(λ (main-exp exp extend acc)
(let loop ([ms (or (match-pattern cp exp) '())]
[acc acc])
(cond
[(null? ms) acc]
[else
(let* ([mtch (car ms)]
[bindings (mtch-bindings mtch)])
(loop (cdr ms)
(f main-exp
(lookup-binding bindings 'exp)
(λ (x) (extend (plug (lookup-binding bindings 'ctxt) x)))
acc)))]))))))
(make-rewrite-proc
(λ (lang)
(let ([f (make-proc lang)])
(λ (main-exp exp extend acc)
(let loop ([ms (or (match-pattern cp exp) '())]
[acc acc])
(cond
[(null? ms) acc]
[else
(let* ([mtch (car ms)]
[bindings (mtch-bindings mtch)])
(loop (cdr ms)
(f main-exp
(lookup-binding bindings 'exp)
(λ (x) (extend (plug (lookup-binding bindings 'ctxt) x)))
acc)))])))))
(rewrite-proc-name make-proc)
(rewrite-proc-lhs make-proc)
(rewrite-proc-id make-proc)))
(reduction-relation-make-procs red))
(reduction-relation-rule-names red)
(reduction-relation-lws red)
@ -200,16 +204,10 @@
(define-syntax-set (do-reduction-relation)
(define (do-reduction-relation/proc stx)
(syntax-case stx ()
[(_ id orig-reduction-relation allow-zero-rules? lang w/domain-args ...)
[(_ id orig-reduction-relation allow-zero-rules? lang . w/domain-args)
(identifier? #'lang)
(let-values ([(args domain-pattern)
(syntax-case #'(w/domain-args ...) ()
;; commented out this case to diable domain specifications
#;
[(#:domain pat args ...)
(values (syntax (args ...)) #'pat)]
[else
(values (syntax (w/domain-args ...)) #'any)])])
(let-values ([(domain-pattern main-arrow args)
(parse-keywords stx #'id #'w/domain-args)])
(with-syntax ([(rules ...) (before-with args)]
[(shortcuts ...) (after-with args)])
(with-syntax ([(lws ...) (map rule->lws (syntax->list #'(rules ...)))])
@ -229,6 +227,51 @@
stx
#'lang)]))
(define (parse-keywords stx id args)
(let ([domain-contract #'any]
[default-arrow #'-->])
;; ensure no duplicate keywords
(let ([ht (make-hash)]
[known-keywords '(#;#:arrow #:domain)]) ;; #:arrow not yet implemented
(for-each (λ (kwd/stx) ;; (not necc a keyword)
(let ([kwd (syntax-e kwd/stx)])
(when (keyword? kwd)
(unless (member kwd known-keywords)
(raise-syntax-error (syntax-e id)
"unknown keyword"
stx
kwd/stx))
(when (hash-ref ht kwd #f)
(raise-syntax-error (syntax-e id)
"duplicate keywords"
stx
kwd/stx
(list (hash-ref ht kwd))))
(hash-set! ht kwd kwd/stx))))
(syntax->list args)))
(let loop ([args args])
(syntax-case args ()
[(#:domain pat args ...)
(begin (set! domain-contract #'pat)
(loop #'(args ...)))]
[(#:domain)
(raise-syntax-error (syntax-e id)
"expected a domain after #:domain"
stx)]
[(#:arrow arrow . args)
(begin (set! default-arrow #'arrow)
(loop #'args))]
[(#:arrow)
(raise-syntax-error (syntax-e id)
"expected an arrow after #:arrow"
stx)]
[_
(begin
(values domain-contract default-arrow args))]))))
(define (before-with stx)
(let loop ([lst (syntax->list stx)])
(cond
@ -337,7 +380,10 @@
(to-lw where-expr))
...))))]))
(define (reduction-relation/helper stx orig-name orig-red-expr lang-id rules shortcuts lws allow-zero-rules? domain-pattern)
(define (reduction-relation/helper stx orig-name orig-red-expr lang-id rules shortcuts
lws
allow-zero-rules?
domain-pattern)
(let ([ht (make-module-identifier-mapping)]
[all-top-levels '()]
[withs (make-module-identifier-mapping)])
@ -399,7 +445,8 @@
(let ([name-ht (make-hasheq)]
[lang-nts (language-id-nts lang-id orig-name)])
(with-syntax ([lang-id lang-id]
[(top-level ...) (get-choices stx orig-name ht lang-id (syntax -->) name-ht lang-id allow-zero-rules?)]
[(top-level ...) (get-choices stx orig-name ht lang-id (syntax -->)
name-ht lang-id allow-zero-rules?)]
[(rule-names ...) (hash-map name-ht (λ (k v) k))]
[lws lws]
@ -407,7 +454,7 @@
(rewrite-side-conditions/check-errs
lang-nts
orig-name
#t
#f
domain-pattern)])
#`(build-reduction-relation
@ -789,8 +836,6 @@
(reduction-relation-make-procs relation))
(make-coverage h)))
;(define fresh-coverage (compose make-coverage make-hasheq))
(define (do-leaf-match name pat w/extras proc)
(let ([case-id (gensym)])
(make-rewrite-proc

63
collects/redex/private/struct.ss
View File

@ -1,5 +1,7 @@
#lang scheme/base
(require "matcher.ss")
;; don't provide reduction-relation directly, so that we can use that for the macro's name.
(provide reduction-relation-lang
reduction-relation-make-procs
@ -20,7 +22,9 @@
;; we want to avoid doing it multiple times, so it is cached in a reduction-relation struct
(define-values (make-rewrite-proc rewrite-proc? rewrite-proc-name rewrite-proc-lhs rewrite-proc-id)
(define-values (make-rewrite-proc
rewrite-proc?
rewrite-proc-name rewrite-proc-lhs rewrite-proc-id)
(let ()
(define-values (type constructor predicate accessor mutator)
(make-struct-type 'rewrite-proc #f 4 0 #f '() #f 0))
@ -45,19 +49,44 @@
;; the domain pattern isn't actually used here.
;; I started to add it, but didn't finish. -robby
(define (build-reduction-relation orig-reduction-relation lang make-procs rule-names lws domain-pattern)
(cond
[orig-reduction-relation
(let* ([new-names (map rewrite-proc-name make-procs)]
[all-make-procs
(append (filter (λ (x) (or (not (rewrite-proc-name x))
(not (member (rewrite-proc-name x) new-names))))
(reduction-relation-make-procs orig-reduction-relation))
make-procs)])
(make-reduction-relation lang
all-make-procs
(append (reduction-relation-rule-names orig-reduction-relation)
rule-names)
lws ;; only keep new lws for typesetting
(map (λ (make-proc) (make-proc lang)) all-make-procs)))]
[else
(make-reduction-relation lang make-procs rule-names lws (map (λ (make-proc) (make-proc lang)) make-procs))]))
(let* ([make-procs/check-domain
(map (λ (make-proc)
(make-rewrite-proc
(λ (lang)
(let ([compiled-domain-pat (compile-pattern lang domain-pattern #f)]
[proc (make-proc lang)])
(λ (tl-exp exp f acc)
(unless (match-pattern compiled-domain-pat tl-exp)
(error 'reduction-relation "relation not defined for ~s" tl-exp))
(let ([ress (proc tl-exp exp f acc)])
(for-each
(λ (res)
(let ([term (cadr res)])
(unless (match-pattern compiled-domain-pat term)
(error 'reduction-relation "relation reduced to ~s, which is outside its domain"
term))))
ress)
ress))))
(rewrite-proc-name make-proc)
(rewrite-proc-lhs make-proc)
(rewrite-proc-id make-proc)))
make-procs)])
(cond
[orig-reduction-relation
(let* ([new-names (map rewrite-proc-name make-procs)]
[all-make-procs
(append
(filter (λ (x) (or (not (rewrite-proc-name x))
(not (member (rewrite-proc-name x) new-names))))
(reduction-relation-make-procs orig-reduction-relation))
make-procs/check-domain)])
(make-reduction-relation lang
all-make-procs
(append (reduction-relation-rule-names orig-reduction-relation)
rule-names)
lws ;; only keep new lws for typesetting
(map (λ (make-proc) (make-proc lang)) all-make-procs)))]
[else
(make-reduction-relation lang make-procs/check-domain rule-names lws
(map (λ (make-proc) (make-proc lang))
make-procs/check-domain))])))

93
collects/redex/private/tl-test.ss
View File

@ -750,6 +750,99 @@
'(p q r))
(list '((p q r))))
#;
(test (apply-reduction-relation
(reduction-relation
empty-language
#:main-arrow :->
(:-> 1 2))
1)
'(2))
(test (apply-reduction-relation
(reduction-relation
empty-language
#:domain number
(--> 1 2))
1)
'(2))
(test (let ([red
(reduction-relation
empty-language
#:domain number
(--> 1 2))])
(with-handlers ((exn? exn-message))
(apply-reduction-relation red 'x)
'no-exception-raised))
"reduction-relation: relation not defined for x")
(test (let ([red
(reduction-relation
empty-language
#:domain number
(--> 1 x))])
(with-handlers ((exn? exn-message))
(apply-reduction-relation red 1)
'no-exception-raised))
"reduction-relation: relation reduced to x, which is outside its domain")
(let* ([red1
(reduction-relation
empty-language
#:domain (side-condition number_1 (even? (term number_1)))
(--> number number))]
[red2
(reduction-relation
empty-language
#:domain (side-condition number_1 (odd? (term number_1)))
(--> number number))]
[red-c
(union-reduction-relations red1 red2)])
;; ensure first branch of 'union' is checked
(test (with-handlers ((exn? exn-message))
(apply-reduction-relation red-c 1)
'no-exception-raised)
"reduction-relation: relation not defined for 1")
;; ensure second branch of 'union' is checked
(test (with-handlers ((exn? exn-message))
(apply-reduction-relation red-c 2)
'no-exception-raised)
"reduction-relation: relation not defined for 2"))
(let ()
(define-language l1
(D 0 1 2))
(define r1
(reduction-relation
l1
#:domain D
(--> D D)))
(define-language l2
(D 0 1 2 3))
(define r2
(extend-reduction-relation r1 l2))
;; test that the domain is re-interpreted for the extended reduction-relation
(test (apply-reduction-relation r2 3)
'(3)))
(let ()
(define-language l1
(D 0 1 2))
(define r1
(reduction-relation
l1
#:domain (D D)
(--> (D_1 D_2) (D_2 D_1))))
;; test that duplicated identifiers in the domain contract do not have to be equal
(test (apply-reduction-relation r1 (term (1 2)))
(list (term (2 1)))))
(parameterize ([current-namespace syn-err-test-namespace])
(eval (quote-syntax
(define-language grammar

11
collects/redex/redex.scrbl
View File

@ -638,15 +638,16 @@ all non-GUI portions of Redex) and also exported by
@schememodname[redex] (which includes all of Redex).
@defform/subs[#:literals (--> fresh side-condition where)
(reduction-relation language reduction-case ...)
([reduction-case (--> #, @|ttpattern| #, @|tttterm| extras ...)]
(reduction-relation language domain reduction-case ...)
([domain (code:line) (code:line #:domain #, @|ttpattern|)]
[reduction-case (--> #, @|ttpattern| #, @|tttterm| extras ...)]
[extras name
(fresh fresh-clause ...)
(side-condition scheme-expression ...)
(where tl-pat #, @|tttterm|)]
[fresh-clause var ((var1 ...) (var2 ...))]
[tl-pat identifier (tl-pat-ele ...)]
[tl-pat-ele tl-pat (code:line tl-pat ... (code:comment "a literal ellipsis"))])]{
[fresh-clause var ((var1 ...) (var2 ...))]
[tl-pat identifier (tl-pat-ele ...)]
[tl-pat-ele tl-pat (code:line tl-pat ... (code:comment "a literal ellipsis"))])]{
Defines a reduction relation casewise, one case for each of the
clauses beginning with @scheme[-->]. Each of the @scheme[pattern]s