还原关系的内孔可能以多种不同方式匹配孔

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）定义，在字段访问中将对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 ...的评估上下文的不同版本都没有关系。错误来自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

如何调试（或修复）问题？通常，我使用Emacs和Racket模式进行开发或使用DrRacket。问题是使用宏步进器时，错误从一个步骤抛出到另一步骤。如果我能看到它捕获的漏洞甚至了解它失败的地方，那将是很好的。所以我也许理解为什么它会完全失败。

Answer 1

如果使用以下上下文定义定义语言，则会出现相同的错误（为简单起见，我将使用类似λ的语言：]

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

例如，这意味着E上下文：

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

但是（IIUC）Redex（或至少为reduction-relation）不允许具有多个漏洞的上下文，因此会抱怨。

您的代码中的问题似乎出在E的最后两个生成中，其中E出现在模式中，其后是椭圆。 （其中一个已注释掉的E产品具有相同的问题。）