		Search-engine friendly clone of the ACL2 documentation.

Major-frame

Make-major-frame

Basic constructor macro for major-frame structures.

Syntax

(make-major-frame [:bindings <bindings>] 
                  [:rule <rule>] 
                  [:phase <phase>] 
                  [:minor-stack <minor-stack>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-major-frame

(defmacro make-major-frame (&rest args)
  (std::make-aggregate 'major-frame
                       args
                       '((:bindings)
                         (:rule)
                         (:phase)
                         (:minor-stack quote
                                       (((bindings)
                                         (scratch)
                                         (term)
                                         (term-index)))))
                       'make-major-frame
                       nil))

Function: major-frame

(defun major-frame (bindings rule phase minor-stack)
  (declare (xargs :guard (and (fgl-object-bindings-p bindings)
                              (maybe-fgl-generic-rule-p rule)
                              (acl2::maybe-natp phase)
                              (minor-stack-p minor-stack))))
  (declare (xargs :guard t))
  (let ((__function__ 'major-frame))
    (declare (ignorable __function__))
    (b* ((bindings (mbe :logic (fgl-object-bindings-fix bindings)
                        :exec bindings))
         (rule (mbe :logic (maybe-fgl-generic-rule-fix rule)
                    :exec rule))
         (phase (mbe :logic (acl2::maybe-natp-fix phase)
                     :exec phase))
         (minor-stack (mbe :logic (minor-stack-fix minor-stack)
                           :exec minor-stack)))
      (list (cons 'bindings bindings)
            (cons 'rule rule)
            (cons 'phase phase)
            (cons 'minor-stack minor-stack)))))