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.
