book-checks

(defun collect-rule-status-changes
  (existent prev-enabled post-enabled)
  (if (atom existent)
    nil
    (let ((prev (consp (member-equal (car existent) prev-enabled))) (post (consp (member-equal (car existent) post-enabled))))
      (if (eq prev post)
        (collect-rule-status-changes (cdr existent)
          prev-enabled
          post-enabled)
        (cons (list (if prev
              'disable
              'enable)
            (car existent))
          (collect-rule-status-changes (cdr existent)
            prev-enabled
            post-enabled))))))

(defun rule-status-changes-between
  (prev-wrld curr-wrld)
  (declare (xargs :mode :program))
  (let* ((curr-theory (current-theory1 curr-wrld nil nil)) (prev-theory (current-theory1 prev-wrld nil nil))
      (prev-univ (universal-theory-fn1 prev-wrld nil nil)))
    (collect-rule-status-changes prev-univ
      prev-theory
      curr-theory)))

(defun rule-status-changes-fn
  (cd state)
  (declare (xargs :mode :program :stobjs state))
  (er-let* ((cmd-wrld (er-decode-cd cd (w state) 'rule-status-changes state)))
    (let ((prev-wrld (scan-to-command (cdr cmd-wrld))))
      (value (rule-status-changes-between prev-wrld cmd-wrld)))))

(defun rule-status-changes-since-fn
  (cd state)
  (declare (xargs :mode :program :stobjs state))
  (er-let* ((cmd-wrld (er-decode-cd cd (w state) 'rule-status-changes state)))
    (value (rule-status-changes-between cmd-wrld (w state)))))

(defun scan-world-for-theory-changes
  (rune enabled-before depth stack wrld)
  (if (atom wrld)
    (mv enabled-before nil)
    (case (caar wrld)
      (current-theory (mv-let (prev-enabled rest)
          (scan-world-for-theory-changes rune
            enabled-before
            depth
            stack
            (cdr wrld))
          (let* ((post-enabled (consp (member-equal rune (cddar wrld)))))
            (if (eq prev-enabled post-enabled)
              (mv prev-enabled rest)
              (mv post-enabled
                (cons (cons (if post-enabled
                      'enable
                      'disable)
                    stack)
                  rest))))))
      (event-landmark (let* ((new-depth (if (consp (caddar wrld))
               (cdr (caddar wrld))
               0)) (stack (cons (nthcdr 4 (car wrld))
                (nthcdr (+ 1 (- depth new-depth)) stack))))
          (scan-world-for-theory-changes rune
            enabled-before
            new-depth
            stack
            (cdr wrld))))
      (otherwise (scan-world-for-theory-changes rune
          enabled-before
          depth
          stack
          (cdr wrld))))))

(defun find-theory-changes-since-fn
  (rune cd state)
  (er-let* ((cmd-wrld (er-decode-cd cd (w state) 'find-theory-change-since state)))
    (let* ((enabled-before (consp (member-equal rune (current-theory1 cmd-wrld nil nil)))) (segment (take (- (len (w state)) (len cmd-wrld)) (w state))))
      (mv-let (enabled res)
        (scan-world-for-theory-changes rune
          enabled-before
          0
          nil
          segment)
        (declare (ignore enabled))
        (value res)))))

(defun find-theory-changes-fn
  (rune cd state)
  (er-let* ((cmd-wrld (er-decode-cd cd (w state) 'find-theory-change-since state)))
    (let* ((prev-wrld (scan-to-command (cdr cmd-wrld))) (enabled-before (consp (member-equal rune (current-theory1 prev-wrld nil nil))))
        (segment (take (- (len cmd-wrld) (len prev-wrld)) cmd-wrld)))
      (mv-let (enabled res)
        (scan-world-for-theory-changes rune
          enabled-before
          0
          nil
          segment)
        (declare (ignore enabled))
        (value res)))))