Great! I've pushed it. Hopefully the docs make it clear how to define
the C you wanted earlier. If they don't let me know and I'll fix 'em.
Robby
On Wed, May 8, 2019 at 11:21 AM William J. Bowman
wrote:
>
> Yeah, I think I would be.
>
> On Wed, May 08, 2019 at 11:13:12AM -0500, Robby Findler
Yeah, I think I would be.
On Wed, May 08, 2019 at 11:13:12AM -0500, Robby Findler wrote:
> Hi William: are you agreeing that if redex added a new pattern that
> you would be in good shape or not?
>
> Thanks,
> Robby
>
> On Wed, May 8, 2019 at 10:05 AM William J. Bowman
> wrote:
> >
> > On Wed,
Hi William: are you agreeing that if redex added a new pattern that
you would be in good shape or not?
Thanks,
Robby
On Wed, May 8, 2019 at 10:05 AM William J. Bowman
wrote:
>
> On Wed, May 08, 2019 at 08:31:26AM -0500, Robby Findler wrote:
> > On Tue, May 7, 2019 at 9:19 PM William J. Bowman
On Wed, May 08, 2019 at 08:31:26AM -0500, Robby Findler wrote:
> On Tue, May 7, 2019 at 9:19 PM William J. Bowman
> wrote:
> >
> > On Tue, May 07, 2019 at 03:55:09PM -0500, Robby Findler wrote:
> > > I can agree that the current definition isn't the best one, but this
> > > one doesn't seem
On Tue, May 7, 2019 at 9:19 PM William J. Bowman
wrote:
>
> On Tue, May 07, 2019 at 03:55:09PM -0500, Robby Findler wrote:
> > I can agree that the current definition isn't the best one, but this
> > one doesn't seem right. I mean, this requires that both sides step? It
> > is a kind of parallel
On Tue, May 07, 2019 at 03:55:09PM -0500, Robby Findler wrote:
> I can agree that the current definition isn't the best one, but this
> one doesn't seem right. I mean, this requires that both sides step? It
> is a kind of parallel reduction? That doesn't seem like something
> commonly wanted.
On Mon, May 6, 2019 at 2:11 PM William J. Bowman
wrote:
>
> I took a quick look at the implementation of `cross` and `compatible-closure`,
> and couldn't make sense of any of it.
> For now, I guess I'll manually write out the contexts, and discuss a feature
> request.
>
> I spoke to Max a bit
I took a quick look at the implementation of `cross` and `compatible-closure`,
and couldn't make sense of any of it.
For now, I guess I'll manually write out the contexts, and discuss a feature
request.
I spoke to Max a bit about what a compatible closure "ought" to be for mutually
defined
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
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
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
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
(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
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
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
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
16 matches
Mail list logo
