		Search-engine friendly clone of the ACL2 documentation.

Parse-vl-lintconfig

Parse-vl-lintconfig-aux

Signature
(parse-vl-lintconfig-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 (vl-lintconfig-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 (vl-lintconfig-p getopt::result), given (force (vl-lintconfig-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-vl-lintconfig-aux

(defun parse-vl-lintconfig-aux (args getopt::acc
                                     getopt::seen getopt::skipped)
 (declare (xargs :guard (and (string-listp args)
                             (vl-lintconfig-p getopt::acc)
                             (string-listp getopt::seen)
                             (string-listp getopt::skipped))))
 (let ((__function__ 'parse-vl-lintconfig-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-vl-lintconfig-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-vl-lintconfig-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-vl-lintconfig-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-vl-lintconfig-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-vl-lintconfig-short->long getopt::alias))
       ((when getopt::err)
        (mv getopt::err getopt::acc args))
       ((mv getopt::err getopt::acc rest)
        (parse-vl-lintconfig-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-vl-lintconfig-aux rest getopt::acc
                               getopt::seen getopt::skipped)))
    ((mv getopt::err getopt::longnames)
     (parse-vl-lintconfig-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"
                       "no-typo" "no-html" "no-sv-use-set"
                       "strict" "debug" "shell" "post-shell")))
    ((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-vl-lintconfig-bundle getopt::longnames (cdr args)
                                 getopt::acc getopt::seen))
    ((when getopt::err)
     (mv getopt::err getopt::acc rest)))
   (parse-vl-lintconfig-aux rest getopt::acc
                            getopt::seen getopt::skipped))))

Theorem: vl-lintconfig-p-of-parse-vl-lintconfig-aux.result

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

Theorem: string-listp-of-parse-vl-lintconfig-aux.skipped

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