4

我有一种用 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 ...) ...))

语言的评估是通过评估上下文和归约关系来完成的。

; 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。问题是当使用宏步进器时，错误会从一个步骤抛出到另一个步骤。如果我能看到它捕获的孔甚至了解它失败的地方，那就太好了。所以我也许明白为什么它完全失败了。

4

1 回答 1

3

如果我使用以下上下文定义定义语言，我会得到同样的错误（为简单起见，我将使用λ-like 语言）：

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

这意味着，例如，以下是一个E上下文：

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

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

您的代码中的问题似乎出在 的最后两个产生中E，其中E出现在后面跟着省略号的模式中。（其中一个被注释掉的E产品也有同样的问题。）

于 2020-01-28T15:18:34.693 回答