Re: [racket-users] Redex: macro expanding to a side-condition clause

2016-10-24 Thread Sam Caldwell
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 
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  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 <
> ro...@eecs.northwestern.edu>
> > 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  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 racket-users+unsubscr...@googlegroups.com.
> >> > 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.
>

-- 
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.


Re: [racket-users] Redex: macro expanding to a side-condition clause

2016-10-24 Thread Robby Findler
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  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 
> 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  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 racket-users+unsubscr...@googlegroups.com.
>> > 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.


Re: [racket-users] Redex: macro expanding to a side-condition clause

2016-10-24 Thread Sam Caldwell
> 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 
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  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 racket-users+unsubscr...@googlegroups.com.
> > 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.


Re: [racket-users] Redex: macro expanding to a side-condition clause

2016-10-24 Thread Robby Findler
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  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 racket-users+unsubscr...@googlegroups.com.
> 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.


[racket-users] Redex: macro expanding to a side-condition clause

2016-10-24 Thread Sam Caldwell
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 racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.