Final work to turn the parsed elements into a real case statement.
(vl-make-case-statement check type expr items atts loc casekey) → stmt?
This either returns a statement or
Function:
(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:
(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)