types-misc

(defun kwassoc
  (x default alist)
  (cond ((atom alist) default)
    ((eq x (caar alist)) (cdar alist))
    (t (kwassoc x default (cdr alist)))))

(defun strip-keywords
  (list)
  (if (atom list)
    (mv list nil)
    (if (keywordp (car list))
      (mv-let (slist keyalist)
        (strip-keywords (cddr list))
        (mv slist (cons (cons (car list) (cadr list)) keyalist)))
      (mv-let (slist keyalist)
        (strip-keywords (cdr list))
        (mv (cons (car list) slist) keyalist)))))

(defun munge-components
  (components)
  (if (atom components)
    nil
    (cons (mv-let (compo kwalist)
        (strip-keywords (car components))
        (if (consp compo)
          (if (consp (cdr compo))
            (list* (cadr compo) (car compo) kwalist)
            (list* (car compo) nil kwalist))
          (list* compo nil kwalist)))
      (munge-components (cdr components)))))

(defun appsyms1
  (symbols)
  (if (atom symbols)
    nil
    (if (atom (cdr symbols))
      symbols
      (list* (car symbols) '- (appsyms1 (cdr symbols))))))

(defun packsyms1
  (lst)
  (cond ((null lst) "")
    (t (concatenate 'string
        (symbol-name (car lst))
        (packsyms1 (cdr lst))))))

(defun packsyms (lst) (intern (packsyms1 lst) "ACL2"))

(defun appsyms (symbols) (packsyms (appsyms1 symbols)))

(defun component-name (component) (car component))

(defun component-type (component) (cadr component))

(defun component-kwalist (component) (cddr component))

(defun product-name (product) (caar product))

(defun product-components (product) (cdar product))

(defun product-kwalist (product) (cdr product))

(defun components-names
  (components)
  (if (atom components)
    nil
    (cons (component-name (car components))
      (components-names (cdr components)))))

(defun accessor-name
  (product component)
  (appsyms (list (product-name product) (component-name component))))

(defun accessor-list
  (product components)
  (if (consp components)
    (cons (accessor-name product (car components))
      (accessor-list product (cdr components)))
    nil))

(defun tm-split-list
  (half rest first)
  (if (zp half)
    (mv (reverse first) rest)
    (tm-split-list (1- half) (cdr rest) (cons (car rest) first))))

(defun argtree
  (cons args)
  (cond ((endp args) nil)
    ((endp (cdr args)) (car args))
    (t (mv-let (first second)
        (tm-split-list (floor (len args) 2) args nil)
        `(,CONS ,(ARGTREE CONS FIRST) ,(ARGTREE CONS SECOND))))))

(defun recog-consp-list
  (nargs obj)
  (if (zp nargs)
    `((eq ,OBJ nil))
    (if (= nargs 1)
      '(t)
      (let ((flo (floor nargs 2)))
        (cons `(consp ,OBJ)
          (append (recog-consp-list flo `(car ,OBJ))
            (recog-consp-list (- nargs flo) `(cdr ,OBJ))))))))

(defun tree-accessor
  (n total nest opt)
  (if (zp total)
    nil
    (if (= 1 total)
      nest
      (let ((flo (floor total 2)))
        (if (<= n flo)
          (tree-accessor n
            flo
            `(,(IF (EQ OPT :SAFE)
     'SAFE-CAR
     'CAR) ,NEST)
            opt)
          (tree-accessor (- n flo)
            (- total flo)
            `(,(IF (EQ OPT :SAFE)
     'SAFE-CDR
     'CDR) ,NEST)
            opt))))))