• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • 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
        • Parsers
          • Custom-parser
          • Parse-nat
          • Parse-plain
          • Parse-string
          • Parse-pos
          • Defparser
        • Sanity-check-formals
        • Formal->parser
        • Formal->argname
        • Formal->longname
        • Formal->alias
        • Formal->usage
        • Formal->merge
        • Formal->hiddenp
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• 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)))