		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Check-expr-call

Check an expression that is a function call.

Signature
(check-expr-call fun args funtab vartab tagenv) → type
Arguments: fun — Guard (identp fun).; args — Guard (expr-listp args).; funtab — Guard (fun-tablep funtab).; vartab — Guard (var-tablep vartab).; tagenv — Guard (tag-envp tagenv).
Returns: type — Type (type-resultp type).

We check the argument expressions, which must be pure (because we restrict them to be so). We retrieve the function type from the function table and we compare the input types with the argument types; this is more restrictive than allowed in [C], but it is adequate for now. Prior to comparing the types, we perform array-to-pointer conversions on all parameter types: this is consistent with the treatment of assignments (namely that the left-hand side of assignment is subjected to this conversion [C:6.3.2.1/3]), given that argument passing is treated like assignment [C:6.5.2.2/2]. Note that check-expr-pure-list already applies that conversion to the argument types, so there is not need to do it here. We return the output type as the type of the call. A function call is never an lvalue; thus, we return a plain type, not an expression type.

Definitions and Theorems

Function: check-expr-call

(defun check-expr-call (fun args funtab vartab tagenv)
  (declare (xargs :guard (and (identp fun)
                              (expr-listp args)
                              (fun-tablep funtab)
                              (var-tablep vartab)
                              (tag-envp tagenv))))
  (let ((__function__ 'check-expr-call))
    (declare (ignorable __function__))
    (b* ((fun (ident-fix fun))
         (args (expr-list-fix args))
         ((okf arg-types)
          (check-expr-pure-list args vartab tagenv))
         (arg-types (apconvert-type-list arg-types))
         (info (fun-table-lookup fun funtab))
         ((unless info)
          (reserrf (list :fun-not-found fun)))
         (param-types (fun-sinfo->inputs info))
         (param-types (apconvert-type-list param-types))
         ((unless (equal param-types arg-types))
          (reserrf (list :call-args-mistype fun args
                         :required param-types
                         :supplied arg-types))))
      (fun-sinfo->output info))))

Theorem: type-resultp-of-check-expr-call

(defthm type-resultp-of-check-expr-call
  (b* ((type (check-expr-call fun args funtab vartab tagenv)))
    (type-resultp type))
  :rule-classes :rewrite)

Theorem: check-expr-call-of-ident-fix-fun

(defthm check-expr-call-of-ident-fix-fun
  (equal (check-expr-call (ident-fix fun)
                          args funtab vartab tagenv)
         (check-expr-call fun args funtab vartab tagenv)))

Theorem: check-expr-call-ident-equiv-congruence-on-fun

(defthm check-expr-call-ident-equiv-congruence-on-fun
 (implies
      (ident-equiv fun fun-equiv)
      (equal (check-expr-call fun args funtab vartab tagenv)
             (check-expr-call fun-equiv args funtab vartab tagenv)))
 :rule-classes :congruence)

Theorem: check-expr-call-of-expr-list-fix-args

(defthm check-expr-call-of-expr-list-fix-args
  (equal (check-expr-call fun (expr-list-fix args)
                          funtab vartab tagenv)
         (check-expr-call fun args funtab vartab tagenv)))

Theorem: check-expr-call-expr-list-equiv-congruence-on-args

(defthm check-expr-call-expr-list-equiv-congruence-on-args
 (implies
      (expr-list-equiv args args-equiv)
      (equal (check-expr-call fun args funtab vartab tagenv)
             (check-expr-call fun args-equiv funtab vartab tagenv)))
 :rule-classes :congruence)

Theorem: check-expr-call-of-fun-table-fix-funtab

(defthm check-expr-call-of-fun-table-fix-funtab
  (equal (check-expr-call fun args (fun-table-fix funtab)
                          vartab tagenv)
         (check-expr-call fun args funtab vartab tagenv)))

Theorem: check-expr-call-fun-table-equiv-congruence-on-funtab

(defthm check-expr-call-fun-table-equiv-congruence-on-funtab
 (implies
      (fun-table-equiv funtab funtab-equiv)
      (equal (check-expr-call fun args funtab vartab tagenv)
             (check-expr-call fun args funtab-equiv vartab tagenv)))
 :rule-classes :congruence)

Theorem: check-expr-call-of-var-table-fix-vartab

(defthm check-expr-call-of-var-table-fix-vartab
  (equal (check-expr-call fun args funtab (var-table-fix vartab)
                          tagenv)
         (check-expr-call fun args funtab vartab tagenv)))

Theorem: check-expr-call-var-table-equiv-congruence-on-vartab

(defthm check-expr-call-var-table-equiv-congruence-on-vartab
 (implies
      (var-table-equiv vartab vartab-equiv)
      (equal (check-expr-call fun args funtab vartab tagenv)
             (check-expr-call fun args funtab vartab-equiv tagenv)))
 :rule-classes :congruence)

Theorem: check-expr-call-of-tag-env-fix-tagenv

(defthm check-expr-call-of-tag-env-fix-tagenv
  (equal (check-expr-call fun
                          args funtab vartab (tag-env-fix tagenv))
         (check-expr-call fun args funtab vartab tagenv)))

Theorem: check-expr-call-tag-env-equiv-congruence-on-tagenv

(defthm check-expr-call-tag-env-equiv-congruence-on-tagenv
 (implies
      (tag-env-equiv tagenv tagenv-equiv)
      (equal (check-expr-call fun args funtab vartab tagenv)
             (check-expr-call fun args funtab vartab tagenv-equiv)))
 :rule-classes :congruence)