		Search-engine friendly clone of the ACL2 documentation.

Parse-statements

Vl-make-case-statement

Final work to turn the parsed elements into a real case statement.

Signature
(vl-make-case-statement check type expr items atts loc casekey) → stmt?
Arguments: check — Guard (vl-casecheck-p check).; type — Guard (vl-casetype-p type).; expr — Guard (vl-expr-p expr).; items — Guard (vl-caselist-p items).; atts — Guard (vl-atts-p atts).; loc — Guard (vl-location-p loc).; casekey — Guard (or (vl-token-p casekey) (not casekey)).
Returns: stmt? — Type (equal (vl-stmt-p stmt?) (if stmt? t nil)).

This either returns a statement or nil for failure. The only reason it can fail is that more than one default statement was provided.

Definitions and Theorems

Function: vl-make-case-statement

(defun vl-make-case-statement
       (check type expr items atts loc casekey)
  (declare (xargs :guard (and (vl-casecheck-p check)
                              (vl-casetype-p type)
                              (vl-expr-p expr)
                              (vl-caselist-p items)
                              (vl-atts-p atts)
                              (vl-location-p loc)
                              (or (vl-token-p casekey)
                                  (not casekey)))))
  (let ((__function__ 'vl-make-case-statement))
    (declare (ignorable __function__))
    (b* (((mv defaults normal-cases)
          (vl-filter-parsed-caseitemlist items))
         ((when (> (len defaults) 1)) nil)
         (casekey (cond ((not casekey) nil)
                        ((eq (vl-token->type casekey)
                             :vl-kwd-inside)
                         :inside)
                        ((eq (vl-token->type casekey)
                             :vl-kwd-matches)
                         :matches)
                        (t nil))))
      (make-vl-casestmt :check check :casetype type :test
                        expr :caselist normal-cases :default
                        (if defaults (car defaults)
                          (make-vl-nullstmt))
                        :atts atts
                        :casekey casekey
                        :loc loc))))

Theorem: return-type-of-vl-make-case-statement

(defthm return-type-of-vl-make-case-statement
  (b*
   ((stmt?
         (vl-make-case-statement check
                                 type expr items atts loc casekey)))
   (equal (vl-stmt-p stmt?)
          (if stmt? t nil)))
  :rule-classes :rewrite)