utilities

(in-package "U")

(include-book "xdoc/top" :dir :system)

(defxdoc utilities
  :parents (data-structures)
  :short "A book of utility functions residing in the package "U".")

(defun import-as-macros-fn
  (package-symbol symbols)
  (declare (xargs :guard (and (symbolp package-symbol) (symbol-listp symbols))
      :verify-guards nil))
  (cond ((atom symbols) nil)
    (t (cons (let ((sym (car symbols)))
          `(defmacro ,U::SYM
            (&rest forms)
            (cons ',(INTERN-IN-PACKAGE-OF-SYMBOL (STRING U::SYM) U::PACKAGE-SYMBOL)
              forms)))
        (import-as-macros-fn package-symbol (cdr symbols))))))

(defmacro import-as-macros
  (package-symbol &rest symbols)
  `(progn ,@(U::IMPORT-AS-MACROS-FN U::PACKAGE-SYMBOL U::SYMBOLS)))

(import-as-macros a-symbol-unique-to-the-acl2-package
  arglistp
  conjoin
  translate-declaration-to-guard-var-lst)

(defxdoc defloop
  :parents (utilities)
  :short "Macro for defining simple iteration schemes as functions."
  :long "<p>Syntax:</p>

@({
   DEFLOOP name arglist [documentation] {declaration}* loop-form

   loop-form ::= (FOR ({!for-clause}+) main-clause)

   for-clause ::= for-in-clause | for-on-clause

   for-in-clause ::= (var IN arg [ BY fn ])

   for-on-clause ::= (var ON arg [ BY fn ])

   main-clause ::= !list-accumulation | (!conditional form !value-clause) |
                   (!termination-test form)

   value-clause ::= !list-accumulation | (RETURN form)

   list-accumulation ::= ({COLLECT | APPEND} form)

   value-clause ::= ({COLLECT | APPEND | RETURN} form)

   conditional ::= IF | WHEN | UNLESS

   termination-test ::= ALWAYS | THEREIS | NEVER
})

<p>Arguments and Values:</p>

@({
   arg -- a symbol appearing in the arglist.

   arglist -- an argument list satisfying ACL2::ARGLISTP.

   declaration -- any valid declaration.

   documentation -- a string; not evaluated.

   form -- a form.

   fn -- a symbol; must be the function symbol of a unary function
         well-defined on true lists.

   var -- a symbol.

   name -- a symbol.
})

<p>Special Note: The symbols FOR, IN, ON, BY, RETURN, COLLECT, APPEND, IF,
WHEN, UNLESS, ALWAYS, THEREIS, and NEVER appearing above may be in any package;
DEFLOOP checks the print name of the symbol, not the symbol itself.</p>

<h3>Description</h3>

<p>DEFLOOP is a macro that creates iterative functions.  The description of the
iteration is specified with an abstract syntax based on a small but useful
subset of the Common Lisp LOOP construct (as defined by ANSI X3J13).  Using
DEFLOOP one can easily define functions analogous to MAPCAR and MAPCAN, list
type recognizers, and MEMBER- and ASSOC-like functions.</p>

<p>The syntax of DEFLOOP is similar to DEFUN: The function name is followed by
the arglist, optional documentation and declarations, and the function body.
Note that any guards on any of the arguments are the responsibility of the
user.</p>

<p>The function body is in a special format, i.e., the loop-form as defined in
the Syntax description.</p>

<p>Each for-clause defines an iteration on one of the args in arglist.  The
 for-in-clause</p>

@({ (var IN arg [ BY fn ]) })

<p>specifies that in each iteration, var will be bound to successive CARs of
 arg, and arg will be reduced by fn on each iteration.  The default value of fn
 is CDR.  The for-on-clause</p>

@({ (var ON arg [ BY fn ]) })

<p>specifies that var will first be bound to arg, and then reduced by fn on
each iteration.  Again, the default value of fn is CDR.</p>

<p>Using a list-accumulation one can specify MAPCAR- and MAPCAN-like functions.
 Here is an example of how the Acl2 function STRIP-CARS could be defined with
 DEFLOOP:</p>

@({
 (DEFLOOP STRIP-CARS (L)
   (DECLARE (XARGS :GUARD (ALISTP L)))
   (FOR ((X IN L))
        (COLLECT (CAR X))))
})

<p>Iteration on multiple lists may be specified; iteration will terminate as
soon as any of the lists are ATOMic, e.g.,</p>

@({
 (DEFLOOP PAIRLIS$ (KEYS VALS)
   (DECLARE (XARGS :GUARD (AND (TRUE-LISTP KEYS)
                               (TRUE-LISTP VALS))))
   (FOR ((KEY IN KEYS) (VAL IN VALS))
        (COLLECT (CONS KEY VAL))))
})

<p>This example shows reduction by a function other than CDR:</p>

@({ (DEFLOOP EVENS (L) (FOR ((X IN L BY CDDR)) (COLLECT X))) })

<p>List-accumulations can be coupled with a test, e.g., this function that
 selects all of the numbers &lt;= n from l, and the ODDS function:</p>

@({
 (DEFLOOP <=-LIST (N L)
   (DECLARE (XARGS :GUARD (AND (INTEGERP N)
                               (INTEGERP-LISTP L))))
   (FOR ((X IN L))
        (WHEN (<= X N)
          (COLLECT X))))

 (DEFLOOP ODDS (L)
   (DECLARE (XARGS :GUARD (TRUE-LISTP L)))
   (FOR ((TAIL ON L BY CDDR))
        (UNLESS (NULL (CDR TAIL))
          (COLLECT (CADR TAIL)))))
})

<p>The definition of @('<=-LIST') shows that any functional arguments may
 appear free in the various DEFLOOP forms.  Non-iterated arguments are simply
 passed unchanged during recursive calls.  Also note that IF and WHEN are
 synonymous as DEFLOOP tests.</p>

<p>A RETURN can also be coupled with a test.  If the test is never satisfied
 then the resulting function will return NIL.  Here are examples of how
 ASSOC-EQUAL and MEMBER-EQUAL could have been defined with DEFLOOP:</p>

@({
 (DEFLOOP ASSOC-EQUAL (KEY ALIST)
   (DECLARE (XARGS :GUARD (ALISTP ALIST)))
   (FOR ((PAIR IN ALIST))
        (WHEN (EQUAL KEY (CAR PAIR))
          (RETURN PAIR))))

 (DEFLOOP MEMBER-EQUAL (X L)
   (DECLARE (XARGS :GUARD (TRUE-LISTP L)))
   (FOR ((TAIL ON L))
        (WHEN (EQUAL X (CAR TAIL))
          (RETURN TAIL))))
})

<p>The termination-tests can be used to create various recognizers and
 `un'-recognizers.  Note that a DEFLOOP with a termination test of ALWAYS or
 NEVER will only return T if iteration terminates on NIL, i.e, they only
 recognize true lists.  The termination test (THEREIS form) will return
 the first non-NIL value returned by form, or NIL if there is none.
 Here for example are functions that recognize true lists of integers,
 true lists of un-integers, and lists containing an integer:</p>

@({
 (DEFLOOP INTEGERP-LISTP (L) (FOR ((X IN L)) (ALWAYS (INTEGERP X))))

 (DEFLOOP NO-INTEGERP-LISTP (L) (FOR ((X IN L)) (NEVER (INTEGERP X))))

 (DEFLOOP HAS-INTEGERP-LISTP (L) (FOR ((X IN L)) (THEREIS (INTEGERP X))))
})

<p>Note that in accordance with the semantics of the LOOP construct, the
 THEREIS form above simply returns the first non-NIL result computed.  If you
 want a function that returns the first integer in a list then you can use a
 conditional return:</p>

@({
 (DEFLOOP FIRST-INTEGER (L)
   (FOR ((X IN L)) (IF (INTEGERP X) (RETURN X))))
})

<p>Final note: If in doubt, simply TRANS1 the DEFLOOP form and have a look at
 the generated function.</p>")

(encapsulate nil
  (program)
  (defmacro bomb
    (ctx str &rest args)
    `(er hard ,U::CTX ,U::STR ,@U::ARGS))
  (defconst *defloop-accumulators*
    '("COLLECT" "APPEND"))
  (defconst *defloop-conditionals*
    '("IF" "WHEN" "UNLESS"))
  (defconst *defloop-terminators*
    '("ALWAYS" "NEVER" "THEREIS"))
  (defconst *defloop-main-clause-legal-cars*
    (append *defloop-accumulators*
      *defloop-conditionals*
      *defloop-terminators*))
  (defconst *defloop-value-clause-legal-cars*
    (cons "RETURN" *defloop-accumulators*))
  (defconst *defloop-accum/terms*
    (append *defloop-accumulators* *defloop-terminators*))
  (defun defloop-strip-nth
    (n l)
    (declare (xargs :guard (and (integerp n) (>= n 0) (true-list-listp l))))
    (cond ((endp l) nil)
      (t (cons (nth n (car l))
          (defloop-strip-nth n (cdr l))))))
  (defun defloop-main-clause-syntax-error
    (main-clause)
    (cond ((not (and (true-listp main-clause)
           (symbolp (first main-clause))
           (member-equal (string (first main-clause))
             *defloop-main-clause-legal-cars*))) (msg "The main-clause must be a true list whose first ~
          element is a symbol whose print name is one of ~v0."
          *defloop-main-clause-legal-cars*))
      ((member-equal (string (first main-clause))
         *defloop-accumulators*) (and (not (equal (length main-clause) 2))
          (msg "Invalid list-accumulation: ~p0." main-clause)))
      ((member-equal (string (first main-clause))
         *defloop-terminators*) (and (not (equal (length main-clause) 2))
          (msg "Invalid termination form: ~p0." main-clause)))
      ((member-equal (string (first main-clause))
         *defloop-conditionals*) (cond ((not (equal (length main-clause) 3)) (msg "Invalid conditional form: ~p0." main-clause))
          (t (let ((value-clause (third main-clause)))
              (and (not (true-listp value-clause))
                (not (equal (length value-clause) 2))
                (not (symbolp (first value-clause)))
                (not (member-equal (string (first value-clause))
                    *defloop-value-clause-legal-cars*))
                (msg "Invalid value-clause: ~p0." value-clause))))))))
  (defun defloop-for-clauses-syntax-error1
    (for-clauses arglist)
    (cond ((atom for-clauses) nil)
      (t (let ((clause (car for-clauses)))
          (cond ((not (and (true-listp clause)
                 (>= (length clause) 3)
                 (symbolp (first clause))
                 (symbolp (second clause))
                 (member-equal (string (second clause)) '("IN" "ON"))
                 (symbolp (third clause))
                 (member (third clause) arglist)
                 (implies (> (length clause) 3)
                   (and (equal (length clause) 5)
                     (symbolp (fourth clause))
                     (equal (string (fourth clause)) "BY")
                     (symbolp (fifth clause)))))) (msg "A for-clause must be of the form:
 (var {IN | ON} arg [ BY fn ])
where var is a symbol, arg is a symbol in ~
the arglist, and fn is a symbol, but ~p0 does not satisfy these constraints."
                clause))
            (t (defloop-for-clauses-syntax-error1 (cdr for-clauses)
                arglist)))))))
  (defun defloop-for-clauses-syntax-error
    (for-clauses arglist)
    (cond ((not (and (true-listp for-clauses) for-clauses)) (msg "The for-clauses must be a non-empty true list but ~p0 is not."
          for-clauses))
      ((defloop-for-clauses-syntax-error1 for-clauses
         arglist))
      ((duplicates (defloop-strip-nth 0 for-clauses)) (msg "Multiple bindings for free-var~#0~[~/s~] ~&0."
          (duplicates (defloop-strip-nth 0 arglist))))
      ((duplicates (defloop-strip-nth 2 for-clauses)) (msg "Multiple for-clauses for arg~#0~[~/s~] ~&0."
          (duplicates (defloop-strip-nth 2 arglist))))
      (t nil)))
  (defun defloop-syntax-error
    (name arglist forms)
    (let ((err (cond ((not (symbolp name)) (msg "The name must be a symbol, but ~p0 is not."
               name))
           ((not (arglistp arglist)) (msg "The arglist must be a valid functional argument list as defined ~
          by ACL2::ARGLISTP, but ~p0 is not."
               arglist))
           ((null forms) (msg "You neglected to include a function body!"))
           (t (let ((loop-form (car (last forms))))
               (cond ((not (and (true-listp loop-form)
                      (equal (length loop-form) 3)
                      (symbolp (first loop-form))
                      (equal (string (first loop-form)) "FOR"))) (msg "The loop-form must be a true list of length 3 whose CAR is ~
              a symbol named FOR, but ~p0 is not."
                     loop-form))
                 ((defloop-for-clauses-syntax-error (second loop-form)
                    arglist))
                 ((defloop-main-clause-syntax-error (third loop-form)))
                 (t nil)))))))
      (if err
        (bomb 'defloop "Syntax error. ~@0" err)
        nil)))
  (defun defloop-atomize
    (l)
    (cond ((null l) nil)
      (t (cons `(atom ,(CAR U::L)) (defloop-atomize (cdr l))))))
  (defun defloop-disjoin
    (l)
    (cond ((atom l) l)
      ((and (consp l) (atom (cdr l))) (car l))
      (t `(or ,@U::L))))
  (defun defloop-by-alist
    (for-clauses)
    (cond ((atom for-clauses) nil)
      (t (let ((clause (car for-clauses)))
          (cons (cons (third clause)
              (cond ((fifth clause) `(,(FIFTH U::CLAUSE) ,(THIRD U::CLAUSE)))
                (t `(cdr ,(THIRD U::CLAUSE)))))
            (defloop-by-alist (cdr for-clauses)))))))
  (defun defloop-reduce-args1
    (arglist alist)
    (cond ((atom arglist) nil)
      (t (cons (let ((pair (assoc (car arglist) alist)))
            (if pair
              (cdr pair)
              (car arglist)))
          (defloop-reduce-args1 (cdr arglist) alist)))))
  (defun defloop-reduce-args
    (arglist for-clauses)
    (defloop-reduce-args1 arglist
      (defloop-by-alist for-clauses)))
  (defun defloop-lambda-args
    (for-clauses)
    (cond ((atom for-clauses) nil)
      (t (cons (let ((clause (car for-clauses)))
            (cond ((equal (string (second clause)) "IN") `(car ,(THIRD U::CLAUSE)))
              ((equal (string (second clause)) "ON") (third clause))
              (t (bomb 'defloop-lambda-args "Bug."))))
          (defloop-lambda-args (cdr for-clauses))))))
  (defun defloop-applied-lambda
    (for-clauses body invertp)
    `((lambda ,(U::DEFLOOP-STRIP-NTH 0 U::FOR-CLAUSES)
       ,(IF U::INVERTP
     `(NOT ,U::BODY)
     U::BODY)) ,@(U::DEFLOOP-LAMBDA-ARGS U::FOR-CLAUSES)))
  (defun defloop-atom-null-check
    (for-clauses)
    (cond ((null (cdr for-clauses)) `(null ,(NTH 2 (CAR U::FOR-CLAUSES))))
      (t `(if (atom ,(NTH 2 (CAR U::FOR-CLAUSES)))
          (null ,(NTH 2 (CAR U::FOR-CLAUSES)))
          ,(U::DEFLOOP-ATOM-NULL-CHECK (CDR U::FOR-CLAUSES))))))
  (defun defloop-accum/term
    (name arglist
      decls
      for-clauses
      main-clause
      main-car)
    `(defun ,U::NAME
      ,U::ARGLIST
      ,@U::DECLS
      (cond (,(U::DEFLOOP-DISJOIN
  (U::DEFLOOP-ATOMIZE (U::DEFLOOP-STRIP-NTH 2 U::FOR-CLAUSES))) ,(COND ((U::MEMBER-EQUAL U::MAIN-CAR '("COLLECT" "APPEND" "THEREIS")) 'NIL)
       ((U::MEMBER-EQUAL U::MAIN-CAR '("ALWAYS" "NEVER"))
        (U::DEFLOOP-ATOM-NULL-CHECK U::FOR-CLAUSES))))
        (t (,(COND ((EQUAL U::MAIN-CAR "COLLECT") 'CONS)
       ((EQUAL U::MAIN-CAR "APPEND") 'APPEND)
       ((EQUAL U::MAIN-CAR "ALWAYS") 'AND) ((EQUAL U::MAIN-CAR "NEVER") 'AND)
       ((EQUAL U::MAIN-CAR "THEREIS") 'OR)
       (T (U::BOMB 'U::DEFLOOP-ACCUM/TERM "Bug."))) ,(U::DEFLOOP-APPLIED-LAMBDA U::FOR-CLAUSES (SECOND U::MAIN-CLAUSE)
  (EQUAL U::MAIN-CAR "NEVER"))
            (,U::NAME ,@(U::DEFLOOP-REDUCE-ARGS U::ARGLIST U::FOR-CLAUSES)))))))
  (defun defloop-conditional
    (name arglist
      decls
      for-clauses
      main-clause
      main-car)
    (let* ((test (second main-clause)) (value-clause (third main-clause))
        (value-car (string (car value-clause))))
      `(defun ,U::NAME
        ,U::ARGLIST
        ,@U::DECLS
        (cond (,(U::DEFLOOP-DISJOIN
  (U::DEFLOOP-ATOMIZE (U::DEFLOOP-STRIP-NTH 2 U::FOR-CLAUSES))) 'nil)
          (,(U::DEFLOOP-APPLIED-LAMBDA U::FOR-CLAUSES U::TEST (EQUAL U::MAIN-CAR "UNLESS")) ,(COND
  ((EQUAL U::VALUE-CAR "COLLECT")
   `(CONS
     ,(U::DEFLOOP-APPLIED-LAMBDA U::FOR-CLAUSES (SECOND U::VALUE-CLAUSE) NIL)
     (,U::NAME ,@(U::DEFLOOP-REDUCE-ARGS U::ARGLIST U::FOR-CLAUSES))))
  ((EQUAL U::VALUE-CAR "APPEND")
   `(APPEND
     ,(U::DEFLOOP-APPLIED-LAMBDA U::FOR-CLAUSES (SECOND U::VALUE-CLAUSE) NIL)
     (,U::NAME ,@(U::DEFLOOP-REDUCE-ARGS U::ARGLIST U::FOR-CLAUSES))))
  ((EQUAL U::VALUE-CAR "RETURN")
   (U::DEFLOOP-APPLIED-LAMBDA U::FOR-CLAUSES (SECOND U::VALUE-CLAUSE) NIL))
  (T (U::BOMB 'U::DEFLOOP-CONDITIONAL "Bug."))))
          (t (,U::NAME ,@(U::DEFLOOP-REDUCE-ARGS U::ARGLIST U::FOR-CLAUSES)))))))
  (defmacro defloop
    (name arglist &rest forms)
    (let ((ignre (defloop-syntax-error name arglist forms)))
      (declare (ignore ignre))
      (let* ((loop-form (car (last forms))) (for-clauses (second loop-form))
          (main-clause (third loop-form))
          (main-car (string (first main-clause))))
        (cond ((member-equal main-car *defloop-accum/terms*) (defloop-accum/term name
              arglist
              (butlast forms 1)
              for-clauses
              main-clause
              main-car))
          ((member-equal main-car *defloop-conditionals*) (defloop-conditional name
              arglist
              (butlast forms 1)
              for-clauses
              main-clause
              main-car))
          (t (bomb 'defloop "Bug.")))))))

(defloop keyword-listp
  (l)
  "Recognizes lists of keywords."
  (declare (xargs :guard t))
  (for ((x in l)) (always (keywordp x))))

(defloop keyword-pair-alistp
  (l)
  "Recognizes alists whose entries are all pairs of keywords."
  (declare (xargs :guard t))
  (for ((pair in l))
    (always (and (consp pair)
        (keywordp (car pair))
        (keywordp (cdr pair))))))

(defun string-designator-p
  (x)
  "The guard of the Common Lisp function STRING."
  (declare (xargs :guard t))
  (or (stringp x)
    (symbolp x)
    (and (characterp x) (standard-char-p x))))

(defsection get-option
  :parents (utilities)
  :short "A set of routines for parsing keyword option lists."
  :long "<p>A keyword option list is a true list, each element of which is
either a keyword, or a true list whose car is a keyword. Here is an
example:</p>

@({
   (:READ-ONLY (:PREFIX "Foo") (:DO-NOT :TAG :NORMALIZE))
})

<p>The GET-OPTION routines provide an easy to use interface that in can handle
a lot of the parsing and syntax checking for keyword option lists.  Some
routines exist in 2 forms: The first form, e.g.,</p>

@({ (GET-OPTION-AS-FLAG ctx option option-list) })

<p>takes a context (a name printed in case of an error), an option keyword, an
  option list, (possible other args as well) and looks for the option in the
  list.  The function will abort if any syntax errors occur.  The second form,
  e.g.,</p>

@({ (GET-OPTION-AS-FLAG-MV option option-list) })

<p>returns 2 values.  The first value, if non-NIL, is an object produced by
  ACL2::MSG that describes the syntax error.  The second value is the actual
  return value of the function.  To avoid redundancy the -MV forms of the
  functions are not documnented.</p>

<p>To begin processing, use the function:</p>

@({
  (GET-OPTION-CHECK-SYNTAX ctx option-list valid-options duplicate-options
                           mutex-options)
})

<p>(or GET-OPTION-CHECK-SYNTAX-MV) to check for basic option list syntax, and
  then use the various option list parsing functions listed above to get the
  values associated with the individual options.</p>")

(defsection keyword-option-listp
  :parents (get-option)
  :short "Checks a list for basic syntax as a keyword option list."
  (defloop keyword-option-listp
    (l)
    (declare (xargs :guard t))
    (for ((x in l))
      (always (if (atom x)
          (keywordp x)
          (and (true-listp x) (keywordp (car x))))))))

(defun reason-for-not-keyword-option-listp
  (l)
  "Completes the sentence `L is not a keyword option list because ..."
  (cond ((atom l) (if (null l)
        (msg "BUG! BUG! BUG!")
        (msg "it is not a proper list.")))
    ((atom (car l)) (if (keywordp (car l))
        (reason-for-not-keyword-option-listp (cdr l))
        (msg "the entry ~p0 is not a keyword." (car l))))
    ((and (keywordp (caar l)) (true-listp (car l))) (reason-for-not-keyword-option-listp (cdr l)))
    (t (msg "the entry ~p0 is not a proper list whose car is a keyword."
        (car l)))))

(defsection get-option-keywords
  :parents (get-option)
  :short "Strip the option keywords from a keyword option list."
  (defloop get-option-keywords
    (l)
    (declare (xargs :guard (keyword-option-listp l)))
    (for ((x in l))
      (collect (if (atom x)
          x
          (car x))))))

(defsection get-option-entry
  :parents (get-option)
  :short "Returns the first occurrence of an option entry for option in l."
  (defloop get-option-entry
    (option l)
    (declare (xargs :guard (and (keywordp option) (keyword-option-listp l))))
    (for ((x in l))
      (when (or (eq option x)
          (and (consp x) (eq option (car x))))
        (return x)))))

(defsection get-option-entries
  :parents (get-option)
  :short "Returns all occurrences of option entries for option in l."
  (defloop get-option-entries
    (option l)
    (declare (xargs :guard (and (keywordp option) (keyword-option-listp l))))
    (for ((x in l))
      (when (or (eq option x)
          (and (consp x) (eq option (car x))))
        (collect x)))))

(defun get-option-check-mutex-mv
  (options mutex-options)
  (declare (xargs :guard (and (keyword-listp options)
        (keyword-pair-alistp mutex-options))))
  (cond ((atom mutex-options) (mv nil t))
    ((and (member (caar mutex-options) options)
       (member (cdar mutex-options) options)) (mv (msg "it contains the options ~p0 and ~p1 which are mutually ~
              exclusive."
          (caar mutex-options)
          (cdar mutex-options))
        nil))
    (t (get-option-check-mutex-mv options
        (cdr mutex-options)))))

(defun get-option-check-syntax-mv
  (option-list valid-options
    duplicate-options
    mutex-options)
  (declare (xargs :guard (and (keyword-listp valid-options)
        (keyword-listp duplicate-options)
        (keyword-pair-alistp mutex-options))
      :mode :program))
  (cond ((not (keyword-option-listp option-list)) (mv (reason-for-not-keyword-option-listp option-list)
        nil))
    (t (let* ((options (get-option-keywords option-list)) (dupes (duplicates options)))
        (cond ((not (subsetp options valid-options)) (mv (msg "it contains the option~#0~[~/s~] ~&0 ~
                  which ~#0~[is~/are~] not ~
                  recognized.  The only recognized option~#1~[~/s~] ~
                  ~#1~[is~/are~] ~&1."
                (set-difference-equal options valid-options)
                valid-options)
              nil))
          ((not (subsetp dupes duplicate-options)) (mv (msg "it contains duplicate occurrences of the ~
                  option~#0~[~/s~] ~&0. ~#1~[~
                  The only option~#2~[~/s~] which may be duplicated ~
                  ~#2~[is~/are~] ~&2.~/.~]"
                (set-difference-equal duplicate-options dupes)
                (if duplicate-options
                  0
                  1)
                duplicate-options)
              nil))
          (t (get-option-check-mutex-mv options mutex-options)))))))

(defsection get-option-check-syntax
  :parents (get-option)
  :short "Check the option list for gross syntax, returning NIL if it's OK, and
  crashing otherwise."
  :long "<p>The argument option-list is the option list entered by the user.
  Valid-options is a list of keywords that specifies which options are valid.
  Duplicate-options is a list of keywords which specifies which options may be
  duplicated.  Mutex-options is an alist of pairs (keyword1 . keyword2) which
  has the meaning `if keyword1 appears as an option then keyword2 may not
  appear as an option'.</p>"
  (defun get-option-check-syntax
    (ctx option-list
      valid-options
      duplicate-options
      mutex-options)
    (declare (xargs :guard (and (keyword-listp valid-options)
          (keyword-listp duplicate-options)
          (keyword-pair-alistp mutex-options))
        :mode :program))
    (mv-let (msg flag)
      (get-option-check-syntax-mv option-list
        valid-options
        duplicate-options
        mutex-options)
      (declare (ignore flag))
      (if msg
        (bomb ctx
          "The keyword option list ~p0 is invalid because ~@1"
          option-list
          msg)
        nil))))

(defun get-option-as-flag-mv
  (option option-list)
  (declare (xargs :guard (and (keywordp option)
        (keyword-option-listp option-list))))
  (let ((opt (get-option-entry option option-list)))
    (cond (opt (cond ((consp opt) (mv (msg "The ~p0 option descriptor may only be specified as ~p0, ~
                  thus ~p1 is illegal."
                option
                opt)
              nil))
          (t (mv nil t))))
      (t (mv nil nil)))))

(defsection get-option-as-flag
  :parents (get-option)
  :short "Look for an stand-alone option, check the syntax, and return T if the
  option is found and NIL otherwise."
  :long "<p>This function is for options that take no arguments, where the
  simple presence or absence of the option is meant to signal the user's
  intention.</p>"
  (defun get-option-as-flag
    (ctx option option-list)
    (declare (xargs :guard (and (keywordp option)
          (keyword-option-listp option-list))
        :mode :program))
    (mv-let (msg flag)
      (get-option-as-flag-mv option option-list)
      (if msg
        (bomb ctx "~@0" msg)
        flag))))

(defun get-option-member-mv
  (option option-list
    choices
    default-if-missing
    default-if-unspecified)
  (declare (xargs :guard (and (keywordp option)
        (keyword-option-listp option-list)
        (eqlable-listp choices))))
  (let ((opt (get-option-entry option option-list)))
    (cond (opt (cond ((or (atom opt) (atom (cdr opt))) (mv nil default-if-unspecified))
          ((or (cddr opt) (not (member (cadr opt) choices))) (mv (msg "The option specification ~p0 is illegal because the ~
                  ~p1 option requires at most one ~
                   argument which is one of ~v2."
                opt
                option
                choices)
              nil))
          (t (mv nil (cadr opt)))))
      (t (mv nil default-if-missing)))))

(defsection get-option-member
  :parents (get-option)
  :short "Process an option whose (optional) argument is a MEMBER of a set of
  choices."
  :long "<p>This function checks for an option that may be specified as either
  :OPTION, (:OPTION), or (:OPTION choice), where in the latter form the
  choice must be a member of the set of choices.  The choice is returned if
  the option is specified by the latter form, otherwise the
  default-if-missing is returned if the option is not present in the
  option-list, and default-if-unspecified is returned if the option if
  specified as :OPTION or (:OPTION).</p>"
  (defun get-option-member
    (ctx option
      option-list
      choices
      default-if-missing
      default-if-unspecified)
    (declare (xargs :guard (and (keywordp option)
          (keyword-option-listp option-list)
          (eqlable-listp choices))
        :mode :program))
    (mv-let (msg value)
      (get-option-member-mv option
        option-list
        choices
        default-if-missing
        default-if-unspecified)
      (if msg
        (bomb ctx "~@0" msg)
        value))))

(defun get-option-subset-mv
  (option option-list the-set default)
  (declare (xargs :guard (and (keywordp option)
        (keyword-option-listp option-list)
        (eqlable-listp the-set))
      :verify-guards nil))
  (let ((opt (get-option-entry option option-list)))
    (cond (opt (cond ((or (atom opt) (not (subsetp (cdr opt) the-set))) (mv (msg "The ~p0 option must be specified as ~p0 consed to a ~
                  true-list l, where l is a subset of the set whose ~
                  elements are ~&1. Thus ~p2 is illegal."
                option
                the-set
                opt)
              nil))
          (t (mv nil (cdr opt)))))
      (t (mv nil default)))))

(defthm true-listp-cdr-get-option-entry
  (implies (keyword-option-listp option-list)
    (true-listp (cdr (get-option-entry option option-list)))))

(verify-guards get-option-subset-mv)

(defsection get-option-subset
  :parents (get-option)
  :short "Process an option of the form (:OPTION . l), where l must be a SUBSETP
  of a given set."
  :long "<p>This function checks for an option that is specified as (:OPTION . l),
  where l must be a proper list and a SUBSETP of the-set. Thus (:OPTION)
  specifies the empty set, and :OPTION by itself is illegal.  If the option
  is missing then the default value is returned, otherwise the subset l
  is returned.</p>"
  (defun get-option-subset
    (ctx option option-list the-set default)
    (declare (xargs :guard (and (keywordp option)
          (keyword-option-listp option-list)
          (eqlable-listp the-set))
        :mode :program))
    (mv-let (msg value)
      (get-option-subset-mv option
        option-list
        the-set
        default)
      (if msg
        (bomb ctx "~@0" msg)
        value))))

(defun get-option-argument-mv
  (option option-list
    kind
    default-if-missing
    default-if-unspecified)
  (declare (xargs :guard (and (keywordp option)
        (keyword-option-listp option-list)
        (member kind '(:form :symbol :string :string-designator)))))
  (let ((opt (get-option-entry option option-list)))
    (cond (opt (cond ((or (atom opt) (atom (cdr opt))) (mv nil default-if-unspecified))
          ((or (cddr opt)
             (case kind
               (:symbol (not (symbolp (cadr opt))))
               (:string (not (stringp (cadr opt))))
               (:string-designator (not (string-designator-p (cadr opt))))
               (t nil))) (mv (msg "The option specification ~p0 is illegal because the ~p1 ~
                  option requires at most 1 argument~@2."
                opt
                option
                (case kind
                  (:symbolp " which must be a symbol")
                  (:string " which must be a string")
                  (:string-designator " which must be a symbol, ~
                                               string, or character")
                  (t "")))
              nil))
          (t (mv nil (cadr opt)))))
      (t (mv nil default-if-missing)))))

(defsection get-option-argument
  :parents (get-option)
  :short "Process an option of the form :OPTION, (:OPTION), or (:OPTION arg),
  where arg is required to be of a certain type."
  :long "<p>This function checks for an option that in the full form is specified as
  (:OPTION arg), where arg must be of a certain kind.  Recognized values
  for kind include:</p>

  @({
  :FORM              -- arg can be anything.
  :SYMBOL            -- arg must be a symbol.
  :STRING            -- arg must be a string.
  :STRING-DESIGNATOR -- arg must be a symbol, string, or character.
  })

  <p>If the option is missing from the option-list, then default-if-missing is
  returned.  If the option is specified as :OPTION or (:OPTION), then
  default-if-unspecified is returned.  Otherwise the arg is returned.</p>"
  (defun get-option-argument
    (ctx option
      option-list
      kind
      default-if-missing
      default-if-unspecified)
    (declare (xargs :guard (and (keywordp option)
          (keyword-option-listp option-list)
          (member kind '(:form :symbol :string :string-designator)))
        :mode :program))
    (mv-let (msg value)
      (get-option-argument-mv option
        option-list
        kind
        default-if-missing
        default-if-unspecified)
      (if msg
        (bomb ctx "~@0" msg)
        value))))

(defmacro naturalp
  (x)
  `(and (integerp ,U::X) (<= 0 ,U::X)))

(defloop string-designator-listp
  (l)
  "Recognizes lists of STRING-DESIGNATOR-P objects."
  (declare (xargs :guard t))
  (for ((x in l))
    (always (string-designator-p x))))

(defloop mapcar-string
  (l)
  "STRING each element of l."
  (declare (xargs :guard (string-designator-listp l)))
  (for ((sd in l)) (collect (string sd))))

(defloop coerce-string-designator-list
  (l)
  "Coerce a list of string-designators to a list of characters."
  (declare (xargs :guard (string-designator-listp l)))
  (for ((sd in l))
    (append (coerce (string sd) 'list))))

(defsection pack-string
  :parents (utilities)
  :short "Given a series of string-designators l, append the STRING of each and
   return the resulting string."
  (defmacro pack-string
    (&rest l)
    `(coerce (coerce-string-designator-list (list ,@U::L))
      'string)))

(defsection pack-intern
  :parents (utilities)
  :short "Given a list of string-designators l, append the STRING of each and
   intern the resulting string in the package of sym."
  (defmacro pack-intern
    (sym &rest l)
    `(intern-in-package-of-symbol (pack-string ,@U::L)
      ,U::SYM)))

(defun unique-symbols1
  (n seed sym-list counter gen-list)
  (declare (xargs :guard (and (naturalp n)
        (symbolp seed)
        (symbol-listp sym-list)
        (naturalp counter))
      :mode :program))
  (cond ((equal n 0) gen-list)
    (t (let ((sym (pack-intern seed
             seed
             (coerce (explode-nonnegative-integer counter 10 nil)
               'string))))
        (cond ((member sym sym-list) (unique-symbols1 n
              seed
              (remove sym sym-list)
              (1+ counter)
              gen-list))
          (t (unique-symbols1 (1- n)
              seed
              sym-list
              (1+ counter)
              (cons sym gen-list))))))))

(defsection unique-symbols
  :parents (utilities)
  :short "Return a list of symbols guaranteed unique with respect to a symbolic
  seed and every symbol in a list of symbols."
  :long "<p>Given a symbolic seed, we generate symbols @('<seed>0'), @('<seed>1'),
  etc. until we have generated n symbols not appearing in sym-list.  This is a
  'poor-man's' GENSYM, and is the best we can do without STATE.  All generated
  symbols are INTERNed in the package of seed.</p>"
  (defun unique-symbols
    (n seed sym-list)
    (declare (xargs :guard (and (naturalp n)
          (symbolp seed)
          (symbol-listp sym-list))
        :mode :program))
    (reverse (unique-symbols1 n seed sym-list 0 nil))))

(defloop force-term-list
  (l)
  "Given a list of terms, `FORCE' each term."
  (for ((x in l)) (collect `(force ,U::X))))

(defloop get-guards-from-declare-body
  (declare-body)
  "This is similar to ACL2::GET-GUARDS-1, but is believed to be `fail-safe'."
  (declare (xargs :mode :program))
  (for ((form in declare-body))
    (append (cond ((and (true-listp form)
           (eq (car form) 'xargs)
           (keyword-value-listp (cdr form))) (let ((temp (assoc-keyword :guard (cdr form))))
            (if temp
              (list (cadr temp))
              nil)))
        ((and (true-listp form)
           (equal (car form) 'type)
           (cadr form)
           (cddr form)
           (symbol-listp (cddr form))) (translate-declaration-to-guard-var-lst (cadr form)
            (cddr form)
            nil))
        (t nil)))))

(defloop get-guards-from-body1
  (body)
  (declare (xargs :mode :program))
  (for ((form in body))
    (when (and (true-listp form) (eq (car form) 'declare))
      (append (get-guards-from-declare-body (cdr form))))))

(defsection get-guards-from-body
  :parents (utilities)
  :short "A user-level function to extract guards from a definition body."
  :long "<p>This function takes a definition body, that is, a list of forms valid as
  the body of a DEFUN, and returns a guard for the DEFUN that consists of all
  guards specified either by (DECLARE (XARGS ... :GUARD g ...)) or (DECLARE
  (TYPE ...)) forms in body. This function is designed to be used by macros
  that create function definitions and lemmas that may depend on the guards
  of the newly defined function.  The guard will be returned as a
  conjunction: either T, NIL (?) a single conjunct, or (AND . conjuncts)
  where conjuncts is a list of the conjuncts.</p>

  <p>Restrictions on the form of macros in Acl2 make it impossible for a macro
  to query the ACL2 database to determine any property of a function, including
  its guards. Therefore we provide this function which parses function bodies
  and extracts the guards from the source text of a function.</p>

  <p>This is a `fail-safe' procedure.  If any syntax errors are encountered
  during guard parsing, those illegal guard specifications are simply ignored,
  under the assumption that when the function is finally submitted to Acl2 that
  Acl2's more powerful error checking facilities will uncover and report the
  errors to the user.  Thus this routine may return garbage, but it shouldn't
  crash!</p>"
  (defun get-guards-from-body
    (body)
    (declare (xargs :mode :program))
    (untranslate (conjoin (get-guards-from-body1 body))
      nil
      nil)))