> On Mar 15, 2018, at 12:35 PM, 'Leandro Facchinetti' via Racket Users > <[email protected]> wrote: > > > Robby’s message dominates mine but I don’t get why you can’t work your way > thru what I provided. > > I don’t see the connection between the issue I brought up and what you > provided. In your program ‘r-r/tick’ is a form to define a reduction relation > which manages ‘clock’, but then ‘clock’ can’t determine the behavior of the > reduction relation (and it isn’t cached by Redex). Note that ‘r-r/tick’ says > ‘(where _ ,(begin (set! clock (u clock)) (o clock)))’, which means the > outputs of the ‘observer’ are ignored. Now, we could modify ‘r-r/tick’ to > take a pattern ‘p’ and say ‘(where p ,(begin (set! clock (u clock)) (o > clock)))’. B
Indeed, there are many ways to get exactly what you’re asking for in this paragraph. This is one of them. But I clearly don’t get what you really want so I will abandon this one. Good luck — Matthias > but then we’re getting further and further away from my intent: having ‘k’ as > an implicit argument to a collection of definitions (metafunctions, judgment > forms, and so forth), beyond a single reduction relation. > > HUH? This is something that you control with the initialization function. The > REDEX results are the same. It is up to your init function to cache or not > cache. > > But if my function doesn’t cache and the reduction relation depends on > ‘clock’ (see previous paragraph), then the Redex results would differ. > > > No, ‘#:initial’ let’s you parameterize ‘clock’ when *defining* the > > reduction relation (‘r-r/tick’), not when *calling* it (‘traces’, > > ‘apply-reduction-relation’ and friends). > > > Really? > > (define *foo 0) > (define (init) .. *foo ..) > > I assume you’re proposing to pass ‘init’ to ‘#:initial’, and then ‘(set! *foo > ___)’ to control the reduction relation’s behavior. And that starts to look > like a dynamically bound variable—better yet, a Racket parameter. We’re on > the right track: Racket parameters is how we got started, and I’m proposing > we need them at the Redex level as well 😀 > > > (define-metafunction X > > [(my-metafunction _) clock]) ;; <= ‘clock’ is just a symbol here, not a > > bound (meta-)variable > > > What does this even mean? Racket-Redex is about variables not symbols. > > Right, Racket–Redex is about variables, but ‘clock’ in ‘my-metafunction’ > isn’t a variable, it’s literally the symbol ‘'clock’. > > * * * > > I feel we’re getting into the weeds and having different conversations. Can I > kindly ask you re-read my original message with a fresh pair of eyes? > > By the way: *thank you all* for the conversation thus far, and for building > Redex in the first place. As usual I’m learning a lot from interacting with > you. > > -- > 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.
