		Search-engine friendly clone of the ACL2 documentation.

Ienv

Make-ienv

Basic constructor macro for ienv structures.

Syntax

(make-ienv [:uchar-format <uchar-format>] 
           [:schar-format <schar-format>] 
           [:char-format <char-format>] 
           [:short-format <short-format>] 
           [:int-format <int-format>] 
           [:long-format <long-format>] 
           [:llong-format <llong-format>])

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
                       '((:uchar-format)
                         (:schar-format)
                         (:char-format)
                         (:short-format)
                         (:int-format)
                         (:long-format)
                         (:llong-format))
                       'make-ienv
                       nil))

Function: ienv

(defun ienv (uchar-format schar-format char-format short-format
                          int-format long-format llong-format)
  (declare (xargs :guard (and (uchar-formatp uchar-format)
                              (schar-formatp schar-format)
                              (char-formatp char-format)
                              (integer-formatp short-format)
                              (integer-formatp int-format)
                              (integer-formatp long-format)
                              (integer-formatp llong-format))))
  (declare (xargs :guard t))
  (let ((__function__ 'ienv))
    (declare (ignorable __function__))
    (b* ((uchar-format (mbe :logic (uchar-format-fix uchar-format)
                            :exec uchar-format))
         (schar-format (mbe :logic (schar-format-fix schar-format)
                            :exec schar-format))
         (char-format (mbe :logic (char-format-fix char-format)
                           :exec char-format))
         (short-format (mbe :logic (integer-format-fix short-format)
                            :exec short-format))
         (int-format (mbe :logic (integer-format-fix int-format)
                          :exec int-format))
         (long-format (mbe :logic (integer-format-fix long-format)
                           :exec long-format))
         (llong-format (mbe :logic (integer-format-fix llong-format)
                            :exec llong-format)))
      (list (cons 'uchar-format uchar-format)
            (cons 'schar-format schar-format)
            (cons 'char-format char-format)
            (cons 'short-format short-format)
            (cons 'int-format int-format)
            (cons 'long-format long-format)
            (cons 'llong-format llong-format)))))