btree - ACL2 Book

other

(in-package "ACL2")

other

(program)

car-cdr-depthfunction

(defun car-cdr-depth
  (name tree)
  (cond ((atom tree) (if (eq name tree)
        0
        nil))
    (t (let ((card (car-cdr-depth name (car tree))))
        (cond (card (+ 1 card))
          (t (let ((cdrd (car-cdr-depth name (cdr tree))))
              (cond (cdrd (+ 1 cdrd)) (t nil)))))))))

car-cdr-depth-lstfunction

(defun car-cdr-depth-lst
  (names tree)
  (cond ((endp names) nil)
    (t (cons (cons (car names) (car-cdr-depth (car names) tree))
        (car-cdr-depth-lst (cdr names) tree)))))

flattenfunction

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

node-cntfunction

(defun node-cnt
  (x)
  (cond ((atom x) 1)
    (t (+ (node-cnt (car x)) (node-cnt (cdr x))))))

log2function

(defun log2
  (n)
  (if (zp n)
    0
    (if (equal n 1)
      0
      (+ 1 (log2 (floor n 2))))))

full-treepfunction

(defun full-treep
  (x)
  (let ((cnt (node-cnt x)))
    (equal cnt (expt 2 (log2 cnt)))))

build-a-btree1mutual-recursion

(mutual-recursion (defun build-a-btree1
    (tree lst)
    (cond ((endp lst) tree)
      (t (build-a-btree1 (add-to-btree tree (car lst)) (cdr lst)))))
  (defun build-a-btree
    (lst)
    (build-a-btree1 (car lst) (cdr lst)))
  (defun add-to-btree
    (x n)
    (cond ((atom x) (cons x n))
      ((< (node-cnt (car x)) (node-cnt (cdr x))) (if (full-treep (cdr x))
          (let ((lst (flatten (cdr x))))
            (cons (add-to-btree (car x) (car lst))
              (build-a-btree (append (cdr lst) (list n)))))
          (cons (car x) (add-to-btree (cdr x) n))))
      (t (cons (car x) (add-to-btree (cdr x) n))))))

test-btreefunction

(defun test-btree
  (lst)
  (let ((tree (build-a-btree lst)))
    (list (list :tree tree)
      (cons :costs (car-cdr-depth-lst lst tree)))))