		Search-engine friendly clone of the ACL2 documentation.

Jfield

Make-jfield

Basic constructor macro for jfield structures.

Syntax

(make-jfield [:access <access>] 
             [:static? <static?>] 
             [:final? <final?>] 
             [:transient? <transient?>] 
             [:volatile? <volatile?>] 
             [:type <type>] 
             [:name <name>] 
             [:init? <init?>])

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

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

Definition

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

Macro: make-jfield

(defmacro make-jfield (&rest args)
  (std::make-aggregate 'jfield
                       args
                       '((:access)
                         (:static?)
                         (:final?)
                         (:transient?)
                         (:volatile?)
                         (:type)
                         (:name)
                         (:init?))
                       'make-jfield
                       nil))

Function: jfield

(defun jfield (access static? final?
                      transient? volatile? type name init?)
  (declare (xargs :guard (and (jaccessp access)
                              (booleanp static?)
                              (booleanp final?)
                              (booleanp transient?)
                              (booleanp volatile?)
                              (jtypep type)
                              (stringp name)
                              (maybe-jexprp init?))))
  (declare (xargs :guard t))
  (let ((__function__ 'jfield))
    (declare (ignorable __function__))
    (b* ((access (mbe :logic (jaccess-fix access)
                      :exec access))
         (static? (mbe :logic (acl2::bool-fix static?)
                       :exec static?))
         (final? (mbe :logic (acl2::bool-fix final?)
                      :exec final?))
         (transient? (mbe :logic (acl2::bool-fix transient?)
                          :exec transient?))
         (volatile? (mbe :logic (acl2::bool-fix volatile?)
                         :exec volatile?))
         (type (mbe :logic (jtype-fix type)
                    :exec type))
         (name (mbe :logic (str-fix name) :exec name))
         (init? (mbe :logic (maybe-jexpr-fix init?)
                     :exec init?)))
      (list (cons 'access access)
            (cons 'static? static?)
            (cons 'final? final?)
            (cons 'transient? transient?)
            (cons 'volatile? volatile?)
            (cons 'type type)
            (cons 'name name)
            (cons 'init? init?)))))