ACL2如何保存列表的一部分？答案

【问题标题】：ACL2 how to keep part of a list?ACL2如何保存列表的一部分？
【发布时间】：2018-10-18 16:59:32
【问题描述】：

所以我对 acl2 和 lisp 还比较陌生，我不知道在 lisp 中如何做到这一点。我怎样才能实现我的评论？（缺点...）我一直在思考迭代器，但有人告诉我 ACL2 只使用递归

(defun keep-at-most-n-bits (l n)
   ;cons a (up to n) 

   )

;;;unit tests.
(check-expect (keep-at-most-n-bits '(1 0 1 1) 3)  '(1 0 1))
(check-expect (keep-at-most-n-bits '(1 0 1 1) 2)  '(1 0))
(check-expect (keep-at-most-n-bits '(1 0 1 1) 8)  '(1 0 1 1))

【问题讨论】：

标签： list recursion lisp acl2

【解决方案1】：

这看起来像你想要的：

(defun first-n (lst n acc)
  (if (or (= n 0) (eq lst nil))
      (reverse acc)
    (first-n (cdr lst) (- n 1) (cons (car lst) acc))))

(defun keep-at-most-n-bits (l n)
  (first-n l n '()))

这是通过创建一个辅助函数 (first-n) 来实现的，该函数接受一个累加器变量。 (acc) first-n 调用自身，每次都使用输入列表的第一个值。一旦输入列表用完或n为0，则该函数将累加器反转并返回。

现在，keep-at-most-n-bits 需要做的就是用一个空的累加器触发辅助函数。

这是 Scheme 中相当常见的模式——但是，在 Scheme 中，您可以在需要它的函数中定义辅助函数。:) 我不确定您正在使用的方言是否支持它，所以我决定像这样安全地玩。 :)

【讨论】：