• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Community
  • Proof-automation
  • ACL2
  • Macro-libraries
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Fgl
      • Fgl-rewrite-rules
      • Fgl-function-mode
      • Fgl-object
      • Fgl-solving
      • Fgl-handling-if-then-elses
      • Fgl-counterexamples
      • Fgl-getting-bits-from-objects
      • Fgl-primitive-and-meta-rules
      • Fgl-interpreter-overview
      • Fgl-correctness-of-binding-free-variables
      • Fgl-debugging
      • Fgl-testbenches
      • Def-fgl-boolean-constraint
      • Fgl-stack
        • Scratchobj
        • Minor-frame
        • Major-frame
          • Major-frame-fix
          • Make-major-frame
          • Major-frame-equiv
          • Major-frame->minor-stack
          • Major-frame->rule
          • Major-frame->bindings
          • Change-major-frame
          • Major-frame->phase
          • Major-frame-p
        • Major-stack
        • Scratchlist
        • Minor-stack
      • Fgl-rewrite-tracing
      • Def-fgl-param-thm
      • Def-fgl-thm
      • Fgl-fast-alist-support
      • Fgl-array-support
      • Advanced-equivalence-checking-with-fgl
      • Fgl-fty-support
      • Fgl-internals
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• 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)))))