		Search-engine friendly clone of the ACL2 documentation.

Address

Make-address

Basic constructor macro for address structures.

Syntax

(make-address [:path <path>] 
              [:index <index>] 
              [:scope <scope>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-address

(defmacro make-address (&rest args)
  (std::make-aggregate 'address
                       args '((:path) (:index) (:scope . 0))
                       'make-address
                       nil))

Function: address

(defun address (path index scope)
  (declare (xargs :guard (and (path-p path)
                              (maybe-natp index)
                              (addr-scope-p scope))))
  (declare (xargs :guard t))
  (let ((__function__ 'address))
    (declare (ignorable __function__))
    (b* ((path (mbe :logic (path-fix path) :exec path))
         (index (mbe :logic (acl2::maybe-natp-fix index)
                     :exec index))
         (scope (mbe :logic (addr-scope-fix scope)
                     :exec scope)))
      (if (and (eql scope 0) (eq index nil))
          path
        (list :address path index scope)))))