utilities

(in-package "ACL2S")

(include-book "kestrel/utilities/proof-builder-macros" :dir :system)

(include-book "std/util/bstar" :dir :system)

(include-book "data-structures/utilities" :dir :system)

(defxdoc acl2s-utilities
  :parents (acl2-sedan)
  :short "Utilities used in ACL2s."
  :long "<p>
This is a collection of utilities used in ACL2s, the ACL2 Sedan.
</p>
")

(defxdoc repeat-until-done
  :parents (proof-builder-commands acl2s-utilities)
  :short "A proof-builder command that repeats the given instructions
  until all goals have been proved"
  :long "<p>
@({
 Example:
 (repeat-until-done induct (repeat bash))

 General Form:
 (repeat-until-done instr1 ... instrk)
 })
</p>

<p>where each @('instri') is a proof-builder instruction.
</p>
")

(define-pc-macro repeat-until-done
  (&rest instrs)
  (value `(repeat (do-all ,@(APPEND ACL2S::INSTRS `((ACL2S::NEGATE (ACL2S::WHEN-NOT-PROVED ACL2S::FAIL))))))))

(defxdoc claim-simple
  :parents (proof-builder-commands acl2s-utilities)
  :short "(atomic macro) add a new hypothesis, without promotion"
  :long "<p>
This command is exactly like @(tsee acl2-pc::claim) except that in the
newly created goal, no promotion is performed.
</p>
<p>We found this useful when automatically generating proof builder
instructions.
</p>
")

(define-pc-atomic-macro claim-simple
  (expr &rest rest-args)
  (when-goals-trip (value (let ((rest-args-1 (if (and rest-args
               (car rest-args)
               (not (keywordp (car rest-args))))
             (list* :hints :none (cdr rest-args))
             rest-args)))
        (mv-let (pairs remaining-rest-args)
          (pair-keywords '(:do-not-flatten) rest-args-1)
          (let ((do-not-flatten-flag (cdr (assoc-eq :do-not-flatten pairs))) (temp (cadr (member-eq :hints rest-args-1))))
            (if (and temp (atom temp))
              `(protect (casesplit ,ACL2S::EXPR
                  nil
                  ,ACL2S::DO-NOT-FLATTEN-FLAG)
                change-goal
                drop-conc
                change-goal)
              `(protect (casesplit ,ACL2S::EXPR
                  nil
                  ,ACL2S::DO-NOT-FLATTEN-FLAG)
                change-goal
                drop-conc
                (prove ,@ACL2S::REMAINING-REST-ARGS)))))))))

(defxdoc pro-or-skip
  :parents (proof-builder-commands acl2s-utilities)
  :short "(atomic macro) repeatedly apply promote, if possible"
  :long "<p>
This command is exactly like @(tsee acl2-pc::pro) except that it
``succeeds'' even when no promotion is possible (e.g. if the current
goal does not contain an implication).
</p>
")

(define-pc-macro pro-or-skip
  nil
  (value `(:orelse :pro :skip)))

(defxdoc drop-or-skip
  :parents (proof-builder-commands acl2s-utilities)
  :short "(atomic macro) drop top-level hypotheses"
  :long "<p>
This command is exactly like @(tsee acl2-pc::drop) except that it
``succeeds'' when there are no top-level hypotheses and it is invoked
with no arguments.
</p>
")

(define-pc-atomic-macro drop-or-skip
  (&rest args)
  (when-goals-trip (if (and (not args) (null (hyps)))
      (value :skip)
      (value (if (consp args)
          `(:drop ,@ACL2S::ARGS)
          :drop)))))

(defxdoc retain-or-skip
  :parents (proof-builder-commands acl2s-utilities)
  :short "(atomic macro) drop all but the indicated top-level hypotheses"
  :long "<p>
This command is exactly like @(tsee acl2-pc::retain) except that it
``succeeds'' even when all hypotheses are retained.
</p>
")

(define-pc-atomic-macro retain-or-skip
  (&rest args)
  (when-goals-trip (if (not (set-difference-equal (fromto 1 (length (hyps t)))
          args))
      (value :skip)
      (value `(:retain ,@ACL2S::ARGS)))))

(defxdoc instantiate
  :parents (proof-builder-commands acl2s-utilities)
  :short "Instantiate a theorem"
  :long "<p>
@({
 Example:
 (instantiate car-cons (x (append a b)) (y nil))
 ;; This will add the following hypothesis:
 ;; (let ((x (append a b))
 ;;       (y nil))
 ;;   (equal (car (cons x y)) x))

 General Form:
 (instantiate thm-name subst1 ... substk)
 })
</p>
<p>where each @('substi') is an assignment of a variable used in the
formula associated with @('thm-name') to a term.
</p>
<p>Note that the variables used in the formula associated with
@('thm-name') may be in a different package than the one you are
currently in. In this case, explicitly specify the package when writing
variable names in substitutions.
</p>
")

(define-pc-macro instantiate
  (lemma-name &rest substitutions)
  (b* ((wrld (w state)) (formula (formula lemma-name t wrld))
      ((when (not formula)) (pprogn (print-no-change "Bad lemma-name argument to INSTANTIATE, ~x0. The ~
                          lemma-name argument should be a name associated with ~
                          a formula."
            (list (cons #\0 lemma-name)))
          (value :fail))))
    (value `(:claim (let ,ACL2S::SUBSTITUTIONS
          ,ACL2S::FORMULA)
        :hints (("Goal" :instructions (:pro-or-skip :drop-or-skip (:expand nil)
             (:prove :hints (("Goal" :by (:instance ,ACL2S::LEMMA-NAME ,@ACL2S::SUBSTITUTIONS)))))))))))

(defxdoc split-in-theory
  :parents (proof-builder-commands acl2s-utilities)
  :short "Split using an optional theory"
  :long "<p>
@({
 Examples:
 (split-in-theory)
 ;; Same as split, using the same theory split uses, namely
 ;; acl2::minimal-theory

 (split-in-theory thy)
 ;; Same as split, but use thy instead of the default
 ;; acl2::minimal-theory

 General Form:
 (split-in-theory thy)
 })
</p>
<p>where @('thy') is an optional theory.
</p>
")

(define-pc-atomic-macro split-in-theory
  (&optional thy)
  (value `(:prove :hints (("Goal" :do-not-induct proof-builder
         :do-not '(generalize eliminate-destructors
           fertilize
           eliminate-irrelevance)
         :in-theory (theory ',(OR ACL2S::THY 'MINIMAL-THEORY)))))))

(defxdoc by
  :parents (proof-builder-commands acl2s-utilities)
  :short "(atomic macro) prove using an existing theorem"
  :long "<p>
@({
 Example:
 (by car-cons (x (append a b)) (y nil))
 ;; This will attempt to prove the current goal by applying
 ;; the theorem car-cons with the given substitution.

 General Form:
 (by thm-name subst1 ... substk)
 })
</p>
<p>Under the hood, this command simply calls @(tsee acl2-pc::prove)
with the appropriate @(':by') hint.
</p>
")

(define-pc-atomic-macro by
  (lemma-name &rest substitutions)
  (value `(:prove :hints (("Goal" :by ,@(IF ACL2S::SUBSTITUTIONS
      `((:INSTANCE ,ACL2S::LEMMA-NAME ,@ACL2S::SUBSTITUTIONS))
      `(,ACL2S::LEMMA-NAME)))))))

(defxdoc cg-or-skip
  :parents (proof-builder-commands acl2s-utilities)
  :short "(atomic macro) change goals when needed"
  :long "<p>
This command is exactly like @(tsee acl2-pc::cg) except that it
``succeeds'' when the current goal is equal to the specified goal,
where @('cg') would fail.
</p>
")

(define-pc-atomic-macro cg-or-skip
  (&optional name)
  (when-goals-trip (if (and (goals t) (equal name (goal-name t)))
      (value :skip)
      (value `(:cg ,ACL2S::NAME)))))

(defxdoc make-n-ary-macro
  :parents (acl2s-utilities)
  :short "A macro that
creates an arbitrary-arity macro given a binary function
and associates the function name with the macro name using
@(see add-macro-fn)."
  :long "<p>
@({
 Examples:
 (make-n-ary-macro set-union binary-set-union nil t)

 (make-n-ary-macro ^ expt 1)

 General Form:
 (make-n-ary-macro new-macro-name binary-fun-name identity right-associate-p)
 })
</p>

<p>where @('new-macro-name') is the name of the macro to define,
@('binary-fun-name') is the name of an existing binary function and
@('identity') is what the macro should return with no arguments.
@('right-associate-p') is an optional argument, which when set to
@('t') flattens right-associated arguments (see @(see add-macro-fn)).
</p>

<p>
Given
one argument, the macro will just return that argument. Given more
than one argument, the macro will expand to a right-associated call of
the function. For example:

@({
(set-union) expands to nil

(set-union arg1) expands to arg1

(set-union arg1 arg2) expands to (binary-set-union arg1 arg2)

(set-union arg1 arg2 arg3) expands to
(binary-set-union arg1 (binary-set-union arg2 arg3))

and so on.
})
</p>
")

(defun pkgp
  (pkg)
  (declare (xargs :guard t))
  (and (stringp pkg) (not (equal pkg ""))))

(defmacro make-n-ary-macro
  (macro bin-fun
    id
    &optional
    right-associate-p)
  (declare (xargs :guard (and (symbolp macro)
        (symbolp bin-fun)
        (booleanp right-associate-p))))
  `(progn (defmacro ,ACL2S::MACRO
      (&rest rst)
      (cond ((null rst) ,ACL2S::ID)
        ((null (cdr rst)) (car rst))
        (t (xxxjoin ',ACL2S::BIN-FUN rst))))
    (add-macro-fn ,ACL2S::MACRO
      ,ACL2S::BIN-FUN
      ,ACL2S::RIGHT-ASSOCIATE-P)))

(defxdoc test-then-skip-proofs
  :parents (acl2s-utilities cgen)
  :short "The ACL2s version of @('skip-proofs')."
  :long "<p>
A macro that is similar to @('skip-proofs'), except that we first perform
testing. The macro supports testing for @(see thm),
@(see defthm), @(see defcong), @(see defequiv), and
@(see defrefinement) forms. All other forms are just turned into
@('skip-proof')s forms, without testing.
</p>
")

(defun gen-acl2s-local-fn
  (var val forms)
  (declare (xargs :mode :program))
  (b* ((set `(with-output :off :all :on (error)
         (local (acl2s-defaults :set ,ACL2S::VAR ,ACL2S::VAL)))) (forms (collect$ '(lambda (x)
            (cons 'with-output
              (cons ':stack (cons ':pop (cons x 'nil)))))
          forms)))
    `(with-output :off :all :stack :push (encapsulate nil ,SET ,@ACL2S::FORMS))))

(defmacro gen-acl2s-local
  (var val forms)
  (gen-acl2s-local-fn var
    val
    forms))

(defmacro test-then-skip-proofs
  (thm)
  (declare (xargs :guard (true-listp thm)))
  (cond ((equal (car thm) 'defthm) `(gen-acl2s-local testing-enabled
        t
        ((test? ,(THIRD ACL2S::THM)) (skip-proofs ,ACL2S::THM))))
    ((equal (car thm) 'thm) `(gen-acl2s-local testing-enabled
        t
        ((test? ,(SECOND ACL2S::THM)) (skip-proofs ,ACL2S::THM))))
    ((member (car thm)
       '(defcong defequiv defrefinement)) `(with-output :off :all :on (error)
        :stack :push (make-event (er-let* ((defthm (macroexpand1* ',ACL2S::THM
                 'ctx
                 (w state)
                 state)) (form (trans-eval (cadadr defthm)
                  'ctx
                  state
                  t)))
            (value `(with-output :stack :pop (gen-acl2s-local testing-enabled
                  t
                  ((test? ,(THIRD (CDR ACL2S::FORM))) (skip-proofs ,',ACL2S::THM)))))))))
    (t `(skip-proofs ,ACL2S::THM))))

(defxdoc thm-no-test
  :parents (acl2s-utilities cgen)
  :short "A version of @('thm') with testing disabled."
  :long "<p>
A macro that locally turns off @('cgen') testing and then calls @('thm').
</p>
")

(defmacro thm-no-test
  (&rest args)
  `(gen-acl2s-local testing-enabled
    nil
    ((thm ,@ACL2S::ARGS))))

(defxdoc defthm-no-test
  :parents (acl2s-utilities cgen)
  :short "A version of @('defthm') with testing disabled."
  :long "<p>
A macro that locally turns off @('cgen') testing and then calls @('defthm').
</p>
")

(defmacro defthm-no-test
  (name &rest args)
  `(gen-acl2s-local testing-enabled
    nil
    ((defthm ,ACL2S::NAME ,@ACL2S::ARGS))))

(defxdoc defthmd-no-test
  :parents (acl2s-utilities cgen)
  :short "A version of @('defthmd') with testing disabled."
  :long "<p>
A macro that locally turns off @('cgen') testing and then calls @('defthmd').
</p>
")

(defmacro defthmd-no-test
  (name &rest args)
  `(gen-acl2s-local testing-enabled
    nil
    ((defthmd ,ACL2S::NAME ,@ACL2S::ARGS))))

(defun best-package
  (x y)
  (declare (xargs :guard (and (stringp x) (stringp y))))
  (let* ((p '("" "ACL2-INPUT-CHANNEL"
         "ACL2-OUTPUT-CHANNEL"
         *main-lisp-package-name*
         "COMMON-LISP"
         "LISP"
         "KEYWORD"
         "CGEN"
         "DEFDATA"
         "ACL2"
         "ACL2S")) (ly (len (member-equal y p)))
      (lx (len (member-equal x p))))
    (if (< lx ly)
      x
      y)))

(defun best-package-symbl-list
  (l s)
  (declare (xargs :guard (and (atom-listp l) (stringp s))))
  (cond ((endp l) s)
    ((symbolp (car l)) (best-package-symbl-list (cdr l)
        (best-package (symbol-package-name (car l))
          s)))
    (t (best-package-symbl-list (cdr l) s))))

(defthm best-package-symbl-list-stringp
  (implies (and (atom-listp l) (stringp s))
    (stringp (best-package-symbl-list l s))))

(defthm best-package-symbl-list-not-empty
  (implies (and (atom-listp l) (pkgp s))
    (not (equal (best-package-symbl-list l s)
        ""))))

(defun gen-keyword
  (symbol)
  (intern (symbol-name symbol) "KEYWORD"))

(defun fix-sym
  (sym)
  (declare (xargs :guard (symbolp sym)))
  (if (equal (symbol-package-name sym)
      *main-lisp-package-name*)
    (pkg-witness "ACL2")
    sym))

(defthm character-listp-explode-nonnegative-integer
  (implies (and (integerp x)
      (<= 0 x)
      (print-base-p b)
      (character-listp ans))
    (character-listp (explode-nonnegative-integer x
        b
        ans))))

(defthm character-listp-explode-atom
  (implies (and (acl2-numberp x)
      (print-base-p b))
    (character-listp (explode-atom x b))))

(verify-termination fix-sym)

(verify-termination pack-to-string)

(verify-termination gen-sym-sym)

(verify-guards fix-sym)

(verify-guards pack-to-string)

(verify-guards gen-sym-sym)

(defun gen-sym-pkg
  (l pkg)
  (declare (xargs :guard (and (atom-listp l)
        (or (null pkg) (pkgp pkg)))))
  (fix-intern$ (pack-to-string l)
    pkg))

(defun make-symbl
  (l pkg)
  (declare (xargs :guard (and (atom-listp l)
        (or (null pkg) (pkgp pkg)))))
  (fix-intern$ (pack-to-string l)
    (if pkg
      pkg
      (best-package-symbl-list l "ACL2"))))

(defun mk-acl2s-sym
  (l)
  (declare (xargs :guard (atom-listp l)))
  (make-symbl l "ACL2S"))

(defmacro make-sym
  (s suf &optional pkg)
  (declare (xargs :guard t))
  `(make-symbl (list ,ACL2S::S '- ,ACL2S::SUF)
    ,ACL2S::PKG))

(defun get-alist
  (key alist)
  (declare (xargs :guard (alistp alist)))
  (cdr (assoc-equal key alist)))

(defxdoc n<
  :parents (acl2s-utilities well-founded-relation)
  :short "The well-founded less-than relation on natural numbers."
  :long "<p>
If @('x') and @('y') are both natural numbers then @('(n< x y)') is true
iff @('x') is strictly less than @('y'). @('n<') is well-founded on the natural
numbers and is useful for beginners who want to use measure
functions over natural numbers.
</p>
")

(defun nat-id
  (x)
  (declare (xargs :guard (natp x)))
  x)

(defun n<
  (x y)
  (declare (xargs :guard (and (natp x) (natp y))))
  (< x y))

(defthm less-than-is-well-founded-relation
  (and (implies (natp x)
      (o-p (nat-id x)))
    (implies (and (natp x)
        (natp y)
        (n< x y))
      (o< (nat-id x)
        (nat-id y))))
  :rule-classes :well-founded-relation)

(defmacro defthm-test-no-proof
  (name &rest args)
  `(gen-acl2s-local testing-enabled
    t
    ((test? ,@ACL2S::ARGS) (skip-proofs (defthm ,ACL2S::NAME ,@ACL2S::ARGS)))))

(defmacro defthmskipall
  (name &rest args)
  `(skip-proofs (defthm-no-test ,ACL2S::NAME ,@ACL2S::ARGS)))

(defmacro defun-no-test
  (name &rest args)
  `(gen-acl2s-local testing-enabled
    nil
    ((defun ,ACL2S::NAME ,@ACL2S::ARGS))))

(defun tbl-set-fn
  (tbl key val)
  `(table ,ACL2S::TBL ,ACL2S::KEY ,ACL2S::VAL))

(defun tbl-get-fn
  (tbl key)
  `(b* ((wrld (w state)))
    (cdr (assoc-eq ,ACL2S::KEY
        (table-alist ',ACL2S::TBL wrld)))))

(defun all-tlps
  (l)
  (declare (xargs :guard t))
  (or (atom l)
    (and (true-listp l)
      (all-tlps (car l))
      (all-tlps (cdr l)))))

(defun eqlable-2-alistp
  (x)
  (declare (xargs :guard t))
  (if (atom x)
    (null x)
    (and (consp (car x))
      (eqlablep (caar x))
      (eqlable-alistp (cdar x))
      (eqlable-2-alistp (cdr x)))))

(defthm eqlable-2-alistp-eqlable-alistp
  (implies (eqlable-2-alistp a)
    (eqlable-alistp a)))

(mutual-recursion (defun subst-var
    (new old form)
    (declare (xargs :guard (atom old)))
    (cond ((atom form) (cond ((equal form old) new)
          (t form)))
      ((fquotep form) form)
      (t (cons (car form)
          (subst-var-lst new
            old
            (cdr form))))))
  (defun subst-var-lst
    (new old l)
    (declare (xargs :guard (atom old)))
    (cond ((atom l) nil)
      (t (cons (subst-var new old (car l))
          (subst-var-lst new old (cdr l)))))))

(mutual-recursion (defun subst-fun-sym
    (new old form)
    (declare (xargs :guard (and (symbolp old) (symbolp new))))
    (cond ((atom form) form)
      ((fquotep form) form)
      (t (cons (if (atom (car form))
            (subst-var new old (car form))
            (subst-fun-sym new
              old
              (car form)))
          (subst-fun-lst new
            old
            (cdr form))))))
  (defun subst-fun-lst
    (new old l)
    (declare (xargs :guard (and (symbolp old) (symbolp new))))
    (cond ((atom l) nil)
      (t (cons (subst-fun-sym new old (car l))
          (subst-fun-lst new old (cdr l)))))))

(mutual-recursion (defun subst-expr1
    (new old term)
    (declare (xargs :guard t :guard-debug t))
    (cond ((equal term old) new)
      ((atom term) term)
      ((quotep term) term)
      (t (cons (car term)
          (subst-expr1-lst new
            old
            (cdr term))))))
  (defun subst-expr1-lst
    (new old args)
    (declare (xargs :guard t))
    (if (atom args)
      nil
      (cons (subst-expr1 new old (car args))
        (subst-expr1-lst new
          old
          (cdr args))))))

(defun subst-expr
  (new old term)
  (declare (xargs :guard (not (quotep old))))
  (if (atom old)
    (subst-var new old term)
    (subst-expr1 new old term)))

(defconst *contract-checking-values*
  '(:on :off))

(defmacro set-contract-checking
  (flg)
  (declare (xargs :guard (let ((flg (if (and (consp flg)
               (eq (car flg) 'quote)
               (consp (cdr flg)))
             (cadr flg)
             flg)))
        (member-eq flg
          *contract-checking-values*))))
  `(let* ((current-flg (f-get-global 'guard-checking-on state)) (flg ,(IF (AND (CONSP ACL2S::FLG) (EQ (CAR ACL2S::FLG) 'QUOTE)
          (CONSP (CDR ACL2S::FLG)))
     (CADR ACL2S::FLG)
     ACL2S::FLG))
      (gflg (if (eq flg :off)
          nil
          :all)))
    (cond ((and (raw-mode-p state) flg) (er soft
          'set-contract-checking
          "It is illegal (and anyhow, would be useless) to attempt to modify ~
            contract checking while in raw mode, since contracts are not checked in ~
            raw mode."))
      ((eq gflg current-flg) (pprogn (fms "Contract-checking already has value ~x0.~%~%"
            (list (cons #\0 flg))
            *standard-co*
            state
            nil)
          (value :invisible)))
      ((eq flg :off) (pprogn (f-put-global 'guard-checking-on
            nil
            state)
          (fms "Turning contract-checking :OFF.~%~%"
            nil
            *standard-co*
            state
            nil)
          (value :invisible)))
      (t (pprogn (f-put-global 'guard-checking-on
            gflg
            state)
          (assert$ (and gflg (not (eq gflg current-flg)))
            (fms "Turning contract-checking :ON.~%~%"
              nil
              *standard-co*
              state
              nil))
          (value :invisible))))))

(defun rquotep
  (x)
  (declare (xargs :guard t))
  (and (consp x)
    (consp (cdr x))
    (eq (car x) 'quote)
    (null (cddr x))))

(defun rfquotep
  (x)
  (declare (xargs :guard (consp x)))
  (and (consp (cdr x))
    (eq (car x) 'quote)
    (null (cdr (cdr x)))))

(defloop rquote-listp
  (xs)
  (declare (xargs :guard t))
  (for ((x in xs))
    (always (rquotep x))))

(defloop unrquote-lst
  (xs)
  (declare (xargs :guard (rquote-listp xs)))
  (for ((x in xs))
    (collect (unquote x))))

(defmacro def-const
  (name form &optional doc)
  `(with-output :off :all :gag-mode nil
    :stack :push (make-event (let ((form ,ACL2S::FORM))
        `(with-output :stack :pop (defconst ,',ACL2S::NAME
            ',ACL2S::FORM
            ,@(AND ,ACL2S::DOC '(,ACL2S::DOC))))))))

(mutual-recursion (defun find-first-call
    (fn term)
    (cond ((variablep term) nil)
      ((fquotep term) nil)
      ((equal (ffn-symb term) fn) term)
      (t (find-first-call-lst fn (fargs term)))))
  (defun find-first-call-lst
    (fn lst)
    (cond ((endp lst) nil)
      (t (or (find-first-call fn (car lst))
          (find-first-call-lst fn (cdr lst)))))))

(defun stage1
  (fn max clause flg)
  (let ((temp (and flg
         (find-first-call-lst fn clause))))
    (if temp
      (if (zp max)
        (cw "~%~%HINT PROBLEM:  The maximum repetition count of ~
                your STAGE hint been reached without eliminating ~
                all of the calls of ~x0.  You could supply a larger ~
                count with the optional second argument to STAGE ~
                (which defaults to 100).  But think about what is ~
                happening! Is each stage permanently eliminating a ~
                call of ~x0?~%~%"
          fn)
        `(:computed-hint-replacement ((stage1 ',ACL2S::FN
             ,(- MAX 1)
             clause
             stable-under-simplificationp))
          :expand (,ACL2S::TEMP)))
      nil)))

(defmacro stage
  (fn &optional (max '100))
  `(stage1 ',ACL2S::FN
    ,MAX
    clause
    stable-under-simplificationp))

(defun pair-tl
  (x y)
  (if (or (endp x) (endp y))
    nil
    (cons (list (car x) (car y))
      (pair-tl (cdr x) (cdr y)))))

(defun stage-rule1
  (fn def-rule
    vars
    max
    clause
    flg)
  (let ((temp (and flg
         (find-first-call-lst fn clause))))
    (if temp
      (if (zp max)
        (cw "~%~%HINT PROBLEM:  The maximum repetition count of ~
                your STAGE hint been reached without eliminating ~
                all of the calls of ~x0.  You could supply a larger ~
                count with the optional second argument to STAGE ~
                (which defaults to 100).  But think about what is ~
                happening! Is each stage permanently eliminating a ~
                call of ~x0?~%~%"
          fn)
        `(:computed-hint-replacement ((stage-rule1 ',ACL2S::FN
             ',ACL2S::DEF-RULE
             ',ACL2S::VARS
             ,(- MAX 1)
             clause
             stable-under-simplificationp))
          :expand (:with ,ACL2S::DEF-RULE ,ACL2S::TEMP)))
      nil)))

(defmacro stage-rule
  (fn def-rule &optional (max '100) vars)
  `(stage-rule1 ',ACL2S::FN
    ',ACL2S::DEF-RULE
    (or ,ACL2S::VARS
      (formals ',ACL2S::FN (w state)))
    ,MAX
    clause
    stable-under-simplificationp))

(defmacro cw?
  (verbose-flag &rest rst)
  `(if ,ACL2S::VERBOSE-FLAG
    (cw ,@ACL2S::RST)
    nil))

(defmacro ecw
  (&rest rst)
  `(prog2$ (cw ,@(BUTLAST ACL2S::RST 1))
    (mv t ,(CAR (LAST ACL2S::RST)) state)))

(defmacro ecw?
  (verbose-flag &rest rst)
  `(if ,ACL2S::VERBOSE-FLAG
    (ecw ,@ACL2S::RST)
    nil))

(defun remove-dups-aux
  (l seen)
  (declare (xargs :guard (and (true-listp l)
        (true-listp seen))))
  (cond ((endp l) (revappend seen nil))
    ((member-equal (car l) seen) (remove-dups-aux (cdr l) seen))
    (t (remove-dups-aux (cdr l)
        (cons (car l) seen)))))

(defthm remove-dups-aux-tp
  (implies (and (true-listp l)
      (true-listp seen))
    (true-listp (remove-dups-aux l seen)))
  :rule-classes :type-prescription)

(defun remove-dups
  (l)
  (declare (xargs :guard (true-listp l)))
  (remove-dups-aux l nil))

(defthm remove-dups-tp
  (implies (true-listp l)
    (true-listp (remove-dups l)))
  :rule-classes :type-prescription)

(defxdoc remove-dups
  :parents (acl2s-utilities)
  :short "Remove duplicates from a true list and maintain the order of elements."
  :long "<p>
If @('l') is a true list then @('(remove-dups l)') is a true list with
no duplicates. In contrast with @(see? remove-duplicates), the order of
elements is the same. That is, if @('x') and @('y') appear in @('l')
and the first occurrence of @('x') appears before the first occurrence of
@('y') in @('l'), then @('x') appears before @('y') in
@('(remove-dups l)').
</p>
")