elide-event - ACL2 Book

other

(in-package "ACL2")

elide-defunfunction

(defun elide-defun
  (ev)
  (declare (xargs :guard (true-listp ev)))
  (cond ((and (cddddr ev) (plausible-dclsp (butlast (cdddr ev) 1))) `(,(CAR EV) ,(CADR EV)
        ,(CADDR EV)
        ,@(STRIP-DCLS
   '(COMMENT :GUARD-HINTS :GUARD-DEBUG :HINTS :MEASURE-DEBUG :OTF-FLG)
   (BUTLAST (CDDDR EV) 1))
        ,(CAR (LAST EV))))
    (t ev)))

elide-defthmfunction

(defun elide-defthm
  (ev)
  (declare (xargs :guard (true-listp ev)))
  (let* ((name (cadr ev)) (body (caddr ev))
      (rest (cdddr ev))
      (tail (and rest (member-eq :rule-classes rest))))
    (cond (tail (list (car ev) name body :rule-classes (cadr tail)))
      (rest (list (car ev) name body))
      (t ev))))

elide-eventmutual-recursion

(mutual-recursion (defun elide-event
    (ev)
    (declare (xargs :guard (true-listp ev)))
    (case (car ev)
      ((defun defund defun-nx defund-nx) (elide-defun ev))
      ((progn mutual-recursion) (cons (car ev) (elide-event-lst (cdr ev))))
      (encapsulate (if (cadr ev)
          ev
          (list* 'encapsulate nil (elide-event-lst (cddr ev)))))
      (defthm (elide-defthm ev))
      (t ev)))
  (defun elide-event-lst
    (lst)
    (declare (xargs :guard (true-listp lst)))
    (cond ((endp lst) nil)
      (t (cons (if (true-listp (car lst))
            (elide-event (car lst))
            (car lst))
          (elide-event-lst (cdr lst)))))))