• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • 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
        • Make-event
        • Defmacro
        • Untranslate-patterns
        • Tc
        • Trans*
        • Macro-aliases-table
        • Macro-args
        • Defabbrev
        • User-defined-functions-table
        • Trans
        • Untranslate-for-execution
        • Add-macro-fn
        • Check-vars-not-free
        • Safe-mode
        • 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
          • Trans1
          • Defmacro-untouchable
          • Set-duplicate-keys-action
          • Add-macro-alias
          • Magic-macroexpand
          • Defmacroq
          • Trans!
          • Remove-macro-fn
          • Remove-macro-alias
          • Add-binop
          • Untrans-table
          • Trans*-
          • Remove-binop
          • Tcp
          • Tca
        • Mailing-lists
        • Interfacing-tools
      • 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
        • 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)))