redef-pkg

(in-package "ACL2")

(defttag :redef-pkg)

(defun set-imported-symbols-to-pkg
  (imports name)
  (declare (ignore imports name)
    (xargs :guard t :mode :program))
  nil)

(defmacro redef-pkg
  (name imports &optional doc book-path)
  (declare (ignore doc book-path))
  `(set-imported-symbols-to-pkg ,IMPORTS ,NAME))

(progn! (set-raw-mode-on state)
  (f-put-global 'program-fns-with-raw-code
    (add-to-set-eq 'set-imported-symbols-to-pkg
      (f-get-global 'program-fns-with-raw-code *the-live-state*))
    *the-live-state*)
  (defun set-imported-symbols-to-pkg
    (syms pkg &aux (state *the-live-state*))
    (let ((pkg-entry0 (assoc-equal pkg *ever-known-package-alist*)) (pkg-entry1 (assoc-equal pkg (known-package-alist *the-live-state*)))
        (syms (if (symbolp syms)
            (list syms)
            syms)))
      (when (or (null pkg-entry0) (null pkg-entry1))
        (error "Uknown pkg, ~s" pkg))
      (when (not (symbol-listp syms))
        (error "Not a symbol-listp: ~s" syms))
      (let ((imports0 (package-entry-imports pkg-entry0)) (imports1 (package-entry-imports pkg-entry1))
          ans)
        (when (not (or (equal imports0 imports1)
              (and (subsetp-eq imports0 imports1)
                (subsetp-eq imports1 imports0))))
          (error "SURPRISE!  Different import lists.  Hmmmm......"))
        (let* ((new (set-difference-eq syms imports0)) (deleted (set-difference-eq imports0 syms))
            (sorted-symbols (sort-symbol-listp syms)))
          (setf (package-entry-imports (assoc-equal pkg *ever-known-package-alist*))
            sorted-symbols)
          (setf (package-entry-imports (assoc-equal pkg (known-package-alist *the-live-state*)))
            sorted-symbols)
          (dolist (sym new)
            (let ((temp (find-symbol (symbol-name sym) pkg)))
              (when temp
                (when (get temp *current-acl2-world-key*)
                  (push (symbol-name temp) ans))
                (unintern temp pkg))))
          (fms "NOTE: Added this list of symbols to the imports of package ~
              ~x0:~| ~x1~|and deleted this list of symbols from the imports ~
              of package ~x0:~| ~x2~|~%"
            (list (cons #\0 pkg) (cons #\1 new) (cons #\2 deleted))
            (standard-co state)
            state
            nil)
          (when ans
            (warning$ 'set-imported-symbols-to-pkg
              "Package"
              "The symbol~#0~[ with name~/s with names~] ~&0 imported ~
                       into the ~x1 package may cause problems, since ~#0~[it ~
                       already has~/they already have~] properties in the ~
                       ACL2 world."
              ans
              pkg))
          (import new pkg)
          (dolist (sym deleted) (unintern sym pkg))))))
  (defun chk-acceptable-defpkg
    (name form defpkg-book-path hidden-p ctx w state)
    (fms "Executing the redefined chk-acceptable-defpkg~%"
      nil
      (standard-co state)
      state
      nil)
    (let ((package-entry (and (not (f-get-global 'boot-strap-flg state))
           (find-package-entry name
             (global-val 'known-package-alist w)))))
      (cond ((not (true-listp defpkg-book-path)) (er soft
            ctx
            "The book-path argument to defpkg, if supplied, must be a ~
           true-listp.  It is not recommended to supply this argument, since ~
           the system makes use of it for producing useful error messages.  ~
           The defpkg of ~x0 is thus illegal."
            name))
        ((get-invalid-book-name defpkg-book-path (os w) w) (er soft
            ctx
            "A defpkg form for ~x0 specifies an invalid book-path entry, ~x1.~@2"
            name
            (get-invalid-book-name defpkg-book-path (os w) w)
            (let ((x (get-invalid-book-name defpkg-book-path (os w) w)))
              (if (and (sysfile-p x)
                  (not (project-dir-lookup (sysfile-key x)
                      (project-dir-alist w)
                      nil)))
                (msg "  Note that the keyword ~x0 is not currently bound in ~
                     the project-dir-alist.  Probably it was bound in the ~
                     project-dir-alist in a previous session, when this ~
                     defpkg form was written to a book's certificate.  See ~
                     :DOC project-dir-alist."
                  (sysfile-key x))
                ""))))
        (t (er-progn (cond ((or package-entry
                 (eq (ld-skip-proofsp state) 'include-book)) (value nil))
              ((not (stringp name)) (er soft
                  ctx
                  "Package names must be string constants and ~x0 is not.  See ~
              :DOC defpkg."
                  name))
              ((equal name "") (er soft
                  ctx
                  "The empty string is not a legal package name for defpkg."
                  name))
              ((not (standard-char-listp (coerce name 'list))) (er soft
                  ctx
                  "~x0 is not a legal package name for defpkg, which requires the ~
              name to contain only standard characters."
                  name))
              ((not (equal (string-upcase name) name)) (er soft
                  ctx
                  "~x0 is not a legal package name for defpkg, which disallows ~
              lower case characters in the name."
                  name))
              ((equal name "LISP") (er soft
                  ctx
                  "~x0 is disallowed as a a package name for defpkg, because this ~
              package name is used under the hood in some Common Lisp ~
              implementations."
                  name))
              ((let ((len (length *1*-pkg-prefix*)))
                 (and (<= len (length name))
                   (string-equal (subseq name 0 len) *1*-pkg-prefix*))) (er soft
                  ctx
                  "It is illegal for a package name to start (even ignoring case) ~
              with the string "~@0".  ACL2 makes internal use of package ~
              names starting with that string."
                  *1*-pkg-prefix*))
              (t (value nil)))
            (state-global-let* ((safe-mode (not (f-get-global 'boot-strap-flg state))))
              (er-let* ((pair (simple-translate-and-eval form
                     nil
                     nil
                     "The second argument to defpkg"
                     ctx
                     w
                     state
                     t)))
                (let ((tform (car pair)) (imports (cdr pair)))
                  (cond ((not (symbol-listp imports)) (er soft
                        ctx
                        "The second argument of defpkg must eval to a list of ~
                  symbols.  See :DOC defpkg."))
                    (t (let* ((imports (sort-symbol-listp imports)) (conflict (conflicting-imports imports))
                          (base-symbol (packn (cons name '("-PACKAGE")))))
                        (cond ((member-symbol-name *pkg-witness-name* imports) (er soft
                              ctx
                              "It is illegal to import symbol ~x0 because its name ~
                        has been reserved for a symbol in the package being ~
                        defined."
                              (car (member-symbol-name *pkg-witness-name* imports))))
                          (conflict (er soft
                              ctx
                              "The value of the second (imports) argument of defpkg ~
                        may not contain two symbols with the same symbol ~
                        name, e.g. ~&0.  See :DOC defpkg."
                              conflict))
                          (t (cond ((and package-entry
                                 (not (equal imports (package-entry-imports package-entry)))) (progn (set-imported-symbols-to-pkg imports name)
                                  (value 'redundant)))
                              ((and package-entry
                                 (or hidden-p (not (package-entry-hidden-p package-entry)))) (prog2$ (chk-package-reincarnation-import-restrictions name imports)
                                  (value 'redundant)))
                              (t (er-progn (chk-new-stringp-name 'defpkg name ctx w state)
                                  (chk-all-but-new-name base-symbol ctx nil w state)
                                  (chk-just-new-name base-symbol nil 'theorem nil ctx w state)
                                  (prog2$ (chk-package-reincarnation-import-restrictions name imports)
                                    (value (list* tform imports package-entry))))))))))))))))))))