racket - リダクション関係内から判断を呼び出す

Question

次のように、キャストとサブタイプを持つ言語の定義に取り組んでいます。

(define-language base 
  (t ::= int any) 
  (e ::= number (cast t e)) 
  #| stuff ... |#)

次に、それに対して次の判断フォームを定義します。

(define-judgment-form base
   #:mode (<: I I)
   #:contract (<: t t)
   [------ 
    (<: t t)]
   [------ 
    (<: int any)])

そして今、私の還元関係では、次のようなものを書きたいです

(define b-> (reduction-relation base
    (--> (cast t v)
         v
         (where-judgment-holds (<: (typeof v) t)))))

(typeof v)値の型を返すと仮定しますv。私が知る限りwhere-judgment-holds、Redex ライブラリにはそのようなものはありません。引用符を外して回避することはできますが、Redex に何かが組み込まれているとよいでしょう。

score 3 · Accepted Answer

あなたが実際に探しているものはと呼ばれjudgment-holds、あなたの例ではあなたが置いた場所で正確に機能しますwhere-judgment-holds:

(define b-> (reduction-relation base
    (--> (cast t v)
         v
         (judgment-holds (<: (typeof v) t)))))

1 に答える 1