从还原关系中调用判断

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) returns 值的类型 v。据我所知，Redex 库中没有 where-judgment-holds 之类的东西，虽然我可以使用取消引号来解决它，但如果 Redex 中内置了一些东西就好了。

Answer 1

您要查找的内容实际上称为 judgment-holds，它在您的示例中恰好位于您放置 where-judgment-holds:

的位置

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

Invoke judgment from from within reduction-relation