ACL2 как сохранить часть списка? - PullRequest
0 голосов
/ 18 октября 2018

Так что я все еще относительно новичок в 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))

1 Ответ

0 голосов
/ 18 октября 2018

Похоже, что он делает то, что вы хотите:

(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, - это запустить вспомогательную функцию с пустым аккумулятором.

Это довольно распространенный шаблон в Схеме, однако в Схеме вы можете определить вспомогательную функцию в той функции, в которой она вам нужна. :) Я не уверен, поддерживается ли она на используемом вами диалекте.с, поэтому я решил, что это безопасно.:)

...