		Search-engine friendly clone of the ACL2 documentation.

Output-files-implementation

Output-files-process-const/arg

Process the :const or arg input.

Signature
(output-files-process-const/arg arg options progp wrld) → (mv erp code)
Arguments: options — Guard (symbol-alistp options).; progp — Guard (booleanp progp).; wrld — Guard (plist-worldp wrld).
Returns: code — Type (code-ensemblep code).

Definitions and Theorems

Function: output-files-process-const/arg

(defun output-files-process-const/arg (arg options progp wrld)
 (declare (xargs :guard (and (symbol-alistp options)
                             (booleanp progp)
                             (plist-worldp wrld))))
 (let ((__function__ 'output-files-process-const/arg))
  (declare (ignorable __function__))
  (b*
   (((reterr) (irr-code-ensemble))
    (const-option (assoc-eq :const options))
    ((erp code)
     (if progp
      (b*
       (((when const-option)
         (reterr
          (msg
           "The :CONST input must not be supplied ~
                                to the programmatic interface."))))
       (retok arg))
      (b*
       (((unless const-option)
         (reterr
          (msg
           "The :CONST input must be supplied, ~
                              but it was not supplied.")))
        (const (cdr const-option))
        ((unless (symbolp const))
         (reterr
          (msg
           "The :CONST input must be a symbol, ~
                              but it is ~x0 instead."
           const)))
        (code (acl2::constant-value const wrld)))
       (retok code))))
    (desc
     (if progp "the required (i.e. non-keyword-option) input"
      (msg
       "the value of the ~x0 named constant, ~
                     specified by the :CONST input,"
       (cdr const-option))))
    ((unless (code-ensemblep code))
     (reterr
      (msg
       "~@0 must be a code ensemble, ~
                      but it is ~x1 instead."
       desc code)))
    ((unless (code-ensemble-unambp code))
     (reterr
      (msg
       "The code ensemble ~x0 passed as ~@1 ~
                      is ambiguous."
       code desc)))
    ((unless (code-ensemble-aidentp code))
     (reterr
      (msg
       "The code ensemble ~x0 passed as ~@1 ~
                      contains non-all-ASCII identifiers."
       code desc)))
    ((unless (or (ienv->gcc (code-ensemble->ienv code))
                 (transunit-ensemble-standardp
                      (code-ensemble->transunits code))))
     (reterr
      (msg
       "The code ensemble ~x0 passed as ~@1 ~
                      uses non-standard syntax (i.e. GCC extensions), ~
                      but the implementation environment indicates that ~
                      GCC extensions are not enabled."
       code desc))))
   (retok code))))

Theorem: code-ensemblep-of-output-files-process-const/arg.code

(defthm code-ensemblep-of-output-files-process-const/arg.code
  (b* (((mv acl2::?erp ?code)
        (output-files-process-const/arg arg options progp wrld)))
    (code-ensemblep code))
  :rule-classes :rewrite)

Theorem: code-ensemblep-when-output-files-process-const/arg

(defthm code-ensemblep-when-output-files-process-const/arg
  (b* (((mv acl2::?erp ?code)
        (output-files-process-const/arg arg options progp wrld)))
    (implies (not erp)
             (code-ensemblep code))))

Theorem: code-ensemble-unambp-when-output-files-process-const/arg

(defthm code-ensemble-unambp-when-output-files-process-const/arg
  (b* (((mv acl2::?erp ?code)
        (output-files-process-const/arg arg options progp wrld)))
    (implies (not erp)
             (code-ensemble-unambp code))))

Theorem: code-ensemble-aidentp-when-output-files-process-const/arg

(defthm code-ensemble-aidentp-when-output-files-process-const/arg
  (b* (((mv acl2::?erp ?code)
        (output-files-process-const/arg arg options progp wrld)))
    (implies (not erp)
             (code-ensemble-aidentp code))))