03.acl2

;; 3.10
(defun fib (n)
  (cond
   ((zp n) 1)
   ((= n 1) 1)
   (t
    (+ (fib (- n 1))
       (fib (- n 2))))))

;; 3.11
(defun pascal (i j)
  (cond ((not (and (integerp i) (integerp j))) 0)
        ((= i j) 1)
        ((< i j) 0)
        ((= j 0) 1)
        ((< i 0) 0)
        ((< j 0) 0)
        (t (+ (pascal (- i 1) (- j 1))
              (pascal (- i 1) j)))))



(defun mem (e x)
  (if (endp x)
      nil
    (if (equal e (car x))
        t
      (mem e (cdr x)))))

;; 3.12
(defun subset (x y)
  (cond ((endp x) t)
        ((mem (car x) y) (subset (cdr x) y))
        (t nil)))

;; 3.13
(defun dedup (in out)
  (cond ((and (atom out) (not (null out))) '())
        ((endp in) out)
        ((mem (car in) out) (dedup (cdr in) out))
        (t (dedup (cdr in) (cons (car in) out)))))

(defun un (x y)
  (dedup (append x y) '()))

;; 3.14
(defun int (x y)
  (cond ((endp x) '())
        ((mem (car x) y) (cons (car x) (int (cdr x) y)))
        (t (int (cdr x) y))))

;; 3.15
(defun diff (x y)
  (cond ((endp x) '())
        ((mem (car x) y) (diff (cdr x) y))
        (t (cons (car x) (diff (cdr x) y)))))

;; 3.16
(defun rev (x)
  (if (endp x)
      '()
    (append (rev (cdr x)) (list (car x)))))

;; 3.17
(defun insert (i l)
  (cond ((endp l) (list i))
        ((<= i (car l)) (cons i l))
        (t (cons (car l) (insert i (cdr l))))))

(defun isort (l)
  (if (endp l)
      '()
    (let ((tail (isort (cdr l))))
      (insert (car l) tail))))

;; binary trees

(defun sum-tips (x)
  (if (atom x)
      x
    (+ (sum-tips (car x))
       (sum-tips (cdr x)))))

(defun replace-tips (old new x)
  (if (atom x)
      (if (equal x old)
          new
        x)
    (cons (replace-tips old new (car x))
          (replace-tips old new (cdr x)))))

;; 3.18

(defun flatten (x)
  (if (atom x)
      (list x)
    (append (flatten (car x))
            (flatten (cdr x)))))

;; 3.19

(defun swap-tree (x)
  (if (atom x)
      x
    (cons (swap-tree (cdr x))
          (swap-tree (car x)))))

;; 3.20

(defun depth (x)
  (if (atom x)
      0
    (+ 1 (max (depth (car x))
              (depth (cdr x))))))

;; 3.21

(defun subtree (tree path)
  (cond ((endp path) tree)
        ((endp tree)tree)
        ((equal (car path) 'a) (subtree (car tree) (cdr path)))
        ((equal (car path) 'd) (subtree (cdr tree) (cdr path)))
        (t nil)))

;; 3.22

(defun replace-subtree (p new x)
  (cond ((endp p) new)
        ((endp x) x)
        ((equal (car p) 'a)
         (cons (replace-subtree (cdr p) new (car x))
               (cdr x)))
        ((equal (car p) 'd)
         (cons (car x)
               (replace-subtree (cdr p) new (cdr x))))
        (t nil)))


;; 3.23

(defun deep-tip (x)
  (if (atom x)
      (mv x 0)
    (mv-let (lft-val lft-depth)
        (deep-tip (car x))
      (mv-let (rt-val rt-depth)
          (deep-tip (cdr x))
        (if (> lft-depth rt-depth)
            (mv lft-val (+ lft-depth 1))
          (mv rt-val (+ rt-depth 1)))))))


(defun fact (n)
  (declare (xargs :guard (and (integerp n) (<= 0 n))
                  :measure (acl2-count n)))
  (if (zp n)
      1
    (* n (fact (- n 1)))))