		Search-engine friendly clone of the ACL2 documentation.

Vl-simple-instantiate

Vl-simple-instantiate-args-main

Create plainargs binding some actuals to their ports, filling in the portnames and directions.

Signature
(vl-simple-instantiate-args-main actuals ports portdecls) → args
Arguments: actuals — Guard (vl-exprlist-p actuals).; ports — Guard (vl-regularportlist-p ports).; portdecls — for figuring out directions.
Guard (vl-portdecllist-p portdecls).
Returns: args — Type (vl-plainarglist-p args).

Definitions and Theorems

Function: vl-simple-instantiate-args-main

(defun vl-simple-instantiate-args-main (actuals ports portdecls)
  (declare (xargs :guard (and (vl-exprlist-p actuals)
                              (vl-regularportlist-p ports)
                              (vl-portdecllist-p portdecls))))
  (declare (xargs :guard (same-lengthp actuals ports)))
  (let ((__function__ 'vl-simple-instantiate-args-main))
    (declare (ignorable __function__))
    (b* (((when (atom actuals)) nil)
         ((vl-regularport port) (car ports))
         ((unless (and port.name
                       port.expr (vl-idexpr-p port.expr)
                       (equal (vl-idexpr->name port.expr)
                              port.name)))
          (raise "Port too complicated: ~x0.~%"
                 (car ports)))
         (decl (vl-find-portdecl port.name portdecls))
         ((unless decl)
          (raise "Port is not declared: ~x0.~%"
                 port.name))
         (actual (vl-expr-fix (car actuals)))
         (dir (vl-portdecl->dir decl))
         (arg (make-vl-plainarg :expr actual
                                :dir dir
                                :portname port.name)))
      (cons arg
            (vl-simple-instantiate-args-main (cdr actuals)
                                             (cdr ports)
                                             portdecls)))))

Theorem: vl-plainarglist-p-of-vl-simple-instantiate-args-main

(defthm vl-plainarglist-p-of-vl-simple-instantiate-args-main
 (b*
  ((args (vl-simple-instantiate-args-main actuals ports portdecls)))
  (vl-plainarglist-p args))
 :rule-classes :rewrite)

Theorem: vl-simple-instantiate-args-main-of-vl-exprlist-fix-actuals

(defthm vl-simple-instantiate-args-main-of-vl-exprlist-fix-actuals
  (equal (vl-simple-instantiate-args-main (vl-exprlist-fix actuals)
                                          ports portdecls)
         (vl-simple-instantiate-args-main actuals ports portdecls)))

Theorem: vl-simple-instantiate-args-main-vl-exprlist-equiv-congruence-on-actuals

(defthm
 vl-simple-instantiate-args-main-vl-exprlist-equiv-congruence-on-actuals
 (implies
  (vl-exprlist-equiv actuals actuals-equiv)
  (equal
   (vl-simple-instantiate-args-main actuals ports portdecls)
   (vl-simple-instantiate-args-main actuals-equiv ports portdecls)))
 :rule-classes :congruence)

Theorem: vl-simple-instantiate-args-main-of-vl-regularportlist-fix-ports

(defthm
    vl-simple-instantiate-args-main-of-vl-regularportlist-fix-ports
  (equal (vl-simple-instantiate-args-main
              actuals (vl-regularportlist-fix ports)
              portdecls)
         (vl-simple-instantiate-args-main actuals ports portdecls)))

Theorem: vl-simple-instantiate-args-main-vl-regularportlist-equiv-congruence-on-ports

(defthm
 vl-simple-instantiate-args-main-vl-regularportlist-equiv-congruence-on-ports
 (implies
  (vl-regularportlist-equiv ports ports-equiv)
  (equal
   (vl-simple-instantiate-args-main actuals ports portdecls)
   (vl-simple-instantiate-args-main actuals ports-equiv portdecls)))
 :rule-classes :congruence)

Theorem: vl-simple-instantiate-args-main-of-vl-portdecllist-fix-portdecls

(defthm
   vl-simple-instantiate-args-main-of-vl-portdecllist-fix-portdecls
  (equal (vl-simple-instantiate-args-main
              actuals
              ports (vl-portdecllist-fix portdecls))
         (vl-simple-instantiate-args-main actuals ports portdecls)))

Theorem: vl-simple-instantiate-args-main-vl-portdecllist-equiv-congruence-on-portdecls

(defthm
 vl-simple-instantiate-args-main-vl-portdecllist-equiv-congruence-on-portdecls
 (implies
  (vl-portdecllist-equiv portdecls portdecls-equiv)
  (equal
   (vl-simple-instantiate-args-main actuals ports portdecls)
   (vl-simple-instantiate-args-main actuals ports portdecls-equiv)))
 :rule-classes :congruence)