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 中内置了一些东西会很好。

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