[racket] (where-not ...) in Redex

On Wed, Aug 29, 2012 at 3:28 PM, Matthias Felleisen
<matthias at ccs.neu.edu> wrote:
>
> On Aug 26, 2012, at 2:33 PM, Robby Findler wrote:
>
>
>
> On Sunday, August 26, 2012, Matthias Felleisen wrote:
>>
>>
>> On Aug 25, 2012, at 10:53 PM, Robby Findler wrote:
>>
>> > On Thu, Aug 23, 2012 at 8:11 AM, Matthias Felleisen
>> > <matthias at ccs.neu.edu> wrote:
>> >>
>> >> I would almost prefer the use of 'when' for 'where' and the
>> >> introduction of 'unless'.
>> >
>> > If we did this, then there could be no judgment-forms name 'when' or
>> > 'unless', which makes me think we shouldn't do this.
>>
>> I don't understand this point at all.
>>
>
> See the docs for define-judgement-form and imagine a judgment-form whose
> name was "unless". You'll notice a conflict in the premise grammar.
>
>
>
> I have taken the time to re-read the docs, and you're saying that someone
> could name a judgment rule 'when' or 'unless' via
> non-ellipsis-non-hyphen-var. Well, let them use strings if they must use
> such special names as rule names. For an SOS, I could imagine when_true and
> when_false as names, and for typing rules I could imagine when_t.
>
>
>
>  >> The type setting of 'when' could still use 'where' as the English word
> (and perhaps we can have a way to override it).
>>
>> >>
>> >> I am not sure how to type set 'unless' other than by providing a the
>> >> negative operator as an argument !=
>> >
>> > Using \neq{} seems right to me.
>>
>> What if you want \not\in or \not\subtype and such?
>>
>
> You can't use where or unless for such things already. Either that or I
> don't understand you?
>
>
> How would you formulate judgments like this:
>
>   |- e -> v
>  ------------------------ when v in Nat & v > 0
>   |- (foo e bar e_1) -> v[e_1}
>

I assume you're defining the -> relation here? I don't know what the
right-hand side of the -> relation in the consequent of this rule is
supposed to be, but lets just say it is some kind of a pairing
operator.

I guess you'd write something like this:

(define-judgment-form L
  #:mode (-> I O)
  [(-> e v)
   (side-condition (positive-nat v))
   ---------------------------
   (foo e bar e_1) -> (v e_1)]

(define-metafunction L
  [(positive-nat natural) ,(> (term natural) 0)]
  [(positive-nat any) #f])

Then, you'd override the typesetting of calls to positive-nat to put
whatever unicode fanciness you wanted there instead.

That'd be one way to do it anyways. I may not be getting your intent,
so there may be other ways.

You cannot, in the current Redex typeset things beside the bar like that.

Robby