• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Recursion-and-induction
    • Hons-and-memoization
    • Events
    • Parallelism
    • History
    • Programming
    • Operational-semantics
    • Real
    • Start-here
    • Debugging
    • Miscellaneous
    • Output-controls
    • Macros
    • 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
  • 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-pos

Parser for options that require a posp argument, e.g., --block-size or --line-number.

Signature

(parse-pos 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 (posp value).

rest-args — Type (string-listp rest-args), given (force (string-listp args)).

This is just like parse-nat except that we also cause an error if the argument is zero.

Definitions and Theorems

Function: parse-pos

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

Theorem: posp-of-parse-pos.value

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

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

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

Theorem: parse-pos-makes-progress

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