		Search-engine friendly clone of the ACL2 documentation.

Modscope-nested

Make-modscope-nested

Basic constructor macro for modscope-nested structures.

Syntax

(make-modscope-nested [:modidx <modidx>] 
                      [:wireoffset <wireoffset>] 
                      [:instoffset <instoffset>] 
                      [:upper <upper>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-modscope-nested

(defmacro make-modscope-nested (&rest args)
  (std::make-aggregate 'modscope-nested
                       args
                       '((:modidx)
                         (:wireoffset)
                         (:instoffset)
                         (:upper))
                       'make-modscope-nested
                       nil))

Function: modscope-nested

(defun modscope-nested (modidx wireoffset instoffset upper)
 (declare (xargs :guard (and (natp modidx)
                             (natp wireoffset)
                             (natp instoffset)
                             (modscope-p upper))))
 (declare (xargs :guard t))
 (let ((__function__ 'modscope-nested))
  (declare (ignorable __function__))
  (b* ((modidx (mbe :logic (nfix modidx) :exec modidx))
       (wireoffset (mbe :logic (nfix wireoffset)
                        :exec wireoffset))
       (instoffset (mbe :logic (nfix instoffset)
                        :exec instoffset))
       (upper (mbe :logic (modscope-fix upper)
                   :exec upper)))
   (cons
      :nested (std::prod-cons (std::prod-cons modidx wireoffset)
                              (std::prod-cons instoffset upper))))))