[racket-dev] Am I misusing judgment-holds ?

I'm using it as a side condition so if I need to typeset, I can just
add a wrapper macro to make it look nicer?

Something like:

#lang racket
(require redex)

(define-language L
  (e integer true false)
  (τ bool int))

(define-judgment-form L
  #:mode (⊢_ I O)
  #:contract (⊢_ e τ)
  [(⊢_ integer int)]
  [(⊢_ true bool)]
  [(⊢_ true bool)])

(define-syntax (⊢ stx)
  (syntax-case stx ()
    [(_ e τ)
     #'(member (term τ) (judgment-holds (⊢_ e τ_1) τ_1))]))

(define-metafunction L
  [(test e τ) e
   (side-condition (⊢ e τ))
   (side-condition (printf "τ = ~a\n" (term τ)))])


Welcome to DrRacket, version 5.3.0.16 [3m].
Language: racket [custom].
> (term (test 1 int))
τ = int
1
> (term (test 1 bool))
. . plt/collects/redex/private/error.rkt:3:0: test: no clauses matched
for (test 1 bool)





On Wed, Aug 22, 2012 at 11:31 AM, Robby Findler
<robby at eecs.northwestern.edu> wrote:
> This is kind of awkward, tho. Do you plan to typeset this portion of your model?
>
> Robby
>
> On Wed, Aug 22, 2012 at 10:07 AM, Stephen Chang <stchang at ccs.neu.edu> wrote:
>> Oh yeah, this first solution should work (I want to keep it as an
>> output though). Thanks.
>>
>>
>> On Wed, Aug 22, 2012 at 9:01 AM, Robby Findler
>> <robby at eecs.northwestern.edu> wrote:
>>> You could do the below, but can you say a little bit more about what
>>> the metafunction and judgment-form you want to combine are?
>>> (Presumably they both are type checking?)
>>>
>>> #lang racket
>>> (require redex)
>>>
>>> (define-language L
>>>   (e integer true false)
>>>   (τ bool int))
>>>
>>> (define-judgment-form L
>>>   #:mode (⊢ I O)
>>>   #:contract (⊢ e τ)
>>>   [(⊢ integer int)]
>>>   [(⊢ true bool)]
>>>   [(⊢ false bool)])
>>>
>>> (define-metafunction L
>>>   [(type-checks? e τ)
>>>    ,(member (term τ) (judgment-holds (⊢ e τ) τ))
>>>    (side-condition (printf "τ = ~a\n" (term τ)))])
>>>
>>> (term (type-checks? true int))
>>> (term (type-checks? true bool))