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 out a weakness of Redex. And while I guess the embedding of Redex in Racket lets us cover a multitude of sins, perhaps the right way to think about this is how the parameter influences the model and how the reader of the paper understands how the parameter influences the model and then see if Redex can be extended to work in the same way. 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 nothing makes sense. Robby On Wed, Mar 14, 2018 at 1:41 PM, 'Leandro Facchinetti' via Racket Users <racket-users@googlegroups.com> 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. — Matthias > > > Do you mean something like > > (define-parameterized-metafunction (k) L > tick : e _ _ _ t -> t > [(tick e _ _ _ t) ,(take (cons (term e) (term t)) k)]) > > which would expand to > > (define-metafunction L > tick : e _ _ _ t _ -> t > [(tick e _ _ _ t k) ,(take (cons (term e) (term t)) k)]) > > ? > > How would the call sites of the metafunction know it expects the extra > argument? > > -- > 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.
