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 <stch...@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 > <ro...@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 <stch...@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 >>> <ro...@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)) _________________________ Racket Developers list: http://lists.racket-lang.org/dev