You are right that we didn't do a good job of making this limitation clear and the error message is indeed pretty horrible.
Your suggestion of having the #:binding-forms declarations effectively turn into metafunction-based definitions of substitution et al makes sense as an approach worth trying. We could special case those metafunctions when doing matching to call directly into the more efficient Racket versions, but keep the more standard metafunctions around for doing generation. If you do give that a try, please let us know how it does! Robby On Fri, Mar 4, 2016 at 9:17 AM, Andrew Kent <sgt...@gmail.com> wrote: > I have been really itching to use Redex's awesome random testing for a model > I'm working with. > > Also, I have been really enjoying the #:binding-forms feature for defining > languages. > > Unfortunately, these two features seem not fully compatible: you cannot use a > judgment which requires 'substitute' to restrict term generation since > 'substitute' is implemented with raw Racket code, which is incompatible with > the #:satisfying option. > > (side note: this restriction appears to still be a secret known only to the > Redex elders and those who have been initiated (i.e. the docs don't mention > this limitation)). > > So I just wanted to ask if anyone had any pointers/suggestions at this point? > > At the moment, I'm thinking of creating some macros which help users (well at > least me for the moment) define Redex languages (and their binding > constructs) in a way which is _entirely_ compatible w/ the constraints > #:satisfying imposes. > > I imagine this will involve using a wrapper around something like Peano-style > naturals instead of raw symbols for language variables (so fresh variables > can be generated in a way that does not require any raw Racket code). From > there I think I can write some macros that generate metafunctions for > substitution, alpha equivalence, and free-variables which are entirely > compatible with #:satisfying. Unfortunately I wont get automatic "freshening" > of binders in my metafunctions/judgments like you currently do when declaring > #:binding-forms =( > > Anyway, am I totally crazy here? Any thoughts? > > Thanks, > 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 racket-users+unsubscr...@googlegroups.com. > 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 racket-users+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
