pseudo-event-landmarkp

(in-package "ACL2")

(defsection pseudo-event-landmarkp
  :parents (system-utilities-non-built-in)
  :short "Recognize event landmarks in the ACL2 @(see world)."
  :long "<p>Discussions of event landmarks may be found
      in the comment in @('make-event-tuple') in the ACL2 sources
      and in the comment, labeled `Event Tuples',
      above @('make-event-tuple').</p>"
  (defconst *event-tuple-from-primordial-world-globals*
    (make-event-tuple -1 0 nil nil 0 nil nil nil))
  (defun pseudo-event-landmarkp
    (val)
    (declare (xargs :guard t))
    (or (equal val *event-tuple-from-primordial-world-globals*)
      (and (consp val)
        (let ((val (remove-local val)))
          (and (consp val)
            (or (natp (car val))
              (and (consp (car val))
                (natp (car (car val)))
                (natp (cdr (car val)))))
            (consp (cdr val))
            (if (symbolp (cadr val))
              (pseudo-event-formp (cdr val))
              (and (consp (cadr val))
                (consp (car (cadr val)))
                (symbolp (car (car (cadr val))))
                (booleanp (cdr (car (cadr val))))
                (consp (cdr (cadr val)))
                (or (symbolp (cadr (cadr val)))
                  (if (eq (car (car (cadr val))) 'include-book)
                    (book-name-p (cadr (cadr val)))
                    (stringp (cadr (cadr val))))
                  (equal 0 (cadr (cadr val)))
                  (string-or-symbol-listp (cadr (cadr val))))
                (member-eq (cddr (cadr val))
                  '(nil :program :ideal :common-lisp-compliant))
                (pseudo-event-formp (cddr val))))))))))