Right, so I need a separate metafunction for each pattern I want to negate.
On Mon, Oct 24, 2016 at 6:56 PM, Robby Findler <[email protected]> wrote: > I am saying to write this: > > (define-metafunction L > [(not-thing pat) #false] > [(not-thing any) #true]) > > and then where you wrote: > > (where/not pat tm) > > write this: > > (where #true (not-thing pat)) > > > > On Mon, Oct 24, 2016 at 5:47 PM, Sam Caldwell <[email protected]> wrote: > >> In the meantime, consider using a metafunction with an `else` clause. > > > > This would entail fixing the pattern, right? As in, I can write a > > metafunction deciding whether a term does not match a pattern, but I > can't > > write a metafunction taking both the term and the pattern. > > > > I'm ok with failed matches not being first-class in Redex, but I'm a > little > > disappointed if I can't create my own shorthand. > > > > Thanks, > > Sam Caldwell > > > > On Mon, Oct 24, 2016 at 6:31 PM, Robby Findler < > [email protected]> > > wrote: > >> > >> Unfortunately, Redex's pattern language does not currently support > >> `not`. It might be easy to add it, or maybe hard, or maybe impossible. > >> Offhand, it seems probably possible to support in the unifier and > >> impossible in the enumerator and not hard in the matcher. > >> > >> In the meantime, consider using a metafunction with an `else` clause. > >> > >> Robby > >> > >> > >> On Mon, Oct 24, 2016 at 5:15 PM, Sam Caldwell <[email protected]> wrote: > >> > I have a Redex judgment that I would like to specify in terms of a > >> > *failed* > >> > pattern match. I can write this like so: > >> > > >> > [(side-condition ,(not (redex-match? L pat (term tm))) > >> > ------------------------------------------------------------------ > >> > ...] > >> > > >> > which works, but I would rather just abbreviate this using a macro > >> > (since > >> > afaict there are no existing constructs in redex to do this), so I > could > >> > write for instance: > >> > > >> > [(where/not pat tm) > >> > -------------------------- > >> > ...] > >> > > >> > But then I get an error: "define-judgment-form: expected judgment form > >> > name > >> > in: where/not" > >> > > >> > Does anybody know how to achieve this? > >> > > >> > Thanks, > >> > Sam Caldwell > >> > > >> > Full example: > >> > > >> > ============================================================== > >> > > >> > #lang racket > >> > > >> > (require redex) > >> > > >> > (define-language L > >> > (E number (+ E E))) > >> > > >> > (define-syntax (where/not stx) > >> > (syntax-case stx () > >> > [(_ pat tm) > >> > #'(side-condition ,(not (redex-match? L pat (term tm))))])) > >> > > >> > (define-judgment-form L > >> > #:mode (j I) > >> > [(where/not number E) > >> > --------------------- > >> > (j E)]) > >> > > >> > -- > >> > 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 [email protected]. > >> > 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 [email protected]. > 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 [email protected]. For more options, visit https://groups.google.com/d/optout.
