PSA - careful using side-conditions in PLT Redex! (I'd stick to 'where' clauses, personally)
The fact that side-conditions exist in both metafunctions/reduction-relations *and* judgment-forms but are *not* in fact the same thing (i.e. those found in the former accept racket expressions, the latter accepts terms) can lead to nasty, subtle little bugs if you're not careful. (yes the difference is documented, however it's still really easy to hang yourself with them if you forget the subtle distinction in a sufficiently complicated model, IMHO). For example, consider a little language which models propositional logic: (define-language propositional-logic [φ ::= variable-not-otherwise-mentioned] [Γ ::= (φ ...)]) (define-judgment-form propositional-logic #:mode (proves I I) #:contract (proves Γ φ) ;; ... [(side-condition (memq (term φ) (term Γ))) -------------------------------- "L-Assumption" (proves Γ φ)] ;; ... ) (test-equal (judgment-holds (proves (P) P)) #t) (test-equal (judgment-holds (proves (P) Q)) #f) ;; <-- fails test! Uh oh, why did our second test fail? Ah yes, but of course! We forgot that in a judgment-form, side-condition will end up quoting Racket expressions (since it accepts terms) and so the condition '(side-condition (memq (term φ) (term Γ)))' is always true. Although what we wrote would have worked as a guard in a metafunction definition, that same code here behaves differently. We should have written (side-condition ,(memq (term φ) (term Γ))) to escape to Racket and actually call 'memq' on the arguments. Because of this, I try to idiot proof things by *always* just use 'where' clauses since they behave the same everywhere. This has worked quite well for me thus far. Anyway, that's all I've got to say about that. Thanks for PLT Redex! Everyone should attend the PLT Redex summer school next year! (Assuming there is one... =) -Andrew -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. For more options, visit https://groups.google.com/d/optout.
