		Search-engine friendly clone of the ACL2 documentation.

Simpadd0-input-processing

Simpadd0-process-inputs

Process all the inputs.

Signature
(simpadd0-process-inputs const-old const-new wrld) → (mv erp code-old const-new$)
Arguments: wrld — Guard (plist-worldp wrld).
Returns: code-old — Type (code-ensemblep code-old).; const-new$ — Type (symbolp const-new$).

Definitions and Theorems

Function: simpadd0-process-inputs

(defun simpadd0-process-inputs (const-old const-new wrld)
 (declare (xargs :guard (plist-worldp wrld)))
 (let ((__function__ 'simpadd0-process-inputs))
  (declare (ignorable __function__))
  (b*
   (((reterr) (irr-code-ensemble) nil)
    ((unless (symbolp const-old))
     (reterr
      (msg
       "The first input must be a symbol, ~
                      but it is ~x0 instead."
       const-old)))
    ((unless (symbolp const-new))
     (reterr
      (msg
       "The second input must be a symbol, ~
                      but it is ~x0 instead."
       const-new)))
    ((unless (constant-symbolp const-old wrld))
     (reterr
      (msg
       "The first input, ~x0, must be a named constant, ~
                      but it is not."
       const-old)))
    (code-old (constant-value const-old wrld))
    ((unless (code-ensemblep code-old))
     (reterr
      (msg
       "The value of the constant ~x0 ~
                      must be a code ensemble, ~
                      but it is ~x1 instead."
       const-old code-old)))
    (tunits-old (code-ensemble->transunits code-old))
    ((unless (transunit-ensemble-unambp tunits-old))
     (reterr
      (msg
       "The translation unit ensemble ~
                      of the code ensemble ~x0 ~
                      that is the value of the constant ~x1 ~
                      must be unambiguous, ~
                      but it is not."
       code-old const-old)))
    ((unless (transunit-ensemble-annop tunits-old))
     (reterr
      (msg
       "The translation unit ensemble ~
                      of the coee ensemble ~x0 ~
                      that is the value of the constant ~x1 ~
                      must contains validation information, ~
                      but it does not."
       code-old const-old))))
   (retok code-old const-new))))

Theorem: code-ensemblep-of-simpadd0-process-inputs.code-old

(defthm code-ensemblep-of-simpadd0-process-inputs.code-old
  (b* (((mv acl2::?erp ?code-old ?const-new$)
        (simpadd0-process-inputs const-old const-new wrld)))
    (code-ensemblep code-old))
  :rule-classes :rewrite)

Theorem: symbolp-of-simpadd0-process-inputs.const-new$

(defthm symbolp-of-simpadd0-process-inputs.const-new$
  (b* (((mv acl2::?erp ?code-old ?const-new$)
        (simpadd0-process-inputs const-old const-new wrld)))
    (symbolp const-new$))
  :rule-classes :rewrite)

Theorem: transunit-ensemble-unambp-of-simpadd0-process-inputs

(defthm transunit-ensemble-unambp-of-simpadd0-process-inputs
  (b* (((mv acl2::?erp ?code-old ?const-new$)
        (simpadd0-process-inputs const-old const-new wrld)))
    (implies (not erp)
             (transunit-ensemble-unambp
                  (code-ensemble->transunits code-old)))))

Theorem: transunit-ensemble-annop-of-simpadd0-process-inputs

(defthm transunit-ensemble-annop-of-simpadd0-process-inputs
  (b* (((mv acl2::?erp ?code-old ?const-new$)
        (simpadd0-process-inputs const-old const-new wrld)))
    (implies (not erp)
             (transunit-ensemble-annop
                  (code-ensemble->transunits code-old)))))