On Wednesday, October 14, 2015 at 7:47:27 AM UTC-4, Andrew Kent wrote: > On Saturday, September 19, 2015 at 1:21:19 PM UTC-4, Robby Findler wrote: > > Paul Stansifer has been implementing the ideas from his dissertation > > work in Redex and is now ready to share them with the world. > > > > Thanks to Paul, Redex languages now understand binding structure, > > meaning that if you write a substitution function that just blindly > > substitutes, it will actually properly do alpha conversion to avoid > > name collisions. In general, pattern matching now has alpha > > equivalence smarts (see the docs for more). > > > > The new features include the #:binding keyword in define-language and > > extend-language, and the alpha-equivalent? and substitute functions. > > > > The plan is to let it stay only in Paul's repo until the next release > > goes out and then push it to the main Redex repo to be included in the > > release after this one. If you'd like to give it a try, some > > instructions are below. Please let us know how it goes! > > > > Robby > > > > > > -------------------------------- > > > > To try it out, first download a snapshot build: > > > > http://pre.racket-lang.org/installers/ > > > > and then create a parent directory to hold the git repo for Redex: > > > > cd PLTDIR; mkdir extra-pkgs; cd extra-pkgs > > > > run this command to get the git version of Redex: > > > > raco pkg update --clone redex \ > > "git://github.com/racket/redex?path=redex" \ > > "git://github.com/racket/redex?path=redex-benchmark" \ > > "git://github.com/racket/redex?path=redex-doc" \ > > "git://github.com/racket/redex?path=redex-examples" \ > > "git://github.com/racket/redex?path=redex-gui-lib" \ > > "git://github.com/racket/redex?path=redex-lib" \ > > "git://github.com/racket/redex?path=redex-pict-lib" \ > > "git://github.com/racket/redex?path=redex-test" > > > > and then get Paul's version: > > > > cd redex > > git remote add paul https://github.com/paulstansifer/redex-1.git > > git checkout public > > raco setup > > First, just want to say I'm loving this feature so far! Thank you. > > One quick question---I have something failing to work, and I'm not sure if > it's a bug, or a feature/capability that's not supported (yet?): > > [;; other details ... > --------------- "S-Refine" > (subtype Δ (Refine [x : S] Q) (Refine [x : T] P))] > > I was hoping that sort of case in a judgment would (1) auto-magically perform > substitution such that any two refinements would be made in terms of the same > variable, and (2) that variable x would be fresh with respect to the other > arguments (i.e. Δ). > > It seems like (2) holds, but (1) does not. For example, this test case does > not even successfully match on this judgment rule: > > (test-equal > (term (subtype (Env ([y : Int]) ()) > (Refine [x : Int] (≤ x y)) > (Refine [z : Int] (≤ z y)))) > #t) > > Thanks, > Andrew
Oh! And I was also curious if a 'free-identifiers' function (similar to 'alpha-equivalent?' and 'substitute') is on a list of future features, perhaps? That would be another nice piece of boilerplate to throw away once binding info is specified for a language... Thanks again for the awesome new features! =) -- 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.
