Thanks! Regarding feature (1), that might be hard to implement because of the internal design of the freshener. But could you send me the Redex model in question so I can poke at it anyways?
`free-identifiers` should be pretty easy to make. What does it tend to be useful for? Paul On Wed, Oct 14, 2015 at 7:47 AM, Andrew Kent <sgt...@gmail.com> 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 > > -- > You received this message because you are subscribed to a topic in the > Google Groups "Racket Users" group. > To unsubscribe from this topic, visit > https://groups.google.com/d/topic/racket-users/CjFIFEhTEj8/unsubscribe. > To unsubscribe from this group and all its topics, 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.
