		Search-engine friendly clone of the ACL2 documentation.

Deftreeops

Deftreeops-show-event

Show the event with a given name from the deftreeops table associated to a given grammar constant name.

If there is no information in the table for the given grammar constant name, or if there is no event with the given name, we print a message saying so.

Macro: deftreeops-show-event

(defmacro deftreeops-show-event (grammar name)
  (declare (xargs :guard (and (common-lisp::symbolp grammar)
                              (common-lisp::symbolp name))))
  (cons 'make-event-terse
        (cons (cons 'deftreeops-show-event-fn
                    (cons (cons 'quote (cons grammar 'nil))
                          (cons (cons 'quote (cons name 'nil))
                                '((w state)))))
              'nil)))

Definitions and Theorems

Function: deftreeops-show-event-fn

(defun deftreeops-show-event-fn (grammar name wrld)
 (declare (xargs :guard (and (common-lisp::symbolp grammar)
                             (common-lisp::symbolp name)
                             (plist-worldp wrld))))
 (let ((__function__ 'deftreeops-show-event-fn))
  (declare (ignorable __function__))
  (b*
   ((info (deftreeops-table-lookup grammar wrld))
    ((unless info)
     (cw "~%No entry in DEFTREEOPS table for grammar ~x0.~%"
         grammar)
     '(value-triple :invisible))
    (event-alist (deftreeops-table-value->event-alist info))
    (name+event (assoc-eq name event-alist))
    ((unless name+event)
     (cw
      "~%No event with name ~x0 ~
               in DEFTREEOPS table entry for grammar ~x1.~%"
      name grammar)
     '(value-triple :invisible))
    (- (cw "~%~x0~%" (cdr name+event))))
   '(value-triple :invisible))))

Theorem: pseudo-event-formp-of-deftreeops-show-event-fn

(defthm pseudo-event-formp-of-deftreeops-show-event-fn
  (b* ((event (deftreeops-show-event-fn grammar name wrld)))
    (pseudo-event-formp event))
  :rule-classes :rewrite)