[racket] [redex] side-condition matching upon errors

It is useful for seeing why a judgment fails -- using build-derivations & show-derivations requires a judgment that actually holds. In Redex's current state, it should be possible to imitate a #t-only side condition as (where #t <condition-check>). One could also use a debug-print metafunction which always returns #t and uses its own internal side-condition to display its argument, though I'm not sure if writing metafunctions that aren't really tied to a particular language is to be encouraged.

I can't speak for the Redex user base as a whole, but debugging is the only use of side-condition where I don't expect to get #t or #f.

---
Justin Slepak
PhD student, Computer Science dept.

----- Original Message -----
From: Robby Findler <robby at eecs.northwestern.edu>
To: Jonathan Schuster <schuster at ccs.neu.edu>
Cc: Racket List <users at racket-lang.org>
Sent: Wed, 4 Sep 2013 15:04:48 -0400 (EDT)
Subject: Re: [racket] [redex] side-condition matching upon errors

Just to be clear, the proposed change would affect only
define-judgment-form, since that's the only place where side-condition is
not implicitly unquoted.

But adding some kind of "debug" annotation that meant "if you get here,
print something out" sounds actually quite useful.

Robby


On Wed, Sep 4, 2013 at 1:50 PM, Jonathan Schuster <schuster at ccs.neu.edu>wrote:

>
>> As for backwards compatibility issues, I don't know how much people rely
>>> on side-condition taking something not-#f/#t... Probably too much :)
>>> (also, there could be a `side-condition-soft' variant that is not strict
>>> in the boolean-ness, or vice-versa)
>>>
>>>
>> Well, if we're willing to force clients to change their code, then it
>> isn't hard for them to write their own metafunctions that turn non-#f
>> things into #ts.
>>
>>  But I think you're right that just changing this is a good idea and
>> backwards compatibility be damned. I'll put it on my list.
>>
>
> There's at least one situation in which non-booleans in side conditions
> are important: debugging. Much of my Redex debugging involves adding code
> along the lines of "(side-condition (displayln (term <something>)))".
> Forcing booleans there would make that line even more verbose, and when
> it's being written a lot, that pain adds up.
>
> I'd be in favor of something like side-condition-soft as described above.
> Or alternatively, it might make sense to have a "debug" clause that acts
> like printf, or even a "racket-expression" clause that evaluates the given
> racket expression, but does not affect the result of a metafunction the way
> side-condition does.
>