progn-bang-enh

(in-package "ACL2")

(defttag defcode)

(progn! (set-ld-redefinition-action '(:doit! . :overwrite) state)
  (defmacro progn!
    (&rest r)
    (declare (xargs :guard (or (not (symbolp (car r)))
          (member-eq (car r)
            '(:state-global-bindings :compile-only :loop-only)))))
    (cond ((not (consp r)) '(progn!-fn nil nil state))
      ((eq (car r) :compile-only) `(progn!-fn nil nil state))
      ((eq (car r) :state-global-bindings) `(state-global-let* ,(CADR R)
          (progn!-fn ',(CDDR R) ',(CADR R) state)))
      ((eq (car r) :loop-only) `(progn!-fn ',(CDR R) nil state))
      (t `(progn!-fn ',R nil state))))
  (set-ld-redefinition-action nil state)
  (set-raw-mode t)
  (progn (defmacro progn!
      (&rest r)
      (let ((sym (gensym)))
        `(let ((state *the-live-state*) (,SYM (f-get-global 'acl2-raw-mode-p *the-live-state*)))
          (declare (ignorable state))
          ,@(COND ((NOT (CONSP R)) (LIST NIL)) ((EQ (CAR R) :LOOP-ONLY) (LIST NIL))
        ((EQ (CAR R) :COMPILE-ONLY) (CDR R))
        ((EQ (CAR R) :STATE-GLOBAL-BINDINGS) (CDDR R)) (T R))
          (f-put-global 'acl2-raw-mode-p ,SYM state)
          (value nil))))
    nil)
  (set-raw-mode nil))