(vl-line-up-define-formals-and-actuals formals actuals name loc ppst) → (mv successp subst ppst)
Function:
(defun vl-line-up-define-formals-and-actuals (formals actuals name loc ppst) (declare (xargs :stobjs (ppst))) (declare (xargs :guard (and (vl-define-formallist-p formals) (string-listp actuals) (stringp name) (vl-location-p loc)))) (let ((__function__ 'vl-line-up-define-formals-and-actuals)) (declare (ignorable __function__)) (b* (((when (atom formals)) (if (atom actuals) (mv t nil ppst) (let ((ppst (vl-ppst-fatal :msg "~a0: too many arguments given to ~s1." :args (list loc name)))) (mv nil nil ppst)))) ((when (atom actuals)) (b* (((mv okp ppst) (vl-check-remaining-formals-all-have-defaults formals name loc ppst)) ((when okp) (mv t (pairlis$ (vl-define-formallist->names formals) (vl-define-formallist->defaults formals)) ppst))) (mv nil nil ppst))) ((mv okp rest-subst ppst) (vl-line-up-define-formals-and-actuals (cdr formals) (cdr actuals) name loc ppst)) ((unless okp) (mv nil nil ppst)) ((vl-define-formal formal1) (car formals)) (actual1 (vl-trim-for-preproc (car actuals))) (value1 (if (and (equal actual1 "") formal1.default) (vl-trim-for-preproc formal1.default) actual1))) (mv t (cons (cons formal1.name value1) rest-subst) ppst))))
Theorem:
(defthm booleanp-of-vl-line-up-define-formals-and-actuals.successp (b* (((mv ?successp common-lisp::?subst ?ppst) (vl-line-up-define-formals-and-actuals formals actuals name loc ppst))) (booleanp successp)) :rule-classes :type-prescription)
Theorem:
(defthm return-type-of-vl-line-up-define-formals-and-actuals.subst (b* (((mv ?successp common-lisp::?subst ?ppst) (vl-line-up-define-formals-and-actuals formals actuals name loc ppst))) (and (alistp subst) (string-listp (alist-keys subst)) (string-listp (alist-vals subst)))) :rule-classes :rewrite)