canonical-print - ACL2 Book

other

(in-package "ACL2S-HOOKS")

other

(program)

other

(set-state-ok t)

put-current-packagefunction

(defun put-current-package
  (pkg state)
  (mv-let (erp v state)
    (set-current-package pkg state)
    (declare (ignore erp v))
    state))

with-upcase-base10macro

(defmacro with-upcase-base10
  (form)
  `(state-global-let* ((print-case :upcase) (print-base 10))
    ,ACL2S-HOOKS::FORM))

with-canonical-printingmacro

(defmacro with-canonical-printing
  (form)
  `(state-global-let* ((print-case :upcase) (print-base 10)
      (current-package "COMMON-LISP"
        put-current-package))
    ,ACL2S-HOOKS::FORM))

fmx-to-comment-windowmacro

(defmacro fmx-to-comment-window
  (format &rest args)
  `(fmt-to-comment-window ,FORMAT
    ,(ACL2S-HOOKS::MAKE-FMT-BINDINGS '(#\0 #\1 #\2 #\3 #\4 #\5 #\6 #\7 #\8 #\9)
  ACL2S-HOOKS::ARGS)
    0
    nil
    10))

fmx-canonicalmacro

(defmacro fmx-canonical
  (formal &rest args)
  `(with-canonical-printing (mv (fmx-to-comment-window ,ACL2S-HOOKS::FORMAL . ,ACL2S-HOOKS::ARGS)
      :invisible state)))

pfmx-canonicalmacro

(defmacro pfmx-canonical
  (format &rest args)
  `(mv-let (erp val state)
    (fmx-canonical ,FORMAT . ,ACL2S-HOOKS::ARGS)
    (declare (ignore erp val))
    state))

print-canonicalmacro

(defmacro print-canonical
  (form)
  `(fmx-canonical "~y0~%" ,ACL2S-HOOKS::FORM))

package-imports-fnfunction

(defun package-imports-fn
  (pack wrld)
  (declare (xargs :guard (and (stringp pack)
        (plist-worldp wrld))))
  (let* ((known (getprop 'known-package-alist
         'global-value
         nil
         'current-acl2-world
         wrld)) (known (if (alistp known)
          known
          nil))
      (entry (find-package-entry pack known))
      (entry (if (and (consp entry)
            (consp (cdr entry)))
          entry
          nil)))
    (if (null entry)
      :no-such-package (package-entry-imports entry))))

package-importsmacro

(defmacro package-imports
  (pack-expr)
  `(package-imports-fn ,ACL2S-HOOKS::PACK-EXPR
    (w state)))

print-package-importsmacro

(defmacro print-package-imports
  (pack-expr)
  `(print-canonical (package-imports-fn ,ACL2S-HOOKS::PACK-EXPR
      (w state))))

non-hidden-known-package-alist0function

(defun non-hidden-known-package-alist0
  (known)
  (if (not (consp known))
    nil
    (let ((entry (car known)) (rst (non-hidden-known-package-alist0 (cdr known))))
      (if (and (consp entry)
          (consp (cdr entry))
          (consp (cddr entry))
          (package-entry-hidden-p entry))
        rst
        (cons entry rst)))))

non-hidden-known-package-alistfunction

(defun non-hidden-known-package-alist
  (wrld)
  (declare (xargs :guard (plist-worldp wrld)))
  (non-hidden-known-package-alist0 (getprop 'known-package-alist
      'global-value
      nil
      'current-acl2-world
      wrld)))

non-hidden-package-listmacro

(defmacro non-hidden-package-list
  nil
  '(strip-cars (non-hidden-known-package-alist (w state))))