• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
    • B*
    • Defunc
    • Fty
      • Deftagsum
      • Defprod
      • Defflexsum
      • Defbitstruct
      • Deflist
      • Defalist
      • Defbyte
      • Defresult
      • Deffixequiv
      • Deffixtype
      • Defoption
      • Fty-discipline
      • Fold
        • Deffold-reduce
        • Deffold-map
          • Deffold-map-implementation
            • Deffold-map-event-generation
            • Deffold-map-process-inputs-and-gen-everything
            • Deffold-map-fn
            • Deffold-map-input-processing
              • Deffold-map-process-inputs
              • Deffold-map-process-override
              • Deffold-map-process-types
              • *deffold-map-allowed-options*
            • Deffold-map-macro-definition
        • Defmake-self
      • Specific-types
      • Fty-extensions
      • Defsubtype
      • Deftypes
      • Defset
      • Defflatsum
      • Deflist-of-len
      • Defomap
      • Defbytelist
      • Fty::basetypes
      • Defvisitors
      • Deffixtype-alias
      • Deffixequiv-sk
      • Defunit
      • Multicase
      • Deffixequiv-mutual
      • Fty::baselists
      • Def-enumcase
      • Defmap
    • Apt
    • Std/util
    • Defdata
    • Defrstobj
    • Seq
    • Match-tree
    • Defrstobj
    • With-supporters
    • Def-partial-measure
    • Template-subst
    • Soft
    • Defthm-domain
    • Event-macros
    • Def-universal-equiv
    • Def-saved-obligs
    • With-supporters-after
    • Definec
    • Sig
    • Outer-local
    • Data-structures
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Deffold-map-input-processing

Deffold-map-process-inputs

Process all the inputs.

Signature

(deffold-map-process-inputs args fty-table) 
  → 
(mv erp suffix 
    types targets extra-args 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).

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: deffold-map-process-inputs

(defun deffold-map-process-inputs (args fty-table)
 (declare (xargs :guard (and (true-listp args)
                             (alistp fty-table))))
 (let ((__function__ 'deffold-map-process-inputs))
  (declare (ignorable __function__))
  (b*
   (((reterr)
     nil nil
     nil nil nil nil nil nil nil nil nil nil)
    ((mv erp suffix options)
     (partition-rest-and-keyword-args
          args *deffold-map-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."
       *deffold-map-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)
     (deffold-map-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)))
    (override-option (assoc-eq :override options))
    (override (if override-option (cdr override-option)
                nil))
    ((erp overrides)
     (deffold-map-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 overrides
          parents-presentp parents short-presentp
          short long-presentp long print))))

Theorem: symbolp-of-deffold-map-process-inputs.suffix

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

Theorem: symbol-listp-of-deffold-map-process-inputs.types

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

Theorem: symbol-listp-of-deffold-map-process-inputs.targets

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

Theorem: true-listp-of-deffold-map-process-inputs.extra-args

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

Theorem: alistp-of-deffold-map-process-inputs.overrides

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

Theorem: booleanp-of-deffold-map-process-inputs.parents-presentp

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

Theorem: booleanp-of-deffold-map-process-inputs.short-presentp

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

Theorem: booleanp-of-deffold-map-process-inputs.long-presentp

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

Theorem: evmac-input-print-p-of-deffold-map-process-inputs.print

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