racket - リレーションシップのインホールは、さまざまな方法でホールに一致する可能性があります

Question

(動的) mixin タイプを持つ 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 ...。エラーはこの場所から来ています。

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 を使用します。問題は、マクロ ステッパーを使用すると、あるステップから別のステップにエラーがスローされることです。どこで失敗したかを理解するために、それがキャプチャする穴を見ることができればいいと思います. だから、なぜそれが正確に失敗するのか理解できるかもしれません。