		Search-engine friendly clone of the ACL2 documentation.

Parsers

Parse-nat

Parser for options that require a natp argument, e.g., --tabsize or -O, etc.

Signature
(parse-nat 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 (natp value).; rest-args — Type (string-listp rest-args), given (force (string-listp args)).

We just read the next string out of the argument list and try to interpret it as a decimal number. This fails if it there is no argument, or if there are any non-numeric characters.

Definitions and Theorems

Function: parse-nat

(defun parse-nat (name explicit-value args)
  (declare (xargs :guard (and (stringp name)
                              (or (not explicit-value)
                                  (stringp explicit-value))
                              (string-listp args))))
  (let ((__function__ 'parse-nat))
    (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)
              0 args))
         (ret (str::strval val))
         ((unless ret)
          (mv (msg "Option ~s0 needs a number, but got ~x1"
                   name val)
              0 args)))
      (mv nil ret args))))

Theorem: natp-of-parse-nat.value

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

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

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

Theorem: parse-nat-makes-progress

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