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

Get-option

A set of routines for parsing keyword option lists.

A keyword option list is a true list, each element of which is either a keyword, or a true list whose car is a keyword. Here is an example:

(:READ-ONLY (:PREFIX "Foo") (:DO-NOT :TAG :NORMALIZE))

The GET-OPTION routines provide an easy to use interface that in can handle a lot of the parsing and syntax checking for keyword option lists. Some routines exist in 2 forms: The first form, e.g.,

(GET-OPTION-AS-FLAG ctx option option-list)

takes a context (a name printed in case of an error), an option keyword, an option list, (possible other args as well) and looks for the option in the list. The function will abort if any syntax errors occur. The second form, e.g.,

(GET-OPTION-AS-FLAG-MV option option-list)

returns 2 values. The first value, if non-NIL, is an object produced by ACL2::MSG that describes the syntax error. The second value is the actual return value of the function. To avoid redundancy the -MV forms of the functions are not documnented.

To begin processing, use the function:

(GET-OPTION-CHECK-SYNTAX ctx option-list valid-options duplicate-options
                         mutex-options)

(or GET-OPTION-CHECK-SYNTAX-MV) to check for basic option list syntax, and then use the various option list parsing functions listed above to get the values associated with the individual options.

Subtopics

Get-option-argument
Process an option of the form :OPTION, (:OPTION), or (:OPTION arg), where arg is required to be of a certain type.
Get-option-member
Process an option whose (optional) argument is a MEMBER of a set of choices.
Get-option-check-syntax
Check the option list for gross syntax, returning NIL if it's OK, and crashing otherwise.
Get-option-subset
Process an option of the form (:OPTION . l), where l must be a SUBSETP of a given set.
Get-option-as-flag
Look for an stand-alone option, check the syntax, and return T if the option is found and NIL otherwise.
Get-option-entries
Returns all occurrences of option entries for option in l.
Keyword-option-listp
Checks a list for basic syntax as a keyword option list.
Get-option-entry
Returns the first occurrence of an option entry for option in l.
Get-option-keywords
Strip the option keywords from a keyword option list.