• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • 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
      • 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
      • 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

      Formal->parser

      Signature
      (formal->parser x world) → parser-fn
      Arguments
      x — Guard (formal-p x).
      world — Guard (plist-worldp world).
      Returns
      parser-fn — Type (symbolp parser-fn).

      Definitions and Theorems

      Function: formal->parser

      (defun formal->parser (x world)
       (declare (xargs :guard (and (formal-p x)
                                   (plist-worldp world))))
       (let ((__function__ 'formal->parser))
        (declare (ignorable __function__))
        (b*
         (((formal x) x)
          (parser (cdr (assoc :parser x.opts)))
          ((when parser)
           (check-plausibly-a-parser-p x.name parser world)
           parser)
          ((unless (and (tuplep 2 x.guard)
                        (equal (second x.guard) x.name)))
           (raise
            "In ~x0, there's no :parser and the type isn't simple enough ~
                      to infer a default."
            x.name))
          (predicate (first x.guard))
          (parser (default-getopt-parser predicate world))
          ((when parser)
           (check-plausibly-a-parser-p x.name parser world)
           parser))
         (raise
          "In ~x0, there's no :parser and there's no default parser for type ~
                  ~x1."
          x.name predicate))))