• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
    • B*
    • Defunc
    • Fty
    • Apt
    • Std/util
    • Defdata
    • Defrstobj
    • Seq
    • Match-tree
    • Defrstobj
    • With-supporters
    • Def-partial-measure
    • Template-subst
    • Soft
    • Defthm-domain
    • Event-macros
    • Def-universal-equiv
    • Def-saved-obligs
    • With-supporters-after
    • Definec
    • Sig
    • Outer-local
    • Data-structures
      • Deflist
      • Defalist
      • Memory
      • Defstructure
      • Array1
      • Utilities
        • Defloop
        • Get-option
          • Get-option-argument
          • Get-option-member
          • Get-option-check-syntax
          • Get-option-subset
          • Get-option-as-flag
          • Get-option-entries
          • Keyword-option-listp
          • Get-option-entry
          • Get-option-keywords
        • Get-guards-from-body
        • Unique-symbols
        • Pack-intern
        • Pack-string
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Get-option

Get-option-argument

Process an option of the form :OPTION, (:OPTION), or (:OPTION arg), where arg is required to be of a certain type.

This function checks for an option that in the full form is specified as (:OPTION arg), where arg must be of a certain kind. Recognized values for kind include:

:FORM              -- arg can be anything.
:SYMBOL            -- arg must be a symbol.
:STRING            -- arg must be a string.
:STRING-DESIGNATOR -- arg must be a symbol, string, or character.

If the option is missing from the option-list, then default-if-missing is returned. If the option is specified as :OPTION or (:OPTION), then default-if-unspecified is returned. Otherwise the arg is returned.

Definitions and Theorems

Function: get-option-argument

(defun get-option-argument (ctx option
                                option-list kind default-if-missing
                                default-if-unspecified)
 (declare
  (xargs :guard (and (keywordp option)
                     (keyword-option-listp option-list)
                     (member kind
                             '(:form :symbol
                                     :string :string-designator)))))
 (mv-let (msg value)
         (get-option-argument-mv option
                                 option-list kind default-if-missing
                                 default-if-unspecified)
   (if msg (bomb ctx "~@0" msg) value)))