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

Adjusted rewrite-side-condition/check-errs so that it normalizes the internal

Browse Source 
redex patterns a bunch:

- repeats are turned into wrappers in sequences,
- names are all explicit,
- non-terminals are wrapped with `nt',
- cross patterns always have the hyphens in them.
- ellipses names are normalized (so there are no "hidden"
  name equalities); this also means that repeat patterns
  can have both a regular name and a mismatch name

Also, added a match-a-pattern helper macro that checks to make sure
that functions that process patterns don't miss any cases
This commit is contained in:
Robby Findler 2011-12-21 17:11:15 -06:00
parent c9fcde258f
commit f1bacffbdc
14 changed files with 1823 additions and 1226 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

131
collects/redex/private/match-a-pattern.rkt Normal file
View File

@ -0,0 +1,131 @@
#lang racket/base
(require racket/match
(for-syntax racket/match
racket/base))
(provide match-a-pattern)
#|
The grammar for the internal patterns is the
contents of the should-be-pats list, where each
'pat' that appears behind an unquote there is
a self-reference in the grammar.
lpat ::= pat
| `(repeat ,pat ,(or/c symbol? #f) ,(or/c symbol? #f))
;; repeat indicates a repetition (ellipsis in the
;; surface language), where the pattern inside is
;; what's repeated, the second position is a name
;; if the ellipsis is named normally and the final
;; position is a name if the ellipsis has a mismatch
;; name (more below).
var ::= symbol?
condition ::= (-> bindings? any) ;; any is treated like a boolean
Also, the `(cross ,nt) pattern alwyas has hypenated non-terminals, ie
(cross e) in the source turns into (cross e-e) after translation (which
means that the other cross non-terminals, e.g. (cross e-v), are not
directly available as redex patterns, but can only be used via the
non-terminals that Redex creates for the cross languages.
Internal patterns also come with the invariant that there are no
redundant or non-local ellipses names. That is, consider this pattern:
(any_1 ..._1 any_1 ..._2)
It might seem like it would turn into something like this:
(list (repeat (name any_1 any) ..._1 #f)
(repeat (name any_1 any) ..._2 #f))
but the _1 and _2 are actually not right, since the x_1 name
will force the two ellipses lengths to be the same. So, this
must turn into this pattern:
(list (repeat (name any_1 any) ..._1 #f)
(repeat (name any_1 any) ..._1 #f))
Similarly, if there are superflous names, they are delete. For
example, this source pattern:
(any_1 ..._1)
turns into this:
(list (repeat (name any_1 any) #f #f))
Also, although there cannot be any patterns at the source level
that have both kinds of names, there can be once the ellipses
have been resolved. For example, this:
(any_1 ..._1
any_1 ..._!_2
any_1 ..._1
any_1 ..._!_2)
turns into this:
(list (repeat (name any_1 any) ..._1 #f)
(repeat (name any_1 any) ..._1 ..._!_2)
(repeat (name any_1 any) ..._1 #f)
(repeat (name any_1 any) ..._1 ..._!_2))
|#
(define-syntax (match-a-pattern stx)
(syntax-case stx ()
[(_ to-match [pats rhs ...] ...)
(let ()
(define should-be-pats
'(`any
`number
`string
`natural
`integer
`real
`variable
`(variable-except ,var ...)
`(variable-prefix ,var)
`variable-not-otherwise-mentioned
`hole
`(nt ,var)
`(name ,var ,pat)
`(mismatch-name ,var ,pat)
`(in-hole ,pat ,pat) ;; context, then contractum
`(hide-hole ,pat)
`(side-condition ,pat ,condition ,srcloc-expr)
`(cross ,var)
`(list ,lpat ...)
(? (compose not pair?)) ;; pattern for literals (numbers, strings, prefabs, etc etc etc)
))
(for ([pat (in-list (syntax->list #'(pats ...)))])
(when (null? should-be-pats)
(raise-syntax-error 'match-a-pattern "too many patterns" stx pat))
(define should-be (car should-be-pats))
(set! should-be-pats (cdr should-be-pats))
(define pats-match?
(let loop ([pat (syntax->datum pat)]
[should-be should-be])
(cond
[(and (null? pat) (null? should-be)) #t]
[(and (pair? pat) (pair? should-be))
(cond
[(eq? (car should-be) 'unquote)
(eq? (car pat) 'unquote)]
[else
(and (loop (car pat) (car should-be))
(loop (cdr pat) (cdr should-be)))])]
[else (equal? pat should-be)])))
(unless pats-match?
(raise-syntax-error 'match-a-pattern
(format "expected pattern ~s"
should-be)
stx
pat)))
(unless (null? should-be-pats)
(raise-syntax-error 'match-a-pattern
(format "did not find pattern ~s"
(car should-be-pats))
stx))
#'(match to-match [pats rhs ...] ...))]))

717
collects/redex/private/matcher.rkt
View File

File diff suppressed because it is too large Load Diff

352
collects/redex/private/reduction-semantics.rkt
View File

@ -52,12 +52,7 @@
(unless (identifier? #'lang) (unless (identifier? #'lang)
(raise-syntax-error (syntax-e #'form-name) "expected an identifier in the language position" orig-stx #'lang)) (raise-syntax-error (syntax-e #'form-name) "expected an identifier in the language position" orig-stx #'lang))
(let ([lang-nts (language-id-nts #'lang (syntax-e #'form-name))]) (let ([lang-nts (language-id-nts #'lang (syntax-e #'form-name))])
(with-syntax ([(((names ...) (names/ellipses ...)) ...) (with-syntax ([((side-conditions-rewritten (names ...) (names/ellipses ...)) ...)
(map (λ (x) (call-with-values
(λ () (extract-names lang-nts (syntax-e #'form-name) #t x))
list))
(syntax->list (syntax (pattern ...))))]
[(side-conditions-rewritten ...)
(map (λ (x) (rewrite-side-conditions/check-errs lang-nts (syntax-e #'form-name) #t x)) (map (λ (x) (rewrite-side-conditions/check-errs lang-nts (syntax-e #'form-name) #t x))
(syntax->list (syntax (pattern ...))))] (syntax->list (syntax (pattern ...))))]
[(cp-x ...) (generate-temporaries #'(pattern ...))] [(cp-x ...) (generate-temporaries #'(pattern ...))]
@ -158,7 +153,7 @@
(syntax-case stx () (syntax-case stx ()
[(_ red lang nt) [(_ red lang nt)
(identifier? (syntax nt)) (identifier? (syntax nt))
(with-syntax ([side-conditions-rewritten (with-syntax ([(side-conditions-rewritten (names ...) (names/ellipses ...))
(rewrite-side-conditions/check-errs (language-id-nts #'lang 'compatible-closure) (rewrite-side-conditions/check-errs (language-id-nts #'lang 'compatible-closure)
'compatible-closure 'compatible-closure
#t #t
@ -170,7 +165,7 @@
(define-syntax (context-closure stx) (define-syntax (context-closure stx)
(syntax-case stx () (syntax-case stx ()
[(_ red lang pattern) [(_ red lang pattern)
(with-syntax ([side-conditions-rewritten (with-syntax ([(side-conditions-rewritten (names ...) (names/ellipses ...))
(rewrite-side-conditions/check-errs (language-id-nts #'lang 'context-closure) (rewrite-side-conditions/check-errs (language-id-nts #'lang 'context-closure)
'context-closure 'context-closure
#t #t
@ -291,8 +286,8 @@
(syntax-case stx () (syntax-case stx ()
[(s (... ...)) [(s (... ...))
(let ([r (id/depth #'s)]) (let ([r (id/depth #'s)])
(make-id/depth (id/depth-id r) (add1 (id/depth-depth r))))] (make-id/depth (id/depth-id r) (add1 (id/depth-depth r)) (id/depth-mismatch? r)))]
[s (make-id/depth #'s 0)])) [s (make-id/depth #'s 0 #f)]))
(define temporaries (generate-temporaries names)) (define temporaries (generate-temporaries names))
(values (values
(for/fold ([cs '()]) (for/fold ([cs '()])
@ -332,37 +327,33 @@
[() body] [() body]
[((-where x e) y ...) [((-where x e) y ...)
(where-keyword? #'-where) (where-keyword? #'-where)
(let-values ([(names names/ellipses) (extract-names lang-nts 'reduction-relation #t #'x)]) (let ()
(define-values (binding-constraints temporaries env+) (with-syntax ([(side-conditions-rewritten (names ...) (names/ellipses ...))
(generate-binding-constraints names names/ellipses env orig-name)) (rewrite-side-conditions/check-errs
(with-syntax ([(binding-constraints ...) binding-constraints] lang-nts
[side-conditions-rewritten (rewrite-side-conditions/check-errs 'reduction-relation
lang-nts #t
'reduction-relation #'x)])
#f (define-values (binding-constraints temporaries env+)
#'x)] (generate-binding-constraints (syntax->list #'(names ...))
[(names ...) names] (syntax->list #'(names/ellipses ...))
[(names/ellipses ...) names/ellipses] env
[(x ...) temporaries]) orig-name))
(let ([rest-body (loop #'(y ...) #`(list x ... #,to-not-be-in) env+)]) (with-syntax ([(binding-constraints ...) binding-constraints]
#`(let* ([mtchs (match-pattern (compile-pattern #,lang `side-conditions-rewritten #t) (term e))] [(x ...) temporaries])
[result (λ (mtch) (define rest-body (loop #'(y ...) #`(list x ... #,to-not-be-in) env+))
(let ([bindings (mtch-bindings mtch)]) #`(#,(case where-mode
(let ([x (lookup-binding bindings 'names)] ...) [(flatten)
(and binding-constraints ... #'combine-where-results/flatten]
(term-let ([names/ellipses x] ...) [(predicate)
#,rest-body)))))]) #'combine-where-results/predicate]
(if mtchs [else (error 'unknown-where-mode "~s" where-mode)])
#, (match-pattern (compile-pattern #,lang `side-conditions-rewritten #t) (term e))
(case where-mode (λ (bindings)
[(flatten) (let ([x (lookup-binding bindings 'names)] ...)
#`(for/fold ([r '()]) ([m mtchs]) (and binding-constraints ...
(let ([s (result m)]) (term-let ([names/ellipses x] ...)
(if s (append s r) r)))] #,rest-body))))))))]
[(predicate)
#`(ormap result mtchs)]
[else (error 'unknown-where-mode "~s" where-mode)])
#f)))))]
[((-side-condition s ...) y ...) [((-side-condition s ...) y ...)
(or (free-identifier=? #'-side-condition #'side-condition) (or (free-identifier=? #'-side-condition #'side-condition)
(free-identifier=? #'-side-condition #'side-condition/hidden)) (free-identifier=? #'-side-condition #'side-condition/hidden))
@ -410,10 +401,12 @@
(let ([ellipsis (syntax/loc premise (... ...))]) (let ([ellipsis (syntax/loc premise (... ...))])
(values #`(#,in #,ellipsis) #`(#,out #,ellipsis))) (values #`(#,in #,ellipsis) #`(#,out #,ellipsis)))
(values in out)))] (values in out)))]
[(output-pattern) [(output-pattern output-names output-names/ellipses)
(rewrite-side-conditions/check-errs lang-nts orig-name #t output-pre-pattern)] (with-syntax ([(output names names/ellipses)
[(output-names output-names/ellipses) (rewrite-side-conditions/check-errs lang-nts orig-name #t output-pre-pattern)])
(extract-names lang-nts orig-name #t output-pre-pattern)] (values #'output
(syntax->list #'names)
(syntax->list #'names/ellipses)))]
[(binding-constraints temporaries env+) [(binding-constraints temporaries env+)
(generate-binding-constraints output-names output-names/ellipses env orig-name)] (generate-binding-constraints output-names output-names/ellipses env orig-name)]
[(rest-body) (loop rest-clauses #`(list judgment-output #,to-not-be-in) env+)] [(rest-body) (loop rest-clauses #`(list judgment-output #,to-not-be-in) env+)]
@ -446,6 +439,17 @@
outputs))) outputs)))
outputs)))))])))) outputs)))))]))))
(define (combine-where-results/flatten mtchs result)
(and mtchs
(for/fold ([r '()]) ([m mtchs])
(let ([s (result (mtch-bindings m))])
(if s (append s r) r)))))
(define (combine-where-results/predicate mtchs result)
(and mtchs
(for/or ([mtch mtchs])
(result (mtch-bindings mtch)))))
(define (repeated-premise-outputs inputs premise) (define (repeated-premise-outputs inputs premise)
(if (null? inputs) (if (null? inputs)
'(()) '(())
@ -815,7 +819,7 @@
(map car (sort (hash-map name-table (λ (k v) (list k (list-ref v 1)))) < #:key cadr)))] (map car (sort (hash-map name-table (λ (k v) (list k (list-ref v 1)))) < #:key cadr)))]
[lws lws] [lws lws]
[domain-pattern-side-conditions-rewritten [(domain-pattern-side-conditions-rewritten (names ...) (names/ellipses ...))
(rewrite-side-conditions/check-errs (rewrite-side-conditions/check-errs
lang-nts lang-nts
orig-name orig-name
@ -868,31 +872,30 @@
(let* ([lang-nts (language-id-nts lang-id orig-name)] (let* ([lang-nts (language-id-nts lang-id orig-name)]
[rewrite-side-conds [rewrite-side-conds
(λ (pat) (rewrite-side-conditions/check-errs lang-nts orig-name #t pat))]) (λ (pat) (rewrite-side-conditions/check-errs lang-nts orig-name #t pat))])
(let-values ([(names names/ellipses) (extract-names lang-nts orig-name #t (syntax rhs-from))]) (with-syntax ([(side-conditions-rewritten (names ...) (names/ellipses ...))
(with-syntax ([(names ...) names] (rewrite-side-conds
[(names/ellipses ...) names/ellipses] (rewrite-node-pat (syntax-e (syntax lhs-frm-id))
[side-conditions-rewritten (rewrite-side-conds (syntax rhs-from)))]
(rewrite-node-pat (syntax-e (syntax lhs-frm-id)) [(fresh-rhs-from (fresh-names ...) (fresh-names/ellipses ...))
(syntax rhs-from)))] (rewrite-side-conds
[fresh-rhs-from (rewrite-side-conds (freshen-names #'rhs-from #'lhs-frm-id lang-nts orig-name))]
(freshen-names #'rhs-from #'lhs-frm-id lang-nts orig-name))] [lang lang])
[lang lang]) (map
(map (λ (child-proc)
(λ (child-proc) #`(do-node-match
#`(do-node-match 'lhs-frm-id
'lhs-frm-id 'lhs-to-id
'lhs-to-id `side-conditions-rewritten
`side-conditions-rewritten (λ (bindings rhs-binder)
(λ (bindings rhs-binder) (term-let ([lhs-to-id rhs-binder]
(term-let ([lhs-to-id rhs-binder] [names/ellipses (lookup-binding bindings 'names)] ...)
[names/ellipses (lookup-binding bindings 'names)] ...) (term rhs-to)))
(term rhs-to))) #,child-proc
#,child-proc `fresh-rhs-from))
`fresh-rhs-from)) (get-choices stx orig-name bm #'lang
(get-choices stx orig-name bm #'lang (syntax lhs-arrow)
(syntax lhs-arrow) name-table lang-id
name-table lang-id allow-zero-rules?))))]))
allow-zero-rules?)))))]))
(define (rewrite-node-pat id term) (define (rewrite-node-pat id term)
(let loop ([t term]) (let loop ([t term])
(syntax-case t (side-condition) (syntax-case t (side-condition)
@ -936,37 +939,37 @@
(let* ([lang-nts (language-id-nts lang-id orig-name)] (let* ([lang-nts (language-id-nts lang-id orig-name)]
[rw-sc (λ (pat) (rewrite-side-conditions/check-errs lang-nts orig-name #t pat))]) [rw-sc (λ (pat) (rewrite-side-conditions/check-errs lang-nts orig-name #t pat))])
(let-values ([(name computed-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)] (with-syntax ([(side-conditions-rewritten (names ...) (names/ellipses ...)) (rw-sc from)])
[(body-code) (define body-code
(bind-withs orig-name (bind-withs orig-name
#'main-exp #'main-exp
lang lang
lang-nts lang-nts
sides/withs/freshs sides/withs/freshs
'flatten 'flatten
#`(list (cons #,(or computed-name #'none) #`(list (cons #,(or computed-name #'none)
(term #,to))) (term #,to)))
names names/ellipses)] (syntax->list #'(names ...))
[(test-case-body-code) (syntax->list #'(names/ellipses ...))))
;; this contains some redundant code (define test-case-body-code
(bind-withs orig-name ;; this contains some redundant code
#'#t (bind-withs orig-name
#'lang-id2 #'#t
lang-nts #'lang-id2
sides/withs/freshs lang-nts
'predicate sides/withs/freshs
#'#t 'predicate
names names/ellipses)]) #'#t
(with-syntax ([side-conditions-rewritten (rw-sc from)] (syntax->list #'(names ...))
[lhs-w/extras (rw-sc #`(side-condition #,from #,test-case-body-code))] (syntax->list #'(names/ellipses ...))))
(with-syntax ([(lhs-w/extras (w/extras-names ...) (w/extras-names/ellipses ...))
(rw-sc #`(side-condition #,from #,test-case-body-code))]
[lhs-source (format "~a:~a:~a" [lhs-source (format "~a:~a:~a"
(syntax-source from) (syntax-source from)
(syntax-line from) (syntax-line from)
(syntax-column from))] (syntax-column from))]
[name name] [name name]
[lang lang] [lang lang]
[(names ...) names]
[(names/ellipses ...) names/ellipses]
[body-code body-code]) [body-code body-code])
#` #`
(build-rewrite-proc/leaf `side-conditions-rewritten (build-rewrite-proc/leaf `side-conditions-rewritten
@ -1263,13 +1266,13 @@
[(form-name lang-exp pattern) [(form-name lang-exp pattern)
(identifier? #'lang-exp) (identifier? #'lang-exp)
(let*-values ([(what) (syntax-e #'form-name)] (let*-values ([(what) (syntax-e #'form-name)]
[(nts) (language-id-nts #'lang-exp what)] [(nts) (language-id-nts #'lang-exp what)])
[(ids/depths _) (extract-names nts what #t #'pattern)]) (with-syntax ([(side-condition-rewritten (vars ...) (ids/depths ...))
(with-syntax ([side-condition-rewritten (rewrite-side-conditions/check-errs nts what #t #'pattern)] (rewrite-side-conditions/check-errs nts what #t #'pattern)])
[binders (map syntax-e ids/depths)] (with-syntax ([binders (map syntax-e (syntax->list #'(ids/depths ...)))]
[name (syntax-local-infer-name stx)]) [name (syntax-local-infer-name stx)])
(syntax (syntax
(do-test-match lang-exp `side-condition-rewritten 'binders 'name))))] (do-test-match lang-exp `side-condition-rewritten 'binders 'name)))))]
[(form-name lang-exp pattern expression) [(form-name lang-exp pattern expression)
(identifier? #'lang-exp) (identifier? #'lang-exp)
(syntax (syntax
@ -1464,7 +1467,7 @@
[codom-contracts (syntax-e #'codom-contracts)] [codom-contracts (syntax-e #'codom-contracts)]
[pats (syntax-e #'pats)] [pats (syntax-e #'pats)]
[relation? (syntax-e #'relation?)] [relation? (syntax-e #'relation?)]
[syn-error-name (syntax-e #'syn-err-name)]) [syn-error-name (syntax-e #'syn-error-name)])
(define lang-nts (define lang-nts
(definition-nts #'lang #'orig-stx syn-error-name)) (definition-nts #'lang #'orig-stx syn-error-name))
(with-syntax ([(((original-names lhs-clauses ...) raw-rhses ...) ...) pats] (with-syntax ([(((original-names lhs-clauses ...) raw-rhses ...) ...) pats]
@ -1477,8 +1480,13 @@
#'((raw-rhses ...) ...))] #'((raw-rhses ...) ...))]
[(lhs ...) #'((lhs-clauses ...) ...)]) [(lhs ...) #'((lhs-clauses ...) ...)])
(parse-extras #'((stuff ...) ...)) (parse-extras #'((stuff ...) ...))
(let-values ([(lhs-namess lhs-namess/ellipsess) (with-syntax ([((side-conditions-rewritten lhs-names lhs-namess/ellipses) ...)
(lhss-bound-names (syntax->list (syntax (lhs ...))) lang-nts syn-error-name)]) (map (λ (x) (rewrite-side-conditions/check-errs
lang-nts
syn-error-name
#t
x))
(syntax->list (syntax (lhs ...))))])
(with-syntax ([(rhs/wheres ...) (with-syntax ([(rhs/wheres ...)
(map (λ (sc/b rhs names names/ellipses) (map (λ (sc/b rhs names names/ellipses)
(bind-withs (bind-withs
@ -1486,10 +1494,12 @@
#'effective-lang lang-nts #'effective-lang lang-nts
sc/b 'flatten sc/b 'flatten
#`(list (term #,rhs)) #`(list (term #,rhs))
names names/ellipses)) (syntax->list names)
(syntax->list names/ellipses)))
(syntax->list #'((stuff ...) ...)) (syntax->list #'((stuff ...) ...))
(syntax->list #'(rhs ...)) (syntax->list #'(rhs ...))
lhs-namess lhs-namess/ellipsess)] (syntax->list #'(lhs-names ...))
(syntax->list #'(lhs-namess/ellipses ...)))]
[(rg-rhs/wheres ...) [(rg-rhs/wheres ...)
(map (λ (sc/b rhs names names/ellipses) (map (λ (sc/b rhs names names/ellipses)
(bind-withs (bind-withs
@ -1497,18 +1507,13 @@
#'effective-lang lang-nts #'effective-lang lang-nts
sc/b 'predicate sc/b 'predicate
#`#t #`#t
names names/ellipses)) (syntax->list names)
(syntax->list names/ellipses)))
(syntax->list #'((stuff ...) ...)) (syntax->list #'((stuff ...) ...))
(syntax->list #'(rhs ...)) (syntax->list #'(rhs ...))
lhs-namess lhs-namess/ellipsess)]) (syntax->list #'(lhs-names ...))
(with-syntax ([(side-conditions-rewritten ...) (syntax->list #'(lhs-namess/ellipses ...)))])
(map (λ (x) (rewrite-side-conditions/check-errs (with-syntax ([((rg-side-conditions-rewritten rg-names rg-names/ellipses ...) ...)
lang-nts
syn-error-name
#t
x))
(syntax->list (syntax (lhs ...))))]
[(rg-side-conditions-rewritten ...)
(map (λ (x) (rewrite-side-conditions/check-errs (map (λ (x) (rewrite-side-conditions/check-errs
lang-nts lang-nts
syn-error-name syn-error-name
@ -1522,14 +1527,15 @@
(syntax-line lhs) (syntax-line lhs)
(syntax-column lhs))) (syntax-column lhs)))
pats)] pats)]
[dom-side-conditions-rewritten [(dom-side-conditions-rewritten dom-names dom-names/ellipses)
(and dom-ctcs (if dom-ctcs
(rewrite-side-conditions/check-errs (rewrite-side-conditions/check-errs
lang-nts lang-nts
syn-error-name syn-error-name
#f #f
dom-ctcs))] dom-ctcs)
[(codom-side-conditions-rewritten ...) #'(any () ()))]
[((codom-side-conditions-rewritten codom-names codom-names/ellipses) ...)
(map (λ (codom-contract) (map (λ (codom-contract)
(rewrite-side-conditions/check-errs (rewrite-side-conditions/check-errs
lang-nts lang-nts
@ -1547,7 +1553,8 @@
(term-let-fn ((name name)) (term-let-fn ((name name))
(term-let ([names/ellipses (lookup-binding bindings 'names)] ...) (term-let ([names/ellipses (lookup-binding bindings 'names)] ...)
rhs/where)))))) rhs/where))))))
lhs-namess lhs-namess/ellipsess (syntax->list #'(lhs-names ...))
(syntax->list #'(lhs-namess/ellipses ...))
(syntax->list (syntax (rhs/wheres ...))))]) (syntax->list (syntax (rhs/wheres ...))))])
(syntax-property (syntax-property
(prune-syntax (prune-syntax
@ -1587,7 +1594,7 @@
dsc dsc
(append cases parent-cases) (append cases parent-cases)
#,relation?)) #,relation?))
dsc #,(if dom-ctcs #'dsc #f)
`(codom-side-conditions-rewritten ...) `(codom-side-conditions-rewritten ...)
'name 'name
#,relation?)))) #,relation?))))
@ -1680,17 +1687,6 @@
(raise-syntax-error (raise-syntax-error
#f "mode and contract specify different numbers of positions" full-def))) #f "mode and contract specify different numbers of positions" full-def)))
(define-for-syntax (lhss-bound-names lhss nts syn-error-name)
(let loop ([lhss lhss])
(if (null? lhss)
(values null null)
(let-values ([(namess namess/ellipsess)
(loop (cdr lhss))]
[(names names/ellipses)
(extract-names nts syn-error-name #t (car lhss))])
(values (cons names namess)
(cons names/ellipses namess/ellipsess))))))
(define-for-syntax (defined-name declared-names clauses orig-stx) (define-for-syntax (defined-name declared-names clauses orig-stx)
(with-syntax ([(((used-names _ ...) _ ...) ...) clauses]) (with-syntax ([(((used-names _ ...) _ ...) ...) clauses])
(define-values (the-name other-names) (define-values (the-name other-names)
@ -1892,26 +1888,30 @@
(syntax-case clause () (syntax-case clause ()
[((_ . conc-pats) . prems) [((_ . conc-pats) . prems)
(let-values ([(input-pats output-pats) (split-by-mode (syntax->list #'conc-pats) mode)]) (let-values ([(input-pats output-pats) (split-by-mode (syntax->list #'conc-pats) mode)])
(define-values (input-names input-names/ellipses)
(extract-names nts syn-error-name #t input-pats))
(define ((rewrite-pattern binds?) pat) (define ((rewrite-pattern binds?) pat)
(rewrite-side-conditions/check-errs nts syn-error-name binds? pat)) (rewrite-side-conditions/check-errs nts syn-error-name binds? pat))
(define (contracts-compilation ctcs) (with-syntax ([(lhs (names ...) (names/ellipses ...)) ((rewrite-pattern #t) input-pats)])
(and ctcs #`(map (λ (p) (compile-pattern #,lang p #f)) `#,ctcs))) (define (contracts-compilation ctcs)
(define-values (input-contracts output-contracts) (and ctcs
(syntax-case contracts () (with-syntax ([(ctc ...) ctcs])
[#f (values #f #f)] #`(list (compile-pattern #,lang `ctc #f) ...))))
[(p ...) (define-values (input-contracts output-contracts)
(let-values ([(ins outs) (split-by-mode (syntax->list #'(p ...)) mode)]) (syntax-case contracts ()
(values (map (rewrite-pattern #f) ins) [#f (values #f #f)]
(map (rewrite-pattern #f) outs)))])) [(p ...)
(define lhs (map (rewrite-pattern #t) input-pats)) (let-values ([(ins outs) (split-by-mode (syntax->list #'(p ...)) mode)])
(define body (with-syntax ([((in-pat in-names in-names/ellipses) ...)
(bind-withs syn-error-name '() lang nts (syntax->list #'prems) (map (rewrite-pattern #f) ins)]
'flatten #`(list (term (#,@output-pats))) input-names input-names/ellipses)) [((out-pat out-names out-names/ellipses) ...)
(with-syntax ([(names ...) input-names] (map (rewrite-pattern #f) outs)])
[(names/ellipses ...) input-names/ellipses]) (values #'(in-pat ...)
#`(let ([compiled-lhs (compile-pattern #,lang `#,lhs #t)] #'(out-pat ...))))]))
(define body
(bind-withs syn-error-name '() lang nts (syntax->list #'prems)
'flatten #`(list (term (#,@output-pats)))
(syntax->list #'(names ...))
(syntax->list #'(names/ellipses ...))))
#`(let ([compiled-lhs (compile-pattern #,lang `lhs #t)]
[compiled-input-ctcs #,(contracts-compilation input-contracts)] [compiled-input-ctcs #,(contracts-compilation input-contracts)]
[compiled-output-ctcs #,(contracts-compilation output-contracts)]) [compiled-output-ctcs #,(contracts-compilation output-contracts)])
(λ (input) (λ (input)
@ -2392,7 +2392,7 @@
(prune-syntax (prune-syntax
(let () (let ()
(let ([all-names (syntax->list #'(all-names ...))]) (let ([all-names (syntax->list #'(all-names ...))])
(with-syntax ([((r-rhs ...) ...) (with-syntax ([(((r-rhs r-names r-names/ellipses) ...) ...)
(map (lambda (rhss) (map (lambda (rhss)
(map (lambda (rhs) (map (lambda (rhs)
(rewrite-side-conditions/check-errs (rewrite-side-conditions/check-errs
@ -2450,7 +2450,7 @@
(begin (void) refs ...)) (begin (void) refs ...))
(compile-language (list (list '(uniform-names ...) rhs/lw ...) ...) (compile-language (list (list '(uniform-names ...) rhs/lw ...) ...)
(list (make-nt 'first-names (list (make-rhs `r-rhs) ...)) ... (list (make-nt 'first-names (list (make-rhs `r-rhs) ...)) ...
(make-nt 'new-name (list (make-rhs 'orig-name))) ...) (make-nt 'new-name (list (make-rhs '(nt orig-name)))) ...)
'((uniform-names ...) ...)))))))))])) '((uniform-names ...) ...)))))))))]))
(define-syntax (define-extended-language stx) (define-syntax (define-extended-language stx)
@ -2483,31 +2483,21 @@
(define-syntax (extend-language stx) (define-syntax (extend-language stx)
(syntax-case stx () (syntax-case stx ()
[(_ lang (all-names ...) (name rhs ...) ...) [(_ lang (all-names ...) (name rhs ...) ...)
(with-syntax ([((r-rhs ...) ...) (map (lambda (rhss) (map (λ (x) (rewrite-side-conditions/check-errs (with-syntax ([(((r-rhs r-names r-names/ellipses) ...) ...)
(append (language-id-nts #'lang 'define-extended-language) (map (lambda (rhss) (map (λ (x) (rewrite-side-conditions/check-errs
(map syntax-e (append (language-id-nts #'lang 'define-extended-language)
(syntax->list #'(all-names ...)))) (map syntax-e
'define-extended-language (syntax->list #'(all-names ...))))
#f 'define-extended-language
x)) #f
(syntax->list rhss))) x))
(syntax->list (syntax ((rhs ...) ...))))] (syntax->list rhss)))
(syntax->list (syntax ((rhs ...) ...))))]
[((rhs/lw ...) ...) (map (lambda (rhss) (map to-lw/proc (syntax->list rhss))) [((rhs/lw ...) ...) (map (lambda (rhss) (map to-lw/proc (syntax->list rhss)))
(syntax->list (syntax ((rhs ...) ...))))] (syntax->list (syntax ((rhs ...) ...))))]
[((uniform-names ...) ...) [((uniform-names ...) ...)
(map (λ (x) (if (identifier? x) (list x) x)) (map (λ (x) (if (identifier? x) (list x) x))
(syntax->list (syntax (name ...))))] (syntax->list (syntax (name ...))))])
[((new-name orig-name) ...)
(apply
append
(map (λ (name-stx)
(if (identifier? name-stx)
'()
(let ([l (syntax->list name-stx)])
(map (λ (x) (list x (car l)))
(cdr l)))))
(syntax->list #'(name ...))))])
(syntax/loc stx (syntax/loc stx
(do-extend-language lang (do-extend-language lang
(list (make-nt '(uniform-names ...) (list (make-rhs `r-rhs) ...)) ...) (list (make-nt '(uniform-names ...) (list (make-rhs `r-rhs) ...)) ...)
@ -2587,7 +2577,7 @@
(for-each (λ (shortcut-name) (for-each (λ (shortcut-name)
(hash-set! new-ht (hash-set! new-ht
shortcut-name shortcut-name
(make-nt shortcut-name (list (make-rhs (car names)))))) (make-nt shortcut-name (list (make-rhs `(nt ,(car names)))))))
(cdr names))))) (cdr names)))))
new-nts) new-nts)

407
collects/redex/private/rewrite-side-conditions.rkt
View File

@ -1,7 +1,9 @@
(module rewrite-side-conditions scheme #lang racket/base
(require mzlib/list (require mzlib/list
"underscore-allowed.rkt") "underscore-allowed.rkt")
(require (for-template (require "term.rkt"
(for-template
mzscheme mzscheme
"term.rkt" "term.rkt"
"matcher.rkt")) "matcher.rkt"))
@ -36,91 +38,310 @@
stx)) stx))
(define (expected-arguments name stx) (define (expected-arguments name stx)
(raise-syntax-error what (format "~a expected to have arguments" name) orig-stx stx)) (raise-syntax-error what (format "~a expected to have arguments" name) orig-stx stx))
(define ((expect-identifier src) stx) (define (expect-identifier src stx)
(unless (identifier? stx) (unless (identifier? stx)
(raise-syntax-error what "expected an identifier" src stx))) (raise-syntax-error what "expected an identifier" src stx)))
;; call this and discard the result to ensure that all names are at the right ellipsis depths. ; union-find w/o balancing or path compression (at least for now)
(extract-names all-nts what bind-names? orig-stx) (define (union e f sets)
(hash-set sets (find f sets) (find e sets)))
(define (find e sets)
(let recur ([chd e] [par (hash-ref sets e #f)])
(if (and par (not (eq? chd par))) (recur par (hash-ref sets par #f)) chd)))
(let loop ([term orig-stx]) (define last-contexts (make-hasheq))
(syntax-case term (side-condition variable-except variable-prefix hole name in-hole hide-hole cross unquote and) (define assignments #hasheq())
[(side-condition pre-pat (and)) (define (record-binder pat-stx under)
;; rewriting metafunctions (and possibly other things) that have no where, etc clauses (define pat-sym (syntax->datum pat-stx))
;; end up with side-conditions that are empty 'and' expressions, so we just toss them here. (set! assignments
(loop #'pre-pat)] (if (null? under)
[(side-condition pre-pat exp) assignments
(with-syntax ([pat (loop (syntax pre-pat))]) (let ([last (hash-ref last-contexts pat-sym #f)])
(let-values ([(names names/ellipses) (extract-names all-nts what bind-names? (syntax pat))]) (if last
(with-syntax ([(name ...) names] (foldl (λ (cur last asgns) (union cur last asgns)) assignments under last)
[(name/ellipses ...) names/ellipses] (begin
(hash-set! last-contexts pat-sym under)
assignments))))))
(define ellipsis-number 0)
(define-values (term names)
(let loop ([term orig-stx]
[under '()])
(syntax-case term (side-condition variable-except variable-prefix hole name in-hole hide-hole cross unquote and)
[(side-condition pre-pat (and))
;; rewriting metafunctions (and possibly other things) that have no where, etc clauses
;; end up with side-conditions that are empty 'and' expressions, so we just toss them here.
(loop #'pre-pat under)]
[(side-condition pre-pat exp)
(let ()
(define-values (pre-term pre-vars) (loop #'pre-pat under))
(define names/ellipses (map build-dots pre-vars))
(with-syntax ([pre-term pre-term]
[((name name/ellipses) ...)
(filter
values
(map (λ (id name/ellipses)
(if (id/depth-mismatch? id)
#f
(list (id/depth-id id)
name/ellipses)))
pre-vars
names/ellipses))]
[src-loc (parameterize ([print-syntax-width 0]) [src-loc (parameterize ([print-syntax-width 0])
(format "~s" #'exp))]) (format "~s" #'exp))])
(syntax/loc term (values (syntax/loc term
(side-condition (side-condition
pat pre-term
,(lambda (bindings) ,(lambda (bindings)
(term-let (term-let
([name/ellipses (lookup-binding bindings 'name)] ...) ([name/ellipses (lookup-binding bindings 'name)] ...)
exp)) exp))
; For use in error messages. ; For use in error messages.
src-loc)))))] src-loc))
[(side-condition a ...) (expected-exact 'side-condition 2 term)] pre-vars)))]
[side-condition (expected-arguments 'side-condition term)] [(side-condition a ...) (expected-exact 'side-condition 2 term)]
[(variable-except a ...) [side-condition (expected-arguments 'side-condition term)]
(for-each (expect-identifier term) (syntax->list #'(a ...))) [(variable-except a ...)
term] (begin
[variable-except (expected-arguments 'variable-except term)] (for ([a (in-list (syntax->list #'(a ...)))])
[(variable-prefix a) (expect-identifier term a))
((expect-identifier term) #'a) (values term '()))]
term] [variable-except (expected-arguments 'variable-except term)]
[(variable-prefix a ...) (expected-exact 'variable-prefix 1 term)] [(variable-prefix a)
[variable-prefix (expected-arguments 'variable-prefix term)] (begin
[hole term] (expect-identifier term #'a)
[(name x y) #`(name x #,(loop #'y))] (values term '()))]
[(name x ...) (expected-exact 'name 2 term)] [(variable-prefix a ...) (expected-exact 'variable-prefix 1 term)]
[name (expected-arguments 'name term)] [variable-prefix (expected-arguments 'variable-prefix term)]
[(in-hole a b) #`(in-hole #,(loop #'a) #,(loop #'b))] [hole (values term '())]
[(in-hole a ...) (expected-exact 'in-hole 2 term)] [(name x y)
[in-hole (expected-arguments 'in-hole term)] (let ()
[(hide-hole a) #`(hide-hole #,(loop #'a))] (define-values (sub-term sub-vars) (loop #'y under))
[(hide-hole a ...) (expected-exact 'hide-hole 1 term)] (record-binder #'x under)
[hide-hole (expected-arguments 'hide-hole term)] (values #`(name x #,sub-term)
[(cross a) (cons (make-id/depth #'x (length under) #f)
((expect-identifier term) #'a) sub-vars)))]
term] [(name x ...) (expected-exact 'name 2 term)]
[(cross a ...) (expected-exact 'cross 1 term)] [name (expected-arguments 'name term)]
[cross (expected-arguments 'cross term)] [(in-hole a b)
[(unquote . _) (let ()
(raise-syntax-error what "unquote disallowed in patterns" orig-stx term)] (define-values (a-term a-vars) (loop #'a under))
[_ (define-values (b-term b-vars) (loop #'b under))
(identifier? term) (values #`(in-hole #,a-term #,b-term)
(match (regexp-match #rx"^([^_]*)_.*" (symbol->string (syntax-e term))) (append a-vars b-vars)))]
[(list _ (app string->symbol s)) [(in-hole a ...) (expected-exact 'in-hole 2 term)]
(if (or (memq s (cons '... underscore-allowed)) [in-hole (expected-arguments 'in-hole term)]
(memq s all-nts)) [(hide-hole a)
term (let ()
(define-values (sub-term vars) (loop #'a under))
(values #`(hide-hole #,sub-term) vars))]
[(hide-hole a ...) (expected-exact 'hide-hole 1 term)]
[hide-hole (expected-arguments 'hide-hole term)]
[(cross a)
(let ()
(expect-identifier term #'a)
(define a-str (symbol->string (syntax-e #'a)))
(values #`(cross #,(string->symbol (format "~a-~a" a-str a-str)))
'()))]
[(cross a ...) (expected-exact 'cross 1 term)]
[cross (expected-arguments 'cross term)]
[(unquote . _)
(raise-syntax-error what "unquote disallowed in patterns" orig-stx term)]
[_
(identifier? term)
(let ()
(define m (regexp-match #rx"^([^_]*)_(.*)$" (symbol->string (syntax-e term))))
(cond
[m
(define prefix (list-ref m 1))
(define suffix (list-ref m 2))
(define suffix-sym (string->symbol suffix))
(define prefix-sym (string->symbol prefix))
(define prefix-stx (datum->syntax term prefix-sym))
(define mismatch? (regexp-match? #rx"^!_" suffix))
(cond
[(eq? prefix-sym '...)
(raise-syntax-error
what
"found an ellipsis outside of a sequence"
orig-stx
term)]
[(memq prefix-sym all-nts)
(record-binder term under)
(values (if mismatch?
`(mismatch-name ,term (nt ,prefix-stx))
`(name ,term (nt ,prefix-stx)))
(list (make-id/depth term (length under) mismatch?)))]
[(memq prefix-sym underscore-allowed)
(record-binder term under)
(values (if mismatch?
`(mismatch-name ,term ,prefix-stx)
`(name ,term ,prefix-stx))
(list (make-id/depth term (length under) mismatch?)))]
[else
(raise-syntax-error
what
(format "before underscore must be either a non-terminal or a built-in pattern, found ~a in ~s"
suffix-sym (syntax-e term))
orig-stx
term)])]
[(eq? (syntax-e term) '...)
(raise-syntax-error (raise-syntax-error
what what
(format "before underscore must be either a non-terminal or a built-in pattern, found ~a in ~s" "found an ellipsis outside of a sequence"
s (syntax-e term))
orig-stx orig-stx
term))] term)]
[_ term])] [(memq (syntax-e term) all-nts)
[(terms ...) (cond
(map loop (syntax->list (syntax (terms ...))))] [bind-names?
[else (record-binder term under)
(when (pair? (syntax-e term)) (values `(name ,term (nt ,term)) (list (make-id/depth term (length under) #f)))]
(let loop ([term term]) [else
(cond (values `(nt ,term) '())])]
[(syntax? term) (loop (syntax-e term))] [(memq (syntax-e term) underscore-allowed)
[(pair? term) (loop (cdr term))] (cond
[(null? term) (void)] [bind-names?
[#t (record-binder #'term under)
(raise-syntax-error what "dotted pairs not supported in patterns" orig-stx term)]))) (values `(name ,term ,term) (list (make-id/depth term (length under) #f)))]
term]))) [else
(values term '())])]
[else
(values term '())]))]
[(terms ...)
(let ()
(define terms-lst (syntax->list #'(terms ...)))
(define (is-ellipsis? term)
(and (identifier? term)
(regexp-match? #rx"^[.][.][.]" (symbol->string (syntax-e term)))))
(when (and (pair? terms-lst) (is-ellipsis? (car terms-lst)))
(raise-syntax-error what
"ellipsis should not appear in the first position of a sequence"
orig-stx
term))
(define-values (updated-terms vars)
(let t-loop ([terms terms-lst])
(cond
[(null? terms) (values '() '())]
[(null? (cdr terms))
(define-values (term vars) (loop (car terms) under))
(values (list term) vars)]
[(is-ellipsis? (cadr terms))
(when (and (pair? (cddr terms))
(is-ellipsis? (caddr terms)))
(raise-syntax-error what
"two ellipses should not appear in a row"
orig-stx
(cadr terms)
(list (caddr terms))))
(define ellipsis-sym (syntax-e (cadr terms)))
(define ellipsis-pre-str (symbol->string ellipsis-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 ellipsis+name (datum->syntax
(cadr terms)
(string->symbol ellipsis-str)
(cadr terms)))
(record-binder ellipsis+name under)
(define-values (fst-term fst-vars)
(loop (car terms) (cons (syntax-e ellipsis+name) under)))
(define-values (rst-terms rst-vars) (t-loop (cddr terms)))
(values (cons `(repeat ,fst-term
,ellipsis+name
,(if mismatch? (cadr terms) #f))
rst-terms)
(append fst-vars rst-vars))]
[else
(define-values (fst-term fst-vars) (loop (car terms) under))
(define-values (rst-terms rst-vars) (t-loop (cdr terms)))
(values (cons fst-term rst-terms)
(append fst-vars rst-vars))])))
(values `(list ,@updated-terms) vars))]
[else
(when (pair? (syntax-e term))
(let loop ([term term])
(cond
[(syntax? term) (loop (syntax-e term))]
[(pair? term) (loop (cdr term))]
[(null? term) (void)]
[#t
(raise-syntax-error what "dotted pairs not supported in patterns" orig-stx term)])))
(values term '())])))
(define-struct id/depth (id depth)) (define closed-table
(make-immutable-hasheq (hash-map assignments (λ (cls _) (cons cls (find cls assignments))))))
(define repeat-id-counts (make-hash))
(define ellipsis-normalized
(let loop ([pat term])
(syntax-case pat (repeat)
[(repeat sub-pat name mismatch-name)
(let ()
(define mapped-name (hash-ref closed-table (syntax-e #'name) #f))
(define new-name (if mapped-name
mapped-name
(syntax-e #'name)))
(hash-set! repeat-id-counts new-name (+ 1 (hash-ref repeat-id-counts new-name 0)))
(let ([id (syntax-e #'mismatch-name)])
(when id
(hash-set! repeat-id-counts id (+ 1 (hash-ref repeat-id-counts id 0)))))
#`(repeat #,(loop #'sub-pat) #,new-name mismatch-name))]
[(a ...)
(let ()
(define new (map loop (syntax->list #'(a ...))))
(if (syntax? pat)
(datum->syntax pat new pat)
new))]
[_ pat])))
;(printf "term ~s\n" (syntax->datum (datum->syntax #'here term)))
;(printf "norm ~s\n" (syntax->datum (datum->syntax #'here ellipsis-normalized)))
;(printf "repeat-id-counts ~s\n" repeat-id-counts)
(define ellipsis-normalized/simplified
(let loop ([pat ellipsis-normalized])
(syntax-case pat (repeat)
[(repeat sub-pat name mismatch-name)
(let ()
#`(repeat #,(loop #'sub-pat)
#,(if (= 1 (hash-ref repeat-id-counts (syntax-e #'name)))
#f
#'name)
#,(if (and (syntax-e #'mismatch-name)
(= 1 (hash-ref repeat-id-counts (syntax-e #'mismatch-name))))
#f
#'mismatch-name)))]
[(a ...)
(let ()
(define new (map loop (syntax->list #'(a ...))))
(if (syntax? pat)
(datum->syntax pat new pat)
new))]
[_ pat])))
(filter-duplicates what orig-stx names)
(let ([without-mismatch-names (filter (λ (x) (not (id/depth-mismatch? x))) names)])
(with-syntax ([(name/ellipses ...) (map build-dots without-mismatch-names)]
[(name ...) (map id/depth-id without-mismatch-names)]
[term ellipsis-normalized/simplified])
#'(term (name ...) (name/ellipses ...)))))
(define-struct id/depth (id depth mismatch?))
;; extract-names : syntax syntax -> (values (listof syntax) (listof syntax[x | (x ...) | ((x ...) ...) | ...])) ;; extract-names : syntax syntax -> (values (listof syntax) (listof syntax[x | (x ...) | ((x ...) ...) | ...]))
(define (extract-names all-nts what bind-names? orig-stx [mode 'rhs-only]) (define (extract-names all-nts what bind-names? orig-stx [mode 'rhs-only])
@ -128,11 +349,11 @@
(let loop ([stx orig-stx] (let loop ([stx orig-stx]
[names null] [names null]
[depth 0]) [depth 0])
(syntax-case stx (name in-hole side-condition cross) (syntax-case stx (name in-hole side-condition cross nt)
[(name sym pat) [(name sym pat)
(identifier? (syntax sym)) (identifier? (syntax sym))
(loop (syntax pat) (loop (syntax pat)
(cons (make-id/depth (syntax sym) depth) names) (cons (make-id/depth (syntax sym) depth #f) names)
depth)] depth)]
[(in-hole pat1 pat2) [(in-hole pat1 pat2)
(loop (syntax pat1) (loop (syntax pat1)
@ -163,7 +384,7 @@
[(rhs-only) binds-in-right-hand-side?] [(rhs-only) binds-in-right-hand-side?]
[(binds-anywhere) binds?]) [(binds-anywhere) binds?])
all-nts bind-names? (syntax x))) all-nts bind-names? (syntax x)))
(cons (make-id/depth (syntax x) depth) names)] (cons (make-id/depth (syntax x) depth #f) names)]
[else names]))] [else names]))]
[no-dups (filter-duplicates what orig-stx dups)]) [no-dups (filter-duplicates what orig-stx dups)])
(values (map id/depth-id no-dups) (values (map id/depth-id no-dups)
@ -189,16 +410,16 @@
(and (not (regexp-match #rx"^\\.\\.\\._" str)) (and (not (regexp-match #rx"^\\.\\.\\._" str))
(not (regexp-match #rx"_!_" str)))))) (not (regexp-match #rx"_!_" str))))))
(define (raise-ellipsis-depth-error what one-binder one-depth another-binder another-depth) (define (raise-ellipsis-depth-error what one-binder one-depth another-binder another-depth [orig-stx #f])
(raise (raise-syntax-error
(make-exn:fail:syntax what
(format "~a: found the same binder, ~s, at different depths, ~a and ~a" (format "found the same binder, ~s, at different depths, ~a and ~a"
what (syntax->datum one-binder)
(syntax->datum one-binder) one-depth
one-depth another-depth)
another-depth) orig-stx
(current-continuation-marks) another-binder
(list one-binder another-binder)))) (list one-binder)))
(define (filter-duplicates what orig-stx dups) (define (filter-duplicates what orig-stx dups)
(let loop ([dups dups]) (let loop ([dups dups])
@ -216,6 +437,8 @@
(raise-ellipsis-depth-error (raise-ellipsis-depth-error
what what
(id/depth-id x) (id/depth-depth x) (id/depth-id x) (id/depth-depth x)
(id/depth-id (car dups)) (id/depth-depth (car dups))))) (id/depth-id (car dups)) (id/depth-depth (car dups))
orig-stx)))
(not same-id?))) (not same-id?)))
(loop (cdr dups))))])))) (loop (cdr dups))))])))

424
collects/redex/private/rg.rkt
View File

@ -6,6 +6,7 @@
"term.rkt" "term.rkt"
"error.rkt" "error.rkt"
"struct.rkt" "struct.rkt"
"match-a-pattern.rkt"
(for-syntax racket/base (for-syntax racket/base
"rewrite-side-conditions.rkt" "rewrite-side-conditions.rkt"
"term-fn.rkt" "term-fn.rkt"
@ -159,8 +160,9 @@
(define-struct rg-lang (non-cross delayed-cross base-cases)) (define-struct rg-lang (non-cross delayed-cross base-cases))
(define (rg-lang-cross x) (force (rg-lang-delayed-cross x))) (define (rg-lang-cross x) (force (rg-lang-delayed-cross x)))
(define (prepare-lang lang) (define (prepare-lang lang)
(let ([parsed (parse-language lang)]) (values lang
(values parsed (map symbol->string (compiled-lang-literals lang)) (find-base-cases parsed)))) (map symbol->string (compiled-lang-literals lang))
(find-base-cases lang)))
(define-struct (exn:fail:redex:generation-failure exn:fail:redex) ()) (define-struct (exn:fail:redex:generation-failure exn:fail:redex) ())
(define (raise-gen-fail who what attempts) (define (raise-gen-fail who what attempts)
@ -198,7 +200,7 @@
[size init-sz] [size init-sz]
[attempt init-att]) [attempt init-att])
(if (zero? remaining) (if (zero? remaining)
(raise-gen-fail what (format "pattern ~a" name) retries) (raise-gen-fail what (format "pattern ~s" name) retries)
(let-values ([(term env) (gen size attempt)]) (let-values ([(term env) (gen size attempt)])
(if (pred term env) (if (pred term env)
(values term env) (values term env)
@ -210,13 +212,16 @@
pre-threshold-incr)))))))) pre-threshold-incr))))))))
(define (generate/prior name env gen) (define (generate/prior name env gen)
;(printf "generate/prior ~s ~s ~s\n" name env gen)
(let* ([none (gensym)] (let* ([none (gensym)]
[prior (hash-ref env name none)]) [prior (hash-ref env name none)])
(if (eq? prior none) (if (eq? prior none)
(let-values ([(term env) (gen)]) (let-values ([(term env) (gen)])
;(printf "generated ~s for ~s\n" term name)
(values term (hash-set env name term))) (values term (hash-set env name term)))
(values prior env)))) (values prior env))))
(define (generate-sequence gen env vars length) (define (generate-sequence gen env vars length)
(define (split-environment env) (define (split-environment env)
(foldl (λ (var seq-envs) (foldl (λ (var seq-envs)
@ -252,7 +257,7 @@
vals)))) vals))))
(for/and ([(name val) env]) (for/and ([(name val) env])
(or (not (mismatch? name)) (or (not (mismatch? name))
(let ([prior (get-group (mismatch-group name))]) (let ([prior (get-group (mismatch-var name))])
(and (not (hash-ref prior val #f)) (and (not (hash-ref prior val #f))
(hash-set! prior val #t)))))) (hash-set! prior val #t))))))
@ -261,8 +266,8 @@
(define (bindings env) (define (bindings env)
(make-bindings (make-bindings
(for/fold ([bindings null]) ([(key val) env]) (for/fold ([bindings null]) ([(key val) env])
(if (binder? key) (if (symbol? key)
(cons (make-bind (binder-name key) val) bindings) (cons (make-bind key val) bindings)
bindings)))) bindings))))
(define-values (langp lits lang-bases) (prepare-lang lang)) (define-values (langp lits lang-bases) (prepare-lang lang))
@ -270,6 +275,73 @@
(define lit-syms (compiled-lang-literals lang)) (define lit-syms (compiled-lang-literals lang))
(define (compile pat any?) (define (compile pat any?)
(define vars-table (make-hash))
(define (find-vars pat) (hash-ref vars-table pat '()))
(define mismatch-id 0)
(define-values (rewritten-pat vars)
(let loop ([pat pat])
(define (add/ret pat vars)
(hash-set! vars-table pat vars)
(values pat vars))
(define (build-mismatch var)
(set! mismatch-id (+ mismatch-id 1))
(make-mismatch mismatch-id var))
(match-a-pattern pat
[`any (values pat '())]
[`number (values pat '())]
[`string (values pat '())]
[`natural (values pat '())]
[`integer (values pat '())]
[`real (values pat '())]
[`variable (values pat '())]
[`(variable-except ,vars ...) (values pat '())]
[`(variable-prefix ,var) (values pat '())]
[`variable-not-otherwise-mentioned (values pat '())]
[`hole (values pat '())]
[`(nt ,x) (values pat '())]
[`(name ,name ,p)
(define-values (p-rewritten p-names) (loop p))
(add/ret `(name ,name ,p-rewritten) (cons name p-names))]
[`(mismatch-name ,name ,p)
(define mm (build-mismatch name))
(define-values (p-rewritten p-names) (loop p))
(add/ret `(mismatch-name ,mm ,p-rewritten)
(cons mm p-names))]
[`(in-hole ,p1 ,p2)
(define-values (p1-rewritten p1-names) (loop p1))
(define-values (p2-rewritten p2-names) (loop p2))
(add/ret `(in-hole ,p1-rewritten ,p2-rewritten)
(append p1-names p2-names))]
[`(hide-hole ,p)
(define-values (p-rewritten p-names) (loop p))
(add/ret `(hide-hole ,p-rewritten) p-names)]
[`(side-condition ,p ,e ,e2)
(define-values (p-rewritten p-names) (loop p))
(add/ret `(side-condition ,p-rewritten ,e ,e2) p-names)]
[`(cross ,var) (values pat '())]
[`(list ,lpats ...)
(define-values (lpats-rewritten vars)
(for/fold ([ps-rewritten '()]
[vars '()])
([lpat (in-list lpats)])
(match lpat
[`(repeat ,p ,name ,mismatch-name)
(define l1 (if name (list name) '()))
(define mm (and mismatch-name
(build-mismatch mismatch-name)))
(define l2 (if mm (cons mm l1) l1))
(define-values (p-rewritten p-vars) (loop p))
(values (cons `(repeat ,p-rewritten ,name ,mm) ps-rewritten)
(append l2 p-vars vars))]
[_
(define-values (p-rewritten p-vars) (loop lpat))
(values (cons p-rewritten ps-rewritten)
(append p-vars vars))])))
(add/ret `(list ,@(reverse lpats-rewritten))
vars)]
[(? (compose not pair?)) (values pat '())])))
(let* ([nt? (is-nt? (if any? sexpp langp))] (let* ([nt? (is-nt? (if any? sexpp langp))]
[mismatches? #f] [mismatches? #f]
[generator [generator
@ -291,12 +363,19 @@
; (W hole ; (W hole
; ; extra parens to avoid matcher loop ; ; extra parens to avoid matcher loop
; (in-hole (W_1) (+ natural hole)))) ; (in-hole (W_1) (+ natural hole))))
(let recur ([pat pat]) (let recur ([pat rewritten-pat])
(match pat (match-a-pattern pat
[`any
(λ (r s a e f)
(let*-values ([(lang nt) ((next-any-decision) langc sexpc)]
[(term) (gen-nt lang nt #f r s a the-not-hole)])
(values term e)))]
[`number (generator/attempts (λ (a) ((next-number-decision) a)))] [`number (generator/attempts (λ (a) ((next-number-decision) a)))]
[`string (generator/attempts (λ (a) ((next-string-decision) lits a)))]
[`natural (generator/attempts (λ (a) ((next-natural-decision) a)))] [`natural (generator/attempts (λ (a) ((next-natural-decision) a)))]
[`integer (generator/attempts (λ (a) ((next-integer-decision) a)))] [`integer (generator/attempts (λ (a) ((next-integer-decision) a)))]
[`real (generator/attempts (λ (a) ((next-real-decision) a)))] [`real (generator/attempts (λ (a) ((next-real-decision) a)))]
[`variable (generator/attempts (λ (a) ((next-variable-decision) lits a)))]
[`(variable-except ,vars ...) [`(variable-except ,vars ...)
(let ([g (recur 'variable)]) (let ([g (recur 'variable)])
(λ (r s a e f) (λ (r s a e f)
@ -304,14 +383,6 @@
(λ (s a) (g r s a e f)) (λ (s a) (g r s a e f))
(λ (var _) (not (memq var vars))) (λ (var _) (not (memq var vars)))
s a r)))] s a r)))]
[`variable (generator/attempts (λ (a) ((next-variable-decision) lits a)))]
[`variable-not-otherwise-mentioned
(let ([g (recur 'variable)])
(λ (r s a e f)
(generate/pred pat
(λ (s a) (g r s a e f))
(λ (var _) (not (memq var lit-syms)))
s a r)))]
[`(variable-prefix ,prefix) [`(variable-prefix ,prefix)
(define (symbol-append prefix suffix) (define (symbol-append prefix suffix)
(string->symbol (string-append (symbol->string prefix) (symbol->string suffix)))) (string->symbol (string-append (symbol->string prefix) (symbol->string suffix))))
@ -319,20 +390,27 @@
(λ (r s a e f) (λ (r s a e f)
(let-values ([(t e) (g r s a e f)]) (let-values ([(t e) (g r s a e f)])
(values (symbol-append prefix t) e))))] (values (symbol-append prefix t) e))))]
[`string (generator/attempts (λ (a) ((next-string-decision) lits a)))] [`variable-not-otherwise-mentioned
[`(side-condition ,pat ,(? procedure? condition) ,guard-src-loc) (let ([g (recur 'variable)])
(let ([g (recur pat)])
(λ (r s a e f) (λ (r s a e f)
(generate/pred `(side-condition ,(unparse-pattern pat) ,guard-src-loc) (generate/pred pat
(λ (s a) (g r s a e f)) (λ (s a) (g r s a e f))
(λ (_ env) (condition (bindings env))) (λ (var _) (not (memq var lit-syms)))
s a r)))] s a r)))]
[`(name ,(? symbol? id) ,p) [`hole (λ (r s a e f) (values f e))]
[`(nt ,nt-id)
(λ (r s a e f)
(values (gen-nt (if any? sexpc langc) nt-id #f r s a f) e))]
[`(name ,id ,p)
(let ([g (recur p)]) (let ([g (recur p)])
(λ (r s a e f) (λ (r s a e f)
(let-values ([(t env) (g r s a e f)]) (generate/prior id e (λ () (g r s a e f)))))]
(values t (hash-set env (make-binder id) t)))))] [`(mismatch-name ,id ,pat)
[`hole (λ (r s a e f) (values f e))] (let ([g (recur pat)])
(set! mismatches? #t)
(λ (r s a e f)
(let-values ([(t e) (g r s a e f)])
(values t (hash-set e id t)))))]
[`(in-hole ,context ,filler) [`(in-hole ,context ,filler)
(let ([c-context (recur context)] (let ([c-context (recur context)]
[c-filler (recur filler)]) [c-filler (recur filler)])
@ -344,54 +422,50 @@
(let ([g (recur pattern)]) (let ([g (recur pattern)])
(λ (r s a e f) (λ (r s a e f)
(g r s a e the-not-hole)))] (g r s a e the-not-hole)))]
[`any [`(side-condition ,pat ,(? procedure? condition) ,guard-src-loc)
(let ([g (recur pat)])
(λ (r s a e f)
(generate/pred `(side-condition ,(unparse-pattern pat) ,guard-src-loc)
(λ (s a) (g r s a e f))
(λ (_ env) (condition (bindings env)))
s a r)))]
[`(cross ,(? symbol? p))
(λ (r s a e f) (λ (r s a e f)
(let*-values ([(lang nt) ((next-any-decision) langc sexpc)] (values (gen-nt (if any? sexpc langc) p #t r s a f) e))]
[(term) (gen-nt lang nt #f r s a the-not-hole)])
(values term e)))] [`(list ,in-lpats ...)
[(or (? symbol? (? nt? p)) `(cross ,(? symbol? p))) (let loop ([lpats in-lpats])
(let ([cross? (not (symbol? pat))]) (match lpats
(λ (r s a e f) [`() (λ (r s a e f) (values '() e))]
(values (gen-nt (if any? sexpc langc) p cross? r s a f) e)))] [(cons `(repeat ,sub-pat ,name ,mismatch-name) rst)
[(? binder?) (let ([elemg (recur sub-pat)]
(let ([g (recur (binder-pattern pat))]) [tailg (loop rst)]
(λ (r s a e f) [vars (find-vars sub-pat)])
(generate/prior pat e (λ () (g r s a e f)))))] (when mismatch-name
[(? mismatch?) (set! mismatches? #t))
(let ([g (recur (mismatch-pattern pat))]) (λ (r s a env0 f)
(set! mismatches? #t) (define len
(λ (r s a e f) (let ([prior (and name (hash-ref env0 name #f))])
(let-values ([(t e) (g r s a e f)]) (if prior
(values t (hash-set e pat t)))))] prior
[(or (? symbol?) (? number?) (? string?) (? boolean?) (? null?)) (if (zero? s) 0 ((next-sequence-decision) s)))))
(λ (r s a e f) (values pat e))] (let*-values ([(seq env) (generate-sequence (λ (e) (elemg r s a e f)) env0 vars len)]
[(list-rest (struct ellipsis (name sub-pat class vars)) rest) [(env) (if name (hash-set env name len) env)]
(let ([elemg (recur sub-pat)] [(env) (if mismatch-name
[tailg (recur rest)]) (hash-set env mismatch-name len)
(when (mismatch? name) env)]
(set! mismatches? #t)) [(tail env) (tailg r s a env f)])
(λ (r s a e f) (values (append seq tail) env))))]
(let*-values ([(len) [(cons hdp tlp)
(let ([prior (hash-ref e class #f)]) (let ([hdg (recur hdp)]
(if prior [tlg (loop tlp)])
prior (λ (r s a env f)
(if (zero? s) 0 ((next-sequence-decision) s))))] (let*-values
[(seq env) ([(hd env) (hdg r s a env f)]
(generate-sequence (λ (e) (elemg r s a e f)) e vars len)] [(tl env) (tlg r s a env f)])
[(tail env) (values (cons hd tl) env))))]))]
(let ([e (hash-set (hash-set env class len) name len)]) [(? (compose not pair?))
(tailg r s a e f))]) (λ (r s a e f) (values pat e))]))])
(values (append seq tail) env))))]
[(list-rest hdp tlp)
(let ([hdg (recur hdp)]
[tlg (recur tlp)])
(λ (r s a e f)
(let*-values
([(hd env) (hdg r s a e f)]
[(tl env) (tlg r s a env f)])
(values (cons hd tl) env))))]
[else
(error what "unknown pattern ~s\n" pat)]))])
(if mismatches? (if mismatches?
(λ (r s a e f) (λ (r s a e f)
(let ([g (λ (s a) (generator r s a e f))] (let ([g (λ (s a) (generator r s a e f))]
@ -413,7 +487,7 @@
(define sexpc (compile-language sexpp sexp-bases #t)) (define sexpc (compile-language sexpp sexp-bases #t))
(define (compile-pattern pat) (compile pat #f)) (define (compile-pattern pat) (compile pat #f))
(λ (pat) (λ (pat)
(define g (compile-pattern (reassign-classes (parse-pattern pat lang 'top-level)))) (define g (compile-pattern pat))
(λ (size attempt retries) (λ (size attempt retries)
(define-values (t e) (g retries size attempt empty-env the-hole)) (define-values (t e) (g retries size attempt empty-env the-hole))
(values (let replace-the-not-hole ([t t]) (values (let replace-the-not-hole ([t t])
@ -450,26 +524,33 @@
(define (rhs->nts pat) (define (rhs->nts pat)
(let ([nts '()]) (let ([nts '()])
(let loop ([pat pat]) (let loop ([pat pat])
(match pat (match-a-pattern pat
[(? binder?) [`any (void)]
(set! nts (cons (cons #f (binder-pattern pat)) nts))] [`number (void)]
[(? mismatch?) [`string (void)]
(set! nts (cons (cons #f (mismatch-pattern pat)) nts))] [`natural (void)]
[(? symbol?) [`integer (void)]
(when ((is-nt? lang) pat) [`real (void)]
(set! nts (cons (cons #f pat) nts)))] [`variable (void)]
[`(cross ,(? symbol? x-nt)) [`(variable-except ,vars ...) (void)]
[`(variable-prefix ,var) (void)]
[`variable-not-otherwise-mentioned (void)]
[`hole (void)]
[`(nt ,var) (set! nts (cons (cons #f var) nts))]
[`(name ,n ,p) (loop p)]
[`(mismatch-name ,n ,p) (loop p)]
[`(in-hole ,p1 ,p2) (loop p1) (loop p2)]
[`(hide-hole ,p) (loop p)]
[`(side-condition ,p ,exp ,info) (loop p)]
[`(cross ,x-nt)
(set! nts (cons (cons #t x-nt) nts))] (set! nts (cons (cons #t x-nt) nts))]
[`(variable-except ,s ...) (void)] [`(list ,lpats ...)
[`(variable-prefix ,p) (void)] (for ([lpat (in-list lpats)])
[`(name ,_ ,p) (loop p)] (match lpat
[`() (void)] [`(repeat ,p ,name ,mismatch?)
[(struct ellipsis (_ p _ _)) (loop p)]
(loop p)] [_ (loop lpat)]))]
[`(,a . ,b) [(? (compose not pair?)) (void)]))
(loop a)
(loop b)]
[_ (void)]))
nts)) nts))
;; build-table : (listof nt) -> hash ;; build-table : (listof nt) -> hash
@ -547,15 +628,11 @@
(let ([match (regexp-match rx (symbol->string x))]) (let ([match (regexp-match rx (symbol->string x))])
(and match (cadr match) (string->symbol (cadr match)))))) (and match (cadr match) (string->symbol (cadr match))))))
(define-struct class (id) #:inspector (make-inspector)) (define-struct class (id) #:transparent)
(define-struct mismatch (id group) #:inspector (make-inspector)) (define-struct mismatch (id var) #:transparent)
(define mismatch-pattern
(match-lambda
[(struct mismatch (_ name))
((symbol-match mismatch-nt-rx) name)]))
(define-struct binder (name) #:inspector (make-inspector)) (define-struct binder (name) #:transparent)
(define binder-pattern (define binder-pattern
(match-lambda (match-lambda
[(struct binder (name)) [(struct binder (name))
@ -574,76 +651,13 @@
;; and after generating an ellipsis ;; and after generating an ellipsis
(define-struct ellipsis (name pattern class vars) #:inspector (make-inspector)) (define-struct ellipsis (name pattern class vars) #:inspector (make-inspector))
;; parse-pattern : pattern compiled-lang (or/c 'cross 'top-level 'grammar) -> parsed-pattern
;; Turns "pat ...", "pat ..._id", and "pat ..._!_id" into ellipsis structs,
;; "nt_!_id" into mismatch structs, "nt_id" into binder structs, and
;; "nt/underscore-allowed" in top-level patterns into binder structs.
(define (parse-pattern pattern lang mode)
(define (recur pat vars)
(match pat
[(or (app (symbol-match named-nt-rx) (or (? (is-nt? lang)) (? built-in?)))
(and (? (λ (_) (eq? mode 'top-level))) (or (? (is-nt? lang)) (? built-in?))))
(let ([b (make-binder pat)])
(values b (cons b vars)))]
[(app (symbol-match mismatch-nt-rx) (or (? (is-nt? lang)) (? built-in?)))
(let ([mismatch (make-mismatch (gensym) pat)])
(values mismatch (cons mismatch vars)))]
[`(name ,name ,sub-pat)
(let-values ([(parsed vars) (recur sub-pat vars)])
(values `(name ,name ,parsed) (cons (make-binder name) vars)))]
[(list-rest sub-pat (and (? symbol?) (app symbol->string (regexp named-ellipsis-rx)) name) rest)
(let*-values ([(sub-pat-parsed sub-pat-vars) (recur sub-pat null)]
[(seq) (make-ellipsis name sub-pat-parsed (make-class name) sub-pat-vars)]
[(vars) (append (list* name (make-class name) sub-pat-vars) vars)]
[(rest-parsed vars) (recur rest vars)])
(values (cons seq rest-parsed) vars))]
[(list-rest sub-pat '... rest)
(let*-values ([(sub-pat-parsed sub-pat-vars) (recur sub-pat null)]
[(class) (make-class (gensym))]
[(seq) (make-ellipsis '... sub-pat-parsed class sub-pat-vars)]
[(rest-parsed vars) (recur rest (cons class (append sub-pat-vars vars)))])
(values (cons seq rest-parsed) vars))]
[(list-rest sub-pat (and (? symbol?) (app symbol->string (regexp mismatch-ellipsis-rx)) name) rest)
(let*-values ([(sub-pat-parsed sub-pat-vars) (recur sub-pat null)]
[(mismatch) (make-mismatch (gensym) name)]
[(class) (make-class (gensym))]
[(seq) (make-ellipsis mismatch sub-pat-parsed class sub-pat-vars)]
[(vars) (append (list* class mismatch sub-pat-vars) vars)]
[(rest-parsed vars) (recur rest vars)])
(values (cons seq rest-parsed) vars))]
[(and (? (λ (_) (not (eq? mode 'cross)))) `(cross ,(and (? (is-nt? lang)) nt)))
(let ([nt-str (symbol->string nt)])
(values `(cross ,(string->symbol (string-append nt-str "-" nt-str))) vars))]
[`(side-condition ,pat ,guard ,guard-src-loc)
(let-values ([(parsed vars) (recur pat vars)])
(values `(side-condition ,parsed ,guard ,guard-src-loc) vars))]
[(cons first rest)
(let-values ([(first-parsed vars) (recur first vars)])
(let-values ([(rest-parsed vars) (recur rest vars)])
(values (cons first-parsed rest-parsed) vars)))]
[_ (values pat vars)]))
(let-values ([(parsed _) (recur pattern null)])
parsed))
;; parse-language: compiled-lang -> compiled-lang
(define (parse-language lang)
(define ((parse-nt mode) nt)
(make-nt (nt-name nt) (map (parse-rhs mode) (nt-rhs nt))))
(define ((parse-rhs mode) rhs)
(make-rhs (reassign-classes (parse-pattern (rhs-pattern rhs) lang mode))))
(struct-copy
compiled-lang lang
[lang (map (parse-nt 'grammar) (compiled-lang-lang lang))]
[delayed-cclang (delay (map (parse-nt 'cross) (compiled-lang-cclang lang)))]))
;; unparse-pattern: parsed-pattern -> pattern ;; unparse-pattern: parsed-pattern -> pattern
(define unparse-pattern (define unparse-pattern
(match-lambda (match-lambda
[(struct binder (name)) name] [(struct binder (name)) name]
[(struct mismatch (_ group)) group] [(struct mismatch (id var)) var]
[(list-rest (struct ellipsis (name sub-pat _ _)) rest) [(list-rest (struct ellipsis (name sub-pat _ _)) rest)
(let ([ellipsis (if (mismatch? name) (mismatch-group name) name)]) (let ([ellipsis (if (mismatch? name) (mismatch-var name) name)])
(list* (unparse-pattern sub-pat) ellipsis (unparse-pattern rest)))] (list* (unparse-pattern sub-pat) ellipsis (unparse-pattern rest)))]
[(cons first rest) [(cons first rest)
(cons (unparse-pattern first) (unparse-pattern rest))] (cons (unparse-pattern first) (unparse-pattern rest))]
@ -659,31 +673,54 @@
(if (and par (not (eq? chd par))) (recur par (hash-ref sets par #f)) chd))) (if (and par (not (eq? chd par))) (recur par (hash-ref sets par #f)) chd)))
(let* ([last-contexts (make-hasheq)] (let* ([last-contexts (make-hasheq)]
[assignments #hasheq()]
[record-binder [record-binder
(λ (pat under assignments) (λ (pat under)
(if (null? under) (set! assignments
assignments (if (null? under)
(let ([last (hash-ref last-contexts pat #f)]) assignments
(if last (let ([last (hash-ref last-contexts pat #f)])
(foldl (λ (cur last asgns) (union cur last asgns)) assignments under last) (if last
(begin (foldl (λ (cur last asgns) (union cur last asgns)) assignments under last)
(hash-set! last-contexts pat under) (begin
assignments)))))] (hash-set! last-contexts pat under)
[assignments assignments))))))])
(let recur ([pat pattern] [under null] [assignments #hasheq()]) (let recur ([pat pattern] [under null])
(match pat (match-a-pattern pat
;; `(name ,id ,sub-pat) not considered, since bindings introduced [`any assignments]
;; by name must be unique. [`number assignments]
[(struct binder (name)) [`string assignments]
(record-binder name under assignments)] [`natural assignments]
[(struct ellipsis (name sub-pat (struct class (cls)) _)) [`integer assignments]
(recur sub-pat (cons cls under) [`real assignments]
(if (and (symbol? name) (regexp-match named-ellipsis-rx (symbol->string name))) [`variable assignments]
(record-binder name under assignments) [`(variable-except ,vars ...) assignments]
assignments))] [`(variable-prefix ,var) assignments]
[(? list?) [`variable-not-otherwise-mentioned assignments]
(foldl (λ (pat asgns) (recur pat under asgns)) assignments pat)] [`hole assignments]
[_ assignments]))]) [`(nt ,var) assignments]
[`(name ,var ,pat)
(record-binder var under)
(recur pat under)]
[`(mismatch-name ,var ,pat)
(recur pat under)]
[`(in-hole ,p1 ,p2)
(recur p2 under)
(recur p1 under)]
[`(hide-hole ,p)
(recur p under)]
[`(side-condition ,p ,exp ,srcloc)
(recur p under)]
[`(cross ,nt) assignments]
[`(list ,lpats ...)
(for ([lpat (in-list lpats)])
(match lpat
[`(repeat ,p ,name ,mismatch?)
(record-binder name under)
(recur p (cons (or name (gensym)) under))]
[else (recur lpat under)]))
assignments]
[(? (compose not pair?)) assignments]))
(make-immutable-hasheq (hash-map assignments (λ (cls _) (cons cls (find cls assignments))))))) (make-immutable-hasheq (hash-map assignments (λ (cls _) (cons cls (find cls assignments)))))))
(define (reassign-classes pattern) (define (reassign-classes pattern)
@ -691,6 +728,11 @@
[rewrite (λ (c) (make-class (hash-ref reassignments (class-id c) (class-id c))))]) [rewrite (λ (c) (make-class (hash-ref reassignments (class-id c) (class-id c))))])
(let recur ([pat pattern]) (let recur ([pat pattern])
(match pat (match pat
#;
[`(repeat ,sub-pat ,name ,mismatch?)
`(repeat ,(recur sub-pat)
,(rewrite name)
,mismatch?)]
[(struct ellipsis (name sub-pat class vars)) [(struct ellipsis (name sub-pat class vars))
(make-ellipsis name (recur sub-pat) (rewrite class) (make-ellipsis name (recur sub-pat) (rewrite class)
(map (λ (v) (if (class? v) (rewrite v) v)) vars))] (map (λ (v) (if (class? v) (rewrite v) v)) vars))]
@ -710,7 +752,7 @@
(if m m (raise-syntax-error #f "not a metafunction" stx name)))) (if m m (raise-syntax-error #f "not a metafunction" stx name))))
(define-for-syntax (term-generator lang pat what) (define-for-syntax (term-generator lang pat what)
(with-syntax ([pattern (with-syntax ([(pattern (vars ...) (vars/ellipses ...))
(rewrite-side-conditions/check-errs (rewrite-side-conditions/check-errs
(language-id-nts lang what) (language-id-nts lang what)
what #t pat)]) what #t pat)])
@ -1067,8 +1109,8 @@
(provide pick-from-list pick-sequence-length pick-nts (provide pick-from-list pick-sequence-length pick-nts
pick-char pick-var pick-string pick-any pick-char pick-var pick-string pick-any
pick-number pick-natural pick-integer pick-real pick-number pick-natural pick-integer pick-real
parse-pattern unparse-pattern unparse-pattern
parse-language prepare-lang prepare-lang
class-reassignments reassign-classes class-reassignments reassign-classes
default-retries proportion-at-size default-retries proportion-at-size
retry-threshold proportion-before-threshold post-threshold-incr retry-threshold proportion-before-threshold post-threshold-incr

2
collects/redex/tests/check-syntax-test.rkt
View File

@ -171,7 +171,7 @@
(test (send annotations collected-rename-class def-name) (test (send annotations collected-rename-class def-name)
(expected-rename-class (list def-name use-name))) (expected-rename-class (list def-name use-name)))
(test (send annotations collected-rename-class def-name) (test (send annotations collected-rename-class use-name)
(expected-rename-class (list def-name use-name)))) (expected-rename-class (list def-name use-name))))
(print-tests-passed 'check-syntax-test.rkt) (print-tests-passed 'check-syntax-test.rkt)

720
collects/redex/tests/matcher-test.rkt
View File

File diff suppressed because it is too large Load Diff

134
collects/redex/tests/rewrite-side-condition-test.rkt Normal file
View File

@ -0,0 +1,134 @@
#lang racket/base
(require (for-syntax "../private/rewrite-side-conditions.rkt"
racket/base)
"../private/term.rkt" ;; to get bindings for 'in-hole' etc
rackunit)
(define-syntax (rsc stx)
(syntax-case stx ()
[(_ pat (nts ...) bind-names?)
(with-syntax ([(pat (vars ...) (vars/ellipses ...))
(rewrite-side-conditions/check-errs
(syntax->datum #'(nts ...))
'rsc
(syntax-e #'bind-names?)
#'pat)])
#'(list `pat
`(vars ...)
`(vars/ellipses ...)))]))
(check-equal? (rsc 1 () #t) `(1 () ()))
(check-equal? (rsc (1) () #t) `((list 1) () ()))
(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 ..._!_3) () #t) `((list (repeat 1 #f #f)) () ()))
(check-equal? (rsc (1 ..._!_3 1 ..._!_3) () #t) `((list (repeat 1 #f ..._!_3) (repeat 1 #f ..._!_3)) () ()))
(check-equal? (rsc x (x) #t) `((name x (nt x)) (x) (x)))
(check-equal? (rsc x (x) #f) `((nt x) () ()))
(check-equal? (rsc x_1 (x) #t) `((name x_1 (nt x)) (x_1) (x_1)))
(check-equal? (rsc x_1 (x) #f) `((name x_1 (nt x)) (x_1) (x_1)))
(check-equal? (rsc any (x) #t) `((name any any) (any) (any)))
(check-equal? (rsc any (x) #f) `(any () ()))
(check-equal? (rsc any_1 (x) #t) `((name any_1 any) (any_1) (any_1)))
(check-equal? (rsc any_1 (x) #f) `((name any_1 any) (any_1) (any_1)))
(check-equal? (rsc ((x ...) ...) (x) #t)
`((list (repeat (list (repeat (name x (nt x)) #f #f)) #f #f))
(x)
(((x ...) ...))))
(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))
()
()))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;
;; test the normalization of the ellipses underscores
;;
(check-equal? (car (rsc (x_1 ..._1 x_2 ..._2 x_2 ..._1) (x) #t))
'(list (repeat (name x_1 (nt x)) ..._1 #f)
(repeat (name x_2 (nt x)) ..._1 #f)
(repeat (name x_2 (nt x)) ..._1 #f)))
(check-equal? (car (rsc ((x_1 ..._1 x_1 ..._2) (x_2 ..._1 x_2 ..._2) x_3 ..._2) (x) #t))
'(list (list (repeat (name x_1 (nt x)) ..._2 #f)
(repeat (name x_1 (nt x)) ..._2 #f))
(list (repeat (name x_2 (nt x)) ..._2 #f)
(repeat (name x_2 (nt x)) ..._2 #f))
(repeat (name x_3 (nt x)) ..._2 #f)))
(check-equal? (car (rsc (x_1 ..._1 x ..._2 x_1 ..._2) (x) #t))
'(list (repeat (name x_1 (nt x)) ..._2 #f)
(repeat (name x (nt x)) ..._2 #f)
(repeat (name x_1 (nt x)) ..._2 #f)))
(check-equal? (car (rsc (x_1 ..._1 x_2 ..._2 (x_1 x_2) ..._3) (x) #t))
'(list (repeat (name x_1 (nt x)) ..._3 #f)
(repeat (name x_2 (nt x)) ..._3 #f)
(repeat (list (name x_1 (nt x)) (name x_2 (nt x))) ..._3 #f)))
(check-equal? (car (rsc ((x_1 ..._1) ..._2 x_2 ..._3 (x_1 ..._4 x_2) ..._5) (x) #t))
'(list (repeat (list (repeat (name x_1 (nt x)) ..._4 #f)) ..._5 #f)
(repeat (name x_2 (nt x)) ..._5 #f)
(repeat (list (repeat (name x_1 (nt x)) ..._4 #f)
(name x_2 (nt x)))
..._5
#f)))
(check-equal? (car (rsc ((x_1 ..._1) ..._2 (x_1 ..._3) ..._4 (x_1 ..._5) ..._6) (x) #t))
'(list (repeat (list (repeat (name x_1 (nt x)) ..._5 #f)) ..._6 #f)
(repeat (list (repeat (name x_1 (nt x)) ..._5 #f)) ..._6 #f)
(repeat (list (repeat (name x_1 (nt x)) ..._5 #f)) ..._6 #f)))
(check-equal? (car (rsc (x_1 ..._1 x_1 ..._2 x_2 ..._1 x_2 ..._4 x_2 ..._3) (x) #t))
'(list (repeat (name x_1 (nt x)) ..._3 #f)
(repeat (name x_1 (nt x)) ..._3 #f)
(repeat (name x_2 (nt x)) ..._3 #f)
(repeat (name x_2 (nt x)) ..._3 #f)
(repeat (name x_2 (nt x)) ..._3 #f)))
(check-equal? (car (rsc (x_1 ... x_1 ..._!_1 x_1 ..._1) (x) #t))
'(list (repeat (name x_1 (nt x)) ..._1 #f)
(repeat (name x_1 (nt x)) ..._1 #f)
(repeat (name x_1 (nt x)) ..._1 #f)))
(check-equal? (car (rsc (x_1 ... x_1 ..._!_1 x_1 ..._1 x_2 ..._!_1) (x) #t))
'(list (repeat (name x_1 (nt x)) ..._1 #f)
(repeat (name x_1 (nt x)) ..._1 ..._!_1)
(repeat (name x_1 (nt x)) ..._1 #f)
(repeat (name x_2 (nt x)) #f ..._!_1)))
(check-equal? (car (rsc ((3 ..._1) ..._2 (4 ..._1) ..._3) (x) #t))
'(list (repeat (list (repeat 3 ..._1 #f)) ..._3 #f)
(repeat (list (repeat 4 ..._1 #f)) ..._3 #f)))
(check-equal? (car (rsc (x ..._1 x ..._2
variable ..._2 variable ..._3 variable_1 ..._3 variable_1 ..._4)
(x) #t))
'(list (repeat (name x (nt x)) ..._4 #f)
(repeat (name x (nt x)) ..._4 #f)
(repeat (name variable variable) ..._4 #f)
(repeat (name variable variable) ..._4 #f)
(repeat (name variable_1 variable) ..._4 #f)
(repeat (name variable_1 variable) ..._4 #f)))
(check-equal? (car (rsc (z_1 ... z_2 ..._!_1 (z_1 z_2) ...) (z) #t))
'(list (repeat (name z_1 (nt z)) ..._r3 #f)
(repeat (name z_2 (nt z)) ..._r3 #f)
(repeat (list (name z_1 (nt z))
(name z_2 (nt z)))
..._r3
#f)))
(check-equal? (car (rsc (z_1 ... z_2 ..._!_1 z_3 ..._!_1 (z_1 z_2) ...) (z) #t))
'(list (repeat (name z_1 (nt z)) ..._r4 #f)
(repeat (name z_2 (nt z)) ..._r4 ..._!_1)
(repeat (name z_3 (nt z)) #f ..._!_1)
(repeat (list (name z_1 (nt z))
(name z_2 (nt z)))
..._r4
#f)))
;;
;; test the normalization of the ellipses underscores
;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

132
collects/redex/tests/rg-test.rkt
View File

@ -43,14 +43,11 @@
[(exn:fail:redex:test _ _ (? exn:fail:contract:blame? e) _) e] [(exn:fail:redex:test _ _ (? exn:fail:contract:blame? e) _) e]
[x x])))])) [x x])))]))
(define find-base-cases/unparsed
(compose find-base-cases parse-language))
(let () (let ()
(define-language lc (define-language lc
(e x (e e) (λ (x) e)) (e x (e e) (λ (x) e))
(x variable)) (x variable))
(let ([bc (find-base-cases/unparsed lc)]) (let ([bc (find-base-cases lc)])
(test (to-table (base-cases-non-cross bc)) (test (to-table (base-cases-non-cross bc))
'((e . (1 2 2)) (x . (0)))) '((e . (1 2 2)) (x . (0))))
(test (to-table (base-cases-cross bc)) (test (to-table (base-cases-cross bc))
@ -59,7 +56,7 @@
(let () (let ()
(define-language lang (define-language lang
(e (e e))) (e (e e)))
(let ([bc (find-base-cases/unparsed lang)]) (let ([bc (find-base-cases lang)])
(test (to-table (base-cases-non-cross bc)) '((e . (inf)))) (test (to-table (base-cases-non-cross bc)) '((e . (inf))))
(test (to-table (base-cases-cross bc)) '((e-e . (0 inf inf)))))) (test (to-table (base-cases-cross bc)) '((e-e . (0 inf inf))))))
@ -67,11 +64,11 @@
(define-language lang (define-language lang
(a 1 2 3) (a 1 2 3)
(b a (a_1 b_!_1))) (b a (a_1 b_!_1)))
(let ([bc (find-base-cases/unparsed lang)]) (let ([bc (find-base-cases lang)])
(test (to-table (base-cases-non-cross bc)) (test (to-table (base-cases-non-cross bc))
'((a . (0 0 0)) (b . (1 2)))) '((a . (0 0 0)) (b . (1 2))))
(test (to-table (base-cases-cross bc)) (test (to-table (base-cases-cross bc))
'((a-a . (0)) (a-b . (1)) (b-b . (0)))))) '((a-a . (0)) (a-b . (1 2 2)) (b-b . (0 1))))))
(let () (let ()
(define-language lc (define-language lc
@ -82,7 +79,7 @@
(v (λ (x) e) (v (λ (x) e)
number) number)
(x variable)) (x variable))
(let ([bc (find-base-cases/unparsed lc)]) (let ([bc (find-base-cases lc)])
(test (to-table (base-cases-non-cross bc)) (test (to-table (base-cases-non-cross bc))
'((e . (2 2 1 1)) (v . (2 0)) (x . (0)))) '((e . (2 2 1 1)) (v . (2 0)) (x . (0))))
(test (to-table (base-cases-cross bc)) (test (to-table (base-cases-cross bc))
@ -96,7 +93,7 @@
(name x 1) (name x 1)
(name y 1)) (name y 1))
(y y)) (y y))
(test (hash-ref (base-cases-non-cross (find-base-cases/unparsed L)) 'x) (test (hash-ref (base-cases-non-cross (find-base-cases L)) 'x)
'(0 0 0 0))) '(0 0 0 0)))
(define (make-random . nums) (define (make-random . nums)
@ -325,7 +322,7 @@
(test (generate-term/decisions lang d 5 0 (decisions #:seq (list (λ (_) 2)))) (test (generate-term/decisions lang d 5 0 (decisions #:seq (list (λ (_) 2))))
'(4 4 4 4 (4 4) (4 4))) '(4 4 4 4 (4 4) (4 4)))
(test (raised-exn-msg exn:fail:redex:generation-failure? (generate-term lang e 5 #:retries 42)) (test (raised-exn-msg exn:fail:redex:generation-failure? (generate-term lang e 5 #:retries 42))
#rx"generate-term: unable to generate pattern \\(n_1 ..._!_1 n_2 ..._!_1 \\(n_1 n_2\\) ..._3\\) in 42") #rx"generate-term: unable to generate pattern .* in 42")
(test (raised-exn-msg (test (raised-exn-msg
exn:fail:redex:generation-failure? exn:fail:redex:generation-failure?
(parameterize ([generation-decisions (parameterize ([generation-decisions
@ -340,7 +337,9 @@
#rx"generate-term: unable to generate pattern variable-not-otherwise-mentioned in 1") #rx"generate-term: unable to generate pattern variable-not-otherwise-mentioned in 1")
(test (generate-term/decisions lang f 5 0 (decisions #:seq (list (λ (_) 0)))) null) (test (generate-term/decisions lang f 5 0 (decisions #:seq (list (λ (_) 0)))) null)
(test (generate-term/decisions (test (generate-term/decisions
lang ((0 ..._!_1) ... (1 ..._!_1) ...) 5 0 lang
((0 ..._!_1) ... (1 ..._!_1) ...)
5 0
(decisions #:seq (list (λ (_) 2) (λ (_) 3) (λ (_) 4) (λ (_) 2) (λ (_) 3) (λ (_) 4) (decisions #:seq (list (λ (_) 2) (λ (_) 3) (λ (_) 4) (λ (_) 2) (λ (_) 3) (λ (_) 4)
(λ (_) 2) (λ (_) 3) (λ (_) 4) (λ (_) 1) (λ (_) 3)))) (λ (_) 2) (λ (_) 3) (λ (_) 4) (λ (_) 1) (λ (_) 3))))
'((0 0 0) (0 0 0 0) (1 1 1))) '((0 0 0) (0 0 0 0) (1 1 1)))
@ -412,7 +411,7 @@
(test (generate-term lang b 5) 43) (test (generate-term lang b 5) 43)
(test (generate-term lang (side-condition a (odd? (term a))) 5) 43) (test (generate-term lang (side-condition a (odd? (term a))) 5) 43)
(test (raised-exn-msg exn:fail:redex:generation-failure? (generate-term lang c 5)) (test (raised-exn-msg exn:fail:redex:generation-failure? (generate-term lang c 5))
#px"unable to generate pattern \\(side-condition a\\_1 #<syntax:.*\\/rg-test\\.(?:.+):\\d+:\\d+>\\)") #rx"unable to generate pattern")
(test (let/ec k (test (let/ec k
(generate-term lang (number_1 (side-condition 7 (k (term number_1)))) 5)) (generate-term lang (number_1 (side-condition 7 (k (term number_1)))) 5))
'number_1) 'number_1)
@ -603,7 +602,7 @@
(decisions #:nt (patterns first))) (decisions #:nt (patterns first)))
47) 47)
(test (hash-ref (base-cases-non-cross (find-base-cases/unparsed name-collision)) 'e-e) (test (hash-ref (base-cases-non-cross (find-base-cases name-collision)) 'e-e)
'(0))) '(0)))
(let () (let ()
@ -1217,109 +1216,66 @@
(check-metafunction n (λ (_) #t) #:retries 42)) (check-metafunction n (λ (_) #t) #:retries 42))
#rx"check-metafunction: unable .* in 42")) #rx"check-metafunction: unable .* in 42"))
;; parse/unparse-pattern
(let-syntax ([test-match (syntax-rules () [(_ p x) (test (match x [p #t] [_ #f]) #t)])])
(define-language lang (x variable))
(let ([pattern '((x_1 number) ... 3)])
(test-match (list
(struct ellipsis
('...
(list (struct binder ('x_1)) (struct binder ('number)))
_
(list (struct binder ('number)) (struct binder ('x_1)))))
3)
(parse-pattern pattern lang 'top-level))
(test (unparse-pattern (parse-pattern pattern lang 'top-level)) pattern))
(let ([pattern '((x_1 ..._1 x_2) ..._!_1)])
(test-match (struct ellipsis
((struct mismatch (i_1 '..._!_1))
(list
(struct ellipsis
('..._1
(struct binder ('x_1))
(struct class ('..._1))
(list (struct binder ('x_1)))))
(struct binder ('x_2)))
_
(list (struct binder ('x_2)) '..._1 (struct class ('..._1)) (struct binder ('x_1)))))
(car (parse-pattern pattern lang 'grammar)))
(test (unparse-pattern (parse-pattern pattern lang 'grammar)) pattern))
(let ([pattern '((name x_1 x_!_2) ...)])
(test-match (struct ellipsis
('... `(name x_1 ,(struct mismatch (i_2 'x_!_2))) _
(list (struct binder ('x_1)) (struct mismatch (i_2 'x_!_2)))))
(car (parse-pattern pattern lang 'grammar)))
(test (unparse-pattern (parse-pattern pattern lang 'grammar)) pattern))
(let ([pattern '((x ...) ..._1)])
(test-match (struct ellipsis
('..._1
(list
(struct ellipsis
('...
(struct binder ('x))
(struct class (c_1))
(list (struct binder ('x))))))
_
(list (struct class (c_1)) (struct binder ('x)))))
(car (parse-pattern pattern lang 'top-level)))
(test (unparse-pattern (parse-pattern pattern lang 'top-level)) pattern))
(let ([pattern '((variable_1 ..._!_1) ...)])
(test-match (struct ellipsis
('...
(list
(struct ellipsis
((struct mismatch (i_1 '..._!_1))
(struct binder ('variable_1))
(struct class (c_1))
(list (struct binder ('variable_1))))))
_
(list (struct class (c_1)) (struct mismatch (i_1 '..._!_1)) (struct binder ('variable_1)))))
(car (parse-pattern pattern lang 'grammar)))
(test (unparse-pattern (parse-pattern pattern lang 'grammar)) pattern))
(test (parse-pattern '(cross x) lang 'grammar) '(cross x-x))
(test (parse-pattern '(cross x) lang 'cross) '(cross x))
(test (parse-pattern 'x lang 'grammar) 'x)
(test (parse-pattern 'variable lang 'grammar) 'variable))
(let () (let ()
(define-language lang (x variable)) (define-language lang (x variable))
(define-syntax test-class-reassignments (define-syntax test-class-reassignments
(syntax-rules () (syntax-rules ()
[(_ pattern expected) [(_ pattern expected)
(test (to-table (class-reassignments (parse-pattern pattern lang 'top-level))) (test (to-table (class-reassignments pattern))
expected)])) expected)]))
(test-class-reassignments (test-class-reassignments
'(x_1 ..._1 x_2 ..._2 x_2 ..._1) '(list (repeat (name x_1 (nt x)) ..._1 #f) (repeat (name x_2 (nt x)) ..._2 #f) (repeat (name x_2 (nt x)) ..._1 #f))
'((..._2 . ..._1))) '((..._2 . ..._1)))
(test-class-reassignments (test-class-reassignments
'((x_1 ..._1 x_1 ..._2) (x_2 ..._1 x_2 ..._2) x_3 ..._2) '(list (list (repeat (name x_1 (nt x)) ..._1 #f) (repeat (name x_1 (nt x)) ..._2 #f))
(list (repeat (name x_2 (nt x)) ..._1 #f) (repeat (name x_2 (nt x)) ..._2 #f))
(repeat (name x_3 (nt x)) ..._2 #f))
'((..._1 . ..._2) (..._2 . ..._2))) '((..._1 . ..._2) (..._2 . ..._2)))
(test-class-reassignments (test-class-reassignments
'(x_1 ..._1 x ..._2 x_1 ..._2) '(list (repeat (name x_1 (nt x)) ..._1 #f) (repeat (name x (nt x)) ..._2 #f) (repeat (name x_1 (nt x)) ..._2 #f))
'((..._1 . ..._2))) '((..._1 . ..._2)))
(test-class-reassignments (test-class-reassignments
'(x_1 ..._1 x_2 ..._2 (x_1 x_2) ..._3) '(list (repeat (name x_1 (nt x)) ..._1 #f) (repeat (name x_2 (nt x)) ..._2 #f) (repeat (list (name x_1 (nt x)) (name x_2 (nt x))) ..._3 #f))
'((..._1 . ..._3) (..._2 . ..._3))) '((..._1 . ..._3) (..._2 . ..._3)))
(test-class-reassignments (test-class-reassignments
'((x_1 ..._1) ..._2 x_2 ..._3 (x_1 ..._4 x_2) ..._5) '(list (repeat (list (repeat (name x_1 (nt x)) ..._1 #f)) ..._2 #f)
(repeat (name x_2 (nt x)) ..._3 #f)
(repeat (list (repeat (name x_1 (nt x)) ..._4 #f)
(name x_2 (nt x)))
..._5
#f))
'((..._1 . ..._4) (..._2 . ..._5) (..._3 . ..._5))) '((..._1 . ..._4) (..._2 . ..._5) (..._3 . ..._5)))
(test-class-reassignments (test-class-reassignments
'((x_1 ..._1) ..._2 (x_1 ..._3) ..._4 (x_1 ..._5) ..._6) '(list (repeat (list (repeat (name x_1 (nt x)) ..._1 #f)) ..._2 #f)
(repeat (list (repeat (name x_1 (nt x)) ..._3 #f)) ..._4 #f)
(repeat (list (repeat (name x_1 (nt x)) ..._5 #f)) ..._6 #f))
'((..._1 . ..._5) (..._2 . ..._6) (..._3 . ..._5) (..._4 . ..._6))) '((..._1 . ..._5) (..._2 . ..._6) (..._3 . ..._5) (..._4 . ..._6)))
(test-class-reassignments (test-class-reassignments
'(x_1 ..._1 x_1 ..._2 x_2 ..._1 x_2 ..._4 x_2 ..._3) '(list (repeat (name x_1 (nt x)) ..._1 #f)
(repeat (name x_1 (nt x)) ..._2 #f)
(repeat (name x_2 (nt x)) ..._1 #f)
(repeat (name x_2 (nt x)) ..._4 #f)
(repeat (name x_2 (nt x)) ..._3 #f))
'((..._1 . ..._3) (..._2 . ..._3) (..._4 . ..._3))) '((..._1 . ..._3) (..._2 . ..._3) (..._4 . ..._3)))
(test (test
(hash-map (hash-map
(class-reassignments (parse-pattern '(x_1 ... x_1 ..._!_1 x_1 ..._1) lang 'top-level)) (class-reassignments '(list (repeat (name x_1 (nt x)) #f #f)
(repeat (name x_1 (nt x)) ..._!_1 #t)
(repeat (name x_1 (nt x)) ..._1 #f)))
(λ (_ cls) cls)) (λ (_ cls) cls))
'(..._1 ..._1)) '(..._1 ..._1))
(test-class-reassignments (test-class-reassignments
'((3 ..._1) ..._2 (4 ..._1) ..._3) '(list (repeat (list (repeat 3 ..._1 #f)) ..._2 #f)
(repeat (list (repeat 4 ..._1 #f)) ..._3 #f))
'((..._2 . ..._3))) '((..._2 . ..._3)))
(test-class-reassignments (test-class-reassignments
'(x ..._1 x ..._2 variable ..._2 variable ..._3 variable_1 ..._3 variable_1 ..._4) '(list (repeat (name x (nt x)) ..._1 #f)
(repeat (name x (nt x)) ..._2 #f)
(repeat (name variable variable) ..._2 #f)
(repeat (name variable variable) ..._3 #f)
(repeat (name variable_1 variable) ..._3 #f)
(repeat (name variable_1 variable) ..._4 #f))
'((..._1 . ..._4) (..._2 . ..._4) (..._3 . ..._4)))) '((..._1 . ..._4) (..._2 . ..._4) (..._3 . ..._4))))
;; redex-test-seed ;; redex-test-seed

2
collects/redex/tests/run-tests.rkt
View File

@ -18,6 +18,7 @@
(append (append
'("lw-test.rkt" '("lw-test.rkt"
"matcher-test.rkt" "matcher-test.rkt"
"rewrite-side-condition-test.rkt"
"tl-test.rkt" "tl-test.rkt"
"term-test.rkt" "term-test.rkt"
"rg-test.rkt" "rg-test.rkt"
@ -34,6 +35,7 @@
'("../examples/cbn-letrec.rkt" '("../examples/cbn-letrec.rkt"
"../examples/stlc.rkt" "../examples/stlc.rkt"
"../examples/pi-calculus.rkt" "../examples/pi-calculus.rkt"
"../examples/list-machine/test.rkt"
("../examples/beginner.rkt" main) ("../examples/beginner.rkt" main)
"../examples/racket-machine/reduction-test.rkt" "../examples/racket-machine/reduction-test.rkt"
"../examples/racket-machine/verification-test.rkt" "../examples/racket-machine/verification-test.rkt"

4
collects/redex/tests/syn-err-tests/judgment-form-definition.rktd
View File

@ -171,8 +171,8 @@
(let () (let ()
(define-judgment-form syn-err-lang (define-judgment-form syn-err-lang
#:mode (pat-depth I O) #:mode (pat-depth I O)
[(pat-depth (binder2 ellipsis) ()) [(pat-depth (binder1 ellipsis) ())
(pat-depth () binder1)]) (pat-depth () binder2)])
(void))) (void)))
(#rx"too many ellipses" (#rx"too many ellipses"
([premise (no-ellipsis any)]) ([premise (no-ellipsis any)])

2
collects/redex/tests/syn-err-tests/reduction-relation-definition.rktd
View File

@ -32,7 +32,7 @@
(#rx"different depths" (#rx"different depths"
([binder2 number_1] [binder1 number_1]) ([ellipsis ...]) ([binder1 number_1] [binder2 number_1]) ([ellipsis ...])
(reduction-relation (reduction-relation
syn-err-lang syn-err-lang
(--> binder1 (--> binder1

4
collects/redex/tests/test-util.rkt
View File

@ -29,7 +29,7 @@
(define-syntax (test stx) (define-syntax (test stx)
(syntax-case stx () (syntax-case stx ()
[(_ expected got) [(_ expected got)
(with-syntax ([line (syntax-line (syntax got))] (with-syntax ([line (syntax-line stx)]
[fn (if (path? (syntax-source (syntax got))) [fn (if (path? (syntax-source (syntax got)))
(path->string (syntax-source (syntax got))) (path->string (syntax-source (syntax got)))
"<unknown file>")]) "<unknown file>")])
@ -142,7 +142,7 @@
(matches? got expected)) (matches? got expected))
(set! failures (+ 1 failures)) (set! failures (+ 1 failures))
(fprintf (current-error-port) (fprintf (current-error-port)
"test/proc: file ~a line ~a:\n got ~s\nexpected ~s\n\n" "test: file ~a line ~a:\n got ~s\nexpected ~s\n\n"
filename filename
line line
got got

4
collects/redex/tests/tl-test.rkt
View File

@ -2533,7 +2533,7 @@
; test that names are properly bound for side-conditions in shortcuts ; test that names are properly bound for side-conditions in shortcuts
(let* ([lhs ((rewrite-proc-lhs (first (reduction-relation-make-procs r))) grammar)] (let* ([lhs ((rewrite-proc-lhs (first (reduction-relation-make-procs r))) grammar)]
[proc (third lhs)] [proc (third lhs)]
[name (cadadr lhs)] [name (cadar (cddadr lhs))]
[bind (λ (n) (make-bindings (list (make-bind name n))))]) [bind (λ (n) (make-bindings (list (make-bind name n))))])
(test (and (proc (bind 4)) (not (proc (bind 3)))) #t)) (test (and (proc (bind 4)) (not (proc (bind 3)))) #t))
@ -2551,7 +2551,7 @@
; test shortcut in terms of shortcut ; test shortcut in terms of shortcut
(test (match ((rewrite-proc-lhs (third (reduction-relation-make-procs r))) grammar) (test (match ((rewrite-proc-lhs (third (reduction-relation-make-procs r))) grammar)
[`(((side-condition 5 ,(? procedure?) ,_) 2) 1) #t] [`(list (list (side-condition 5 ,(? procedure?) ,_) 2) 1) #t]
[else #f]) [else #f])
#t)) #t))