defredundant

(defun get-event-tuple
  (name world)
  (b* ((?__function__ 'get-event-tuple) (ev-world (decode-logical-name name world))
      ((unless (consp ev-world)) (raise "Not a logical name: ~x0." name))
      (landmark (car ev-world))
      ((unless (and (consp landmark)
           (eq (first landmark) 'event-landmark)
           (eq (second landmark) 'global-value))) (raise "Expected (EVENT-LANDMARK GLOBAL-VALUE . <event-tuple>) but found ~x0."
          landmark))
      (tuple (cddr landmark))
      (form (access-event-tuple-form tuple)))
    (cond ((and (consp form)
         (eq (car form) 'verify-termination-boot-strap)) (get-event-tuple name
          (scan-to-event (cdr ev-world))))
      (t tuple))))

(defun runes-to-e/ds
  (runes enables disables state)
  (b* (((when (atom runes)) (mv enables disables)) (rune1 (car runes))
      (ens (ens state))
      (enabled1 (active-runep rune1))
      ((when enabled1) (runes-to-e/ds (cdr runes)
          (cons rune1 enables)
          disables
          state)))
    (runes-to-e/ds (cdr runes)
      enables
      (cons rune1 disables)
      state)))

(defun name-to-e/ds
  (name state)
  (b* ((runic-mapping-pairs (getprop name
         'runic-mapping-pairs
         nil
         'current-acl2-world
         (w state))) (runes (strip-cdrs runic-mapping-pairs)))
    (runes-to-e/ds runes nil nil state)))

(defun names-to-e/ds
  (names state)
  (b* (((when (atom names)) (mv nil nil)) ((mv es1 ds1) (name-to-e/ds (car names) state))
      ((mv es2 ds2) (names-to-e/ds (cdr names) state)))
    (mv (append es1 es2)
      (append ds1 ds2))))

(defun redundant-clean-up-xargs
  (x)
  (b* ((?__function__ 'redundant-clean-up-xargs) ((when (atom x)) nil)
      ((when (atom (cdr x))) (raise "Invalid xargs... ~x0" x))
      ((list* kwd val rest) x)
      ((when (member kwd
           '(:measure :mode :verify-guards :guard-debug :guard-hints :hints :otf-flg))) (redundant-clean-up-xargs rest)))
    (list* kwd
      val
      (redundant-clean-up-xargs rest))))

(defun redundant-clean-up-decl-args
  (x)
  (b* ((?__function__ 'redundant-clean-up-decl-args) ((when (atom x)) nil)
      ((cons arg1 rest) x)
      ((unless (consp arg1)) (raise "Bad form in declare: ~x0" x))
      ((when (member-eq (car arg1)
           '(type ignore ignorable irrelevant optimize))) (cons arg1 (redundant-clean-up-decl-args rest)))
      ((when (eq (car arg1) 'xargs)) (cons (cons 'xargs
            (redundant-clean-up-xargs (cdr arg1)))
          (redundant-clean-up-decl-args rest))))
    (raise "Bad form in declare: ~x0" x)))

(defun redundant-clean-up-decls
  (x)
  (b* ((?__function__ 'redundant-clean-up-decls) ((when (atom x)) nil)
      ((cons decl1 rest) x)
      ((when (stringp decl1)) (redundant-clean-up-decls rest))
      ((unless (and (consp decl1) (eq (car decl1) 'declare))) (raise "Bad declaration ~x0" x))
      (decl1-args (cdr decl1)))
    (cons (cons 'declare
        (redundant-clean-up-decl-args decl1-args))
      (redundant-clean-up-decls rest))))

(defun redundant-clean-up-defun
  (form force-programp state)
  (b* ((__function__ 'redundant-rewrite-defun) (world (w state))
      ((unless (and (consp form)
           (or (eq (car form) 'defun)
             (eq (car form) 'defund)))) (raise "Called redundant-rewrite-defun on ~x0?"
          form))
      (fn (second form))
      (formals (third form))
      (decls (redundant-clean-up-decls (butlast (cdddr form) 1)))
      (body (car (last form)))
      (world-formals (getprop fn
          'formals
          :bad 'current-acl2-world
          world))
      ((unless (equal world-formals formals)) (raise "Problem with formals for ~x0: ~x1 vs ~x2?"
          fn
          formals
          world-formals))
      (just (getprop fn
          'justification
          nil
          'current-acl2-world
          world))
      (decls (if (not just)
          decls
          (cons `(declare (xargs :measure (:? . ,(ACCESS JUSTIFICATION STD::JUST :SUBSET))))
            decls)))
      (symbol-class (getprop fn
          'symbol-class
          nil
          'current-acl2-world
          world))
      (decls (cond ((or force-programp (eq symbol-class :program)) (cons `(declare (xargs :mode :program)) decls))
          ((eq symbol-class :ideal) (cons `(declare (xargs :mode :logic :verify-guards nil))
              decls))
          ((eq symbol-class :common-lisp-compliant) (cons `(declare (xargs :mode :logic :verify-guards t))
              decls))
          (t (raise "Expected valid symbol-class for ~x0, found ~x1."
              fn
              symbol-class)))))
    `(defun ,STD::FN ,STD::FORMALS ,@STD::DECLS ,STD::BODY)))

(defun redundant-clean-up-defuns
  (forms force-programp state)
  (if (atom forms)
    nil
    (cons (redundant-clean-up-defun (car forms)
        force-programp
        state)
      (redundant-clean-up-defuns (cdr forms)
        force-programp
        state))))

(defun redundant-defun
  (event-tuple force-programp state)
  (b* ((?__function__ 'redundant-defun) (form (access-event-tuple-form event-tuple))
      (cleaned-up-form (redundant-clean-up-defun form
          force-programp
          state))
      (fn (second form))
      ((mv enables disables) (if force-programp
          (mv nil nil)
          (name-to-e/ds fn state))))
    `((value-triple (cw "Defun: ~x0.~%" ',STD::FN)) ,STD::CLEANED-UP-FORM
      (in-theory (e/d ,STD::ENABLES ,STD::DISABLES)))))

(defun redundant-mutrec
  (event-tuple force-programp state)
  (b* ((?__function__ 'redundant-mutual-recursion) (form (access-event-tuple-form event-tuple))
      ((unless (and (consp form)
           (eq (car form) 'mutual-recursion))) (raise "Called redundant-mutual-recursion on ~x0?"
          event-tuple))
      (defuns (cdr form))
      (cleaned-up-defuns (redundant-clean-up-defuns defuns
          force-programp
          state))
      ((mv enables disables) (if force-programp
          (mv nil nil)
          (names-to-e/ds (strip-cadrs defuns)
            state)))
      (cleaned-up-form `(mutual-recursion . ,STD::CLEANED-UP-DEFUNS)))
    `((value-triple (cw "Mutual: ~x0.~%"
         ',(STD::STRIP-CADRS (CDR STD::FORM)))) ,STD::CLEANED-UP-FORM
      (in-theory (e/d ,STD::ENABLES ,STD::DISABLES)))))

(defun redundant-clean-defthm-kwdargs
  (kwdargs)
  (b* ((?__function__ 'redundant-clean-defthm-kwdargs) ((when (atom kwdargs)) nil)
      ((when (atom (cdr kwdargs))) (raise "odd number of elements in (:kwd val) list?"))
      ((list* kwd val rest) kwdargs)
      ((when (or (eq kwd :otf-flg)
           (eq kwd :doc)
           (eq kwd :hints)
           (eq kwd :instructions))) (redundant-clean-defthm-kwdargs rest)))
    (list* kwd
      val
      (redundant-clean-defthm-kwdargs rest))))

(defun redundant-defthm
  (event-tuple state)
  (declare (ignorable state))
  (b* ((?__function__ 'redundant-defthm) (form (access-event-tuple-form event-tuple))
      ((unless (and (consp form) (eq (car form) 'defthm))) (raise "Called redundant-defthm on ~x0?"
          event-tuple))
      (name (second form))
      (formula (third form))
      (kwdargs (redundant-clean-defthm-kwdargs (nthcdr 3 form)))
      ((mv enables disables) (name-to-e/ds name state)))
    `((value-triple (cw "Defthm: ~x0.~%" ',STD::NAME)) (defthm ,STD::NAME ,STD::FORMULA . ,STD::KWDARGS)
      (in-theory (e/d ,STD::ENABLES ,STD::DISABLES)))))

(defun redundant-defmacro
  (event-tuple state)
  (declare (ignorable state))
  (b* ((?__function__ 'redundant-defmacro) (form (access-event-tuple-form event-tuple))
      ((unless (and (consp form) (eq (car form) 'defmacro))) (raise "Called redundant-defmacro on ~x0?"
          event-tuple))
      (name (second form))
      (formals (third form))
      (decls (redundant-clean-up-decls (butlast (nthcdr 3 form) 1)))
      (body (car (last form))))
    `((value-triple (cw "Macro: ~x0.~%" ',STD::NAME)) (defmacro ,STD::NAME ,STD::FORMALS ,@STD::DECLS ,STD::BODY))))

(defun redundant-defconst
  (event-tuple state)
  (declare (ignorable state))
  (b* ((?__function__ 'redundant-defmacro) (form (access-event-tuple-form event-tuple))
      ((unless (and (consp form) (eq (car form) 'defconst))) (raise "Called redundant-defconst on ~x0?"
          event-tuple))
      (name (second form))
      (value (third form))
      (?doc (fourth form)))
    `((value-triple (cw "Const: ~x0.~%" ',STD::NAME)) (defconst ,STD::NAME ,STD::VALUE))))

(defun redundant-defstobj
  (event-tuple state)
  (declare (ignorable state))
  (b* ((?__function__ 'redundant-defmacro) (form (access-event-tuple-form event-tuple))
      ((unless (and (consp form) (eq (car form) 'defstobj))) (raise "Called redundant-defstobj on ~x0?"
          event-tuple))
      (name (second form))
      (rest (cddr form)))
    `((value-triple (cw "Stobj: ~x0.~%" ',STD::NAME)) (defstobj ,STD::NAME . ,REST))))

(defun redundant-encapsulate
  (event-tuple state)
  (declare (ignorable state))
  (b* ((?__function__ 'redundant-encapsulate) (form (access-event-tuple-form event-tuple))
      ((unless (and (consp form)
           (eq (car form) 'encapsulate))) (raise "Called redundant-encapsulate on ~x0?"
          event-tuple))
      (bound-fns (second form))
      (rest (cddr form)))
    `((value-triple (cw "Encapsulate: ~x0.~%"
         ',(STD::STRIP-CARS STD::BOUND-FNS))) (encapsulate ,STD::BOUND-FNS . ,REST))))

(defun redundant-event1
  (name force-programp state)
  (b* ((?__function__ 'redundant-event1) (world (w state))
      (event-tuple (get-event-tuple name world))
      (form (access-event-tuple-form event-tuple))
      ((unless (consp form)) (raise "For ~x0: expected a valid event form, but found ~x1."
          name
          form))
      (type (car form))
      ((when (eq type 'defthm)) (redundant-defthm event-tuple state))
      ((when (eq type 'defconst)) (redundant-defconst event-tuple state))
      ((when (eq type 'defun)) (redundant-defun event-tuple
          force-programp
          state))
      ((when (eq type 'defmacro)) (redundant-defmacro event-tuple state))
      ((when (eq type 'mutual-recursion)) (redundant-mutrec event-tuple
          force-programp
          state))
      ((when (eq type 'defstobj)) (redundant-defstobj event-tuple state))
      ((when (eq type 'encapsulate)) (redundant-encapsulate event-tuple state)))
    (raise "For ~x0: unsupported event type: ~x1"
      name
      type)))

(defun redundant-events1
  (names force-programp state)
  (if (atom names)
    nil
    (append (redundant-event1 (car names)
        force-programp
        state)
      (redundant-events1 (cdr names)
        force-programp
        state))))

(defun find-macro-aliases-for-defun
  (form world)
  (b* ((__function__ 'find-macro-aliases-for-defun) ((unless (and (consp form)
           (or (eq (car form) 'defun)
             (eq (car form) 'defund)))) (raise "Expected a defun form, not ~x0." form))
      (name (second form))
      (alias (car (rassoc name
            (table-alist 'macro-aliases-table world))))
      ((when alias) (list alias)))
    nil))

(defun find-macro-aliases-for-defuns
  (forms world)
  (if (atom forms)
    nil
    (append (find-macro-aliases-for-defun (car forms)
        world)
      (find-macro-aliases-for-defuns (cdr forms)
        world))))

(defun find-defun-aliases-for-macro
  (form world)
  (b* ((__function__ 'find-defun-alias-for-macro) ((unless (and (consp form) (eq (car form) 'defmacro))) (raise "Expected a defmacro form, not ~x0." form)
        (mv nil nil))
      (name (second form))
      (fn (cdr (assoc name
            (table-alist 'macro-aliases-table world))))
      ((unless fn) (mv (list name) nil))
      (defun-form (access-event-tuple-form (get-event-tuple fn world)))
      (type (car defun-form))
      ((when (eq type 'mutual-recursion)) (b* ((fns (strip-cadrs (cdr defun-form))) (macros (find-macro-aliases-for-defuns (cdr defun-form)
                world)))
          (or (and (member name macros)
              (member fn fns))
            (raise "Macro alias problem."))
          (mv macros fns)))
      ((when (eq type 'defun)) (mv (list name) (list fn))))
    (raise "Expected macro alias for ~x0 to be a mutual-recursion or defun, ~
            but found ~x1."
      name
      defun-form)
    (mv nil nil)))

(defun redundant-event
  (name force-programp state)
  (b* ((?__function__ 'redundant-event) (world (w state))
      (event-tuple (get-event-tuple name world))
      (form (access-event-tuple-form event-tuple))
      ((unless (consp form)) (raise "For ~x0: expected a valid event form, but found ~x1."
          name
          form))
      (type (car form))
      ((when (or (eq type 'defthm)
           (eq type 'defconst)
           (eq type 'defstobj)
           (eq type 'encapsulate))) (redundant-event1 name
          force-programp
          state))
      ((when (eq type 'defun)) (b* ((fn-events (redundant-event1 name
               force-programp
               state)) (defun (access-event-tuple-form event-tuple))
            (macro-names (find-macro-aliases-for-defun defun world))
            (macro-events (redundant-events1 macro-names
                force-programp
                state)))
          (append macro-events fn-events)))
      ((when (eq type 'mutual-recursion)) (b* ((fn-events (redundant-event1 name
               force-programp
               state)) (defuns (cdr (access-event-tuple-form event-tuple)))
            (macro-names (find-macro-aliases-for-defuns defuns world))
            (- (cw "Macro names for mutual recursion ~x0: ~x1.~%"
                name
                macro-names))
            (macro-events (redundant-events1 macro-names
                force-programp
                state)))
          (append macro-events fn-events)))
      ((when (eq type 'defmacro)) (b* ((defmacro (access-event-tuple-form event-tuple)) ((mv macros fns) (find-defun-aliases-for-macro defmacro world))
            (macro-events (redundant-events1 macros
                force-programp
                state))
            (fn-events (redundant-events1 fns
                force-programp
                state)))
          (append macro-events fn-events))))
    (raise "For ~x0: unsupported event type: ~x1 form: ~x2~%"
      name
      type
      (access-event-tuple-form event-tuple))))

(defun redundant-events
  (names force-programp state)
  (if (atom names)
    nil
    (append (redundant-event (car names)
        force-programp
        state)
      (redundant-events (cdr names)
        force-programp
        state))))

(defun defredundant-fn
  (names force-programp state)
  (let ((events (redundant-events names
         force-programp
         state)))
    `(encapsulate nil
      ,(IF STD::FORCE-PROGRAMP
     '(STD::PROGRAM)
     '(STD::LOGIC)) . ,STD::EVENTS)))