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]> 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]. > 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.
