		Search-engine friendly clone of the ACL2 documentation.

Parse-stv2c-opts

Parse-stv2c-opts-long

Signature
(parse-stv2c-opts-long getopt::longname getopt::explicit-val args getopt::acc getopt::seen) → (mv getopt::errmsg getopt::acc rest)
Arguments: getopt::longname — Longname we've just found, e.g., "foo" if we've just seen --foo=bar.
Guard (stringp getopt::longname).; getopt::explicit-val — Any explicit value passed to this option, e.g., "bar" if we've just seen --foo=bar, or NIL if we've just seen --foo.
Guard (or (not getopt::explicit-val) (stringp getopt::explicit-val)).; args — Remaining arguments past longname.
Guard (string-listp args).; getopt::acc — Structure we're updating.
Guard (stv2c-opts-p getopt::acc).; getopt::seen — List of longnames that we've seen so far.
Guard (string-listp getopt::seen).
Returns: getopt::errmsg — NIL on success or an error message.; getopt::acc — Updated structure.
Type (stv2c-opts-p getopt::acc), given (force (stv2c-opts-p getopt::acc)).; rest — Rest after this one.
Type (string-listp rest), given (force (string-listp args)).

Definitions and Theorems

Function: parse-stv2c-opts-long

(defun parse-stv2c-opts-long
       (getopt::longname getopt::explicit-val
                         args getopt::acc getopt::seen)
 (declare (xargs :guard (and (stringp getopt::longname)
                             (or (not getopt::explicit-val)
                                 (stringp getopt::explicit-val))
                             (string-listp args)
                             (stv2c-opts-p getopt::acc)
                             (string-listp getopt::seen))))
 (let ((__function__ 'parse-stv2c-opts-long))
  (declare (ignorable __function__))
  (cond
   ((equal getopt::longname "help")
    (b* (((when (member-equal getopt::longname getopt::seen))
          (mv (msg "Option --~s0 given multiple times"
                   getopt::longname)
              getopt::acc args))
         ((mv getopt::err value rest)
          (getopt::parse-plain (str::cat "--" getopt::longname)
                               getopt::explicit-val args))
         ((when getopt::err)
          (mv getopt::err getopt::acc args))
         (getopt::acc (change-stv2c-opts getopt::acc
                                         :help value)))
      (mv nil getopt::acc rest)))
   ((equal getopt::longname "readme")
    (b* (((when (member-equal getopt::longname getopt::seen))
          (mv (msg "Option --~s0 given multiple times"
                   getopt::longname)
              getopt::acc args))
         ((mv getopt::err value rest)
          (getopt::parse-plain (str::cat "--" getopt::longname)
                               getopt::explicit-val args))
         ((when getopt::err)
          (mv getopt::err getopt::acc args))
         (getopt::acc (change-stv2c-opts getopt::acc
                                         :readme value)))
      (mv nil getopt::acc rest)))
   ((equal getopt::longname "stv")
    (b* (((when (member-equal getopt::longname getopt::seen))
          (mv (msg "Option --~s0 given multiple times"
                   getopt::longname)
              getopt::acc args))
         ((mv getopt::err value rest)
          (getopt::parse-string (str::cat "--" getopt::longname)
                                getopt::explicit-val args))
         ((when getopt::err)
          (mv getopt::err getopt::acc args))
         (getopt::acc (change-stv2c-opts getopt::acc
                                         :stv value)))
      (mv nil getopt::acc rest)))
   ((equal getopt::longname "search")
    (b* (((mv getopt::err value rest)
          (getopt::parse-string (str::cat "--" getopt::longname)
                                getopt::explicit-val args))
         ((when getopt::err)
          (mv getopt::err getopt::acc args))
         (getopt::old-value (stv2c-opts->search-path getopt::acc))
         (value (rcons value getopt::old-value))
         (getopt::acc (change-stv2c-opts getopt::acc
                                         :search-path value)))
      (mv nil getopt::acc rest)))
   ((equal getopt::longname "searchext")
    (b* (((mv getopt::err value rest)
          (getopt::parse-string (str::cat "--" getopt::longname)
                                getopt::explicit-val args))
         ((when getopt::err)
          (mv getopt::err getopt::acc args))
         (getopt::old-value (stv2c-opts->search-exts getopt::acc))
         (value (rcons value getopt::old-value))
         (getopt::acc (change-stv2c-opts getopt::acc
                                         :search-exts value)))
      (mv nil getopt::acc rest)))
   ((equal getopt::longname "define")
    (b* (((mv getopt::err value rest)
          (getopt::parse-string (str::cat "--" getopt::longname)
                                getopt::explicit-val args))
         ((when getopt::err)
          (mv getopt::err getopt::acc args))
         (getopt::old-value (stv2c-opts->defines getopt::acc))
         (value (cons value getopt::old-value))
         (getopt::acc (change-stv2c-opts getopt::acc
                                         :defines value)))
      (mv nil getopt::acc rest)))
   ((equal getopt::longname "edition")
    (b* (((when (member-equal getopt::longname getopt::seen))
          (mv (msg "Option --~s0 given multiple times"
                   getopt::longname)
              getopt::acc args))
         ((mv getopt::err value rest)
          (vl2014::vl-parse-edition (str::cat "--" getopt::longname)
                                    getopt::explicit-val args))
         ((when getopt::err)
          (mv getopt::err getopt::acc args))
         (getopt::acc (change-stv2c-opts getopt::acc
                                         :edition value)))
      (mv nil getopt::acc rest)))
   ((equal getopt::longname "strict")
    (b* (((when (member-equal getopt::longname getopt::seen))
          (mv (msg "Option --~s0 given multiple times"
                   getopt::longname)
              getopt::acc args))
         ((mv getopt::err value rest)
          (getopt::parse-plain (str::cat "--" getopt::longname)
                               getopt::explicit-val args))
         ((when getopt::err)
          (mv getopt::err getopt::acc args))
         (getopt::acc (change-stv2c-opts getopt::acc
                                         :strict value)))
      (mv nil getopt::acc rest)))
   ((equal getopt::longname "mem")
    (b* (((when (member-equal getopt::longname getopt::seen))
          (mv (msg "Option --~s0 given multiple times"
                   getopt::longname)
              getopt::acc args))
         ((mv getopt::err value rest)
          (getopt::parse-pos (str::cat "--" getopt::longname)
                             getopt::explicit-val args))
         ((when getopt::err)
          (mv getopt::err getopt::acc args))
         (getopt::acc (change-stv2c-opts getopt::acc
                                         :mem value)))
      (mv nil getopt::acc rest)))
   (t (mv (msg "Unrecognized option --~s0"
               getopt::longname)
          getopt::acc args)))))

Theorem: stv2c-opts-p-of-parse-stv2c-opts-long.acc

(defthm stv2c-opts-p-of-parse-stv2c-opts-long.acc
 (implies
  (force (stv2c-opts-p getopt::acc))
  (b* (((mv getopt::?errmsg
            getopt::?acc common-lisp::?rest)
        (parse-stv2c-opts-long getopt::longname getopt::explicit-val
                               args getopt::acc getopt::seen)))
    (stv2c-opts-p getopt::acc)))
 :rule-classes :rewrite)

Theorem: string-listp-of-parse-stv2c-opts-long.rest

(defthm string-listp-of-parse-stv2c-opts-long.rest
 (implies
  (force (string-listp args))
  (b* (((mv getopt::?errmsg
            getopt::?acc common-lisp::?rest)
        (parse-stv2c-opts-long getopt::longname getopt::explicit-val
                               args getopt::acc getopt::seen)))
    (string-listp rest)))
 :rule-classes :rewrite)

Theorem: parse-stv2c-opts-long-makes-progress

(defthm parse-stv2c-opts-long-makes-progress
 (<=
  (len
   (mv-nth
        2
        (parse-stv2c-opts-long getopt::longname getopt::explicit-val
                               args getopt::acc getopt::seen)))
  (len args))
 :rule-classes ((:rewrite) (:linear)))