I think the right way to approach such questions is to start from a more realistic example and then ask "what do we want the typeset version of this to look like?". The answer, when looked at that way is almost never "extend the pattern language" since additional complexity there is not something readers of your paper will understand. I find the answer generally takes the form of an additional meta function that hides some complexity but is given a nice name.
Robby On Thursday, March 24, 2016, 'William J. Bowman' via Racket Users < racket-users@googlegroups.com> wrote: > #lang scribble/doc Ha, you can run this email! > > In Redex, I have on several occasions found myself trying to use a > pattern to constrain a sequence's member to match that pattern. > i.e., I want to use a pattern bound at depth 0 to constrain a pattern > at depth 1. > Unfortunately, I can't do this, so it seems I must escape into Racket > and enforce this constraint with andmap and equal?. > I'm hoping someone can tell me there is a better way. > > For example: > > @(require > redex/reduction-semantics > racket/function) > > @(define-language testL > [x ::= variable-not-otherwise-mentioned]) > > (define-judgment-form testL > #:mode (complex-match I) > #:contract (complex-match (x (x ...))) > > [----------------- > (complex-match (x (x ...)))]) > > Gives this error: > ; ....: define-judgment-form: found the same binder, x, at different > depths, 0 and 1 > ; at: x > ; in: (x (x ...)) > > So, I am forced to write this: > > @(define-judgment-form testL > #:mode (complex-match_0 I) > #:contract (complex-match_0 (x (x ...))) > > [;; NB: Ugh this should be possible with pattern matching alone .... > (side-condition ,(andmap (curry equal? (term x)) (term (x_0 ...)))) > ----------------- > (complex-match_0 (x (x_0 ...)))]) > > @(require rackunit) > @(check-true > (judgment-holds (complex-match_0 (x (x))))) > @(check-true > (judgment-holds (complex-match_0 (foo (foo foo))))) > @(check-false > (judgment-holds (complex-match_0 (x (y z)))))) > > > This is particularly annoying, since I can easily do almost the > *opposite*, i.e., use a depth 0 pattern while constraining a sequence's > members to be distinct. > > @(define-judgment-form testL > #:mode (complex-not-match I) > #:contract (complex-not-match (x (x ...))) > > [----------------- > (complex-not-match (x_!_0 (x_!_0 ...)))]) > > @(check-false > (judgment-holds (complex-not-match (x (x))))) > @(check-false > (judgment-holds (complex-not-match (foo (foo foo))))) > @(check-true > (judgment-holds (complex-not-match (x (y z)))))) > > > If there is no better way, would it be too much to ask for a new > pattern that does this? E.g., perhaps (x_=_0 (x_=_0 ...))? > > -- > William J. Bowman > Northeastern University > College of Computer and Information Science > > -- > You received this message because you are subscribed to the Google Groups > "Racket Users" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to racket-users+unsubscr...@googlegroups.com <javascript:;>. > For more options, visit https://groups.google.com/d/optout. > -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to racket-users+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
