Invoke Urteil aus Reduktions-Beziehung

Question

ich auf, die eine Sprache gerade arbeite, die Abgüsse und Subtypisierung hat wie folgt:

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

ich folgendes Urteil bilden über sie dann definieren:

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

Und jetzt, in meiner Reduktion Beziehung, möchte ich so etwas wie

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

schreiben, wo wir tha nehmen t (typeof v) gibt den Typ des Werts v zurück. Soweit ich das beurteilen kann, gibt es in der Redex-Bibliothek nichts Vergleichbares wie where-judgment-holds, und obwohl ich es mit einer unquote umgehen könnte, wäre es schön, wenn etwas in Redex eingebaut wäre.

Answer 1

Was Sie suchen tatsächlich judgment-holds genannt, und es funktioniert genau in Ihrem Beispiel, wo Sie setzen where-judgment-holds:

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