		Search-engine friendly clone of the ACL2 documentation.

Sv::vl-expr.lisp

Vl-funcall-args-to-ordered

Signature
(vl-funcall-args-to-ordered ports plainargs namedargs) → (mv err args)
Arguments: ports — port declarations of the function.
Guard (vl-portdecllist-p ports).; plainargs — initial plainargs.
Guard (vl-maybe-exprlist-p plainargs).; namedargs — named args.
Guard (vl-call-namedargs-p namedargs).
Returns: err — Type (iff (vl-msg-p err) err).; args — Type (vl-exprlist-p args).

Definitions and Theorems

Function: vl-funcall-args-to-ordered

(defun vl-funcall-args-to-ordered (ports plainargs namedargs)
 (declare (xargs :guard (and (vl-portdecllist-p ports)
                             (vl-maybe-exprlist-p plainargs)
                             (vl-call-namedargs-p namedargs))))
 (let ((__function__ 'vl-funcall-args-to-ordered))
   (declare (ignorable __function__))
   (b*
     (((when (atom ports)) (mv nil nil))
      ((vl-portdecl port) (car ports))
      (arg (if (consp plainargs)
               (car plainargs)
             (cdr (assoc-equal port.name
                               (vl-call-namedargs-fix namedargs)))))
      ((unless arg)
       (mv (vmsg "Blank or no argument for port ~a0"
                 port.name)
           nil))
      ((mv err rest)
       (vl-funcall-args-to-ordered (cdr ports)
                                   (cdr plainargs)
                                   namedargs)))
     (mv err
         (and (not err)
              (cons (vl-expr-fix arg) rest))))))

Theorem: return-type-of-vl-funcall-args-to-ordered.err

(defthm return-type-of-vl-funcall-args-to-ordered.err
  (b* (((mv ?err acl2::?args)
        (vl-funcall-args-to-ordered ports plainargs namedargs)))
    (iff (vl-msg-p err) err))
  :rule-classes :rewrite)

Theorem: vl-exprlist-p-of-vl-funcall-args-to-ordered.args

(defthm vl-exprlist-p-of-vl-funcall-args-to-ordered.args
  (b* (((mv ?err acl2::?args)
        (vl-funcall-args-to-ordered ports plainargs namedargs)))
    (vl-exprlist-p args))
  :rule-classes :rewrite)

Theorem: len-of-args-when-no-error

(defthm len-of-args-when-no-error
  (b* (((mv ?err acl2::?args)
        (vl-funcall-args-to-ordered ports plainargs namedargs)))
    (implies (not err)
             (equal (len args) (len ports)))))

Theorem: count-of-vl-funcall-args-to-ordered

(defthm count-of-vl-funcall-args-to-ordered
  (b* (((mv ?err acl2::?args)
        (vl-funcall-args-to-ordered ports plainargs namedargs)))
    (implies (and (no-duplicatesp (vl-portdecllist->names ports))
                  (not err))
             (<= (vl-exprlist-count args)
                 (+ (vl-maybe-exprlist-count plainargs)
                    (vl-call-namedargs-count namedargs)))))
  :rule-classes :linear)

Theorem: count-of-vl-funcall-args-to-ordered-rw

(defthm count-of-vl-funcall-args-to-ordered-rw
  (b* (((vl-call x))
       ((mv err args)
        (vl-funcall-args-to-ordered ports x.plainargs x.namedargs)))
    (implies (and (no-duplicatesp (vl-portdecllist->names ports))
                  (not err)
                  (equal (vl-expr-kind x) :vl-call))
             (< (vl-exprlist-count args)
                (vl-expr-count x))))
  :rule-classes (:rewrite :linear))

Theorem: vl-funcall-args-to-ordered-of-vl-portdecllist-fix-ports

(defthm vl-funcall-args-to-ordered-of-vl-portdecllist-fix-ports
  (equal (vl-funcall-args-to-ordered (vl-portdecllist-fix ports)
                                     plainargs namedargs)
         (vl-funcall-args-to-ordered ports plainargs namedargs)))

Theorem: vl-funcall-args-to-ordered-vl-portdecllist-equiv-congruence-on-ports

(defthm
 vl-funcall-args-to-ordered-vl-portdecllist-equiv-congruence-on-ports
 (implies
  (vl-portdecllist-equiv ports ports-equiv)
  (equal
      (vl-funcall-args-to-ordered ports plainargs namedargs)
      (vl-funcall-args-to-ordered ports-equiv plainargs namedargs)))
 :rule-classes :congruence)

Theorem: vl-funcall-args-to-ordered-of-vl-maybe-exprlist-fix-plainargs

(defthm
      vl-funcall-args-to-ordered-of-vl-maybe-exprlist-fix-plainargs
  (equal (vl-funcall-args-to-ordered
              ports (vl-maybe-exprlist-fix plainargs)
              namedargs)
         (vl-funcall-args-to-ordered ports plainargs namedargs)))

Theorem: vl-funcall-args-to-ordered-vl-maybe-exprlist-equiv-congruence-on-plainargs

(defthm
 vl-funcall-args-to-ordered-vl-maybe-exprlist-equiv-congruence-on-plainargs
 (implies
  (vl-maybe-exprlist-equiv plainargs plainargs-equiv)
  (equal
      (vl-funcall-args-to-ordered ports plainargs namedargs)
      (vl-funcall-args-to-ordered ports plainargs-equiv namedargs)))
 :rule-classes :congruence)

Theorem: vl-funcall-args-to-ordered-of-vl-call-namedargs-fix-namedargs

(defthm
      vl-funcall-args-to-ordered-of-vl-call-namedargs-fix-namedargs
 (equal
      (vl-funcall-args-to-ordered ports plainargs
                                  (vl-call-namedargs-fix namedargs))
      (vl-funcall-args-to-ordered ports plainargs namedargs)))

Theorem: vl-funcall-args-to-ordered-vl-call-namedargs-equiv-congruence-on-namedargs

(defthm
 vl-funcall-args-to-ordered-vl-call-namedargs-equiv-congruence-on-namedargs
 (implies
  (vl-call-namedargs-equiv namedargs namedargs-equiv)
  (equal
      (vl-funcall-args-to-ordered ports plainargs namedargs)
      (vl-funcall-args-to-ordered ports plainargs namedargs-equiv)))
 :rule-classes :congruence)