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

Oh, so 'test' is just something that you use in your test suite or in
the REPL or something? If so, you might be better off just using a
regular Racket function or macro for that.

Robby

On Wed, Aug 22, 2012 at 11:31 AM, Stephen Chang <stchang at ccs.neu.edu> wrote:
> 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))