• 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

    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))))