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 <[email protected]> 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 <[email protected]> > 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 <[email protected]> > 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 < > [email protected]> 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 [email protected]. > > > >> 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 [email protected]. > > > 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 [email protected]. > > 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 [email protected]. > 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 [email protected]. For more options, visit https://groups.google.com/d/optout.
