racket - 省略号在 redex 术语中取消引用

Question

我正在尝试定义一个 Redex 元函数，它将对列表转换为单个数字列表，如下所示：

#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不接受最后一个定义 - Redex 抱怨e_1并e_2要求省略号，尽管它们已经低于一个省略号。有没有办法将球拍取消引用应用于 Redex 中省略号的每个成员？

Answer 1

这里的问题是您有模式变量e_1，并通过取消引号 ( )e_2与省略号分隔。Redex 模式匹配器不够聪明，无法查看取消引号，因为您可以将任意 Racket 放在那里。...,

但是，您可以做的是使用 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 ...)))))