I have a language defined with PLT-Redex that has (dynamic) mixin types. Expressions look like the following:
; terms / expressions
(e ::= x
(lkp e f)
(call e m e ...)
(new C e ... ⊕ (e R e ...) ...)
(bind x ... with (e R e ...) ... from y ... e))
; values
(v ::= (new C v ... ⊕ (v R v ...) ...))
Evaluation of the language is done w.r.t. evaluation contexts and reduction-relations.
; evaluation contexts
(E ::= hole
(lkp E f) ; CR-FIELD
(call E m e ...) ; CR-INVK
(call v m v ... E e ...) ; CR-INVK-ARG
;(new C v ... E e ... ⊕ (e R e ...) ...)
;(new C v ... ⊕ (E R e ...) ...)
;(new C v ... ⊕ (v R v ... E e ...) ...)
(bind x ... with (E R e ...) ... from y ... e)
(bind x ... with (v R v ... E e ...) ... from y ... e))
where my reduction-relation is currently only defined for field access (lkp
) where it reduces a lookup on a mixin to its value.
(define red
(reduction-relation
fej
#:domain (e CT)
;R-FIELD
(--> ((in-hole E (lkp (new C v_0 ... ⊕ (v_1 R v_2 ...) ...) f_i)) CT)
((in-hole E v_i) CT)
"(R-FIELD)"
(where v_i (fvalue CT f_i (new C v_0 ... ⊕ (v_1 R v_2 ...) ...))))
))
I have tests for my meta-functions (fvalue
) to verify that they work. However, redex tells me that my reduction-relation maps to a hole in many different ways. It does not matter if I comment the different versions of evaluation contexts for new C ...
. The error comes from this place.
reduction-relation: in-hole's first argument is expected to match exactly one hole, but it may match a hole many different way
How can I debug (or fix) the problem? Normally, I develop with Emacs and Racket mode or use DrRacket. The problem is when using Macro Stepper the error is thrown from one step to another. Would be nice if I could see the holes it captures to even understand where it fails. So I maybe understand why it fails exactly.
I get the same error if I define a language with the following definition of contexts (for simplicity, I'll use a λ
-like language):
(E hole
(E e ...)
(v E ...)) ;; <-- problem
That means, for example, the following is an E
context:
((lambda (x y) x) hole hole)
But (IIUC) Redex (or at least reduction-relation
) doesn't allow contexts with multiple holes, so it complains.
The problem in your code seems to be in the last two productions of E
, where E
occurs inside a pattern that is followed by ellipses. (One of the commented-out E
productions has the same problem.)