I can see why you might have expected that to work that way. Unfortunately, it doesn't. The identifiers in those places in shortcuts (Add2, x, and n in your examples below) are not pattern positions. They are simply identifiers.
In the code you wrote, one could change the rule's left-hand side to (+ V_1 V_2) to achieve the desired effect, but maybe that doesn't work in your larger model? Perhaps if you explained a little more why something like that is problematic, we could be of more use. Meanwhile, I've pushed a fix to the bug in the error-checking that you found, added some more checking, and tried to emphasize this point more clearly in the documentation. The commit cbb2d88b would probably have been the most helpful to you, but it's backwards incompatible, so it may need to be reverted. Robby On Fri, Dec 11, 2015 at 3:09 PM, Sam Caldwell <s...@ccs.neu.edu> wrote: > Hi, > > I'm working on a redex model where I want to constrain the shape of terms > used > to fill the hole in an evaluation context. I thought it would be fairly > straightforward to do so using a `with` clause in my reduction-relation, but > I've run into some difficulty, and consulting the docs [1] left me unsure of > where I went wrong. > > In the docs for `reduction-relation`, the old-arrow-name clause of shortcuts > are defined in terms of patterns and terms. However, the docs later say "The > left- and right-hand sides of a shortcut definition are identifiers, not > patterns and terms." I don't understand what is and is not allowed when > using > shortcuts. > > I have a small model that I think illustrates what I'm after. Say I have a > tiny addition language but for some reason I want to restrict reduction to > two-argument terms: > > ================================================================== > > #lang racket > > (require redex) > > (define-language add > (M (+ M ...) V) > (V natural) > (Add2 (+ V V)) > (E hole (+ V ... hole M ...))) > > (define red > (reduction-relation > add > (==> (+ V ...) > ,(apply + (term (V ...))) > +) > with > [(--> (in-hole E Add2) (in-hole E n)) > (==> Add2 n)])) > > ================================================================== > > This does not behave as I would have expected, for example reducing > `(term (+ 1 2 (+ 3 4) 4 (+ 0 1)))` down to `15`. > > It seems like the issue is that `Add2` in the shortcut is not being used as > a > pattern. For example, if I replace `Add2` with its definition: > > [(--> (in-hole E (name x (+ V V))) (in-hole E n)) > (==> x n)] > > I get the following error message: > > free-identifier=?: contract violation > expected: identifier? > given: #<syntax (name x any_2)> > argument position: 2nd > other arguments.: > > So my question boils down to: > 1) What is/is not allowed in each position when defining a shortcut? > 2) How can I constrain what is used to fill a hole, as attempted in my > example? > > Thanks, > Sam Caldwell > > [1] > http://docs.racket-lang.org/redex/The_Redex_Reference.html#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._reduction-relation%29%29 > > -- > 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.
