racketplt-redexredex

Reduction-relation's in-hole may match a hole many different ways


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.


Solution

  • 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.)