Search code examples
listrecursionlispacl2

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

Solution

  • 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. :)