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