[racket-dev] [plt] Push #23181: master branch updated

On Sat, Aug 6, 2011 at 2:47 PM, Casey Klein
<clklein at eecs.northwestern.edu> wrote:
> On Sat, Aug 6, 2011 at 1:58 PM, Robby Findler
> <robby at eecs.northwestern.edu> wrote:
>> On Sat, Aug 6, 2011 at 1:53 PM, Casey Klein
>> <clklein at eecs.northwestern.edu> wrote:
>>> On Sat, Aug 6, 2011 at 10:43 AM, Matthias Felleisen
>>> <matthias at ccs.neu.edu> wrote:
>>>>
>>>> 1. I like Robby's mode suggestion.
>>>> 2. I prefer shorter keywords, e.g., define-judgment.
>>>
>>> I'm having trouble reconciling these comments. Robby's suggestion, if
>>> I understand it correctly, is to overload the `define-relation' name
>>> instead of choosing a new one. If you supply the #:mode keyword, you
>>> get the `define-judgment-form' behavior (inputs and outputs, static
>>> checking, the `judgment-holds' syntax for application); if not, you
>>> get the current `define-relation' behavior.
>>
>> My suggestion was meant to be separate from the overloading thing. You
>> could use a #:mode even for define-judgment.
>>
>
> Oh, I see. I like that. How do you feel about using the same style for
> contracts? For example:
>
> (define-judgment-form nats
>    #:mode (sum I I O)
>    #:contract (sum n n n)
>    [(sum z n n)]
>    [(sum (s n_1) n_2 (s n_3))
>     (sum n_1 n_2 n_3)])
>

I'm having trouble getting syntax/parse to produce good error messages
for this grammar. Here's a stripped down version of my best attempt:

(define-for-syntax (mode-keyword stx)
  (raise-syntax-error #f "keyword invalid outside of mode specification" stx))
(define-syntax I mode-keyword)
(define-syntax O mode-keyword)

(define-syntax (define-judgment-form stx)
  (define-syntax-class mode
    #:literals (I O)
    (pattern I)
    (pattern O))
  (define-syntax-class rule
    #:description "rule"
    (pattern [conc:expr prem:expr ...]))
  (syntax-parse stx
    [(_ (~or (~once (~seq #:mode (name-mode:id pos-mode:mode ...))
                    #:name "mode specification")
             (~optional (~seq #:contract (name-ctc:id pos-ctc:expr ...))
                        #:name "contract specification"))
        ...
        rule:rule ...)
     #''OK]))

This definition rejects the right uses, but I'm not satisfied with the
error message produced in this case:

(define-judgment-form
  #:contract (sum n n n)
  [(sum z n n )]
  [(sum (s n_1) n_2 (s n_3))
   (sum n_1 n_2 n_3)])

The error points to the first rule and says, "expected the literal
#:contract or expected the literal #:mode." I'd like it to say that
the mode spec is missing, since another contract spec just leads to a
different error.

I can get what I want by doing more of the parsing by hand, but I
wonder if there's an easier way than this:

(define-syntax (define-judgment-form stx)
  (define-syntax-class mode
    #:literals (I O)
    (pattern I)
    (pattern O))
  (define-syntax-class mode-spec
    #:description "mode specification"
    (pattern (name:id modes:mode ...)))
  (define-syntax-class contract-spec
    #:description "contract specification"
    (pattern (name:id contracts:expr ...)))
  (syntax-parse stx
    [(_ (~or (~seq #:mode mode:mode-spec)
             (~seq #:contract contract:contract-spec))
        ...
        rule ...)
     (let-values ([(name/mode mode)
                   (syntax-parse #'(mode ...)
                     [((name . mode)) (values #'name #'mode)]
                     [_ (raise-syntax-error #f "expected a mode
specification" stx)])]
                  [(name/ctc ctc)
                   (syntax-parse #'(contract ...)
                     [() (values #f #f)]
                     [((name . contract)) (values #'name #'contract)]
                     [(_ . dups)
                      (raise-syntax-error #f "expected at most one
contract specification"
                                          #f #f (syntax->list #'dups))])])
       #''OK)]))