CODEWITHSUNDEEP
listrecursionlispacl2
William Machado
William Machado

Reputation: 109

ACL2 how to keep part of a list?

So I am still relatively new to acl2 and lisp, I do not know of a way to do this in lisp. How can i go about achieving my comment?(cons a...) I keep thinking iterator, but i have been told ACL2 only uses recursion

(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))

Upvotes: 1

Views: 121

Answers (1)

Ashton Wiersdorf
Ashton Wiersdorf

Reputation: 2010

This looks like it does what you want:

(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 '()))

This works by creating an auxiliary function (first-n) which takes an accumulator variable. (acc) first-n calls itself, each time cons'ing on the first value of the input list. Once the input list is exhausted or n is 0, then the function reverses the accumulator and returns it.

Now, all keep-at-most-n-bits needs to do is fire off the helper function with an empty accumulator.

This is a fairly common pattern in Scheme—in Scheme, however, you can define the helper function within the function you need it in. :) I'm not sure if that's supported in the dialect you're working with, so I decided to play it safe like this. :)

Upvotes: 2

Related Questions