		Search-engine friendly clone of the ACL2 documentation.

Input-processing

Process-const-old

Process the :const-old input of a transformation.

Signature
(process-const-old const-old suppliedp wrld) → (mv erp code-old)
Arguments: suppliedp — Guard (booleanp suppliedp).; wrld — Guard (plist-worldp wrld).
Returns: code-old — Type (code-ensemblep code-old).

We check that the input was supplied and that it is a constant symbol whose value is an unambiguous annotate code ensemble. We return the code ensemble if successful.

Definitions and Theorems

Function: process-const-old

(defun process-const-old (const-old suppliedp wrld)
 (declare (xargs :guard (and (booleanp suppliedp)
                             (plist-worldp wrld))))
 (let ((__function__ 'process-const-old))
  (declare (ignorable __function__))
  (b*
   (((reterr) (irr-code-ensemble))
    ((unless suppliedp)
     (reterr (msg "The :CONST-OLD input must be supplied.")))
    ((unless (symbolp const-old))
     (reterr
      (msg
       "The :CONST-OLD must be a symbol, ~
                      but it is ~x0 instead."
       const-old)))
    ((unless (constant-symbolp const-old wrld))
     (reterr
      (msg
       "The :CONST-OLD 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)))
    ((unless (code-ensemble-unambp code-old))
     (reterr
      (msg
       "The code ensemble ~x0 ~
                      that is the value of the constant ~x1 ~
                      must be unambiguous, ~
                      but it is not."
       code-old const-old)))
    ((unless (code-ensemble-annop code-old))
     (reterr
      (msg
       "The code 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))))

Theorem: code-ensemblep-of-process-const-old.code-old

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

Theorem: code-ensemble-unambp-of-process-const-old

(defthm code-ensemble-unambp-of-process-const-old
  (b* (((mv acl2::?erp ?code-old)
        (process-const-old const-old suppliedp wrld)))
    (implies (not erp)
             (code-ensemble-unambp code-old))))

Theorem: code-ensemble-annop-of-process-const-old

(defthm code-ensemble-annop-of-process-const-old
  (b* (((mv acl2::?erp ?code-old)
        (process-const-old const-old suppliedp wrld)))
    (implies (not erp)
             (code-ensemble-annop code-old))))