		Search-engine friendly clone of the ACL2 documentation.

Input-files-implementation

Input-files-process-ienv

Process the :std, :gcc, :short-bytes, :int-bytes, :long-bytes, :long-long-bytes, :plain-char-signed inputs.

Signature
(input-files-process-ienv std gcc short-bytes int-bytes long-bytes long-long-bytes plain-char-signed) → (mv erp ienv)
Returns: ienv — Type (ienvp ienv).

These are the inputs that define the implementation environment, which we return if the processing of these inputs is successful.

Definitions and Theorems

Function: input-files-process-ienv

(defun input-files-process-ienv
       (std gcc short-bytes int-bytes long-bytes
            long-long-bytes plain-char-signed)
 (declare (xargs :guard t))
 (let ((__function__ 'input-files-process-ienv))
  (declare (ignorable __function__))
  (b*
   (((reterr) (ienv-default))
    ((unless (member-equal std '(17 23)))
     (reterr
      (msg
       "The :STD input must be 17 or 23, ~
                      but it is ~x0 instead."
       std)))
    ((unless (booleanp gcc))
     (reterr
      (msg
       "The :GCC input must be a boolean, ~
                      but it is ~x0 instead."
       gcc)))
    ((unless (and (integerp short-bytes)
                  (>= short-bytes 2)))
     (reterr
      (msg
       "The :SHORT-BYTES input must be ~
                      an integer greater than or equal to 2, ~
                      but it is ~x0 instead."
       short-bytes)))
    ((unless (and (integerp int-bytes)
                  (>= int-bytes 2)
                  (>= int-bytes short-bytes)))
     (reterr
      (msg
       "The :INT-BYTES input must be ~
                      an integer greater than or equal to 2, ~
                      and greater than or equal to ~
                      the value ~x0 of :SHORT-BYTES, ~
                      but it is ~x1 instead."
       short-bytes int-bytes)))
    ((unless (and (integerp long-bytes)
                  (>= long-bytes 4)
                  (>= long-bytes int-bytes)))
     (reterr
      (msg
       "The :LONG-BYTES input must be ~
                      an integer greater than or equal to 4, ~
                      and greater than or equal to ~
                      the value ~x0 of :INT-BYTES, ~
                      but it is ~x1 instead."
       int-bytes long-bytes)))
    ((unless (and (integerp long-long-bytes)
                  (>= long-long-bytes 8)
                  (>= long-long-bytes long-bytes)))
     (reterr
      (msg
       "The :LONG-LONG-BYTES input must be ~
                      an integer greater than or equal to 8, ~
                      and greater than or equal to ~
                      the value ~x0 of :LONG-BYTES, ~
                      but it is ~x1 instead."
       long-bytes long-long-bytes)))
    ((unless (booleanp plain-char-signed))
     (reterr
      (msg
       "The :PLAIN-CHAR-SIGNED input must be a boolean, ~
                      but it is ~x0 instead."
       plain-char-signed)))
    (version (cond ((= std 17)
                    (if gcc (c::version-c17+gcc)
                      (c::version-c17)))
                   ((= std 23)
                    (if gcc (c::version-c23+gcc)
                      (c::version-c23)))))
    (ienv (make-ienv :version version
                     :short-bytes short-bytes
                     :int-bytes int-bytes
                     :long-bytes long-bytes
                     :llong-bytes long-long-bytes
                     :plain-char-signedp plain-char-signed)))
   (retok ienv))))

Theorem: ienvp-of-input-files-process-ienv.ienv

(defthm ienvp-of-input-files-process-ienv.ienv
  (b* (((mv acl2::?erp ?ienv)
        (input-files-process-ienv
             std gcc short-bytes int-bytes long-bytes
             long-long-bytes plain-char-signed)))
    (ienvp ienv))
  :rule-classes :rewrite)