I just ported Cur to use this version of Redex (https://github.com/wilbowma/cur/tree/redex-with-binding), and was able to delete and simplify many lines of code and get all tests passing in minutes. Hurrah! Although, I do not have interesting binding structure.
A few comments 0. Was very easy; kudos. The new Redex build was completely backwards compatible, and all changes to my code were simplifications, such as deleting my hand-rolled α-equivalence relation, and deleting substitution. 1. It was not obvious to me that /binding-pattern/ was not just a grammar but a pattern. I tried to specify binding with: #:binding-forms (Π (x : t) t #:refers-to x), but this caused problems until I changed it to: #:binding-forms (Π (x : t_0) t_1 #:refers-to x) 2. default-lang was not properly linked in at least one place in the documentation (in the explanation of default-equiv). 3. I'm getting some seriously long names, making output rather unreadable. The output of some of my tests: '(λ (x159160161162 : Bool) x159160161162) '(λ (x168169170171172 : Bool) x168169170171172) '(λ (x178179180181182183 : Bool) x178179180181182183) '(λ (x189190191192193194195 : Bool) x189190191192193194195) Previously, this output was '(λ (x2 : Bool) x2) '(λ (x1 : Bool) x1) '(λ (x2 : Bool) x2) '(λ (x1 : Bool) x1) -- William J. Bowman On Sat, Sep 19, 2015 at 12:21:17PM -0500, 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 > > -- > 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.
pgpGTGix3Meza.pgp
Description: PGP signature
