Отверстие редукционного отношения может соответствовать дыре многими различными способами. - PullRequest
Новая
       27

Отверстие редукционного отношения может соответствовать дыре многими различными способами.

4 голосов
/ 28 января 2020

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

; 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), где он уменьшает поиск в mixin до его значения. 

(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 ошибка переходит от одного шага к другому. Было бы хорошо, если бы я мог видеть дыры, которые он захватывает, чтобы даже понять, где это терпит неудачу. Так что, может быть, я понимаю, почему это именно так.

1 Ответ

3 голосов
/ 28 января 2020

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

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

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

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

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

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

...