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.
