• 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
          • Parse-demo
            • Parse-demo-long
            • Parse-demo-aux
            • Parse-demo-bundle
            • Parse-demo-short->long-list
            • Parse-demo-short->long
          • Demo
          • Make-demo
          • Change-demo
          • Honsed-demo
          • Make-honsed-demo
          • *demo-usage*
          • Demo->version
          • Demo->verbose
          • Demo->username
          • Demo->port
          • Demo->help
          • Demo->extra-stuff2
          • Demo->extra-stuff
          • Demo->dirs
        • Defoptions
        • Demo2
        • 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-demo

Parse-demo-aux

Signature

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

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

Theorem: demo-p-of-parse-demo-aux.result

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

Theorem: string-listp-of-parse-demo-aux.skipped

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