		Search-engine friendly clone of the ACL2 documentation.

Parsers

Parse-string

Parser for options that require an argument, but where any arbitrary string will do, e.g., --username or --eval.

Signature
(parse-string name explicit-value args) → (mv err value rest-args)
Arguments: name — Guard (stringp name).; explicit-value — Guard (or (not explicit-value) (stringp explicit-value)).; args — Guard (string-listp args).
Returns: value — Type (stringp value).; rest-args — Type (string-listp rest-args), given (force (string-listp args)).

The only way this can fail is if there aren't any more arguments, e.g., someone types something like myprogram --username and doesn't say what username to use.

Definitions and Theorems

Function: parse-string

(defun parse-string (name explicit-value args)
  (declare (xargs :guard (and (stringp name)
                              (or (not explicit-value)
                                  (stringp explicit-value))
                              (string-listp args))))
  (let ((__function__ 'parse-string))
    (declare (ignorable __function__))
    (b* (((mv val args)
          (if explicit-value (mv explicit-value args)
            (mv (car args) (cdr args))))
         ((unless val)
          (mv (msg "Option ~s0 needs an argument" name)
              "" args)))
      (mv nil (acl2::str-fix val) args))))

Theorem: stringp-of-parse-string.value

(defthm stringp-of-parse-string.value
  (b* (((mv ?err acl2::?value ?rest-args)
        (parse-string name explicit-value args)))
    (stringp value))
  :rule-classes :type-prescription)

Theorem: string-listp-of-parse-string.rest-args

(defthm string-listp-of-parse-string.rest-args
  (implies (force (string-listp args))
           (b* (((mv ?err acl2::?value ?rest-args)
                 (parse-string name explicit-value args)))
             (string-listp rest-args)))
  :rule-classes :rewrite)

Theorem: parse-string-makes-progress

(defthm parse-string-makes-progress
  (<= (len (mv-nth 2
                   (parse-string name explicit-value args)))
      (len args))
  :rule-classes ((:rewrite) (:linear)))