		Search-engine friendly clone of the ACL2 documentation.

Ienv

Make-ienv

Basic constructor macro for ienv structures.

Syntax

(make-ienv [:version <version>] 
           [:short-bytes <short-bytes>] 
           [:int-bytes <int-bytes>] 
           [:long-bytes <long-bytes>] 
           [:llong-bytes <llong-bytes>] 
           [:plain-char-signedp <plain-char-signedp>])

This is the usual way to construct ienv structures. It simply conses together a structure with the specified fields.

This macro generates a new ienv structure from scratch. See also change-ienv, which can "change" an existing structure, instead.

Definition

This is an ordinary make- macro introduced by fty::defprod.

Macro: make-ienv

(defmacro make-ienv (&rest args)
  (std::make-aggregate 'ienv
                       args
                       '((:version)
                         (:short-bytes)
                         (:int-bytes)
                         (:long-bytes)
                         (:llong-bytes)
                         (:plain-char-signedp))
                       'make-ienv
                       nil))

Function: ienv

(defun ienv (version short-bytes int-bytes long-bytes
                     llong-bytes plain-char-signedp)
  (declare (xargs :guard (and (c::versionp version)
                              (posp short-bytes)
                              (posp int-bytes)
                              (posp long-bytes)
                              (posp llong-bytes)
                              (booleanp plain-char-signedp))))
  (declare (xargs :guard (and (<= short-bytes int-bytes)
                              (<= int-bytes long-bytes)
                              (<= long-bytes llong-bytes)
                              (<= 2 short-bytes)
                              (<= 2 int-bytes)
                              (<= 4 long-bytes)
                              (<= 8 llong-bytes))))
  (b* ((version (mbe :logic (c::version-fix version)
                     :exec version))
       (short-bytes (mbe :logic (pos-fix short-bytes)
                         :exec short-bytes))
       (int-bytes (mbe :logic (pos-fix int-bytes)
                       :exec int-bytes))
       (long-bytes (mbe :logic (pos-fix long-bytes)
                        :exec long-bytes))
       (llong-bytes (mbe :logic (pos-fix llong-bytes)
                         :exec llong-bytes))
       (plain-char-signedp (mbe :logic (bool-fix plain-char-signedp)
                                :exec plain-char-signedp)))
    (let ((short-bytes (mbe :logic
                            (if (and (<= short-bytes int-bytes)
                                     (<= int-bytes long-bytes)
                                     (<= long-bytes llong-bytes)
                                     (<= 2 short-bytes)
                                     (<= 2 int-bytes)
                                     (<= 4 long-bytes)
                                     (<= 8 llong-bytes))
                                short-bytes
                              2)
                            :exec short-bytes))
          (int-bytes (mbe :logic
                          (if (and (<= short-bytes int-bytes)
                                   (<= int-bytes long-bytes)
                                   (<= long-bytes llong-bytes)
                                   (<= 2 short-bytes)
                                   (<= 2 int-bytes)
                                   (<= 4 long-bytes)
                                   (<= 8 llong-bytes))
                              int-bytes
                            2)
                          :exec int-bytes))
          (long-bytes (mbe :logic
                           (if (and (<= short-bytes int-bytes)
                                    (<= int-bytes long-bytes)
                                    (<= long-bytes llong-bytes)
                                    (<= 2 short-bytes)
                                    (<= 2 int-bytes)
                                    (<= 4 long-bytes)
                                    (<= 8 llong-bytes))
                               long-bytes
                             4)
                           :exec long-bytes))
          (llong-bytes (mbe :logic
                            (if (and (<= short-bytes int-bytes)
                                     (<= int-bytes long-bytes)
                                     (<= long-bytes llong-bytes)
                                     (<= 2 short-bytes)
                                     (<= 2 int-bytes)
                                     (<= 4 long-bytes)
                                     (<= 8 llong-bytes))
                                llong-bytes
                              8)
                            :exec llong-bytes)))
      (list (cons 'version version)
            (cons 'short-bytes short-bytes)
            (cons 'int-bytes int-bytes)
            (cons 'long-bytes long-bytes)
            (cons 'llong-bytes llong-bytes)
            (cons 'plain-char-signedp
                  plain-char-signedp)))))