Filtering...

redefun

books/hacking/redefun
other
(in-package "ACL2")
other
(program)
other
(set-state-ok t)
chk-acceptable-redefunfunction
(defun chk-acceptable-redefun
  (def ctx wrld state)
  (er-let* ((tuple (chk-acceptable-defuns (list def) ctx wrld state)))
    (assert$ (equal (length tuple) 26)
      (let* ((name (car def)) (new-wrld (nth 18 tuple))
          (old-symbol-class (getprop name 'symbol-class 0 'current-acl2-world wrld))
          (new-symbol-class (nth 15 tuple))
          (old-formals (getprop name 'formals 0 'current-acl2-world wrld))
          (new-formals (getprop name 'formals 0 'current-acl2-world new-wrld))
          (old-stobjs-in (getprop name 'stobjs-in 0 'current-acl2-world wrld))
          (new-stobjs-in (getprop name 'stobjs-in 0 'current-acl2-world new-wrld))
          (old-stobjs-out (getprop name 'stobjs-out 0 'current-acl2-world wrld))
          (new-stobjs-out (getprop name 'stobjs-out 0 'current-acl2-world new-wrld)))
        (cond ((eql old-symbol-class 0) (er soft ctx "No existing definition: ~x0" name))
          ((nth 19 tuple) (er soft
              ctx
              "Please do not redefun a non-executable function.  The ~
                  offending definition is: ~x0."
              def))
          ((not (eq ':program old-symbol-class)) (er soft
              ctx
              "Old definition should have defun-mode :program.  Sorry."))
          ((not (eq ':program new-symbol-class)) (er soft
              ctx
              "New definition should have defun-mode :program.  Sorry."))
          ((not (equal new-formals old-formals)) (er soft
              ctx
              "Please use the same formal parameter list when redefining. ~
                  Previous formals: ~x0"
              old-formals))
          ((not (equal new-stobjs-in old-stobjs-in)) (er soft
              ctx
              "New definition should have the same stobjs-in.Previously, ~
                  ~x0.  Specified, ~x1."
              old-stobjs-in
              new-stobjs-in))
          ((not (equal new-stobjs-out old-stobjs-out)) (er soft
              ctx
              "New definition should have the same stobjs-out.Previously, ~
                  ~x0.  Specified, ~x1."
              old-stobjs-out
              new-stobjs-out))
          (t (value :invisible)))))))
redefunmacro
(defmacro redefun
  (name ll &rest decls-and-body)
  (declare (xargs :guard (and (symbolp name)
        (symbol-listp ll)
        (consp decls-and-body))))
  (let ((def (list* name ll decls-and-body)))
    `(progn+redef (assert-include-defun-matches-certify-defun ,NAME)
      (defcode :loop (er-progn (assert-no-special-raw-definition ,NAME)
          (chk-acceptable-redefun ',DEF 'redefun (w state) state)
          (ensure-program-only-flag ,NAME)
          (defun . ,DEF))
        :extend (in-raw-mode (defun-*1* ,NAME
            ,LL
            (if (f-get-global 'safe-mode *the-live-state*)
              (throw-raw-ev-fncall (list 'program-only-er ',NAME (list . ,LL) 't '(nil) t))
              (,NAME . ,LL))))
        :compile (defun . ,DEF)))))
redefun+rewritemacro
(defmacro redefun+rewrite
  (name &rest rewrite-spec)
  (declare (xargs :guard (symbolp name)))
  `(make-event (compute-copy-defun+rewrite ',NAME
      ',NAME
      ',REWRITE-SPEC
      'redefun
      state)))