		Search-engine friendly clone of the ACL2 documentation.

Atc-input-processing

Atc-process-pretty-printing

Process the :pretty-printing input.

Signature
(atc-process-pretty-printing options) → (mv erp ppoptions)
Arguments: options — Guard (symbol-alistp options).
Returns: ppoptions — Type (pprint-options-p ppoptions).

Definitions and Theorems

Function: atc-process-pretty-printing

(defun atc-process-pretty-printing (options)
 (declare (xargs :guard (symbol-alistp options)))
 (let ((__function__ 'atc-process-pretty-printing))
  (declare (ignorable __function__))
  (b*
   (((reterr) (irr-pprint-options))
    (pretty-printing-option (assoc-eq :pretty-printing options))
    (pretty-printing
         (if pretty-printing-option (cdr pretty-printing-option)
           nil))
    ((unless (keyword-value-listp pretty-printing))
     (reterr
      (msg
       "The :PRETTY-PRINTING input must be a keyword-value list, ~
                      but ~x0 is not a keyword-value list."
       pretty-printing)))
    (alist (keyword-value-list-to-alist pretty-printing))
    (keywords (strip-cars alist))
    (desc
       (msg "The list of keywords in the :PRETTY-PRINTING input ~x0"
            keywords))
    ((unless (no-duplicatesp-eq keywords))
     (reterr (msg "~@0 must have no duplicates." desc)))
    ((unless (subsetp-eq keywords
                         *atc-allowed-pretty-printing-options*))
     (reterr (msg "~@0 must be a subset of ~x1." desc
                  *atc-allowed-pretty-printing-options*)))
    (parenthesize-nested-conditionals
         (cdr (assoc-eq :parenthesize-nested-conditionals alist)))
    ((unless (booleanp parenthesize-nested-conditionals))
     (reterr
      (msg
       "The value ~x0 of the pretty-printing option ~
                      :PARENTHESIZE-NESTED-CONDITIONALS must be a boolean."
       parenthesize-nested-conditionals))))
   (retok (make-pprint-options :parenthesize-nested-conditionals
                               parenthesize-nested-conditionals)))))

Theorem: pprint-options-p-of-atc-process-pretty-printing.ppoptions

(defthm pprint-options-p-of-atc-process-pretty-printing.ppoptions
  (b* (((mv acl2::?erp ?ppoptions)
        (atc-process-pretty-printing options)))
    (pprint-options-p ppoptions))
  :rule-classes :rewrite)