		Search-engine friendly clone of the ACL2 documentation.

Preprocessor

Vl-line-up-define-formals-and-actuals

Signature
(vl-line-up-define-formals-and-actuals formals actuals name loc ppst) → (mv successp subst ppst)
Arguments: formals — Guard (vl-define-formallist-p formals).; actuals — Guard (string-listp actuals).; name — Name of macro being expanded, context for error messages.
Guard (stringp name).; loc — Location of macro being expanded, context for error messages.
Guard (vl-location-p loc).
Returns: successp — Type (booleanp successp).; subst — Type (and (alistp subst) (string-listp (alist-keys subst)) (string-listp (alist-vals subst))) .

Definitions and Theorems

Function: vl-line-up-define-formals-and-actuals

(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: booleanp-of-vl-line-up-define-formals-and-actuals.successp

(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: return-type-of-vl-line-up-define-formals-and-actuals.subst

(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)