Adjust rewrite-side-conditions/check-errs so that it
returns the ellipses names in addition to the regular names keeping the names in the pattern and including them in the last two results closes PR 14291
This commit is contained in:
Robby Findler
parent
a391556faa
commit
b5cfb7affe
|
|
@ -147,8 +147,10 @@
|
|||
[res-term-stx #`(#,jf-id #,@args-stx)]
|
||||
[property #`(bind-prop
|
||||
(λ (bindings)
|
||||
(term-let ([names/ellipses (lookup-binding bindings 'names)] ...)
|
||||
#,property)))])
|
||||
#,(bind-pattern-names 'redex-check
|
||||
#'(names/ellipses ...)
|
||||
#'((lookup-binding bindings 'names) ...)
|
||||
property)))])
|
||||
(quasisyntax/loc orig-stx
|
||||
(let ([term-match (λ (generated)
|
||||
(cond [(test-match #,lang res-term-stx generated) => values]
|
||||
|
|
@ -183,9 +185,12 @@
|
|||
[show (show-message orig-stx)]
|
||||
[property #`(bind-prop
|
||||
(λ (bindings)
|
||||
(term-let ([lhs-names/ellipses (lookup-binding bindings 'lhs-names)] ...
|
||||
[rhs-names/ellipses (lookup-binding bindings 'rhs-names)] ...)
|
||||
#,property)))])
|
||||
#,(bind-pattern-names 'redex-check
|
||||
#'(lhs-names/ellipses ...
|
||||
rhs-names/ellipses ...)
|
||||
#'((lookup-binding bindings 'lhs-names) ...
|
||||
(lookup-binding bindings 'rhs-names) ...)
|
||||
property)))])
|
||||
(quasisyntax/loc orig-stx
|
||||
(let ([term-match (λ (generated)
|
||||
(cond [(test-match #,lang res-term-stx generated) => values]
|
||||
|
|
@ -214,8 +219,10 @@
|
|||
(parse-redex-check-kw-args kw-args orig-stx form))
|
||||
(with-syntax ([property #`(bind-prop
|
||||
(λ (bindings)
|
||||
(term-let ([name/ellipses (lookup-binding bindings 'name)] ...)
|
||||
#,property)))])
|
||||
#,(bind-pattern-names 'redex-check
|
||||
#'(name/ellipses ...)
|
||||
#'((lookup-binding bindings 'name) ...)
|
||||
property)))])
|
||||
(quasisyntax/loc orig-stx
|
||||
(let ([att #,attempts-stx]
|
||||
[ret #,retries-stx]
|
||||
|
|
|
|||
|
|
@ -154,8 +154,10 @@
|
|||
(λ (bindings)
|
||||
(let ([x (lookup-binding bindings 'names)] ...)
|
||||
(and binding-constraints ...
|
||||
(term-let ([names/ellipses x] ...)
|
||||
#,rest-body)))))))))]
|
||||
#,(bind-pattern-names orig-name
|
||||
#'(names/ellipses ...)
|
||||
#'(x ...)
|
||||
rest-body)))))))))]
|
||||
[((-side-condition s ...) y ...)
|
||||
(side-condition-keyword? #'-side-condition)
|
||||
(if side-condition-unquoted?
|
||||
|
|
@ -239,8 +241,10 @@
|
|||
(λ (bindings #,(if jf-results-id jf-results-id '_ignored))
|
||||
(let ([temp (lookup-binding bindings 'output-name)] ...)
|
||||
(and binding-constraint ...
|
||||
(term-let ([output-name/ellipsis temp] ...)
|
||||
#,rest-body))))))))]))))
|
||||
#,(bind-pattern-names orig-name
|
||||
#'(output-name/ellipsis ...)
|
||||
#'(temp ...)
|
||||
rest-body))))))))]))))
|
||||
|
||||
(define (judgment-form-bind-withs/proc lang output-pattern output under-ellipsis? old-maps do-something)
|
||||
(let ([compiled-pattern (compile-pattern lang output-pattern #t)])
|
||||
|
|
@ -816,8 +820,10 @@
|
|||
compiled-lhs
|
||||
input
|
||||
(λ (bnds)
|
||||
(term-let ([names/ellipses (lookup-binding bnds 'names)] ...)
|
||||
#,body))
|
||||
#,(bind-pattern-names 'judgment-form
|
||||
#'(names/ellipses ...)
|
||||
#'((lookup-binding bnds 'names) ...)
|
||||
body))
|
||||
#,(if output-contracts
|
||||
#`(λ (output)
|
||||
(check-judgment-form-contract '#,name output compiled-output-ctcs 'O '#,mode))
|
||||
|
|
|
|||
|
|
@ -47,17 +47,24 @@
|
|||
(syntax->list (syntax (pattern ...))))]
|
||||
[(cp-x ...) (generate-temporaries #'(pattern ...))]
|
||||
[make-matcher make-matcher])
|
||||
#'(begin
|
||||
syncheck-expr ...
|
||||
(make-matcher
|
||||
'form-name lang
|
||||
(list 'pattern ...)
|
||||
(list (compile-pattern lang `side-conditions-rewritten #t) ...)
|
||||
(list (λ (match)
|
||||
(term-let/error-name
|
||||
form-name
|
||||
([names/ellipses (lookup-binding (mtch-bindings match) 'names)] ...)
|
||||
rhs)) ...)))))]))
|
||||
(with-syntax ([(mtch-procs ...)
|
||||
(for/list ([names/ellipses (in-list (syntax->list #'((names/ellipses ...) ...)))]
|
||||
[names (in-list (syntax->list #'((names ...) ...)))]
|
||||
[rhs (in-list (syntax->list #'(rhs ...)))])
|
||||
(with-syntax ([(names ...) names])
|
||||
#`(λ (match)
|
||||
#,(bind-pattern-names
|
||||
#'form-name
|
||||
names/ellipses
|
||||
#'((lookup-binding (mtch-bindings match) 'names) ...)
|
||||
rhs))))])
|
||||
#`(begin
|
||||
syncheck-expr ...
|
||||
(make-matcher
|
||||
'form-name lang
|
||||
(list 'pattern ...)
|
||||
(list (compile-pattern lang `side-conditions-rewritten #t) ...)
|
||||
(list mtch-procs ...))))))]))
|
||||
|
||||
(define-syntax (term-match/single stx)
|
||||
(term-matcher stx #'term-match/single/proc))
|
||||
|
|
@ -683,10 +690,12 @@
|
|||
'lhs-frm-id
|
||||
'lhs-to-id
|
||||
`side-conditions-rewritten
|
||||
(λ (bindings rhs-binder)
|
||||
(term-let ([lhs-to-id rhs-binder]
|
||||
[names/ellipses (lookup-binding bindings 'names)] ...)
|
||||
(term rhs-to #:lang lang)))
|
||||
(λ (bindings rhs-binder)
|
||||
(term-let ([lhs-to-id rhs-binder])
|
||||
#,(bind-pattern-names 'reduction-relation
|
||||
#'(names/ellipses ...)
|
||||
#'((lookup-binding bindings 'names) ...)
|
||||
#'(term rhs-to #:lang lang))))
|
||||
#,child-proc
|
||||
`fresh-rhs-from)))
|
||||
(get-choices stx orig-name bm #'lang
|
||||
|
|
@ -779,13 +788,16 @@
|
|||
[body-code body-code])
|
||||
#`(begin
|
||||
lhs-syncheck-expr
|
||||
(build-rewrite-proc/leaf `side-conditions-rewritten
|
||||
(λ (main-exp bindings)
|
||||
(term-let ([names/ellipses (lookup-binding bindings 'names)] ...)
|
||||
body-code))
|
||||
lhs-source
|
||||
name
|
||||
(λ (lang-id2) `lhs-w/extras))))))
|
||||
(build-rewrite-proc/leaf
|
||||
`side-conditions-rewritten
|
||||
(λ (main-exp bindings)
|
||||
#,(bind-pattern-names 'reduction-relation
|
||||
#'(names/ellipses ...)
|
||||
#'((lookup-binding bindings 'names) ...)
|
||||
#'body-code))
|
||||
lhs-source
|
||||
name
|
||||
(λ (lang-id2) `lhs-w/extras))))))
|
||||
|
||||
(define (process-extras stx orig-name name-table extras)
|
||||
(let* ([the-name #f]
|
||||
|
|
@ -1085,12 +1097,15 @@
|
|||
(let ([ans (match-pattern cpat exp)])
|
||||
(and ans
|
||||
(map (λ (m) (make-match (sort-bindings
|
||||
(filter (λ (x) (memq (bind-name x) binders))
|
||||
(filter (λ (x) (and (memq (bind-name x) binders)
|
||||
(not-ellipsis-name (bind-name x))))
|
||||
(bindings-table (mtch-bindings m))))))
|
||||
ans))))))
|
||||
(if name
|
||||
(procedure-rename redex-match-proc name)
|
||||
redex-match-proc))
|
||||
(define (not-ellipsis-name x)
|
||||
(not (regexp-match? #rx"^[.][.][.]" (symbol->string x))))
|
||||
|
||||
(define (sort-bindings bnds)
|
||||
(sort
|
||||
|
|
@ -1704,6 +1719,10 @@
|
|||
"cannot use pattern language keyword as a non-terminal name")
|
||||
(check-each names (λ (x) (regexp-match? #rx"_" (symbol->string (syntax-e x))))
|
||||
"cannot use _ in a non-terminal name")
|
||||
(check-each names (λ (x) (regexp-match? #rx"^[.][.][.]$" (symbol->string (syntax-e x))))
|
||||
"cannot name a non-terminal `...'")
|
||||
(check-each names (λ (x) (regexp-match? #rx"^[.][.][.]_" (symbol->string (syntax-e x))))
|
||||
"cannot start a non-terminal name with `..._'")
|
||||
|
||||
(when (null? prods)
|
||||
(raise-syntax-error #f "expected at least one production to follow"
|
||||
|
|
|
|||
|
|
@ -14,7 +14,8 @@
|
|||
(rename-out [binds? id-binds?])
|
||||
raise-ellipsis-depth-error
|
||||
make-language-id
|
||||
language-id-nts)
|
||||
language-id-nts
|
||||
bind-pattern-names)
|
||||
|
||||
(provide (struct-out id/depth))
|
||||
|
||||
|
|
@ -59,6 +60,11 @@
|
|||
;; hash[sym -o> (listof stx)]
|
||||
(define var-locs-table (make-hash))
|
||||
|
||||
;; hash[sym -o> sym]
|
||||
;; tells the original names for any given repeat to be replaced after
|
||||
;; normalization and checking has finished
|
||||
(define original-repeat-names (make-hash))
|
||||
|
||||
(define (record-binder pat-stx under under-mismatch-ellipsis)
|
||||
(define pat-sym (syntax->datum pat-stx))
|
||||
(hash-set! var-locs-table pat-sym (cons pat-stx (hash-ref var-locs-table pat-sym '())))
|
||||
|
|
@ -288,24 +294,29 @@
|
|||
orig-stx
|
||||
(cadr terms)
|
||||
(list (caddr terms))))
|
||||
(define ellipsis-sym (syntax-e (cadr terms)))
|
||||
(define ellipsis-pre-str (symbol->string ellipsis-sym))
|
||||
(define ellipsis-pre-sym (syntax-e (cadr terms)))
|
||||
(define ellipsis-pre-str (symbol->string ellipsis-pre-sym))
|
||||
(define mismatch? (regexp-match? #rx"^[.][.][.]_!_" ellipsis-pre-str))
|
||||
(define ellipsis-str (cond
|
||||
[mismatch?
|
||||
(set! ellipsis-number (+ ellipsis-number 1))
|
||||
(format "..._r~a" ellipsis-number)]
|
||||
[(regexp-match? #rx"^[.][.][.]_r" ellipsis-pre-str)
|
||||
(string-append (substring ellipsis-str 0 4)
|
||||
"r"
|
||||
(substring ellipsis-str
|
||||
4
|
||||
(string-length ellipsis-str)))]
|
||||
[(regexp-match? #rx"^[.][.][.]_" ellipsis-pre-str)
|
||||
ellipsis-pre-str]
|
||||
[else
|
||||
(set! ellipsis-number (+ ellipsis-number 1))
|
||||
(format "..._r~a" ellipsis-number)]))
|
||||
(define-values (ellipsis-str was-named-ellipsis?)
|
||||
(cond
|
||||
[mismatch?
|
||||
(set! ellipsis-number (+ ellipsis-number 1))
|
||||
(values (format "..._r~a" ellipsis-number) #f)]
|
||||
[(regexp-match? #rx"^[.][.][.]_r" ellipsis-pre-str)
|
||||
(values (string-append (substring ellipsis-str 0 4)
|
||||
"r"
|
||||
(substring ellipsis-str
|
||||
4
|
||||
(string-length ellipsis-str)))
|
||||
#t)]
|
||||
[(regexp-match? #rx"^[.][.][.]_" ellipsis-pre-str)
|
||||
(values ellipsis-pre-str #t)]
|
||||
[else
|
||||
(set! ellipsis-number (+ ellipsis-number 1))
|
||||
(values (format "..._r~a" ellipsis-number) #f)]))
|
||||
(define ellipsis-sym (string->symbol ellipsis-str))
|
||||
(when was-named-ellipsis?
|
||||
(hash-set! original-repeat-names ellipsis-sym ellipsis-pre-sym))
|
||||
(define ellipsis+name (datum->syntax
|
||||
(cadr terms)
|
||||
(string->symbol ellipsis-str)
|
||||
|
|
@ -318,11 +329,13 @@
|
|||
(cons (syntax-e (cadr terms)) under-mismatch-ellipsis)
|
||||
under-mismatch-ellipsis)))
|
||||
(define-values (rst-terms rst-vars) (t-loop (cddr terms)))
|
||||
(values (cons `(repeat ,fst-term
|
||||
,ellipsis+name
|
||||
,(if mismatch? (cadr terms) #f))
|
||||
(values (cons `(repeat ,fst-term ,ellipsis+name ,(if mismatch? (cadr terms) #f))
|
||||
rst-terms)
|
||||
(append fst-vars rst-vars))]
|
||||
(append fst-vars
|
||||
(if was-named-ellipsis?
|
||||
(list (id/depth (cadr terms) (length under) #f))
|
||||
'())
|
||||
rst-vars))]
|
||||
[else
|
||||
(define-values (fst-term fst-vars)
|
||||
(loop (car terms) under under-mismatch-ellipsis))
|
||||
|
|
@ -425,7 +438,7 @@
|
|||
(let ()
|
||||
(define final-match-repeat-name
|
||||
(if (= 1 (hash-ref repeat-id-counts (syntax-e #'name)))
|
||||
#f
|
||||
(hash-ref original-repeat-names (syntax-e #'name) #f)
|
||||
#'name))
|
||||
(define final-mismatch-repeat-name
|
||||
(if (and (syntax-e #'mismatch-name)
|
||||
|
|
@ -569,3 +582,13 @@
|
|||
orig-stx)))
|
||||
(not same-id?)))
|
||||
(loop (cdr dups))))])))
|
||||
|
||||
|
||||
|
||||
(define (bind-pattern-names err-name names/ellipses vals body)
|
||||
(with-syntax ([(names/ellipsis ...) names/ellipses]
|
||||
[(val ...) vals])
|
||||
#`(term-let/error-name
|
||||
#,err-name
|
||||
([names/ellipsis val] ...)
|
||||
#,body)))
|
||||
|
|
@ -168,7 +168,9 @@
|
|||
(judgment-form-id? #'jf-name))
|
||||
(begin
|
||||
(unless (not (memq 'O (judgment-form-mode (syntax-local-value #'jf-name))))
|
||||
(raise-syntax-error 'term "judgment forms with output mode (\"O\") positions disallowed" arg-stx stx))
|
||||
(raise-syntax-error 'term
|
||||
"judgment forms with output mode (\"O\") positions disallowed"
|
||||
arg-stx stx))
|
||||
(rewrite-application #'jf-name (syntax/loc stx (arg ...)) depth))]
|
||||
[f
|
||||
(and (identifier? (syntax f))
|
||||
|
|
@ -255,7 +257,9 @@
|
|||
(define m (regexp-match #rx"^([^_]*)_" (symbol->string id)))
|
||||
(when m
|
||||
(unless (memq (string->symbol (list-ref m 1)) (append pattern-symbols lang-nts))
|
||||
(raise-syntax-error 'term "before underscore must be either a non-terminal or a built-in pattern" arg-stx stx)))))
|
||||
(raise-syntax-error 'term
|
||||
"before underscore must be either a non-terminal or a built-in pattern"
|
||||
arg-stx stx)))))
|
||||
|
||||
(values
|
||||
(with-syntax ([rewritten (rewrite arg-stx)])
|
||||
|
|
@ -374,40 +378,46 @@
|
|||
(define-syntax (term-let/error-name stx)
|
||||
(syntax-case stx ()
|
||||
[(_ error-name ([x1 rhs1] [x rhs] ...) body1 body2 ...)
|
||||
(let-values ([(orig-names new-names depths new-x1)
|
||||
(let loop ([stx #'x1] [depth 0])
|
||||
(define ((combine orig-names new-names depths new-pat)
|
||||
orig-names* new-names* depths* new-pat*)
|
||||
(values (append orig-names orig-names*)
|
||||
(append new-names new-names*)
|
||||
(append depths depths*)
|
||||
(cons new-pat new-pat*)))
|
||||
(syntax-case stx (...)
|
||||
[x
|
||||
(and (identifier? #'x)
|
||||
(not (free-identifier=? (quote-syntax ...) #'x)))
|
||||
(let ([new-name (datum->syntax #'here (syntax-e #'x) #'x #'x)])
|
||||
(values (list #'x)
|
||||
(list new-name)
|
||||
(list depth)
|
||||
new-name))]
|
||||
[(x (... ...) . xs)
|
||||
(let-values ([(orig-names new-names depths new-pat)
|
||||
(call-with-values
|
||||
(λ () (loop #'xs depth))
|
||||
(call-with-values
|
||||
(λ () (loop #'x (add1 depth)))
|
||||
combine))])
|
||||
(values orig-names new-names depths
|
||||
(list* (car new-pat) #'(... ...) (cdr new-pat))))]
|
||||
[(x . xs)
|
||||
(call-with-values
|
||||
(λ () (loop #'xs depth))
|
||||
(call-with-values
|
||||
(λ () (loop #'x depth))
|
||||
combine))]
|
||||
[_
|
||||
(values '() '() '() stx)]))])
|
||||
(let ()
|
||||
(unless (identifier? #'error-name)
|
||||
(raise-syntax-error 'term-let/error-name
|
||||
"expected an identifier as the first argument"
|
||||
stx
|
||||
#'error-name))
|
||||
(define-values (orig-names new-names depths new-x1)
|
||||
(let loop ([stx #'x1] [depth 0])
|
||||
(define ((combine orig-names new-names depths new-pat)
|
||||
orig-names* new-names* depths* new-pat*)
|
||||
(values (append orig-names orig-names*)
|
||||
(append new-names new-names*)
|
||||
(append depths depths*)
|
||||
(cons new-pat new-pat*)))
|
||||
(syntax-case stx (...)
|
||||
[x
|
||||
(and (identifier? #'x)
|
||||
(not (free-identifier=? (quote-syntax ...) #'x)))
|
||||
(let ([new-name (datum->syntax #'here (syntax-e #'x) #'x #'x)])
|
||||
(values (list #'x)
|
||||
(list new-name)
|
||||
(list depth)
|
||||
new-name))]
|
||||
[(x (... ...) . xs)
|
||||
(let-values ([(orig-names new-names depths new-pat)
|
||||
(call-with-values
|
||||
(λ () (loop #'xs depth))
|
||||
(call-with-values
|
||||
(λ () (loop #'x (add1 depth)))
|
||||
combine))])
|
||||
(values orig-names new-names depths
|
||||
(list* (car new-pat) #'(... ...) (cdr new-pat))))]
|
||||
[(x . xs)
|
||||
(call-with-values
|
||||
(λ () (loop #'xs depth))
|
||||
(call-with-values
|
||||
(λ () (loop #'x depth))
|
||||
combine))]
|
||||
[_
|
||||
(values '() '() '() stx)])))
|
||||
(with-syntax ([(orig-names ...) orig-names]
|
||||
[(new-names ...) new-names]
|
||||
[(depths ...) depths]
|
||||
|
|
|
|||
|
|
@ -24,8 +24,9 @@
|
|||
(check-equal? (rsc (1) () #t) `((list 1) () ()))
|
||||
(check-equal? (rsc (_ _ (name x _)) () #t) `((list any any (name x any)) (x) (x)))
|
||||
(check-equal? (rsc (1 ...) () #t) `((list (repeat 1 #f #f)) () ()))
|
||||
(check-equal? (rsc (1 ..._2) () #t) `((list (repeat 1 #f #f)) () ()))
|
||||
(check-equal? (rsc (1 ..._2 1 ..._2) () #t) `((list (repeat 1 ..._2 #f) (repeat 1 ..._2 #f)) () ()))
|
||||
(check-equal? (rsc (1 ..._2) () #t) `((list (repeat 1 ..._2 #f)) (..._2) (..._2)))
|
||||
(check-equal? (rsc (1 ..._2 1 ..._2) () #t)
|
||||
`((list (repeat 1 ..._2 #f) (repeat 1 ..._2 #f)) (..._2 ..._2) (..._2 ..._2)))
|
||||
(check-equal? (rsc (1 ..._!_3) () #t) `((list (repeat 1 #f #f)) () ()))
|
||||
(check-equal? (rsc (1 ..._!_3 1 ..._!_3) () #t)
|
||||
`((list (repeat 1 #f ..._!_3) (repeat 1 #f ..._!_3)) () ()))
|
||||
|
|
@ -42,7 +43,9 @@
|
|||
`((list (repeat (list (repeat (name x (nt x)) #f #f)) #f #f))
|
||||
(x)
|
||||
(((x ...) ...))))
|
||||
|
||||
(check-equal? (rsc (any_1 any_1) (x) #f) `((list (name any_1 any) (name any_1 any))
|
||||
(any_1 any_1)
|
||||
(any_1 any_1)))
|
||||
(check-equal? (rsc (in-hole (hole a #f (hide-hole hole)) (cross x)) '(x) #f)
|
||||
`((in-hole (list hole a #f (hide-hole hole)) (cross x-x))
|
||||
()
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user