Adds the feature requested in PR 10388
This commit is contained in:
Casey Klein
parent
5bbe748485
commit
fbd2c3c86f
|
|
@ -38,6 +38,7 @@
|
|||
with-atomic-rewriter
|
||||
STIX?
|
||||
white-bracket-sizing
|
||||
apply-rewrites
|
||||
|
||||
;; for test suite
|
||||
build-lines
|
||||
|
|
|
|||
|
|
@ -97,7 +97,9 @@
|
|||
(hash-set! ht (rule-pict-label rp) rp))
|
||||
(reduction-relation-lws rr))
|
||||
(map (lambda (label)
|
||||
(hash-ref ht label
|
||||
(hash-ref ht (if (string? label)
|
||||
(string->symbol label)
|
||||
label)
|
||||
(lambda ()
|
||||
(error what
|
||||
"no rule found for label: ~e"
|
||||
|
|
@ -124,6 +126,15 @@
|
|||
(tp (rule-pict-lhs rp))
|
||||
(tp (rule-pict-rhs rp))
|
||||
(rule-pict-label rp)
|
||||
(and (rule-pict-computed-label rp)
|
||||
(let ([rewritten (apply-rewrites (rule-pict-computed-label rp))])
|
||||
(and (not (and (rule-pict-label rp)
|
||||
(let has-unq? ([x rewritten])
|
||||
(and (lw? x)
|
||||
(or (lw-unq? x)
|
||||
(and (list? (lw-e x))
|
||||
(ormap has-unq? (lw-e x))))))))
|
||||
(tp rewritten))))
|
||||
(map (lambda (v)
|
||||
(if (pair? v)
|
||||
(cons (tp (car v)) (tp (cdr v)))
|
||||
|
|
@ -332,17 +343,22 @@
|
|||
max-w))
|
||||
|
||||
(define (rp->pict-label rp)
|
||||
(if (rule-pict-label rp)
|
||||
(let ([m (regexp-match #rx"^([^_]*)(?:_([^_]*)|)$"
|
||||
(format "~a" (rule-pict-label rp)))])
|
||||
(hbl-append
|
||||
((current-text) " [" (label-style) (label-font-size))
|
||||
((current-text) (cadr m) (label-style) (label-font-size))
|
||||
(if (caddr m)
|
||||
((current-text) (caddr m) `(subscript . ,(label-style)) (label-font-size))
|
||||
(blank))
|
||||
((current-text) "]" (label-style) (label-font-size))))
|
||||
(blank)))
|
||||
(define (bracket label)
|
||||
(hbl-append
|
||||
((current-text) " [" (label-style) (label-font-size))
|
||||
label
|
||||
((current-text) "]" (label-style) (label-font-size))))
|
||||
(cond [(rule-pict-computed-label rp) => bracket]
|
||||
[(rule-pict-label rp)
|
||||
(let ([m (regexp-match #rx"^([^_]*)(?:_([^_]*)|)$"
|
||||
(format "~a" (rule-pict-label rp)))])
|
||||
(bracket
|
||||
(hbl-append
|
||||
((current-text) (cadr m) (label-style) (label-font-size))
|
||||
(if (caddr m)
|
||||
((current-text) (caddr m) `(subscript . ,(label-style)) (label-font-size))
|
||||
(blank)))))]
|
||||
[else (blank)]))
|
||||
|
||||
(define (add-between i l)
|
||||
(cond
|
||||
|
|
|
|||
|
|
@ -175,7 +175,7 @@
|
|||
(define-syntax (fresh stx) (raise-syntax-error 'fresh "used outside of reduction-relation"))
|
||||
(define-syntax (with stx) (raise-syntax-error 'with "used outside of reduction-relation"))
|
||||
|
||||
(define (apply-reduction-relation/tag-with-names p v)
|
||||
(define (apply-reduction-relation/tagged p v)
|
||||
(let loop ([procs (reduction-relation-procs p)]
|
||||
[acc '()])
|
||||
(cond
|
||||
|
|
@ -184,7 +184,8 @@
|
|||
(loop (cdr procs)
|
||||
((car procs) v v values acc))])))
|
||||
|
||||
(define (apply-reduction-relation p v) (map cadr (apply-reduction-relation/tag-with-names p v)))
|
||||
(define (apply-reduction-relation/tag-with-names p v) (map cdr (apply-reduction-relation/tagged p v)))
|
||||
(define (apply-reduction-relation p v) (map caddr (apply-reduction-relation/tagged p v)))
|
||||
|
||||
(define-for-syntax (extract-pattern-binds lhs)
|
||||
(let loop ([lhs lhs])
|
||||
|
|
@ -420,20 +421,23 @@
|
|||
(define (rule->lws rule)
|
||||
(syntax-case rule ()
|
||||
[(arrow lhs rhs stuff ...)
|
||||
(let-values ([(label scs/withs fvars)
|
||||
(let-values ([(label computed-label scs/withs fvars)
|
||||
(let loop ([stuffs (syntax->list #'(stuff ...))]
|
||||
[label #f]
|
||||
[computed-label #f]
|
||||
[scs/withs null]
|
||||
[fvars null])
|
||||
(cond
|
||||
[(null? stuffs) (values label (reverse scs/withs) (reverse fvars))]
|
||||
[(null? stuffs) (values label computed-label (reverse scs/withs) (reverse fvars))]
|
||||
[else
|
||||
(syntax-case (car stuffs) (where where/hidden
|
||||
side-condition side-condition/hidden
|
||||
fresh variable-not-in)
|
||||
fresh variable-not-in
|
||||
computed-name)
|
||||
[(fresh xs ...)
|
||||
(loop (cdr stuffs)
|
||||
label
|
||||
computed-label
|
||||
scs/withs
|
||||
(append
|
||||
(reverse (map (λ (x)
|
||||
|
|
@ -460,28 +464,38 @@
|
|||
[(where x e)
|
||||
(loop (cdr stuffs)
|
||||
label
|
||||
computed-label
|
||||
(cons #`(cons #,(to-lw/proc #'x) #,(to-lw/proc #'e))
|
||||
scs/withs)
|
||||
fvars)]
|
||||
[(where/hidden x e)
|
||||
(loop (cdr stuffs) label scs/withs fvars)]
|
||||
(loop (cdr stuffs) label computed-label scs/withs fvars)]
|
||||
[(side-condition sc)
|
||||
(loop (cdr stuffs)
|
||||
label
|
||||
computed-label
|
||||
(cons (to-lw/uq/proc #'sc) scs/withs)
|
||||
fvars)]
|
||||
[(side-condition/hidden sc)
|
||||
(loop (cdr stuffs) label scs/withs fvars)]
|
||||
(loop (cdr stuffs) label computed-label scs/withs fvars)]
|
||||
[x
|
||||
(identifier? #'x)
|
||||
(loop (cdr stuffs)
|
||||
#''x
|
||||
computed-label
|
||||
scs/withs
|
||||
fvars)]
|
||||
[x
|
||||
(string? (syntax-e #'x))
|
||||
(loop (cdr stuffs)
|
||||
#'x
|
||||
#'(string->symbol x)
|
||||
computed-label
|
||||
scs/withs
|
||||
fvars)]
|
||||
[(computed-name e)
|
||||
(loop (cdr stuffs)
|
||||
label
|
||||
#'e
|
||||
scs/withs
|
||||
fvars)])]))])
|
||||
(with-syntax ([(scs/withs ...) scs/withs]
|
||||
|
|
@ -494,6 +508,8 @@
|
|||
#,(to-lw/proc #'lhs)
|
||||
#,(to-lw/proc #'rhs)
|
||||
#,label
|
||||
#,(and computed-label
|
||||
(to-lw/proc #`,#,computed-label))
|
||||
(list scs/withs ...
|
||||
#,@(map (λ (bind-id bind-pat)
|
||||
#`(cons #,(to-lw/proc bind-id)
|
||||
|
|
@ -721,7 +737,7 @@
|
|||
(define (do-leaf stx orig-name lang name-table from to extras lang-id)
|
||||
(let* ([lang-nts (language-id-nts lang-id orig-name)]
|
||||
[rw-sc (λ (pat) (rewrite-side-conditions/check-errs lang-nts orig-name #t pat))])
|
||||
(let-values ([(name sides/withs/freshs) (process-extras stx orig-name name-table extras)])
|
||||
(let-values ([(name computed-name sides/withs/freshs) (process-extras stx orig-name name-table extras)])
|
||||
(let*-values ([(names names/ellipses) (extract-names lang-nts orig-name #t from)]
|
||||
[(body-code)
|
||||
(bind-withs orig-name
|
||||
|
|
@ -730,7 +746,8 @@
|
|||
lang-nts
|
||||
sides/withs/freshs
|
||||
'flatten
|
||||
#`(list (term #,to))
|
||||
#`(list (cons #,(or computed-name #'none)
|
||||
(term #,to)))
|
||||
names names/ellipses)]
|
||||
[(test-case-body-code)
|
||||
;; this contains some redundant code
|
||||
|
|
@ -782,7 +799,12 @@
|
|||
(cover-case case-id c))))
|
||||
(relation-coverage))
|
||||
(loop (cdr mtchs)
|
||||
(map/mt (λ (x) (list name (f x))) really-matched acc))]
|
||||
(map/mt (λ (x) (list name
|
||||
(if (none? (car x))
|
||||
name
|
||||
(format "~a" (car x)))
|
||||
(f (cdr x))))
|
||||
really-matched acc))]
|
||||
[else
|
||||
(loop (cdr mtchs) acc)]))]))
|
||||
other-matches)))))
|
||||
|
|
@ -794,12 +816,13 @@
|
|||
(define (process-extras stx orig-name name-table extras)
|
||||
(let* ([the-name #f]
|
||||
[the-name-stx #f]
|
||||
[computed-name-stx #f]
|
||||
[sides/withs/freshs
|
||||
(let loop ([extras extras])
|
||||
(cond
|
||||
[(null? extras) '()]
|
||||
[else
|
||||
(syntax-case (car extras) (fresh)
|
||||
(syntax-case (car extras) (fresh computed-name)
|
||||
[name
|
||||
(or (identifier? (car extras))
|
||||
(string? (syntax-e (car extras))))
|
||||
|
|
@ -865,9 +888,17 @@
|
|||
(or (free-identifier=? #'-where #'where)
|
||||
(free-identifier=? #'-where #'where/hidden))
|
||||
(raise-syntax-error orig-name "malformed where clause" stx (car extras))]
|
||||
[(computed-name e)
|
||||
(if computed-name-stx
|
||||
(raise-syntax-errors orig-name "expected at most one computed-name clause"
|
||||
stx (list computed-name-stx #'e))
|
||||
(set! computed-name-stx #'e))
|
||||
(loop (cdr extras))]
|
||||
[(computed-name . _)
|
||||
(raise-syntax-error orig-name "malformed computed-name clause" stx (car extras))]
|
||||
[_
|
||||
(raise-syntax-error orig-name "unknown extra" stx (car extras))])]))])
|
||||
(values the-name sides/withs/freshs)))
|
||||
(values the-name computed-name-stx sides/withs/freshs)))
|
||||
|
||||
|
||||
|
||||
|
|
@ -2252,6 +2283,7 @@
|
|||
(provide language-nts
|
||||
apply-reduction-relation
|
||||
apply-reduction-relation/tag-with-names
|
||||
apply-reduction-relation/tagged
|
||||
apply-reduction-relation*
|
||||
variable-not-in
|
||||
variables-not-in)
|
||||
|
|
|
|||
|
|
@ -17,6 +17,7 @@ todo:
|
|||
scheme/gui/base
|
||||
scheme/list
|
||||
scheme/class
|
||||
scheme/set
|
||||
framework
|
||||
mrlib/graph
|
||||
scheme/contract
|
||||
|
|
@ -236,7 +237,7 @@ todo:
|
|||
(cond
|
||||
[(send (car new-children) in-cycle?)
|
||||
(reverse (cons new-children new-nodes))]
|
||||
[(member looking-for (find-reduction-label next-node (car new-children)))
|
||||
[(member looking-for (find-reduction-label next-node (car new-children) #f))
|
||||
(reverse (cons new-children new-nodes))]
|
||||
[else
|
||||
(loop (car new-children)
|
||||
|
|
@ -367,7 +368,7 @@ todo:
|
|||
|
||||
(when red-name-message
|
||||
(let ([label (map (λ (x) (if x (format "[~a]" x) "≪unknown≫"))
|
||||
(find-reduction-label parent child))])
|
||||
(find-reduction-label parent child #t))])
|
||||
(cond
|
||||
[(null? label) (void)]
|
||||
[(null? (cdr label))
|
||||
|
|
@ -379,11 +380,13 @@ todo:
|
|||
(map (λ (x) (format " and ~a" x))
|
||||
(cdr label)))]))))
|
||||
|
||||
(define (find-reduction-label parent child)
|
||||
(define (find-reduction-label parent child computed?)
|
||||
(let ([children (send parent get-children)])
|
||||
(and children
|
||||
(let loop ([children children]
|
||||
[red-names (send parent get-successor-names)])
|
||||
[red-names (if computed?
|
||||
(send parent get-successor-computed-names)
|
||||
(send parent get-successor-names))])
|
||||
(cond
|
||||
[(null? children) #f]
|
||||
[else
|
||||
|
|
@ -481,32 +484,31 @@ todo:
|
|||
;; (listof (listof string))
|
||||
;; one list element for each successor, one nested list element for each reduction that applied (typically 1)
|
||||
(define successor-names #f)
|
||||
(define successor-computed-names #f)
|
||||
(define/public (get-successors)
|
||||
(unless successors
|
||||
(let ([names/succs (apply-reduction-relation/tag-with-names red term)]
|
||||
[ht (make-hash)])
|
||||
(for-each (λ (name/succ)
|
||||
(let ([name (car name/succ)]
|
||||
[succ (cadr name/succ)])
|
||||
(hash-set! ht succ (cons name (hash-ref ht succ '())))))
|
||||
names/succs)
|
||||
(let ([merged-names/succs
|
||||
(let loop ([succs (map cadr names/succs)])
|
||||
(cond
|
||||
[(null? succs) null]
|
||||
[else
|
||||
(let ([succ (car succs)])
|
||||
(if (hash-ref ht succ)
|
||||
(cons (begin0 (list (hash-ref ht succ) succ)
|
||||
(hash-set! ht succ #f))
|
||||
(loop (cdr succs)))
|
||||
(loop (cdr succs))))]))])
|
||||
(set! successor-names (map car merged-names/succs))
|
||||
(set! successors (map cadr merged-names/succs)))))
|
||||
(let-values ([(succs names comp-names)
|
||||
(for/fold ([succs (set)]
|
||||
[names #hash()]
|
||||
[comp-names #hash()])
|
||||
([reduction (apply-reduction-relation/tagged red term)])
|
||||
(let ([name (first reduction)]
|
||||
[comp-name (second reduction)]
|
||||
[succ (third reduction)]
|
||||
[add (λ (x) (λ (xs) (cons x xs)))])
|
||||
(values (set-add succs succ)
|
||||
(hash-update names succ (add name) '())
|
||||
(hash-update comp-names succ (add comp-name) '()))))])
|
||||
(set! successors (set-map succs values))
|
||||
(set! successor-names (map (λ (s) (hash-ref names s)) successors))
|
||||
(set! successor-computed-names (map (λ (s) (hash-ref comp-names s)) successors))))
|
||||
successors)
|
||||
(define/public (get-successor-names)
|
||||
(get-successors) ;; force the variables to be defined
|
||||
successor-names)
|
||||
(define/public (get-successor-computed-names)
|
||||
(get-successors) ;; force the variables to be defined
|
||||
successor-computed-names)
|
||||
|
||||
(define/public (move-path)
|
||||
(change-path this))
|
||||
|
|
|
|||
|
|
@ -15,7 +15,7 @@
|
|||
rewrite-proc-lhs rewrite-proc-lhs-src rewrite-proc-id
|
||||
(struct-out rule-pict))
|
||||
|
||||
(define-struct rule-pict (arrow lhs rhs label side-conditions/pattern-binds fresh-vars))
|
||||
(define-struct rule-pict (arrow lhs rhs label computed-label side-conditions/pattern-binds fresh-vars))
|
||||
|
||||
;; type proc = (exp exp (any -> any) (listof any) -> (listof any)))
|
||||
;; a proc is a `cached' version of a make-proc, specialized to a particular langugage
|
||||
|
|
@ -68,7 +68,7 @@
|
|||
(let ([ress (proc tl-exp exp f acc)])
|
||||
(for-each
|
||||
(λ (res)
|
||||
(let ([term (cadr res)])
|
||||
(let ([term (caddr res)])
|
||||
(unless (match-pattern compiled-domain-pat term)
|
||||
(error 'reduction-relation "relation reduced to ~s via ~a, which is outside its domain"
|
||||
term
|
||||
|
|
|
|||
|
|
@ -679,12 +679,15 @@ all non-GUI portions of Redex) and also exported by
|
|||
([domain (code:line) (code:line #:domain @#,ttpattern)]
|
||||
[main-arrow (code:line) (code:line #:arrow arrow)]
|
||||
[reduction-case (--> @#,ttpattern @#,tttterm extras ...)]
|
||||
[extras name
|
||||
[extras rule-name
|
||||
(fresh fresh-clause ...)
|
||||
(side-condition racket-expression)
|
||||
(where tl-pat @#,tttterm)
|
||||
(side-condition/hidden racket-expression)
|
||||
(where/hidden tl-pat @#,tttterm)]
|
||||
[rule-name identifier
|
||||
string
|
||||
(computed-name racket-expression)]
|
||||
[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"))])]{
|
||||
|
|
@ -697,8 +700,25 @@ refers to the @racket[language], and binds variables in the
|
|||
|
||||
Following the @|pattern| and @|tterm| can be the name of the
|
||||
reduction rule, declarations of some fresh variables, and/or
|
||||
some side-conditions. The name can either be a literal
|
||||
name (identifier), or a literal string.
|
||||
some side-conditions.
|
||||
|
||||
The rule's name (used in @seclink["Typesetting" "typesetting"],
|
||||
the @racket[stepper], @racket[traces], and
|
||||
@racket[apply-reduction-relation/tag-with-names]) can be given
|
||||
as a literal (an identifier or a string) or as an expression
|
||||
that computes a name using the values of the bound pattern
|
||||
variables (much like the rule's right-hand side). Some operations
|
||||
require literal names, so a rule definition may provide both
|
||||
a literal name and a computed name. In particular, only rules that include
|
||||
a literal name may be replaced using @racket[extend-reduction-relation],
|
||||
used as breakpoints in the @racket[stepper], and selected using
|
||||
@racket[render-reduction-relation-rules]. The output of
|
||||
@racket[apply-reduction-relation/tag-with-names], @racket[traces], and
|
||||
the @racket[stepper] prefers the computed name, if it exists. Typesetting
|
||||
a rule with a computed name shows the expression that computes the name
|
||||
only when the rule has no literal name or when it would not typeset in
|
||||
pink due to @racket[with-unquote-rewriter]s in the context; otherwise,
|
||||
the literal name (or nothing) is shown.
|
||||
|
||||
The fresh variables clause generates variables that do not
|
||||
occur in the term being matched. If the @racket[fresh-clause] is a
|
||||
|
|
|
|||
|
|
@ -36,6 +36,34 @@
|
|||
(extend-reduction-relation red lang (--> 1 2)))
|
||||
"extended-reduction-relation.png")
|
||||
|
||||
(test (render-reduction-relation
|
||||
(with-unquote-rewriter
|
||||
(let ([once? #f])
|
||||
(λ (l)
|
||||
(if once?
|
||||
l
|
||||
(begin0
|
||||
(struct-copy lw
|
||||
l
|
||||
[e "a: any"]
|
||||
[unq? #f])
|
||||
(set! once? #t)))))
|
||||
(reduction-relation
|
||||
lang
|
||||
(--> (a any) 1 "a" (computed-name (format "a: ~a" (term any))))
|
||||
(--> (b any) 2 "b" (computed-name (format "b: ~a" (term any))))
|
||||
(--> (c any) 3 (computed-name (format "c: ~a" (term any)))))))
|
||||
"reduction-relation-with-computed-labels.png")
|
||||
|
||||
(let ([R (reduction-relation
|
||||
lang
|
||||
(--> 1 1 "a")
|
||||
(--> 2 2 "b" (computed-name "a"))
|
||||
(--> 3 3 (computed-name "c")))])
|
||||
(test (parameterize ([render-reduction-relation-rules (remq 'b (reduction-relation->rule-names R))])
|
||||
(render-reduction-relation R))
|
||||
"reduction-relation-with-computed-labels-and-hiding.png"))
|
||||
|
||||
;; this test should fail because it gets the order wrong
|
||||
;; for the where/side-conditions
|
||||
(define red2
|
||||
|
|
|
|||
Binary file not shown.
|
After Width: | Height: | Size: 626 B |
Binary file not shown.
|
After Width: | Height: | Size: 4.3 KiB |
|
|
@ -959,6 +959,25 @@
|
|||
'((2 3) (4 5)))
|
||||
(list (list "mult" '((2 3) 20))))
|
||||
|
||||
(test (apply-reduction-relation/tag-with-names
|
||||
(reduction-relation
|
||||
grammar
|
||||
(--> any
|
||||
(number_i number_i*)
|
||||
(where (number_0 ... number_i number_i+1 ...) any)
|
||||
(where (number_0* ... number_i* number_i+1* ...) any)
|
||||
pick-two
|
||||
(computed-name
|
||||
(format "(~s, ~s)"
|
||||
(length (term (number_0 ...)))
|
||||
(length (term (number_0* ...)))))))
|
||||
'(9 7))
|
||||
'(("(0, 0)" (9 9)) ("(0, 1)" (9 7)) ("(1, 0)" (7 9)) ("(1, 1)" (7 7))))
|
||||
|
||||
(test (apply-reduction-relation/tag-with-names
|
||||
(reduction-relation grammar (--> 1 2 (computed-name 3))) 1)
|
||||
'(("3" 2)))
|
||||
|
||||
(test (apply-reduction-relation
|
||||
(union-reduction-relations
|
||||
(reduction-relation empty-language
|
||||
|
|
@ -1399,6 +1418,22 @@
|
|||
1)
|
||||
'(3 2))
|
||||
|
||||
(test (apply-reduction-relation
|
||||
(extend-reduction-relation
|
||||
(reduction-relation empty-language (--> 1 2 (computed-name 1)))
|
||||
empty-language
|
||||
(--> 1 3 (computed-name 1)))
|
||||
1)
|
||||
'(3 2))
|
||||
|
||||
(test (apply-reduction-relation
|
||||
(extend-reduction-relation
|
||||
(reduction-relation empty-language (--> 1 2 (computed-name 1) x))
|
||||
empty-language
|
||||
(--> 1 3 (computed-name 1) x))
|
||||
1)
|
||||
'(3))
|
||||
|
||||
(let ()
|
||||
(define-language e1
|
||||
(e 1))
|
||||
|
|
@ -1485,6 +1520,13 @@
|
|||
(--> r p x)))
|
||||
'(a b c z y x))
|
||||
|
||||
(test (reduction-relation->rule-names
|
||||
(reduction-relation
|
||||
empty-language
|
||||
(--> x y a (computed-name "x to y"))
|
||||
(--> y z (computed-name "y to z"))))
|
||||
'(a))
|
||||
|
||||
(test (reduction-relation->rule-names
|
||||
(extend-reduction-relation
|
||||
(reduction-relation
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user