Filtering...

origin

books/system/origin

Included Books

top
other
(in-package "ACL2")
include-book
(include-book "xdoc/top" :dir :system)
other
(set-state-ok t)
other
(program)
other
(defxdoc origin
  :parents (pe)
  :short "Returns a summary of where a @(see logical-name) originates from."
  :long "<p>Examples:</p>
@({
  (include-book "system/origin" :dir :system)

  ;; built-in names get a return value of :built-in
  (origin 'consp)    --> (value :built-in)
  (origin 'car-cons) --> (value :built-in)

  ;; include-book path is reported for events included from other books
  (origin 'xdoc::save) --> (value ("/home/jared/acl2/books/system/origin.lisp"
                                   "/home/jared/acl2/books/xdoc/top.lisp"))

  (origin 'lnfix) --> (value ("/home/jared/acl2/books/system/origin.lisp"
                              "/home/jared/acl2/books/xdoc/top.lisp"
                              "/home/jared/acl2/books/xdoc/base.lisp"))

  ;; some definitions are from the current session, e.g.:
  (defun f (x) x)
  (origin 'f)     --> (value :TOP-LEVEL)

  ;; bad names
  (mv-let (er val state)               ;; ((:er ("Not a logical name: ~x0"
          (origin 'not-defined-thing)  ;;        (#0 . NOT-DEFINED-THING))
   (mv (list :er er :val val)          ;;   :val nil)
       state))                         ;;  <state>)

})")
origin-fnfunction
(defun origin-fn
  (logical-name state)
  (let* ((wrld (w state)))
    (cond ((acl2-system-namep logical-name wrld) (value :built-in))
      (t (let ((ev-wrld (decode-logical-name logical-name wrld)))
          (cond (ev-wrld (value (let ((book-path (global-val 'include-book-path ev-wrld)))
                  (cond (book-path (reverse book-path)) (t :top-level)))))
            (t (mv (msg "Not logical name: ~x0." logical-name) nil state))))))))
originmacro
(defmacro origin
  (logical-name)
  `(origin-fn ,LOGICAL-NAME state))