Redex passt nicht

Question

Eine übliche Art Semantik definieren ist (zum Beispiel):

return v if [some other condition] 
otherwise, return error 

Betrachten wir zum Beispiel

(define-language simple-dispatch 
    (e ::= v (+ e e)) 
    (v ::= number string) 
    (res ::= e err) 
    (E ::= hole (+ E e) (+ v E))) 

Wir könnten dann

(define s-> (reduction-relation simple-dispatch 
    #:domain res 
    (--> (in-hole E (+ number_1 number_2)) 
     (in-hole E ,(+ number_1 number_2))) 
    (--> (in-hole E (+ any any)) 
     err))) 

die Reduktion Beziehung definieren

Dies ist der natürliche Weg, dies zu tun, da es nicht erforderlich ist, individuelle Matcher für jeden der 3 Fehlerfälle zu schreiben (num String, String Nummer, String String). Allerdings schafft es dann das Problem, dass es wie folgt ausgeführt werden:

(apply-reduction-relation s-> (term (+ 2 2))) 

Shows (richtig), dass es Sie beide können auf einen Fehler reduzieren oder auf die Zahl 4. Gibt es eine Möglichkeit, eine „Ausnahme“ Muster zu machen das vermeidet es, alle konstituierenden Fälle zu überprüfen?

Answer 1

Was Sie hier verwenden möchten, ist eine Kombination aus side-condition und redex-match?. Erweiterung Ihrer Reduktions-Beziehung gibt:

(define s-> (reduction-relation simple-dispatch 
    #:domain res 
    (--> (in-hole E (+ number_1 number_2)) 
     (in-hole E ,(+ (term number_1) (term number_2)))) 
    (--> (in-hole E (+ any_1 any_2)) 
     err 
     (side-condition 
     (not (redex-match? simple-dispatch 
          (+ number number) 
          (term (+ any_1 any_2)))))))) 

Dies sagt Ihnen nur die zweite Regel so lange dauern kann als der erste nicht wahr ist, das ist, was die Papiere implizit sagen, und hat ziehen einfach nicht aus ausdrücklich in der Figur. (Beachten Sie, dass Sie side-condition/hidden verwenden können, damit die Seitenbedingung beim Rendern der Figur nicht gezeichnet wird).

Sie können diese Methode verwenden, um auf eine beliebige Anzahl von Mustern zu skalieren, die Sie nicht zulassen möchten.