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

Parser for plain, argument-free options that are off by default and must be explicitly enabled, e.g., --verbose or --force.

Signature

(parse-plain 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 (booleanp value).

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

We just return true, because by typing the name of the option the user is saying they want to turn it on. This is useful for options that the user has to explicitly ask for because they are unsafe or just unusual.

Definitions and Theorems

Function: parse-plain

(defun parse-plain (name explicit-value args)
  (declare (xargs :guard (and (stringp name)
                              (or (not explicit-value)
                                  (stringp explicit-value))
                              (string-listp args))))
  (let ((__function__ 'parse-plain))
    (declare (ignorable __function__))
    (if explicit-value (mv (msg "Option ~s0 can't take an argument"
                                name)
                           nil args)
      (mv nil t args))))

Theorem: booleanp-of-parse-plain.value

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

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

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

Theorem: parse-plain-makes-progress

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