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的类型。据我所知，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)))))