		Search-engine friendly clone of the ACL2 documentation.

Program-execution

Funparams-match-funargs

Match function arguments to function parameters.

Signature
(funparams-match-funargs params args) → vals
Arguments: params — Guard (funparam-listp params).; args — Guard (funarg-listp args).
Returns: vals — Type (value-list-resultp vals).

We go through the parameters in order. For each parameter, we try and find an argument with the same name; if none is found, matching fails. If one is found, we ensure that it has the same sort as the parameter, and also that the value has the type of the parameter. When we run out of parameters, for now we ignore any remaining arguments, but eventually we will want to fail if there are remaining arguments. If we reach the end of parameters without arguments left, parameters and arguments match up to permutation.

As we go through the parameters and find matching arguments, we collect the values of the arguments, in the same order as the parameters. We return the resulting list of values if successful, which forms the list of values to pass to the main function.

Definitions and Theorems

Function: funparams-match-funargs

(defun funparams-match-funargs (params args)
  (declare (xargs :guard (and (funparam-listp params)
                              (funarg-listp args))))
  (let ((__function__ 'funparams-match-funargs))
    (declare (ignorable __function__))
    (b* (((when (endp params)) nil)
         ((funparam param) (car params))
         (arg (lookup-funarg param.name args))
         ((unless arg)
          (reserrf (list :no-param param.name)))
         ((unless (equal param.sort (funarg->sort arg)))
          (reserrf (list :mismatched-sorts
                         :param param.sort
                         :arg (funarg->sort arg))))
         (val (funarg->value arg))
         (args (remove1-equal arg (funarg-list-fix args)))
         ((okf vals)
          (funparams-match-funargs (cdr params)
                                   args)))
      (cons val vals))))

Theorem: value-list-resultp-of-funparams-match-funargs

(defthm value-list-resultp-of-funparams-match-funargs
  (b* ((vals (funparams-match-funargs params args)))
    (value-list-resultp vals))
  :rule-classes :rewrite)

Theorem: funparams-match-funargs-of-funparam-list-fix-params

(defthm funparams-match-funargs-of-funparam-list-fix-params
  (equal (funparams-match-funargs (funparam-list-fix params)
                                  args)
         (funparams-match-funargs params args)))

Theorem: funparams-match-funargs-funparam-list-equiv-congruence-on-params

(defthm
   funparams-match-funargs-funparam-list-equiv-congruence-on-params
  (implies (funparam-list-equiv params params-equiv)
           (equal (funparams-match-funargs params args)
                  (funparams-match-funargs params-equiv args)))
  :rule-classes :congruence)

Theorem: funparams-match-funargs-of-funarg-list-fix-args

(defthm funparams-match-funargs-of-funarg-list-fix-args
  (equal (funparams-match-funargs params (funarg-list-fix args))
         (funparams-match-funargs params args)))

Theorem: funparams-match-funargs-funarg-list-equiv-congruence-on-args

(defthm funparams-match-funargs-funarg-list-equiv-congruence-on-args
  (implies (funarg-list-equiv args args-equiv)
           (equal (funparams-match-funargs params args)
                  (funparams-match-funargs params args-equiv)))
  :rule-classes :congruence)