added specification for the main arrow to redex
svn: r13924
This commit is contained in:
parent
e1dab52b07
commit
9297ffa2a3
|
@ -220,7 +220,8 @@
|
||||||
(syntax->list (syntax (shortcuts ...)))
|
(syntax->list (syntax (shortcuts ...)))
|
||||||
#'(list lws ...)
|
#'(list lws ...)
|
||||||
(syntax-e #'allow-zero-rules?)
|
(syntax-e #'allow-zero-rules?)
|
||||||
domain-pattern))))]
|
domain-pattern
|
||||||
|
main-arrow))))]
|
||||||
[(_ id orig-reduction-relation lang args ...)
|
[(_ id orig-reduction-relation lang args ...)
|
||||||
(raise-syntax-error (syntax-e #'id)
|
(raise-syntax-error (syntax-e #'id)
|
||||||
"expected an identifier for the language name"
|
"expected an identifier for the language name"
|
||||||
|
@ -233,7 +234,7 @@
|
||||||
|
|
||||||
;; ensure no duplicate keywords
|
;; ensure no duplicate keywords
|
||||||
(let ([ht (make-hash)]
|
(let ([ht (make-hash)]
|
||||||
[known-keywords '(#;#:arrow #:domain)]) ;; #:arrow not yet implemented
|
[known-keywords '(#:arrow #:domain)]) ;; #:arrow not yet implemented
|
||||||
(for-each (λ (kwd/stx) ;; (not necc a keyword)
|
(for-each (λ (kwd/stx) ;; (not necc a keyword)
|
||||||
(let ([kwd (syntax-e kwd/stx)])
|
(let ([kwd (syntax-e kwd/stx)])
|
||||||
(when (keyword? kwd)
|
(when (keyword? kwd)
|
||||||
|
@ -261,8 +262,14 @@
|
||||||
"expected a domain after #:domain"
|
"expected a domain after #:domain"
|
||||||
stx)]
|
stx)]
|
||||||
[(#:arrow arrow . args)
|
[(#:arrow arrow . args)
|
||||||
|
(identifier? #'arrow)
|
||||||
(begin (set! default-arrow #'arrow)
|
(begin (set! default-arrow #'arrow)
|
||||||
(loop #'args))]
|
(loop #'args))]
|
||||||
|
[(#:arrow arrow . args)
|
||||||
|
(raise-syntax-error (syntax-e id)
|
||||||
|
"expected an arrow after #:arrow, not a compound expression"
|
||||||
|
stx
|
||||||
|
#'arrow)]
|
||||||
[(#:arrow)
|
[(#:arrow)
|
||||||
(raise-syntax-error (syntax-e id)
|
(raise-syntax-error (syntax-e id)
|
||||||
"expected an arrow after #:arrow"
|
"expected an arrow after #:arrow"
|
||||||
|
@ -383,7 +390,8 @@
|
||||||
(define (reduction-relation/helper stx orig-name orig-red-expr lang-id rules shortcuts
|
(define (reduction-relation/helper stx orig-name orig-red-expr lang-id rules shortcuts
|
||||||
lws
|
lws
|
||||||
allow-zero-rules?
|
allow-zero-rules?
|
||||||
domain-pattern)
|
domain-pattern
|
||||||
|
main-arrow)
|
||||||
(let ([ht (make-module-identifier-mapping)]
|
(let ([ht (make-module-identifier-mapping)]
|
||||||
[all-top-levels '()]
|
[all-top-levels '()]
|
||||||
[withs (make-module-identifier-mapping)])
|
[withs (make-module-identifier-mapping)])
|
||||||
|
@ -421,14 +429,17 @@
|
||||||
(set! all-top-levels (cons #'arrow all-top-levels))
|
(set! all-top-levels (cons #'arrow all-top-levels))
|
||||||
(table-cons! ht (syntax arrow) rule))]))
|
(table-cons! ht (syntax arrow) rule))]))
|
||||||
rules)
|
rules)
|
||||||
|
|
||||||
;; signal a syntax error if there are shortcuts defined, but no rules that use them
|
;; signal a syntax error if there are shortcuts defined, but no rules that use them
|
||||||
(unless (null? shortcuts)
|
(unless (null? shortcuts)
|
||||||
(unless (module-identifier-mapping-get ht (syntax -->) (λ () #f))
|
(unless (module-identifier-mapping-get ht main-arrow (λ () #f))
|
||||||
(raise-syntax-error orig-name "no --> rules" stx)))
|
(raise-syntax-error orig-name
|
||||||
|
(format "no ~a rules" (syntax-e main-arrow))
|
||||||
|
stx)))
|
||||||
|
|
||||||
(for-each (λ (tl)
|
(for-each (λ (tl)
|
||||||
(let loop ([id tl])
|
(let loop ([id tl])
|
||||||
(unless (free-identifier=? #'--> id)
|
(unless (free-identifier=? main-arrow id)
|
||||||
(let ([nexts
|
(let ([nexts
|
||||||
(module-identifier-mapping-get
|
(module-identifier-mapping-get
|
||||||
withs id
|
withs id
|
||||||
|
@ -445,7 +456,7 @@
|
||||||
(let ([name-ht (make-hasheq)]
|
(let ([name-ht (make-hasheq)]
|
||||||
[lang-nts (language-id-nts lang-id orig-name)])
|
[lang-nts (language-id-nts lang-id orig-name)])
|
||||||
(with-syntax ([lang-id lang-id]
|
(with-syntax ([lang-id lang-id]
|
||||||
[(top-level ...) (get-choices stx orig-name ht lang-id (syntax -->)
|
[(top-level ...) (get-choices stx orig-name ht lang-id main-arrow
|
||||||
name-ht lang-id allow-zero-rules?)]
|
name-ht lang-id allow-zero-rules?)]
|
||||||
[(rule-names ...) (hash-map name-ht (λ (k v) k))]
|
[(rule-names ...) (hash-map name-ht (λ (k v) k))]
|
||||||
[lws lws]
|
[lws lws]
|
||||||
|
|
|
@ -843,6 +843,15 @@
|
||||||
(test (apply-reduction-relation r1 (term (1 2)))
|
(test (apply-reduction-relation r1 (term (1 2)))
|
||||||
(list (term (2 1)))))
|
(list (term (2 1)))))
|
||||||
|
|
||||||
|
;;test that #:arrow keyword works
|
||||||
|
(test (apply-reduction-relation
|
||||||
|
(reduction-relation
|
||||||
|
empty-language
|
||||||
|
#:arrow :->
|
||||||
|
(:-> 1 2))
|
||||||
|
1)
|
||||||
|
'(2))
|
||||||
|
|
||||||
(parameterize ([current-namespace syn-err-test-namespace])
|
(parameterize ([current-namespace syn-err-test-namespace])
|
||||||
(eval (quote-syntax
|
(eval (quote-syntax
|
||||||
(define-language grammar
|
(define-language grammar
|
||||||
|
|
|
@ -638,8 +638,9 @@ all non-GUI portions of Redex) and also exported by
|
||||||
@schememodname[redex] (which includes all of Redex).
|
@schememodname[redex] (which includes all of Redex).
|
||||||
|
|
||||||
@defform/subs[#:literals (--> fresh side-condition where)
|
@defform/subs[#:literals (--> fresh side-condition where)
|
||||||
(reduction-relation language domain reduction-case ...)
|
(reduction-relation language domain main-arrow reduction-case ...)
|
||||||
([domain (code:line) (code:line #:domain #, @|ttpattern|)]
|
([domain (code:line) (code:line #:domain #, @|ttpattern|)]
|
||||||
|
[main-arrow (code:line) (code:line #:arrow arrow)]
|
||||||
[reduction-case (--> #, @|ttpattern| #, @|tttterm| extras ...)]
|
[reduction-case (--> #, @|ttpattern| #, @|tttterm| extras ...)]
|
||||||
[extras name
|
[extras name
|
||||||
(fresh fresh-clause ...)
|
(fresh fresh-clause ...)
|
||||||
|
@ -650,7 +651,8 @@ all non-GUI portions of Redex) and also exported by
|
||||||
[tl-pat-ele tl-pat (code:line tl-pat ... (code:comment "a literal ellipsis"))])]{
|
[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
|
Defines a reduction relation casewise, one case for each of the
|
||||||
clauses beginning with @scheme[-->]. Each of the @scheme[pattern]s
|
clauses beginning with @scheme[-->] (or with @scheme[arrow], if
|
||||||
|
specified). Each of the @scheme[pattern]s
|
||||||
refers to the @scheme[language], and binds variables in the
|
refers to the @scheme[language], and binds variables in the
|
||||||
@|tttterm|.
|
@|tttterm|.
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue
Block a user