		Search-engine friendly clone of the ACL2 documentation.

Output-files-implementation

Output-files-process-printer-options

Process the :printer-options input.

Signature
(output-files-process-printer-options options) → (mv erp indent-size paren-nested-conds)
Arguments: options — Guard (symbol-alistp options).
Returns: indent-size — Type (posp indent-size).; paren-nested-conds — Type (booleanp paren-nested-conds).

Definitions and Theorems

Function: output-files-process-printer-options

(defun output-files-process-printer-options (options)
 (declare (xargs :guard (symbol-alistp options)))
 (let ((__function__ 'output-files-process-printer-options))
  (declare (ignorable __function__))
  (b*
   (((reterr) 1 nil)
    (printer-options-option (assoc-eq :printer-options options))
    (printer-options
         (if printer-options-option (cdr printer-options-option)
           nil))
    ((unless (keyword-value-listp printer-options))
     (reterr
      (msg
       "The :PRINTER-OPTIONS input must be ~
                      a value-keyword list, ~
                      but it is ~x0 instead."
       printer-options)))
    (printer-options-alist
         (keyword-value-list-to-alist printer-options))
    (printer-options-keywords (strip-cars printer-options-alist))
    ((unless (no-duplicatesp-eq printer-options-keywords))
     (reterr
      (msg
       "The list of keywords in the :PRINTER-OPTIONS input ~
                      must have no duplicates, ~
                      but the supplied :PRINTER-OPTIONS input ~x0 ~
                      violates that requirement."
       printer-options)))
    ((unless (subsetp-eq printer-options-keywords
                         *output-files-printer-options*))
     (reterr
      (msg
       "The list of keywords in the :PRINTER-OPTIONS input ~
                      must be among ~&0, ~
                      but the supplied :PRINTER-OPTIONS input ~x0 ~
                      violates that requirement."
       *output-files-printer-options*
       printer-options)))
    (indent-size-option
         (assoc-eq :indentation-size printer-options-alist))
    (indent-size (if indent-size-option (cdr indent-size-option)
                   2))
    ((unless (posp indent-size))
     (reterr
      (msg
       "The :INDENTATION-LEVEL option ~
                      of the :PRINTER-OPTIONS input ~
                      must be a positive integer, ~
                      but it is ~x0 instead."
       indent-size)))
    (paren-nested-conds-option
       (assoc-eq
            :parenthesize-nested-conditional printer-options-alist))
    (paren-nested-conds
       (if paren-nested-conds-option (cdr paren-nested-conds-option)
         nil))
    ((unless (booleanp paren-nested-conds))
     (reterr
      (msg
       "The :PARENTHESIZE-NESTED-CONDITIONALS option ~
                      of the :PRINTER-OPTIONS input ~
                      must be a boolean, ~
                      but it is ~x0 instead."
       paren-nested-conds))))
   (retok indent-size paren-nested-conds))))

Theorem: posp-of-output-files-process-printer-options.indent-size

(defthm posp-of-output-files-process-printer-options.indent-size
  (b* (((mv acl2::?erp
            ?indent-size ?paren-nested-conds)
        (output-files-process-printer-options options)))
    (posp indent-size))
  :rule-classes :rewrite)

Theorem: booleanp-of-output-files-process-printer-options.paren-nested-conds

(defthm
 booleanp-of-output-files-process-printer-options.paren-nested-conds
 (b* (((mv acl2::?erp
           ?indent-size ?paren-nested-conds)
       (output-files-process-printer-options options)))
   (booleanp paren-nested-conds))
 :rule-classes :rewrite)