Отношение приведения в отверстии может соответствовать отверстию разными способами.

Question

У меня есть язык, определенный с помощью PLT-Redex, который имеет (динамические) типы миксинов. Выражения выглядят так:

; 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 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))

где мое отношение сокращения в настоящее время определено только для доступа к полю (lkp), где он сокращает поиск по миксину до его значения.

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

У меня есть тесты для моих мета-функций (fvalue), чтобы убедиться, что они работают. Однако redex говорит мне, что мое отношение редукции отображается на дыру разными способами. Неважно, комментирую ли я разные версии контекстов оценки дляnew C .... Ошибка исходит из этого места.

reduction-relation: in-hole's first argument is expected to match exactly one hole, but it may match a hole many different way

Как я могу отладить (или исправить) проблему? Обычно я работаю в режиме Emacs и Racket или использую DrRacket. Проблема в том, что при использовании Macro Stepper ошибка перебрасывается с одного шага на другой. Было бы неплохо, если бы я мог видеть дыры, которые он захватывает, чтобы даже понять, где он не работает. Так что, может быть, я понимаю, почему именно это не удается.

Answer 1

Я получаю ту же ошибку, если определяю язык со следующим определением контекстов (для простоты я буду использовать λ-подобный язык):

(E hole
   (E e ...)
   (v E ...))  ;; <-- problem

Это означает, например, что следующее E контекст:

((lambda (x y) x) hole hole)

Но (IIUC) Redex (или, по крайней мере, reduction-relation) не допускает контекстов с множеством дыр, поэтому жалуется.

Проблема в вашем коде, похоже, заключается в последних двух продуктах E, где Eпроисходит внутри узора, за которым следуют эллипсы. (Один из закомментированныхE Productions имеет ту же проблему.)