		Search-engine friendly clone of the ACL2 documentation.

Statement-switch

Make-statement-switch

Basic constructor macro for statement-switch structures.

Syntax

(make-statement-switch [:target <target>] 
                       [:cases <cases>] 
                       [:default <default>])

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

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

Definition

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

Macro: make-statement-switch

(defmacro make-statement-switch (&rest args)
  (std::make-aggregate 'statement-switch
                       args '((:target) (:cases) (:default))
                       'make-statement-switch
                       nil))

Function: statement-switch

(defun statement-switch (target cases default)
  (declare (xargs :guard (and (expressionp target)
                              (swcase-listp cases)
                              (block-optionp default))))
  (declare (xargs :guard t))
  (let ((__function__ 'statement-switch))
    (declare (ignorable __function__))
    (b* ((target (mbe :logic (expression-fix target)
                      :exec target))
         (cases (mbe :logic (swcase-list-fix cases)
                     :exec cases))
         (default (mbe :logic (block-option-fix default)
                       :exec default)))
      (cons :switch (list target cases default)))))