dead-events

(defun absolute-event-number
  (namex wrld quietp)
  (let ((name (if (consp namex)
         (car namex)
         namex)))
    (cond ((getprop name
         'absolute-event-number
         nil
         'current-acl2-world
         wrld))
      (quietp nil)
      (t (er hard
          'absolute-event-number
          "There is no event in the current ACL2 world that ~
                  corresponds to the name ~x0."
          name)))))

(defun make-supp-ar-1
  (supp-alist supp-ar wrld)
  (cond ((endp supp-alist) supp-ar)
    (t (let* ((n (absolute-event-number (caar supp-alist) wrld nil)) (supps (cdar supp-alist))
          (supp-ar (assert$ (null (aref1 *supp-ar-name* supp-ar n))
              (aset1 *supp-ar-name* supp-ar n supps))))
        (make-supp-ar-1 (cdr supp-alist) supp-ar wrld)))))

(defun make-supp-ar
  (wrld)
  (let ((size (next-absolute-event-number wrld)) (supp-alist (global-val 'proof-supporters-alist wrld)))
    (make-supp-ar-1 supp-alist
      (compress1 *supp-ar-name*
        (list (list :header :dimensions (list size)
            :maximum-length (1+ size)
            :default nil
            :name *supp-ar-name*)))
      wrld)))

(defun make-live-names-ar-nil
  (names supp-ar live-names-ar wrld)
  (cond ((endp names) live-names-ar)
    (t (let ((n (absolute-event-number (car names) wrld nil)))
        (cond ((aref1 *live-names-ar-name* live-names-ar n) (make-live-names-ar-nil (cdr names)
              supp-ar
              live-names-ar
              wrld))
          (t (let ((live-names-ar (aset1 *live-names-ar-name* live-names-ar n t)) (supps (aref1 *supp-ar-name* supp-ar n)))
              (make-live-names-ar-nil (append supps (cdr names))
                supp-ar
                live-names-ar
                wrld))))))))

(defun immediate-syntactic-supporters
  (name wrld)
  (cond ((function-symbolp name wrld) (let ((guard (guard name t wrld)) (anc (immediate-instantiable-ancestors name wrld nil)))
        (cond ((equal guard *t*) anc)
          (t (all-ffn-symbs (guard name t wrld) anc)))))
    (t (let ((thm (getprop name 'theorem nil 'current-acl2-world wrld)))
        (if thm
          (all-ffn-symbs thm nil)
          nil)))))

(defun make-live-names-ar-t
  (names supp-ar live-names-ar wrld)
  (cond ((endp names) live-names-ar)
    (t (let ((n (absolute-event-number (car names) wrld nil)))
        (cond ((aref1 *live-names-ar-name* live-names-ar n) (make-live-names-ar-t (cdr names)
              supp-ar
              live-names-ar
              wrld))
          (t (let ((live-names-ar (aset1 *live-names-ar-name* live-names-ar n t)) (supps (aref1 *supp-ar-name* supp-ar n))
                (supps-syn (immediate-syntactic-supporters (car names) wrld)))
              (make-live-names-ar-t (append supps-syn supps (cdr names))
                supp-ar
                live-names-ar
                wrld))))))))

(defun make-live-names-ar
  (syntaxp names supp-ar wrld)
  (let* ((dimensions (dimensions *supp-ar-name* supp-ar)) (maximum-length (maximum-length *supp-ar-name* supp-ar))
      (live-names-ar (compress1 *live-names-ar-name*
          (list (list :header :dimensions dimensions
              :maximum-length maximum-length
              :default nil
              :name *live-names-ar-name*)))))
    (if syntaxp
      (make-live-names-ar-t names supp-ar live-names-ar wrld)
      (make-live-names-ar-nil names supp-ar live-names-ar wrld))))

(defun dead-events-1
  (start live-names-ar trips wrld acc)
  (cond ((null trips) (er hard
        'dead-events-1
        "Implementation error!  Somehow missed event landmark for ~x0."
        start))
    (t (let ((trip (car trips)))
        (case-match trip
          (('event-landmark 'global-value . rest) (cond ((eql (access-event-tuple-number rest) start) acc)
              (t (dead-events-1 start live-names-ar (cdr trips) wrld acc))))
          ((name prop . &) (dead-events-1 start
              live-names-ar
              (cdr trips)
              wrld
              (if (and (or (eq prop 'theorem)
                    (and (eq prop 'formals)
                      (not (eq (symbol-class name wrld) :program))))
                  (let ((n (absolute-event-number name wrld t)))
                    (and n (not (aref1 *live-names-ar-name* live-names-ar n)))))
                (cons name acc)
                acc)))
          (& (er hard
              'dead-events-1
              "Implementation error: Found non-triple in world!")))))))

(defun max-live-names-ar-number
  (live-names-ar acc)
  (cond ((endp live-names-ar) acc)
    (t (max-live-names-ar-number (cdr live-names-ar)
        (if (eq (caar live-names-ar) :header)
          acc
          (max acc (caar live-names-ar)))))))

(defun return-tail-of-world
  (max-live-event-number wrld)
  (cond ((endp wrld) (er hard
        'return-tail-of-world
        "Implementation error: Reached the end of the world!"))
    (t (let ((trip (car wrld)))
        (case-match trip
          (('event-landmark 'global-value . rest) (cond ((eql (access-event-tuple-number rest) max-live-event-number) wrld)
              (t (return-tail-of-world max-live-event-number (cdr wrld)))))
          ((& & . &) (return-tail-of-world max-live-event-number (cdr wrld)))
          (& (er hard
              'return-tail-of-world
              "Implementation error: Found non-triple in world!")))))))

(defun dead-events-fn
  (names syntaxp start redef-ok wrld)
  (let ((ctx 'dead-events))
    (cond ((null names) (er hard
          ctx
          "At least one name must be supplied to DEAD-EVENTS."))
      ((not (symbol-listp names)) (er hard
          ctx
          "The argument of DEAD-EVENTS must evaluate to a true list of ~
           symbols, but instead it evaluates to ~x0."
          names))
      ((and (not redef-ok) (global-val 'redef-seen wrld)) (er hard
          ctx
          "Redefinition has taken place in the current ACL2 world.  However, ~
           the DEAD-EVENTS utility has been designed under the assumption ~
           that there has not been any redefinition.  If you wish to risk ~
           hard errors and surprising results, use keyword parameter ~
           :REDEF-OK T."))
      (t (let* ((supp-ar (make-supp-ar wrld)) (live-names-ar (make-live-names-ar syntaxp names supp-ar wrld))
            (start (cond ((symbolp start) (if start
                    (1- (absolute-event-number start wrld nil))
                    (absolute-event-number 'end-of-pass-2 wrld nil)))
                ((posp start) (1- start))
                (t (er hard
                    ctx
                    "The first argument of dead-events must ~
                                  evaluate to a positive integer or a symbol, ~
                                  but ~x0 is neither."
                    start))))
            (max (max-live-names-ar-number live-names-ar -1))
            (trips (return-tail-of-world max wrld)))
          (dead-events-1 start live-names-ar trips wrld nil))))))

(defun event-supports-fn
  (name supp-alist events-acc)
  (let ((supporters (cdar supp-alist)))
    (if (endp supp-alist)
      events-acc
      (event-supports-fn name
        (cdr supp-alist)
        (if (member-eq name supporters)
          (cons (caar supp-alist) events-acc)
          events-acc)))))

(defun event-supports-fn-lst
  (names supp-alist acc)
  (cond ((endp names) acc)
    (t (event-supports-fn-lst (cdr names)
        supp-alist
        (cons (cons (car names)
            (event-supports-fn (car names) supp-alist nil))
          acc)))))