• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
      • Warnings
      • Primitives
      • Use-set
      • Syntax
      • Getting-started
      • Utilities
      • Loader
      • Transforms
      • Lint
      • Mlib
      • Server
      • Kit
        • Vl-model
        • Vl-json
        • Vl-gather
        • Vl-server
        • Vl-pp
          • Vl-pp-opts-p
            • Parse-vl-pp-opts
              • Parse-vl-pp-opts-long
              • Parse-vl-pp-opts-aux
              • Parse-vl-pp-opts-bundle
              • Parse-vl-pp-opts-short->long-list
              • Parse-vl-pp-opts-short->long
            • Vl-pp-opts
            • Make-vl-pp-opts
            • Change-vl-pp-opts
            • Honsed-vl-pp-opts
            • Make-honsed-vl-pp-opts
            • *vl-pp-opts-usage*
            • Vl-pp-opts->strict
            • Vl-pp-opts->start-files
            • Vl-pp-opts->readme
            • Vl-pp-opts->output
            • Vl-pp-opts->outdefs
            • Vl-pp-opts->mem
            • Vl-pp-opts->include-dirs
            • Vl-pp-opts->help
            • Vl-pp-opts->edition
            • Vl-pp-opts->defines
        • Vl-lint
        • Vl-main
        • Vl-toolkit-other-command
        • Vl-help
      • Printer
      • Esim-vl
      • Well-formedness
    • Sv
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Parse-vl-pp-opts

Parse-vl-pp-opts-aux

Signature

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

(defun parse-vl-pp-opts-aux (args getopt::acc
                                  getopt::seen getopt::skipped)
 (declare (xargs :guard (and (string-listp args)
                             (vl-pp-opts-p getopt::acc)
                             (string-listp getopt::seen)
                             (string-listp getopt::skipped))))
 (let ((__function__ 'parse-vl-pp-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-vl-pp-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-vl-pp-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-vl-pp-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-vl-pp-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-vl-pp-opts-short->long getopt::alias))
          ((when getopt::err)
           (mv getopt::err getopt::acc args))
          ((mv getopt::err getopt::acc rest)
           (parse-vl-pp-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-vl-pp-opts-aux rest getopt::acc
                             getopt::seen getopt::skipped)))
    ((mv getopt::err getopt::longnames)
     (parse-vl-pp-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-vl-pp-opts-bundle getopt::longnames (cdr args)
                              getopt::acc getopt::seen))
    ((when getopt::err)
     (mv getopt::err getopt::acc rest)))
   (parse-vl-pp-opts-aux rest getopt::acc
                         getopt::seen getopt::skipped))))

Theorem: vl-pp-opts-p-of-parse-vl-pp-opts-aux.result

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

Theorem: string-listp-of-parse-vl-pp-opts-aux.skipped

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