		Search-engine friendly clone of the ACL2 documentation.

Deffold-reduce-input-processing

Deffoldred-process-inputs

Process all the inputs.

Signature
(deffoldred-process-inputs args fty-table) → (mv erp suffix types targets extra-args result default combine overrides parents-presentp parents short-presentp short long-presentp long print)
Arguments: args — Guard (true-listp args).; fty-table — Guard (alistp fty-table).
Returns: suffix — Type (symbolp suffix).; types — Type (symbol-listp types).; targets — Type (symbol-listp targets).; extra-args — Type (true-listp extra-args).; result — Type (symbolp result).; combine — Type (symbolp combine).; overrides — Type (alistp overrides).; parents-presentp — Type (booleanp parents-presentp).; short-presentp — Type (booleanp short-presentp).; long-presentp — Type (booleanp long-presentp).; print — Type (acl2::evmac-input-print-p print).

Definitions and Theorems

Function: deffoldred-process-inputs

(defun deffoldred-process-inputs (args fty-table)
 (declare (xargs :guard (and (true-listp args)
                             (alistp fty-table))))
 (let ((__function__ 'deffoldred-process-inputs))
  (declare (ignorable __function__))
  (b*
   (((reterr)
     nil nil nil nil nil
     nil nil nil nil nil nil nil nil nil nil)
    ((mv erp suffix options)
     (partition-rest-and-keyword-args
          args *deffoldred-allowed-options*))
    ((when (or erp (not (consp suffix))
               (not (endp (cdr suffix)))))
     (reterr
      (msg
       "The inputs must be the suffix name ~
                      followed by the options ~&0."
       *deffoldred-allowed-options*)))
    (suffix (car suffix))
    ((unless (symbolp suffix))
     (reterr
      (msg
       "The SUFFIX input must be a symbol, ~
                      but it is ~x0 instead."
       suffix)))
    (types-option (assoc-eq :types options))
    ((unless types-option)
     (reterr (msg "The :TYPES input must be supplied.")))
    (types (cdr types-option))
    ((erp types targets)
     (deffoldred-process-types types fty-table))
    (extra-args-option (assoc-eq :extra-args options))
    (extra-args (if extra-args-option (cdr extra-args-option)
                  nil))
    ((unless (true-listp extra-args))
     (reterr
      (msg
       "The :EXTRA-ARGS input must be a list, ~
                      but it is ~x0 instead."
       extra-args)))
    (result-option (assoc-eq :result options))
    ((unless result-option)
     (reterr (msg "The :RESULT input must be supplied.")))
    (result (cdr result-option))
    ((unless (symbolp result))
     (reterr
      (msg
       "The :RESULT input must be a symbol, ~
                      but it is ~x0 instead."
       result)))
    (default-option (assoc-eq :default options))
    ((unless default-option)
     (reterr (msg "The :DEFAULT input must be supplied.")))
    (default (cdr default-option))
    (combine-option (assoc-eq :combine options))
    ((unless combine-option)
     (reterr (msg "The :COMBINE input must be supplied.")))
    (combine (cdr combine-option))
    ((unless (symbolp combine))
     (reterr
      (msg
       "The :COMBINE input must be a symbol, ~
                      but it is ~x0 instead."
       combine)))
    (override-option (assoc-eq :override options))
    (override (if override-option (cdr override-option)
                nil))
    ((erp overrides)
     (deffoldred-process-override override fty-table))
    (parents-option (assoc-eq :parents options))
    (parents-presentp (consp parents-option))
    (parents (cdr parents-option))
    (short-option (assoc-eq :short options))
    (short-presentp (consp short-option))
    (short (cdr short-option))
    (long-option (assoc-eq :long options))
    (long-presentp (consp long-option))
    (long (cdr long-option))
    (print-option (assoc-eq :print options))
    ((unless (or (atom print-option)
                 (acl2::evmac-input-print-p (cdr print-option))))
     (reterr
      (msg
       "The :PRINT input must be one of: nil, :error, :result, ~
                      :info, or :all, but it is ~x0 instead."
       print-option)))
    (print (if (consp print-option)
               (cdr print-option)
             :result)))
   (retok suffix types targets extra-args
          result default combine overrides
          parents-presentp parents short-presentp
          short long-presentp long print))))

Theorem: symbolp-of-deffoldred-process-inputs.suffix

(defthm symbolp-of-deffoldred-process-inputs.suffix
  (b* (((mv ?erp ?suffix ?types ?targets ?extra-args
            ?result acl2::?default ?combine
            ?overrides ?parents-presentp ?parents
            ?short-presentp ?short ?long-presentp
            ?long common-lisp::?print)
        (deffoldred-process-inputs args fty-table)))
    (symbolp suffix))
  :rule-classes :rewrite)

Theorem: symbol-listp-of-deffoldred-process-inputs.types

(defthm symbol-listp-of-deffoldred-process-inputs.types
  (b* (((mv ?erp ?suffix ?types ?targets ?extra-args
            ?result acl2::?default ?combine
            ?overrides ?parents-presentp ?parents
            ?short-presentp ?short ?long-presentp
            ?long common-lisp::?print)
        (deffoldred-process-inputs args fty-table)))
    (symbol-listp types))
  :rule-classes :rewrite)

Theorem: symbol-listp-of-deffoldred-process-inputs.targets

(defthm symbol-listp-of-deffoldred-process-inputs.targets
  (b* (((mv ?erp ?suffix ?types ?targets ?extra-args
            ?result acl2::?default ?combine
            ?overrides ?parents-presentp ?parents
            ?short-presentp ?short ?long-presentp
            ?long common-lisp::?print)
        (deffoldred-process-inputs args fty-table)))
    (symbol-listp targets))
  :rule-classes :rewrite)

Theorem: true-listp-of-deffoldred-process-inputs.extra-args

(defthm true-listp-of-deffoldred-process-inputs.extra-args
  (b* (((mv ?erp ?suffix ?types ?targets ?extra-args
            ?result acl2::?default ?combine
            ?overrides ?parents-presentp ?parents
            ?short-presentp ?short ?long-presentp
            ?long common-lisp::?print)
        (deffoldred-process-inputs args fty-table)))
    (true-listp extra-args))
  :rule-classes :rewrite)

Theorem: symbolp-of-deffoldred-process-inputs.result

(defthm symbolp-of-deffoldred-process-inputs.result
  (b* (((mv ?erp ?suffix ?types ?targets ?extra-args
            ?result acl2::?default ?combine
            ?overrides ?parents-presentp ?parents
            ?short-presentp ?short ?long-presentp
            ?long common-lisp::?print)
        (deffoldred-process-inputs args fty-table)))
    (symbolp result))
  :rule-classes :rewrite)

Theorem: symbolp-of-deffoldred-process-inputs.combine

(defthm symbolp-of-deffoldred-process-inputs.combine
  (b* (((mv ?erp ?suffix ?types ?targets ?extra-args
            ?result acl2::?default ?combine
            ?overrides ?parents-presentp ?parents
            ?short-presentp ?short ?long-presentp
            ?long common-lisp::?print)
        (deffoldred-process-inputs args fty-table)))
    (symbolp combine))
  :rule-classes :rewrite)

Theorem: alistp-of-deffoldred-process-inputs.overrides

(defthm alistp-of-deffoldred-process-inputs.overrides
  (b* (((mv ?erp ?suffix ?types ?targets ?extra-args
            ?result acl2::?default ?combine
            ?overrides ?parents-presentp ?parents
            ?short-presentp ?short ?long-presentp
            ?long common-lisp::?print)
        (deffoldred-process-inputs args fty-table)))
    (alistp overrides))
  :rule-classes :rewrite)

Theorem: booleanp-of-deffoldred-process-inputs.parents-presentp

(defthm booleanp-of-deffoldred-process-inputs.parents-presentp
  (b* (((mv ?erp ?suffix ?types ?targets ?extra-args
            ?result acl2::?default ?combine
            ?overrides ?parents-presentp ?parents
            ?short-presentp ?short ?long-presentp
            ?long common-lisp::?print)
        (deffoldred-process-inputs args fty-table)))
    (booleanp parents-presentp))
  :rule-classes :rewrite)

Theorem: booleanp-of-deffoldred-process-inputs.short-presentp

(defthm booleanp-of-deffoldred-process-inputs.short-presentp
  (b* (((mv ?erp ?suffix ?types ?targets ?extra-args
            ?result acl2::?default ?combine
            ?overrides ?parents-presentp ?parents
            ?short-presentp ?short ?long-presentp
            ?long common-lisp::?print)
        (deffoldred-process-inputs args fty-table)))
    (booleanp short-presentp))
  :rule-classes :rewrite)

Theorem: booleanp-of-deffoldred-process-inputs.long-presentp

(defthm booleanp-of-deffoldred-process-inputs.long-presentp
  (b* (((mv ?erp ?suffix ?types ?targets ?extra-args
            ?result acl2::?default ?combine
            ?overrides ?parents-presentp ?parents
            ?short-presentp ?short ?long-presentp
            ?long common-lisp::?print)
        (deffoldred-process-inputs args fty-table)))
    (booleanp long-presentp))
  :rule-classes :rewrite)

Theorem: evmac-input-print-p-of-deffoldred-process-inputs.print

(defthm evmac-input-print-p-of-deffoldred-process-inputs.print
  (b* (((mv ?erp ?suffix ?types ?targets ?extra-args
            ?result acl2::?default ?combine
            ?overrides ?parents-presentp ?parents
            ?short-presentp ?short ?long-presentp
            ?long common-lisp::?print)
        (deffoldred-process-inputs args fty-table)))
    (acl2::evmac-input-print-p print))
  :rule-classes :rewrite)