Re: [racket-users] Redex compatible closure of mutually defined nonterminals

[Robby Findler]

I just kind of made up the algorithm for what Redex does. It seems to
coincide with what one expects for some cases at least. :)

Robby

On Fri, May 3, 2019 at 9:09 PM William J. Bowman 
wrote:

> I can't seem to use (cross t).
> If it were as easy as (C ::= (cross t) (cross v)), I'd be sufficiently
> happy.
> But alas:
>   https://github.com/racket/redex/issues/92
>   https://github.com/racket/redex/issues/54
>   https://github.com/racket/redex/pull/147
>
> I'll see about tweaking Redex, but now I'm wondering what to call this
> "closure".
> To me, it's the obvious compatible closure, but apparently not.
> (It's the one the paper I'm reading calls "the congruence closure", as far
> as I
> can tell; the definition is missing, hence my Redex modeling.)
>
> --
> William J. Bowman
>
> On Fri, May 03, 2019 at 09:00:34PM -0500, Robby Findler wrote:
> > There isn't a simple way to do that using the exported  stuff currently
> but
> > those nonterminals are hiding inside and one could expose them in the
> > pattern language I think. (TT is accessible via (cross t) I think.)
> > definitely requires fiddling with intervals but the work would be more
> > exposing and documenting and the like, not really deep changes.
> >
> > But there may be a clever way to make it work with the existing APIs? I
> am
> > not sure.
> >
> > Robby
> >
> > On Fri, May 3, 2019 at 8:38 PM William J. Bowman  >
> > wrote:
> >
> > > Ah, I see.
> > > Those are the VT and TT I want, but then I also want to define:
> > >
> > > (C ::= VT TT)
> > >
> > > and take the context-closure of C.
> > > (see attached)
> > >
> > > Can I get my hands on the generated VT and TT easily, or would I need
> to
> > > tweak
> > > Redex internals to automate this?
> > >
> > > --
> > > William J. Bowman
> > >
> > > On Fri, May 03, 2019 at 07:52:09PM -0500, Robby Findler wrote:
> > > > (thunk TT) isn't a TT, tho? It will reduce only in a TT.
> > > >
> > > > Robby
> > > >
> > > > On Fri, May 3, 2019 at 7:16 PM William J. Bowman <
> w...@williamjbowman.com>
> > > wrote:
> > > > >
> > > > > That looks like the contexts I want, but it doesn't seem to reduce
> > > under a (thunk TT) in my example model.
> > > > >
> > > > > --
> > > > > Sent from my phoneamajig
> > > > >
> > > > > > On May 3, 2019, at 20:02, Robby Findler <
> ro...@cs.northwestern.edu>
> > > wrote:
> > > > > >
> > > > > > Redex, when asked to create the compatible closure, creates a
> context
> > > > > > and then uses that. In this case, it will create a context
> something
> > > > > > like this:
> > > > > >
> > > > > > TT ::= hole | (\ (x) TT) | (TT v) | (t VT) | (force VT) |
> (return VT)
> > > > > > VT ::= (thunk TT)
> > > > > >
> > > > > > If you want something else (I'm not sure of an algorithm to
> handle
> > > > > > this kind of thing without coming with something like that), it
> might
> > > > > > be simplest to write out the contexts that you want directly and
> use
> > > > > > context-closure.
> > > > > >
> > > > > > Robby
> > > > > >
> > > > > >> On Fri, May 3, 2019 at 6:42 PM William J. Bowman <
> > > w...@williamjbowman.com> wrote:
> > > > > >>
> > > > > >> Hello all,
> > > > > >>
> > > > > >> I'm trying to define a model in Redex where values and terms are
> > > separate
> > > > > >> nonterminals, and then define a reduction relation using
> > > `compatible-closure`
> > > > > >> to lift the small steps to the, well, compatible closure.
> > > > > >> Unfortunately, it doesn't do what I expect, presumably because
> the
> > > nonterminals
> > > > > >> for values and terms are mutually defined, but
> `compatible-closure`
> > > takes
> > > > > >> exactly one nonterminal.
> > > > > >>
> > > > > >> Is there a way to do what I want?
> > > > > >> See attached.
> > > > > >>
> > > > > >> --
> > > > > >> 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.
> > > > >
> > > > > --
> > > > > 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.
> > >
> > > --
> > > You received this message because you are subscribed to the Google
> Groups
> > > "Racket Users" group.
> > > To unsubscribe from 

Re: [racket-users] Redex compatible closure of mutually defined nonterminals

[William J. Bowman]

I can't seem to use (cross t).
If it were as easy as (C ::= (cross t) (cross v)), I'd be sufficiently happy.
But alas:
  https://github.com/racket/redex/issues/92
  https://github.com/racket/redex/issues/54
  https://github.com/racket/redex/pull/147

I'll see about tweaking Redex, but now I'm wondering what to call this
"closure".
To me, it's the obvious compatible closure, but apparently not.
(It's the one the paper I'm reading calls "the congruence closure", as far as I
can tell; the definition is missing, hence my Redex modeling.)

--
William J. Bowman

On Fri, May 03, 2019 at 09:00:34PM -0500, Robby Findler wrote:
> There isn't a simple way to do that using the exported  stuff currently but
> those nonterminals are hiding inside and one could expose them in the
> pattern language I think. (TT is accessible via (cross t) I think.)
> definitely requires fiddling with intervals but the work would be more
> exposing and documenting and the like, not really deep changes.
> 
> But there may be a clever way to make it work with the existing APIs? I am
> not sure.
> 
> Robby
> 
> On Fri, May 3, 2019 at 8:38 PM William J. Bowman 
> wrote:
> 
> > Ah, I see.
> > Those are the VT and TT I want, but then I also want to define:
> >
> > (C ::= VT TT)
> >
> > and take the context-closure of C.
> > (see attached)
> >
> > Can I get my hands on the generated VT and TT easily, or would I need to
> > tweak
> > Redex internals to automate this?
> >
> > --
> > William J. Bowman
> >
> > On Fri, May 03, 2019 at 07:52:09PM -0500, Robby Findler wrote:
> > > (thunk TT) isn't a TT, tho? It will reduce only in a TT.
> > >
> > > Robby
> > >
> > > On Fri, May 3, 2019 at 7:16 PM William J. Bowman 
> > wrote:
> > > >
> > > > That looks like the contexts I want, but it doesn't seem to reduce
> > under a (thunk TT) in my example model.
> > > >
> > > > --
> > > > Sent from my phoneamajig
> > > >
> > > > > On May 3, 2019, at 20:02, Robby Findler 
> > wrote:
> > > > >
> > > > > Redex, when asked to create the compatible closure, creates a context
> > > > > and then uses that. In this case, it will create a context something
> > > > > like this:
> > > > >
> > > > > TT ::= hole | (\ (x) TT) | (TT v) | (t VT) | (force VT) | (return VT)
> > > > > VT ::= (thunk TT)
> > > > >
> > > > > If you want something else (I'm not sure of an algorithm to handle
> > > > > this kind of thing without coming with something like that), it might
> > > > > be simplest to write out the contexts that you want directly and use
> > > > > context-closure.
> > > > >
> > > > > Robby
> > > > >
> > > > >> On Fri, May 3, 2019 at 6:42 PM William J. Bowman <
> > w...@williamjbowman.com> wrote:
> > > > >>
> > > > >> Hello all,
> > > > >>
> > > > >> I'm trying to define a model in Redex where values and terms are
> > separate
> > > > >> nonterminals, and then define a reduction relation using
> > `compatible-closure`
> > > > >> to lift the small steps to the, well, compatible closure.
> > > > >> Unfortunately, it doesn't do what I expect, presumably because the
> > nonterminals
> > > > >> for values and terms are mutually defined, but `compatible-closure`
> > takes
> > > > >> exactly one nonterminal.
> > > > >>
> > > > >> Is there a way to do what I want?
> > > > >> See attached.
> > > > >>
> > > > >> --
> > > > >> 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.
> > > >
> > > > --
> > > > 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.
> >
> > --
> > 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.

-- 
You received this message because you are 

Re: [racket-users] Redex compatible closure of mutually defined nonterminals

[Robby Findler]

There isn't a simple way to do that using the exported  stuff currently but
those nonterminals are hiding inside and one could expose them in the
pattern language I think. (TT is accessible via (cross t) I think.)
definitely requires fiddling with intervals but the work would be more
exposing and documenting and the like, not really deep changes.

But there may be a clever way to make it work with the existing APIs? I am
not sure.

Robby

On Fri, May 3, 2019 at 8:38 PM William J. Bowman 
wrote:

> Ah, I see.
> Those are the VT and TT I want, but then I also want to define:
>
> (C ::= VT TT)
>
> and take the context-closure of C.
> (see attached)
>
> Can I get my hands on the generated VT and TT easily, or would I need to
> tweak
> Redex internals to automate this?
>
> --
> William J. Bowman
>
> On Fri, May 03, 2019 at 07:52:09PM -0500, Robby Findler wrote:
> > (thunk TT) isn't a TT, tho? It will reduce only in a TT.
> >
> > Robby
> >
> > On Fri, May 3, 2019 at 7:16 PM William J. Bowman 
> wrote:
> > >
> > > That looks like the contexts I want, but it doesn't seem to reduce
> under a (thunk TT) in my example model.
> > >
> > > --
> > > Sent from my phoneamajig
> > >
> > > > On May 3, 2019, at 20:02, Robby Findler 
> wrote:
> > > >
> > > > Redex, when asked to create the compatible closure, creates a context
> > > > and then uses that. In this case, it will create a context something
> > > > like this:
> > > >
> > > > TT ::= hole | (\ (x) TT) | (TT v) | (t VT) | (force VT) | (return VT)
> > > > VT ::= (thunk TT)
> > > >
> > > > If you want something else (I'm not sure of an algorithm to handle
> > > > this kind of thing without coming with something like that), it might
> > > > be simplest to write out the contexts that you want directly and use
> > > > context-closure.
> > > >
> > > > Robby
> > > >
> > > >> On Fri, May 3, 2019 at 6:42 PM William J. Bowman <
> w...@williamjbowman.com> wrote:
> > > >>
> > > >> Hello all,
> > > >>
> > > >> I'm trying to define a model in Redex where values and terms are
> separate
> > > >> nonterminals, and then define a reduction relation using
> `compatible-closure`
> > > >> to lift the small steps to the, well, compatible closure.
> > > >> Unfortunately, it doesn't do what I expect, presumably because the
> nonterminals
> > > >> for values and terms are mutually defined, but `compatible-closure`
> takes
> > > >> exactly one nonterminal.
> > > >>
> > > >> Is there a way to do what I want?
> > > >> See attached.
> > > >>
> > > >> --
> > > >> 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.
> > >
> > > --
> > > 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.
>
> --
> 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.

Re: [racket-users] Redex compatible closure of mutually defined nonterminals

[William J. Bowman]

Ah, I see.
Those are the VT and TT I want, but then I also want to define:

(C ::= VT TT)

and take the context-closure of C.
(see attached)

Can I get my hands on the generated VT and TT easily, or would I need to tweak
Redex internals to automate this?

--
William J. Bowman

On Fri, May 03, 2019 at 07:52:09PM -0500, Robby Findler wrote:
> (thunk TT) isn't a TT, tho? It will reduce only in a TT.
> 
> Robby
> 
> On Fri, May 3, 2019 at 7:16 PM William J. Bowman  
> wrote:
> >
> > That looks like the contexts I want, but it doesn't seem to reduce under a 
> > (thunk TT) in my example model.
> >
> > --
> > Sent from my phoneamajig
> >
> > > On May 3, 2019, at 20:02, Robby Findler  wrote:
> > >
> > > Redex, when asked to create the compatible closure, creates a context
> > > and then uses that. In this case, it will create a context something
> > > like this:
> > >
> > > TT ::= hole | (\ (x) TT) | (TT v) | (t VT) | (force VT) | (return VT)
> > > VT ::= (thunk TT)
> > >
> > > If you want something else (I'm not sure of an algorithm to handle
> > > this kind of thing without coming with something like that), it might
> > > be simplest to write out the contexts that you want directly and use
> > > context-closure.
> > >
> > > Robby
> > >
> > >> On Fri, May 3, 2019 at 6:42 PM William J. Bowman 
> > >>  wrote:
> > >>
> > >> Hello all,
> > >>
> > >> I'm trying to define a model in Redex where values and terms are separate
> > >> nonterminals, and then define a reduction relation using 
> > >> `compatible-closure`
> > >> to lift the small steps to the, well, compatible closure.
> > >> Unfortunately, it doesn't do what I expect, presumably because the 
> > >> nonterminals
> > >> for values and terms are mutually defined, but `compatible-closure` takes
> > >> exactly one nonterminal.
> > >>
> > >> Is there a way to do what I want?
> > >> See attached.
> > >>
> > >> --
> > >> 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.
> >
> > --
> > 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.

-- 
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.
#lang racket/base

(require
 redex/reduction-semantics)

(define-language λvL
  (x ::= variable-not-otherwise-mentioned)

  (v w ::= (thunk t) () x)

  (t u ::= (λ (x) t) (t v) (force v) (return v))

  (TT ::= hole (λ (x) TT) (TT v) (t VT) (force VT) (return VT))
  (VT ::= (thunk TT))

  (C ::= VT TT)

  ;; How do I tell redex to compatible-close over both v and t?
  (anyterm ::= v t)

  #:binding-forms
  (λ (x) any_1 #:refers-to x))

(define λv-->
  (reduction-relation
   λvL
   (--> ((λ (x) t) v)
(substitute t x v)
"β")
   (--> (force (thunk t)) t
"force")))

(define λv-->*
  (context-closure λv--> λvL C))

(test-->
 λv-->
 (term ((λ (x) (force (thunk (return x ()))
 (term (force (thunk (return ())

(test-->>
 λv-->*
 (term ((λ (x) (force (thunk (return x ()))
 (term (return (

(test-->>
 λv-->*
 (term (λ (x) (force (thunk (return x)
 (term (λ (x) (return x

;; Fails, since thunk is a v, not a t.
(test-->>
 λv-->*
 (term (thunk (λ (x) (force (thunk (return x))
 (term (thunk (λ (x) (return x)

Re: [racket-users] Redex compatible closure of mutually defined nonterminals

[Robby Findler]

(thunk TT) isn't a TT, tho? It will reduce only in a TT.

Robby

On Fri, May 3, 2019 at 7:16 PM William J. Bowman  
wrote:
>
> That looks like the contexts I want, but it doesn't seem to reduce under a 
> (thunk TT) in my example model.
>
> --
> Sent from my phoneamajig
>
> > On May 3, 2019, at 20:02, Robby Findler  wrote:
> >
> > Redex, when asked to create the compatible closure, creates a context
> > and then uses that. In this case, it will create a context something
> > like this:
> >
> > TT ::= hole | (\ (x) TT) | (TT v) | (t VT) | (force VT) | (return VT)
> > VT ::= (thunk TT)
> >
> > If you want something else (I'm not sure of an algorithm to handle
> > this kind of thing without coming with something like that), it might
> > be simplest to write out the contexts that you want directly and use
> > context-closure.
> >
> > Robby
> >
> >> On Fri, May 3, 2019 at 6:42 PM William J. Bowman  
> >> wrote:
> >>
> >> Hello all,
> >>
> >> I'm trying to define a model in Redex where values and terms are separate
> >> nonterminals, and then define a reduction relation using 
> >> `compatible-closure`
> >> to lift the small steps to the, well, compatible closure.
> >> Unfortunately, it doesn't do what I expect, presumably because the 
> >> nonterminals
> >> for values and terms are mutually defined, but `compatible-closure` takes
> >> exactly one nonterminal.
> >>
> >> Is there a way to do what I want?
> >> See attached.
> >>
> >> --
> >> 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.
>
> --
> 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.

Re: [racket-users] Redex compatible closure of mutually defined nonterminals

[William J. Bowman]

That looks like the contexts I want, but it doesn't seem to reduce under a 
(thunk TT) in my example model.

-- 
Sent from my phoneamajig

> On May 3, 2019, at 20:02, Robby Findler  wrote:
> 
> Redex, when asked to create the compatible closure, creates a context
> and then uses that. In this case, it will create a context something
> like this:
> 
> TT ::= hole | (\ (x) TT) | (TT v) | (t VT) | (force VT) | (return VT)
> VT ::= (thunk TT)
> 
> If you want something else (I'm not sure of an algorithm to handle
> this kind of thing without coming with something like that), it might
> be simplest to write out the contexts that you want directly and use
> context-closure.
> 
> Robby
> 
>> On Fri, May 3, 2019 at 6:42 PM William J. Bowman  
>> wrote:
>> 
>> Hello all,
>> 
>> I'm trying to define a model in Redex where values and terms are separate
>> nonterminals, and then define a reduction relation using `compatible-closure`
>> to lift the small steps to the, well, compatible closure.
>> Unfortunately, it doesn't do what I expect, presumably because the 
>> nonterminals
>> for values and terms are mutually defined, but `compatible-closure` takes
>> exactly one nonterminal.
>> 
>> Is there a way to do what I want?
>> See attached.
>> 
>> --
>> 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.

-- 
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 compatible closure of mutually defined nonterminals

[Robby Findler]

Redex, when asked to create the compatible closure, creates a context
and then uses that. In this case, it will create a context something
like this:

TT ::= hole | (\ (x) TT) | (TT v) | (t VT) | (force VT) | (return VT)
VT ::= (thunk TT)

If you want something else (I'm not sure of an algorithm to handle
this kind of thing without coming with something like that), it might
be simplest to write out the contexts that you want directly and use
context-closure.

Robby

On Fri, May 3, 2019 at 6:42 PM William J. Bowman  
wrote:
>
> Hello all,
>
> I'm trying to define a model in Redex where values and terms are separate
> nonterminals, and then define a reduction relation using `compatible-closure`
> to lift the small steps to the, well, compatible closure.
> Unfortunately, it doesn't do what I expect, presumably because the 
> nonterminals
> for values and terms are mutually defined, but `compatible-closure` takes
> exactly one nonterminal.
>
> Is there a way to do what I want?
> See attached.
>
> --
> 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.

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

[racket-users] Redex compatible closure of mutually defined nonterminals

[William J. Bowman]

Hello all,

I'm trying to define a model in Redex where values and terms are separate
nonterminals, and then define a reduction relation using `compatible-closure`
to lift the small steps to the, well, compatible closure.
Unfortunately, it doesn't do what I expect, presumably because the nonterminals
for values and terms are mutually defined, but `compatible-closure` takes
exactly one nonterminal.

Is there a way to do what I want?
See attached.

-- 
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.
#lang racket/base

(require
 redex/reduction-semantics)

(define-language λvL
  (x ::= variable-not-otherwise-mentioned)

  (v w ::= (thunk t) () x)

  (t u ::= (λ (x) t) (t v) (force v) (return v))

  ;; How do I tell redex to compatible-close over both v and t?
  (anyterm ::= v t)

  #:binding-forms
  (λ (x) any_1 #:refers-to x))

(define λv-->
  (reduction-relation
   λvL
   (--> ((λ (x) t) v)
(substitute t x v)
"β")
   (--> (force (thunk t)) t
"force")))

; This ought to reduce under vs, as well ts, since they are mutually defined.
; But it only uses t.
(define λv-->*
  (compatible-closure λv--> λvL t))

; Doesn't work, but in a different way.
#;(define λv-->*
  (compatible-closure λv--> λvL anyterm))

(test-->
 λv-->
 (term ((λ (x) (force (thunk (return x ()))
 (term (force (thunk (return ())

(test-->>
 λv-->*
 (term ((λ (x) (force (thunk (return x ()))
 (term (return (

(test-->>
 λv-->*
 (term (λ (x) (force (thunk (return x)
 (term (λ (x) (return x

;; Fails, since thunk is a v, not a t.
(test-->>
 λv-->*
 (term (thunk (λ (x) (force (thunk (return x))
 (term (thunk (λ (x) (return x)

Re: [racket-users] Beginning of the end for googlegroups?

[Steve Byan]

> On Jan 25, 2019, at 7:48 PM, Jack Rosenthal  wrote:
> 
> On Fri, 25 Jan 2019 at 23:59 +0100, 'Paulo Matos' via Racket Users wrote:
>> Not sure of the size of the mailing list but I wonder if this is the
>> beginning of the end and we should have instead a plan B.
> 
> We could always go back to Mailman…

Why not groups.io?

-- 
Steve Byan
st...@byan-roper.org



-- 
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] escape ~ in scribble's bib-entry

[stewart mackenzie]

I'm humbled,

I'll use `scheme-full`, thanks to you Ben and Leif for your time and
assistance.

I'll keep in mind that technique for better errors.

kr/sjm

On Sat, 4 May 2019, 01:47 Ben Greenman,  wrote:

> With `scheme-full`, we were able to build a pdf.
>

-- 
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] escape ~ in scribble's bib-entry

[Ben Greenman]

It's definitely a TeX issue.

Leif Andersen and I were able to reproduce the error (thanks Leif!).

Then we ran `scribble --latex test.scrbl` to make a .tex file and
`pdflatex test.tex` for a nicer error message.

The message gives a hint that the texlive `scheme-basic` is not enough:

```
cannot open Type 1 font file for reading
```

With `scheme-full`, we were able to build a pdf. Here's our `shell.nix`:

```
{ nixpkgs ?  
, pkgs ? import nixpkgs {}
}:
with pkgs;
let
latex = texlive.combine {
  inherit (texlive)
scheme-full
;};
in
pkgs.mkShell {
  buildInputs = [
racket
latex
  ];
}
```

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

[racket-users] Can phase-1 transformer bindings be overridden locally?

[Eric Griffis]

I have a macro that creates transformer bindings at phases 0 and 1:

(define-syntax (f stx)
  (with-syntax ([name (cadr (syntax-e stx))])
#'(begin
(define-syntax name (syntax-id-rules () [_ 1]))
(begin-for-syntax (define-syntax name (syntax-id-rules () [_
2]))

Normally, this works fine. I have syntax transformers bound at both phases
that can resolve "name" with syntax-local-value.

In an expression context, the phase-0 transformer binding can be
overridden temporarily with let-syntax:

(cons
 x (let-syntax
   ([x (syntax-id-rules () [_ 'one])]
[y (λ (stx) (datum->syntax stx (syntax-local-value #'x)))])
 (list x y)))

This produces '(1 one #). With syntax-local-eval instead
of syntax-local-value, it produces '(1 one 2).

Because "f" produces begin-for-syntax, it only works in a module or
top-level evaluation context:

(let () (f x) x)

/tmp/g.rkt:10:8: begin-for-syntax: not in a definition context
  in: (begin-for-syntax (define-syntax x (syntax-id-rules () (_ 2

Is there a way to override temporarily the phase-1 transformer binding as
well?

Eric

-- 
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] I wrote my first macro ever!

[Jérôme Martin]

> https://www.mail-archive.com/racket-users@googlegroups.com/msg40201.html

This was effectively the best writing I could read about syntax-parse 
templates and the quirks of using ~@ and ~?.
Thank you so much Alexis for those explanations! You rock.

On Tuesday, April 30, 2019 at 10:12:15 PM UTC+2, David Storrs wrote:
>
> Congratulations on dipping into the macro world!  It is an interesting, 
> terrifying, and often frustrating experience. :>
>
> I see that you've already read Fear of Macros, which is great.  In 
> addition to FoM, one of the most useful resources I've found for 
> understanding ... in macros has been Alexis King's module 'struct-update', 
> the code for which is linked below.  In addition, she provides a very good 
> explanation of ... in this thread: 
> https://www.mail-archive.com/racket-users@googlegroups.com/msg40196.html 
> which could supplement what Jérôme Martin said below.
>
> HTH,
>
> Dave
>
> struct-update docs: https://docs.racket-lang.org/struct-update/index.html
> struct-update code: 
> https://github.com/lexi-lambda/struct-update/blob/master/struct-update-lib/struct-update/main.rkt
>

-- 
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] Stack trace

[Mark Engelberg]

If you open up the details of BSL and select to enable tracing, and run my
example, you do indeed see a stack trace in a panel on the right:
 (sub2 2)
 (reciprocal 0)

However, there are clearly some limitations to this tracing mechanism, when
my student tried to enable tracing on his big-bang program, running the
program caused the whole thing to blow up with the error:
syntax-original?: expects a syntax, given '...signature-syntax.rkt:58:42

Is this a bug in the tracing mechanism, or a known limitation?

The stepper works great for simple expressions to build understanding of
evaluation processes, but for a larger big-bang program, where the
underlying model has potentially been changed by multiple tick and handler
functions, it offers little assistance for determining what the model is at
the time of error, and how it got that way.

If tracing is not easily available in BSL, my ideal would be that every
error prints out not only the function/line where the error occurred, but
also the input(s) to the function which triggered the error.  (Example: a
function containing a cond, and every branch tests as false, so it reports
an error -- but it currently doesn't tell you what the input was which
caused all the cases to fall through).  Even without a full stacktrace,
that would be incredibly useful. It gives you something to reason about,
something to build a failing test case which you can then try to fix.
Any preferences or settings that can be tweaked to achieve something like
this? I showed my student how to build an else case with (error x) to print
the value of input x if all the cases fall through, but would prefer a more
automatic approach.

--Mark


On Thu, May 2, 2019 at 4:15 PM John Clements 
wrote:

> Well, I see two things going on here.
>
> First, this example is an interesting one, because there’s no stack trace
> to display; the (/ 1 n) is the only “frame” left on the “stack”, because
> the call to sub2 has already returned, and the body of “reciprocal” is in
> tail position with respect to the call. If you add a “(+ 1 …)” around the
> reciprocal call, then there’s a stack to display…
>
> …except that you still won’t see an arrow in BSL, because that’s a #lang
> racket thing. That is: if you change the language to “Use language defined
> in source”, and insert #lang racket at the beginning, and add a (+ 1 …)
> around the reciprocal, and run the program, you’ll see an arrow from the (/
> 1 n) to the (+ 1 …) context as I believe you expected.
>
> I think the pedagogically correct answer here is that the arrows that you
> see in racket aren’t really the “right thing” for an educational setting.
> Instead, I think I might suggest using the stepper, instead. (Me? Biased?)
> In this case, I think I would jump to the end of the evaluation, and then
> step backward to see where the error came from.
>
> I also think that there’s probably value in the “tree-cer” approach that
> Krishnamurthi et al. have been working on[*] for Pyret, which shows the
> evaluation of a term as a single large tree, allowing you to inspect each
> call and the arguments that were passed to each call.
>
> John
>
> [*] I thought of it independently, but they thought of it first, and
> actually implemented it. :)
>
>
> > On May 2, 2019, at 4:02 PM, Mark Engelberg 
> wrote:
> >
> > Working with a student in DrRacket for the first time in a while.
> >
> > I notice that in BSL, an error in a function does not tell you what
> input to the function caused the error, nor does it show the stack trace by
> drawing arrows in the definitions window the way I remember.
> >
> > When did this behavior change? Is there a way to turn on better error
> reporting and stack traces?
> >
> > Example:
> >
> > (define (reciprocal n)
> >   (/ 1 n))
> >
> > (define (sub2 n)
> >   (- n 2))
> >
> > (define a (reciprocal (sub2 2)))
> >
> >
> >
> > --
> > 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.

Re: [racket-users] Re: Racket News - Issue 7

['Paulo Matos' via Racket Users]

Hi Stephen,

Great to hear you're enjoying RN and enjoyed my choice of Automata via
Macros for this issue.

It's always exciting to hear that people are enjoying these issues.

All the best,
Paulo Matos

On 02/05/2019 22:13, Stephen Foster wrote:
> Yes!  Years ago, "Automata via Macros" was the paper that helped me see
> that macros are cool. :)  Thanks for including that.
> 
> I've been enjoying these Racket News issues!
> 
> On Wednesday, May 1, 2019 at 7:21:56 AM UTC-7, Paulo Matos wrote:
> 
> Issue 7 is here.
> 
> http://racket-news.com/2019/05/racket-news-issue-7.html
> 
> 
> Americano time, enjoy!
> -- 
> Paulo Matos
> 
> -- 
> 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.

-- 
Paulo Matos

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