		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Check-call-expression

Check if a function call is statically well-formed.

Signature
(check-call-expression function types args args-result expr ctxt) → result
Arguments: function — Guard (identifierp function).; types — Guard (type-listp types).; args — Guard (expression-listp args).; args-result — Guard (type-resultp args-result).; expr — Guard (expressionp expr).; ctxt — Guard (contextp ctxt).
Returns: result — Type (type-resultp result).

We check that the argument types match the function's input types. If the function has a precondition, we also generate a proof obligation saying that the arguments satisfy it. The call has the output types of the function.

Definitions and Theorems

Function: check-call-expression

(defun check-call-expression
       (function types args args-result expr ctxt)
 (declare (xargs :guard (and (identifierp function)
                             (type-listp types)
                             (expression-listp args)
                             (type-resultp args-result)
                             (expressionp expr)
                             (contextp ctxt))))
 (declare
      (xargs :guard (type-result-case args-result
                                      :err t
                                      :ok (= (len args-result.types)
                                             (len args)))))
 (let ((__function__ 'check-call-expression))
  (declare (ignorable __function__))
  (type-result-case
   args-result
   :err (type-result-err args-result.info)
   :ok
   (b*
    (((mv err? inputs outputs precond &)
      (get-function-in/out/pre/post function types ctxt))
     ((when err?) (type-result-err err?))
     (input-types (typed-variable-list->type-list inputs))
     (output-types (typed-variable-list->type-list outputs))
     ((mv okp obligs)
      (match-type-list args
                       args-result.types input-types ctxt))
     ((when (not okp))
      (type-result-err (list :type-mismatch-call
                             (identifier-fix function)
                             (expression-list-fix args)
                             args-result.types input-types)))
     (oblig?
      (if precond
       (b*
        ((input-names (typed-variable-list->name-list inputs))
         (subst
          (omap::from-lists input-names (expression-list-fix args)))
         (formula (subst-expression subst precond)))
        (non-trivial-proof-obligation
             (context->obligation-vars ctxt)
             (context->obligation-hyps ctxt)
             formula expr))
       nil)))
    (make-type-result-ok
         :types output-types
         :obligations (append args-result.obligations
                              obligs oblig?))))))

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

(defthm type-resultp-of-check-call-expression
  (b*
    ((result
          (check-call-expression function
                                 types args args-result expr ctxt)))
    (type-resultp result))
  :rule-classes :rewrite)

Theorem: check-call-expression-of-identifier-fix-function

(defthm check-call-expression-of-identifier-fix-function
  (equal (check-call-expression (identifier-fix function)
                                types args args-result expr ctxt)
         (check-call-expression function
                                types args args-result expr ctxt)))

Theorem: check-call-expression-identifier-equiv-congruence-on-function

(defthm
      check-call-expression-identifier-equiv-congruence-on-function
 (implies
   (identifier-equiv function function-equiv)
   (equal (check-call-expression function
                                 types args args-result expr ctxt)
          (check-call-expression function-equiv
                                 types args args-result expr ctxt)))
 :rule-classes :congruence)

Theorem: check-call-expression-of-type-list-fix-types

(defthm check-call-expression-of-type-list-fix-types
  (equal (check-call-expression function (type-list-fix types)
                                args args-result expr ctxt)
         (check-call-expression function
                                types args args-result expr ctxt)))

Theorem: check-call-expression-type-list-equiv-congruence-on-types

(defthm check-call-expression-type-list-equiv-congruence-on-types
 (implies
     (type-list-equiv types types-equiv)
     (equal (check-call-expression function
                                   types args args-result expr ctxt)
            (check-call-expression function types-equiv
                                   args args-result expr ctxt)))
 :rule-classes :congruence)

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

(defthm check-call-expression-of-expression-list-fix-args
  (equal (check-call-expression function
                                types (expression-list-fix args)
                                args-result expr ctxt)
         (check-call-expression function
                                types args args-result expr ctxt)))

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

(defthm
     check-call-expression-expression-list-equiv-congruence-on-args
 (implies
   (expression-list-equiv args args-equiv)
   (equal (check-call-expression function
                                 types args args-result expr ctxt)
          (check-call-expression function types
                                 args-equiv args-result expr ctxt)))
 :rule-classes :congruence)

Theorem: check-call-expression-of-type-result-fix-args-result

(defthm check-call-expression-of-type-result-fix-args-result
 (equal
     (check-call-expression function
                            types args (type-result-fix args-result)
                            expr ctxt)
     (check-call-expression function
                            types args args-result expr ctxt)))

Theorem: check-call-expression-type-result-equiv-congruence-on-args-result

(defthm
  check-call-expression-type-result-equiv-congruence-on-args-result
 (implies
   (type-result-equiv args-result args-result-equiv)
   (equal (check-call-expression function
                                 types args args-result expr ctxt)
          (check-call-expression function types
                                 args args-result-equiv expr ctxt)))
 :rule-classes :congruence)

Theorem: check-call-expression-of-expression-fix-expr

(defthm check-call-expression-of-expression-fix-expr
  (equal
       (check-call-expression function types
                              args args-result (expression-fix expr)
                              ctxt)
       (check-call-expression function
                              types args args-result expr ctxt)))

Theorem: check-call-expression-expression-equiv-congruence-on-expr

(defthm check-call-expression-expression-equiv-congruence-on-expr
 (implies
   (expression-equiv expr expr-equiv)
   (equal (check-call-expression function
                                 types args args-result expr ctxt)
          (check-call-expression function types
                                 args args-result expr-equiv ctxt)))
 :rule-classes :congruence)

Theorem: check-call-expression-of-context-fix-ctxt

(defthm check-call-expression-of-context-fix-ctxt
  (equal (check-call-expression function types args
                                args-result expr (context-fix ctxt))
         (check-call-expression function
                                types args args-result expr ctxt)))

Theorem: check-call-expression-context-equiv-congruence-on-ctxt

(defthm check-call-expression-context-equiv-congruence-on-ctxt
 (implies
   (context-equiv ctxt ctxt-equiv)
   (equal (check-call-expression function
                                 types args args-result expr ctxt)
          (check-call-expression function types
                                 args args-result expr ctxt-equiv)))
 :rule-classes :congruence)