+1 On Friday, August 28, 2015, Matthias Felleisen <[email protected]> wrote:
> > Yes, the inconsistency is frustrating. We are keeping it for backwards > compatibility but it should be overcome with the addition of a different > form of s-e in the future. Lucky you, we drilled ‘exampling’ and ‘testing’ > at the summer school so that you caught this small problem before it causes > a big one in context — Matthias > > > > > > On Aug 28, 2015, at 12:44 PM, Andrew Kent <[email protected] > <javascript:;>> wrote: > > > > 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] <javascript:;>. > > For more options, visit https://groups.google.com/d/optout. > > -- > 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] <javascript:;>. > For more options, visit https://groups.google.com/d/optout. > -- 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.
