Re: [racket-users] Parameterized Redex models

As far as I understand, your ‘length-ok’ is implementing in Redex the ‘(<= (length ___) ___)’ I had in my ‘side-condition’. But I can’t see how it addresses two important features from my original code: (1) ‘k’ is parameterizable, and its value influences whether a list is valid or not; and

Re: [racket-users] Parameterized Redex models

If you want to stay inside redex-land, you have to do something like the code below, where you use typesetting to turn uses of length-ok (in other relations) into something like "#(l) = k". hth, Robby #lang racket (require redex) (define-term k 3) (define-language L) (define-judgment-form L

Re: [racket-users] Parameterized Redex models

> But I clearly don’t get what you really want so I will abandon this one. > > Good luck — Matthias > Thanks for trying, talking to you is always instructive  For people that hasn’t abandoned this one: I decided to bite the bullet and thread the ‘metaparameter’ in my definitions. This will

Re: [racket-users] Parameterized Redex models

> On Mar 15, 2018, at 12:35 PM, 'Leandro Facchinetti' via Racket Users > 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

Re: [racket-users] Parameterized Redex models

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

Re: [racket-users] Parameterized Redex models

> Stepping back a little bit here, if you were to write this down in a > way that were to make sense to a reader of a paper, how would you > communicate with them how/when this parameter changes? > When defining metafunctions/reduction relations/judgment forms and so on, authors generally

Re: [racket-users] Parameterized Redex models

Stepping back a little bit here, if you were to write this down in a way that were to make sense to a reader of a paper, how would you communicate with them how/when this parameter changes? I think we've already agreed that one can think of the entire paper and its development having exactly one

Re: [racket-users] Parameterized Redex models

This is going further in the wrong direction  1. The cache for the reduction relation is invalid. 2. There’s no way to parameterize ‘clock’ when calling the reduction relation (I think it’d really help to think of ‘k’ instead of ‘clock’). 3. ‘clock’ isn’t available to metafunctions called

Re: [racket-users] Parameterized Redex models

#lang racket (require redex) (require (for-syntax syntax/parse)) (define-syntax (r-r/tick stx) (syntax-parse stx [(_ PL #:domain x #:initial go #:observe o #:update u ((~literal -->) lhs rhs) ...) #'(let ((clock (go))) (reduction-relation PL #:domain x

Re: [racket-users] Parameterized Redex models

I see how this makes typesetting work. But I’m sorry but I don’t see how this program addresses any of my concerns: ‘clock’ is still unavailable to when defining ‘go’; and worse, there’s no way to set it from the outside. -- You received this message because you are subscribed to the Google

Re: [racket-users] Parameterized Redex models

#lang racket (require redex) (require (for-syntax syntax/parse)) (define-syntax (r-r/tick stx) (syntax-parse stx [(_ PL #:domain x ((~literal -->) lhs rhs) ...) #'(let ((clock 0)) (reduction-relation PL #:domain x (--> lhs rhs (where _ ,(set!

Re: [racket-users] Parameterized Redex models

Thanks for the clarification, I think I understand your proposal. And I see three problems: 1. I believe ‘traces/t’ is the evidence of the issue I brought up earlier: How do call sites know the form expects the extra argument? As your example demonstrates, call sites need to be explicit about

Re: [racket-users] Parameterized Redex models

How about this: #lang racket (require redex) (require (for-syntax syntax/parse)) (define-syntax (r-r/tick stx) (syntax-parse stx [(_ PL #:domain x ((~literal -->) lhs rhs) ...) #'(reduction-relation PL #:domain (x natural) (--> (lhs natural) (rhs ,(+ (term

Re: [racket-users] Parameterized Redex models

> On Mar 14, 2018, at 2:41 PM, 'Leandro Facchinetti' via Racket Users > wrote: > > > What if you wrote macros over reduction-relation instead of the exact model? > These macros could implement threading and hide it. They would kind of be > like monads here. —

Re: [racket-users] Parameterized Redex models

A related question is > to ask if maybe the parameter is intended to be so "dyanmic". Maybe > you should have to recompile the redex program to change the parameter > sometimes because, after all, if runs of the abstract machine with > different values of `k` interact with each other, maybe

Re: [racket-users] Parameterized Redex models

I guess most people already know this much, but one of the main ideas of the design of Redex is to support the notations that people actually use in their papers requiring only a minimal bit of information extra that lets us be able to actually run them. So, from this perspective, you're pointing

Re: [racket-users] Parameterized Redex models

> What if you wrote macros over reduction-relation instead of the exact > model? These macros could implement threading and hide it. They would kind > of be like monads here. — Matthias > Do you mean something like (define-parameterized-metafunction (k) L tick : e _ _ _ t -> t

Re: [racket-users] Parameterized Redex models

What if you wrote macros over reduction-relation instead of the exact model? These macros could implement threading and hide it. They would kind of be like monads here. — Matthias -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To

Re: [racket-users] Parameterized Redex models

> Yes, it looks like the original cache is just re-installed when re-enabled. > > Perhaps there should be an operation provided by Redex to clear away the > cache. > That’s one my proposals, yes  (see § Solutions on my original message) -- You received this message because you are

Re: [racket-users] Parameterized Redex models

Yes, it looks like the original cache is just re-installed when re-enabled. Perhaps there should be an operation provided by Redex to clear away the cache. David On Wed, Mar 14, 2018 at 2:17 PM, 'Leandro Facchinetti' via Racket Users < racket-users@googlegroups.com> wrote: > > First, thanks

Re: [racket-users] Parameterized Redex models

First, thanks for the reply. It’s valuable to have the author of the paper from where I draw my example chime in  1) Instead of turning the cache off completely, you could just invalidate the cache when the parameter changes, i.e. write a `set-k!' function that updates the parameter and

Re: [racket-users] Parameterized Redex models

Some small improvements to your suggestions: 1) Instead of turning the cache off completely, you could just invalidate the cache when the parameter changes, i.e. write a `set-k!' function that updates the parameter and toggles the cache off and back on (I assume this will clear it out). 3) Move