ubi

(defun unwrap-cmd-for-ubi
  (cmd)
  (if (not (consp cmd))
    cmd
    (if (eq 'local (car cmd))
      (unwrap-cmd-for-ubi (cadr cmd))
      (if (eq 'with-output (car cmd))
        (unwrap-cmd-for-ubi (car (last cmd)))
        (if (and (eq 'progn (car cmd))
            (equal (cddr cmd) '((value-triple :invisible))))
          (unwrap-cmd-for-ubi (cadr cmd))
          cmd)))))

(defun boot-strap-command-p
  (cmd)
  (let ((cmd (unwrap-cmd-for-ubi cmd)))
    (and (consp cmd)
      (member-eq (car cmd)
        '(exit-boot-strap-mode reset-prehistory)))))

(defun cmds-back-to-boot-strap
  (wrld acc)
  (declare (xargs :guard (plist-worldp wrld)))
  (cond ((endp wrld) acc)
    ((and (eq (caar wrld) 'command-landmark)
       (eq (cadar wrld) 'global-value)) (let ((cmd (access-command-tuple-form (cddar wrld))))
        (cond ((boot-strap-command-p cmd) acc)
          (t (cmds-back-to-boot-strap (cdr wrld) (cons cmd acc))))))
    (t (cmds-back-to-boot-strap (cdr wrld) acc))))

(defun initial-keeper-cmds-length
  (cmds keeper-cmds acc)
  (cond ((endp cmds) acc)
    (t (let* ((cmd0 (car cmds)) (cmd (unwrap-cmd-for-ubi cmd0))
          (keeper-p (and (consp cmd) (member-eq (car cmd) keeper-cmds))))
        (cond (keeper-p (initial-keeper-cmds-length (cdr cmds) keeper-cmds (1+ acc)))
          (t acc))))))

(defun ubi-fn
  (args state)
  (declare (xargs :guard (symbol-listp args) :stobjs state))
  (let* ((wrld (w state)) (cmds (cmds-back-to-boot-strap wrld nil))
      (keeper-cmds (union-eq args *keeper-cmds*))
      (len-cmds (length cmds))
      (len-keeper-cmds (initial-keeper-cmds-length cmds keeper-cmds 0)))
    (cond ((eql len-cmds len-keeper-cmds) (pprogn (fms "There is nothing to undo, since all commands after ~
                         the boot-strap are ~v0 commands.~|"
            (list (cons #\0 keeper-cmds))
            *standard-co*
            state
            nil)
          (value :invisible)))
      (t (ubu len-keeper-cmds)))))