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

 From: Robby Findler (robby at eecs.northwestern.edu) Date: Wed Aug 29 17:46:27 EDT 2012 Previous message: [racket] (where-not ...) in Redex Next message: [racket] (where-not ...) in Redex Messages sorted by: [date] [thread] [subject] [author]

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


 Posted on the users mailing list. Previous message: [racket] (where-not ...) in Redex Next message: [racket] (where-not ...) in Redex Messages sorted by: [date] [thread] [subject] [author]