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
