Re: [racket-users] Redex: difficulty with #refers-to

2017-06-27 Thread 'William J. Bowman' via Racket Users
On Tue, Jun 27, 2017 at 07:21:48PM -0500, Robby Findler wrote:
> On Tue, Jun 27, 2017 at 3:23 PM, 'William J. Bowman' via Racket Users
>  wrote:
> > (Unfortunately, there is a known bug in Redex that #...bind is 
> > undocumented, so you had no way to know about this)
> 
> I agree that #:...bind is complex and the documentation is not ideal,
> but I believe you helped me improve it, so I'm not that known bug is
> really the most helpful reply here. Perhaps a pointer to the docs is
> better. Here it is:
> 
> https://plt.eecs.northwestern.edu/snapshots/current/doc/redex/The_Redex_Reference.html#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._define-language%29%29
Oh I didn't realize that documentation was live already. Should the bug be 
closed?
(this should probably go off-list)

--
William J. Bowman

-- 
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.


signature.asc
Description: PGP signature


Re: [racket-users] Redex: difficulty with #refers-to

2017-06-27 Thread Robby Findler
On Tue, Jun 27, 2017 at 3:23 PM, 'William J. Bowman' via Racket Users
 wrote:
> (Unfortunately, there is a known bug in Redex that #...bind is undocumented, 
> so you had no way to know about this)

I agree that #:...bind is complex and the documentation is not ideal,
but I believe you helped me improve it, so I'm not that known bug is
really the most helpful reply here. Perhaps a pointer to the docs is
better. Here it is:

https://plt.eecs.northwestern.edu/snapshots/current/doc/redex/The_Redex_Reference.html#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._define-language%29%29

Meanwhile, Justin, I wasn't able to make your example work exactly the
way you had it, but with an extra pair of parens around the `d`s thing
seem fine.

#lang racket
(require redex/reduction-semantics)

(define-language L
  (p ::= (prog (d ...) e))
  (d ::= (defun (x x) e))
  (e ::= x (e e) (+ e e) natural)
  (x ::= variable-not-otherwise-mentioned)
  #:binding-forms
  (defun (x_fun x_param) e #:refers-to x_param) #:exports x_fun
  (prog (d ...) #:refers-to (shadow d ...)
e_main #:refers-to (shadow d ...)))

(term (substitute (prog ((defun (f x) (g x))
 (defun (g x) (f (+ x y
(+ (f 1) (g 2)))
  f
  1)
  #:lang L)

hth,
Robby

-- 
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.


Re: [racket-users] Redex: difficulty with #refers-to

2017-06-27 Thread Justin Pombrio
On Tuesday, June 27, 2017 at 4:23:35 PM UTC-4, William J. Bowman wrote:
> On Tue, Jun 27, 2017 at 09:21:59AM -0700, Justin Pombrio wrote:
> > I'm trying to define a language in Redex that includes a list of top-level 
> > function definitions:
> > 
> >   (p ::= 
> > (prog (defun (x x) e) ... e))
> > 
> > And all function names should be in scope in all function bodies (other 
> > things should be in scope as well, but I'm ignoring them here for 
> > simplicity):
> > 
> >   (prog (defun (x_fun x_param) e_body #:refers-to (shadow x_fun ...)) ...
> > e_main))
> This looks ill-formed to me. Inside e_body, there is only one x_fun bound, so 
> x_fun ... doesn't make
> sense.
> This would make sense if you had a multi-argument functions, e.g.,
>(prog (defun (x_fun x ...) e_body #:refers-to (shadow x ...)) ...
>  e_main))
> 
> You're trying to express a more complicated binding pattern than merely a 
> list of binders.
> This is expressing that each definition d inside (prog d ...) exports a name 
> that is bound for all other definitions.
> You need #:exports.
> Maybe something like
>(defun (x_fun x ...) e_body #:refers-to (shadow x ...)) #:exports x_fun
>(prog d #:...bind (defs d (shadows defs d
> 
> This may not be quite right yet.
> 
> (Unfortunately, there is a known bug in Redex that #...bind is undocumented, 
> so you had no way to know about this)
> 
> --
> William J. Bowman

Ah, thanks Will.

-- 
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.


Re: [racket-users] Redex: difficulty with #refers-to

2017-06-27 Thread 'William J. Bowman' via Racket Users
On Tue, Jun 27, 2017 at 09:21:59AM -0700, Justin Pombrio wrote:
> I'm trying to define a language in Redex that includes a list of top-level 
> function definitions:
> 
>   (p ::= 
> (prog (defun (x x) e) ... e))
> 
> And all function names should be in scope in all function bodies (other 
> things should be in scope as well, but I'm ignoring them here for simplicity):
> 
>   (prog (defun (x_fun x_param) e_body #:refers-to (shadow x_fun ...)) ...
> e_main))
This looks ill-formed to me. Inside e_body, there is only one x_fun bound, so 
x_fun ... doesn't make
sense.
This would make sense if you had a multi-argument functions, e.g.,
   (prog (defun (x_fun x ...) e_body #:refers-to (shadow x ...)) ...
 e_main))

You're trying to express a more complicated binding pattern than merely a list 
of binders.
This is expressing that each definition d inside (prog d ...) exports a name 
that is bound for all other definitions.
You need #:exports.
Maybe something like
   (defun (x_fun x ...) e_body #:refers-to (shadow x ...)) #:exports x_fun
   (prog d #:...bind (defs d (shadows defs d

This may not be quite right yet.

(Unfortunately, there is a known bug in Redex that #...bind is undocumented, so 
you had no way to know about this)

--
William J. Bowman

-- 
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.


signature.asc
Description: PGP signature