• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Community
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
    • Io
    • Defttag
    • Sys-call
    • Save-exec
    • Quicklisp
    • Std/io
    • Oslib
    • Bridge
    • Clex
    • Tshell
    • Unsound-eval
    • Hacker
    • ACL2s-interface
    • Startup-banner
    • Command-line
      • Save-exec
      • Argv
      • Getopt
        • Demo-p
        • Defoptions
        • Demo2
          • Demo2-opts-p
            • Parse-demo2-opts
              • Parse-demo2-opts-long
              • Parse-demo2-opts-aux
              • Parse-demo2-opts-bundle
              • Parse-demo2-opts-short->long-list
              • Parse-demo2-opts-short->long
            • Demo2-opts
            • Make-demo2-opts
            • Change-demo2-opts
            • Make-honsed-demo2-opts
            • Honsed-demo2-opts
            • *demo2-opts-usage*
            • Demo2-opts->version
            • Demo2-opts->help
            • Demo2-opts->fail
          • Demo2-main
        • Parsers
        • Sanity-check-formals
        • Formal->parser
        • Formal->argname
        • Formal->longname
        • Formal->alias
        • Formal->usage
        • Formal->merge
        • Formal->hiddenp
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Parse-demo2-opts

Parse-demo2-opts-aux

Signature

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

(defun parse-demo2-opts-aux (args getopt::acc
                                  getopt::seen getopt::skipped)
 (declare (xargs :guard (and (string-listp args)
                             (demo2-opts-p getopt::acc)
                             (string-listp getopt::seen)
                             (string-listp getopt::skipped))))
 (let ((acl2::__function__ 'parse-demo2-opts-aux))
  (declare (ignorable acl2::__function__))
  (b*
   (((when (or (atom args)
               (equal (car args) "--")))
     (mv nil getopt::acc
         (revappend getopt::skipped args)))
    ((unless (str::strprefixp "-" (car args)))
     (parse-demo2-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-demo2-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-demo2-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 (acl2::explode getopt::shortnames))
    ((when (atom getopt::aliases))
     (parse-demo2-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-demo2-opts-short->long getopt::alias))
          ((when getopt::err)
           (mv getopt::err getopt::acc args))
          ((mv getopt::err getopt::acc rest)
           (parse-demo2-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-demo2-opts-aux rest getopt::acc
                             getopt::seen getopt::skipped)))
    ((mv getopt::err getopt::longnames)
     (parse-demo2-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" "version" "fail")))
    ((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-demo2-opts-bundle getopt::longnames (cdr args)
                              getopt::acc getopt::seen))
    ((when getopt::err)
     (mv getopt::err getopt::acc rest)))
   (parse-demo2-opts-aux rest getopt::acc
                         getopt::seen getopt::skipped))))

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

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

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

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