On Friday, March 4, 2016 at 10:17:00 AM UTC-5, Andrew Kent 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
Ah, or perhaps I can use the standard #:binding-forms declarations and then just macro-generate definitions for substitution, alpha-equiv and free-variables from there (which should be easy with automatic freshening on matches?)? -- 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.
