		Search-engine friendly clone of the ACL2 documentation.

Ienv

Make-ienv

Basic constructor macro for ienv structures.

Syntax

(make-ienv [: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
                       '((:short-bytes)
                         (:int-bytes)
                         (:long-bytes)
                         (:llong-bytes)
                         (:plain-char-signedp))
                       'make-ienv
                       nil))

Function: ienv

(defun ienv (short-bytes int-bytes long-bytes
                         llong-bytes plain-char-signedp)
 (declare (xargs :guard (and (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)
                             (<= 4 int-bytes)
                             (<= 8 long-bytes)
                             (<= 8 llong-bytes))))
 (let ((__function__ 'ienv))
  (declare (ignorable __function__))
  (b* ((short-bytes (mbe :logic (acl2::pos-fix short-bytes)
                         :exec short-bytes))
       (int-bytes (mbe :logic (acl2::pos-fix int-bytes)
                       :exec int-bytes))
       (long-bytes (mbe :logic (acl2::pos-fix long-bytes)
                        :exec long-bytes))
       (llong-bytes (mbe :logic (acl2::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)
                                     (<= 4 int-bytes)
                                     (<= 8 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)
                                   (<= 4 int-bytes)
                                   (<= 8 long-bytes)
                                   (<= 8 llong-bytes))
                              int-bytes
                            4)
                          :exec int-bytes))
          (long-bytes (mbe :logic
                           (if (and (<= short-bytes int-bytes)
                                    (<= int-bytes long-bytes)
                                    (<= long-bytes llong-bytes)
                                    (<= 2 short-bytes)
                                    (<= 4 int-bytes)
                                    (<= 8 long-bytes)
                                    (<= 8 llong-bytes))
                               long-bytes
                             8)
                           :exec long-bytes))
          (llong-bytes (mbe :logic
                            (if (and (<= short-bytes int-bytes)
                                     (<= int-bytes long-bytes)
                                     (<= long-bytes llong-bytes)
                                     (<= 2 short-bytes)
                                     (<= 4 int-bytes)
                                     (<= 8 long-bytes)
                                     (<= 8 llong-bytes))
                                llong-bytes
                              8)
                            :exec llong-bytes)))
      (list (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))))))