		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 tunits-old const-new$)
Arguments: wrld — Guard (plist-worldp wrld).
Returns: tunits-old — Type (transunit-ensemblep tunits-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-transunit-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)))
    (tunits-old (constant-value const-old wrld))
    ((unless (transunit-ensemblep tunits-old))
     (reterr
      (msg
       "The value of the constant ~x0 ~
                      must be a translation unit ensemble, ~
                      but it is ~x1 instead."
       const-old tunits-old)))
    ((unless (transunit-ensemble-unambp tunits-old))
     (reterr
      (msg
       "The translation unit ensemble ~x0 ~
                      that is the value of the constant ~x1 ~
                      must be unambiguous, ~
                      but it is not."
       tunits-old const-old)))
    ((unless (transunit-ensemble-annop tunits-old))
     (reterr
      (msg
       "The translation unit ensemble ~x0 ~
                      that is the value of the constant ~x1 ~
                      must contains validation information, ~
                      but it does not."
       tunits-old const-old))))
   (retok tunits-old const-new))))

Theorem: transunit-ensemblep-of-simpadd0-process-inputs.tunits-old

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

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

(defthm symbolp-of-simpadd0-process-inputs.const-new$
  (b* (((mv acl2::?erp ?tunits-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 ?tunits-old ?const-new$)
        (simpadd0-process-inputs const-old const-new wrld)))
    (implies (not erp)
             (transunit-ensemble-unambp tunits-old))))

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

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