省略了在歸約長期

Question

我試圖定義一個歸約元函數，它轉換爲對單個號碼的列表清單，如下所享有：

#lang racket 
(require redex) 

(define-language L 
    (e n ((n n) ...) (n ...)) 
    (n number)) 

(define-metafunction L 
    ((add-up n) n) 
    ((add-up ((e_1 e_2) ...)) (,(+ (term e_1) (term e_2)) ...))) 

然而，對於add-up ISN最後一個定義」 t接受 - Redex抱怨需要省略號的e_1和e_2，儘管它們已經低於一個省略號。有沒有一種方法可以將Recket應用到Redex的每個省略號的成員？

Answer 1

這裏的問題是，你有模式變量e_1和e_2與橢圓...分開（,）。 Redex模式匹配器不夠聰明，因爲您可以將任意球拍放在那裏。

但是，您可以做的是使用Racket結構（在本例中爲map）來合計您的號碼。該表達式將是這樣的：

,(map + (term (e_1 ...)) (term (e_2 ...))) 

或者把他們放在一起：

#lang racket 
(require redex) 

(define-language L 
    (e n ((n n) ...) (n ...)) 
    (n number)) 

(define-metafunction L 
    ((add-up n) n) 
    ((add-up ((e_1 e_2) ...)) ,(map + (term (e_1 ...)) (term (e_2 ...)))))