Main function the parser uses for creating task declarations.
(vl-make-taskdecl-for-parser &key name lifetime ports decls body atts loc) → task
This mainly just adds the
Function:
(defun vl-make-taskdecl-for-parser-fn (name lifetime ports decls body atts loc) (declare (xargs :guard (and (stringp name) (vl-lifetime-p lifetime) (vl-portdecllist-p ports) (vl-blockitemlist-p decls) (vl-stmt-p body) (vl-atts-p atts) (vl-location-p loc)))) (let ((__function__ 'vl-make-taskdecl-for-parser)) (declare (ignorable __function__)) (b* ((port-vars (vl-make-hidden-variables-for-portdecls ports)) (decls (append port-vars decls)) ((mv vardecls paramdecls imports) (vl-sort-blockitems decls))) (make-vl-taskdecl :name name :lifetime lifetime :portdecls ports :blockitems decls :vardecls vardecls :paramdecls paramdecls :imports imports :body body :atts atts :loc loc))))
Theorem:
(defthm vl-taskdecl-p-of-vl-make-taskdecl-for-parser (b* ((task (vl-make-taskdecl-for-parser-fn name lifetime ports decls body atts loc))) (vl-taskdecl-p task)) :rule-classes :rewrite)