racket - Reduction-relation 的 in-hole 可能以多种不同的方式匹配一个孔

Question

我有一种用 PLT-Redex 定义的语言，它具有(动态)mixin 类型。表达式如下所示:

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

语言的评估是在 w.r.t.评估上下文和减少关系。

; 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 作品之一也有同样的问题。)