		Search-engine friendly clone of the ACL2 documentation.

Parse-stv2c-opts

Parse-stv2c-opts-aux

Signature
(parse-stv2c-opts-aux args getopt::acc getopt::seen getopt::skipped) → (mv getopt::errmsg getopt::result getopt::skipped)
Arguments: args — Arguments we're processing.
Guard (string-listp args).; getopt::acc — Structure we're building.
Guard (stv2c-opts-p getopt::acc).; getopt::seen — List of longnames that we've seen so far.
Guard (string-listp getopt::seen).; getopt::skipped — Arguments we've skipped since they don't go with options, in reverse order.
Guard (string-listp getopt::skipped).
Returns: getopt::result — Type (stv2c-opts-p getopt::result), given (force (stv2c-opts-p getopt::acc)).; getopt::skipped — Type (string-listp getopt::skipped), given (and (force (string-listp getopt::skipped)) (force (string-listp args))) .

Definitions and Theorems

Function: parse-stv2c-opts-aux

(defun parse-stv2c-opts-aux (args getopt::acc
                                  getopt::seen getopt::skipped)
 (declare (xargs :guard (and (string-listp args)
                             (stv2c-opts-p getopt::acc)
                             (string-listp getopt::seen)
                             (string-listp getopt::skipped))))
 (let ((__function__ 'parse-stv2c-opts-aux))
  (declare (ignorable __function__))
  (b*
   (((when (or (atom args)
               (equal (car args) "--")))
     (mv nil getopt::acc
         (revappend getopt::skipped args)))
    ((unless (str::strprefixp "-" (car args)))
     (parse-stv2c-opts-aux (cdr args)
                           getopt::acc getopt::seen
                           (cons (car args) getopt::skipped)))
    ((when (str::strprefixp "--" (car args)))
     (b* (((mv getopt::longname getopt::explicit-value)
           (getopt::split-equals (subseq (car args) 2 nil)))
          ((mv getopt::err getopt::acc rest)
           (parse-stv2c-opts-long getopt::longname
                                  getopt::explicit-value (cdr args)
                                  getopt::acc getopt::seen))
          ((when getopt::err)
           (mv getopt::err getopt::acc rest))
          (getopt::seen (cons getopt::longname getopt::seen)))
       (parse-stv2c-opts-aux rest getopt::acc
                             getopt::seen getopt::skipped)))
    ((mv getopt::shortnames
         getopt::explicit-value)
     (getopt::split-equals (subseq (car args) 1 nil)))
    (getopt::aliases (explode getopt::shortnames))
    ((when (atom getopt::aliases))
     (parse-stv2c-opts-aux (cdr args)
                           getopt::acc getopt::seen
                           (cons (car args) getopt::skipped)))
    ((when (atom (cdr getopt::aliases)))
     (b* ((getopt::alias (car getopt::aliases))
          ((mv getopt::err getopt::longname)
           (parse-stv2c-opts-short->long getopt::alias))
          ((when getopt::err)
           (mv getopt::err getopt::acc args))
          ((mv getopt::err getopt::acc rest)
           (parse-stv2c-opts-long getopt::longname
                                  getopt::explicit-value (cdr args)
                                  getopt::acc getopt::seen))
          ((when getopt::err)
           (mv getopt::err getopt::acc rest))
          (getopt::seen (cons getopt::longname getopt::seen)))
       (parse-stv2c-opts-aux rest getopt::acc
                             getopt::seen getopt::skipped)))
    ((mv getopt::err getopt::longnames)
     (parse-stv2c-opts-short->long-list getopt::aliases))
    ((when getopt::err)
     (mv getopt::err getopt::acc args))
    ((when getopt::explicit-value)
     (mv
      (msg
       "Option bundle ~s0 is not allowed (bundles can't have ~
                       arguments)."
       (car args))
      getopt::acc args))
    (getopt::illegal-to-bundle
         (set-difference-equal getopt::longnames
                               '("help" "readme" "strict")))
    ((when getopt::illegal-to-bundle)
     (mv
      (msg
        "Option bundle ~s0 is not allowed (--~s1 needs an argument)"
        (car args)
        (car getopt::illegal-to-bundle))
      getopt::acc args))
    ((mv getopt::err
         getopt::acc getopt::seen rest)
     (parse-stv2c-opts-bundle getopt::longnames (cdr args)
                              getopt::acc getopt::seen))
    ((when getopt::err)
     (mv getopt::err getopt::acc rest)))
   (parse-stv2c-opts-aux rest getopt::acc
                         getopt::seen getopt::skipped))))

Theorem: stv2c-opts-p-of-parse-stv2c-opts-aux.result

(defthm stv2c-opts-p-of-parse-stv2c-opts-aux.result
  (implies
       (force (stv2c-opts-p getopt::acc))
       (b* (((mv getopt::?errmsg
                 getopt::?result getopt::?skipped)
             (parse-stv2c-opts-aux args getopt::acc
                                   getopt::seen getopt::skipped)))
         (stv2c-opts-p getopt::result)))
  :rule-classes :rewrite)

Theorem: string-listp-of-parse-stv2c-opts-aux.skipped

(defthm string-listp-of-parse-stv2c-opts-aux.skipped
  (implies
       (and (force (string-listp getopt::skipped))
            (force (string-listp args)))
       (b* (((mv getopt::?errmsg
                 getopt::?result getopt::?skipped)
             (parse-stv2c-opts-aux args getopt::acc
                                   getopt::seen getopt::skipped)))
         (string-listp getopt::skipped)))
  :rule-classes :rewrite)