• 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
        • Sanity-check-formals
        • Formal->parser
        • Formal->argname
        • Formal->longname
        • Formal->alias
        • Formal->usage
        • Formal->merge
        • Formal->hiddenp
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Getopt

Sanity-check-formals

Make sure longnames and aliases are unique, every field has a parser, and so forth. This only applies to visible options.

Signature

(sanity-check-formals basename x world) → *

Arguments

basename — Guard (symbolp basename).

x — Guard (formallist-p x).

world — Guard (plist-worldp world).

Definitions and Theorems

Function: sanity-check-formals

(defun sanity-check-formals (basename x world)
  (declare (xargs :guard (and (symbolp basename)
                              (formallist-p x)
                              (plist-worldp world))))
  (let ((__function__ 'sanity-check-formals))
    (declare (ignorable __function__))
    (b* ((longnames (formallist->longnames x))
         ((unless (uniquep longnames))
          (raise "In ~x0, multiple fields have :longname ~&1."
                 basename
                 (duplicated-members longnames)))
         (aliases (remove nil (formallist->aliases x)))
         ((unless (uniquep aliases))
          (raise "In ~x0, multiple fields have :alias ~&1."
                 basename (duplicated-members aliases)))
         (?parsers (formallist->parsers x world))
         (?merges (formallist->merges x)))
      t)))