		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Check-function-definition-top/nontop

Check if a function definition (at the top level or not) is statically well-formed.

Signature
(check-function-definition-top/nontop fundef ctxt) → (mv err? obligs)
Arguments: fundef — Guard (function-definitionp fundef).; ctxt — Guard (contextp ctxt).
Returns: obligs — Type (proof-obligation-listp obligs).

This is used both by check-function-definition and by check-function-definition-list.

At the top level, the context has no types being defined, functions being defined, variables in scope, obligation variables, or obligation hypotheses. But the caller of this function, either check-function-definition or check-function-definition-list, extends the context component for the functions being defined; thus, this function definition's header is always in the context. This motivates the extra guard condition of this ACL2 function.

First we check the header; recall that part of that check is that no function with that name is already defined. We augment the context with the function's inputs. If here is a precondition, we check it and ensure it returns a boolean, and we add the precondition as an obligation hypothesis to the context. We check the function's definer. We further augment the context with the function outputs. If there is a postcondition, we check it and ensure it returns a boolean; note that we are assuming the precondition (if any) in checking the postcondition. We also generate a proof obligation saying that the postcondition holds; note that the precondition (if any) is in the hypotheses of that proof obligation.

Definitions and Theorems

Function: check-function-definition-top/nontop

(defun check-function-definition-top/nontop (fundef ctxt)
 (declare (xargs :guard (and (function-definitionp fundef)
                             (contextp ctxt))))
 (declare
  (xargs
      :guard (and (null (context->types ctxt))
                  (member-equal (function-definition->header fundef)
                                (context->functions ctxt))
                  (omap::emptyp (context->variables ctxt))
                  (null (context->obligation-vars ctxt))
                  (null (context->obligation-hyps ctxt)))))
 (let ((__function__ 'check-function-definition-top/nontop))
  (declare (ignorable __function__))
  (b*
   (((function-definition fundef) fundef)
    (err? (check-function-header fundef.header ctxt))
    (fn-name
         (identifier->name (function-header->name fundef.header)))
    ((when err?) (mv err? nil))
    (inputs (function-header->inputs fundef.header))
    (outputs (function-header->outputs fundef.header))
    (in-var-ctxt (typed-variables-to-variable-context inputs))
    (ctxt (context-add-variables in-var-ctxt ctxt))
    (ctxt (change-context ctxt
                          :obligation-vars inputs))
    ((mv err? pre-obligs ctxt)
     (if (not fundef.precondition)
         (mv nil nil ctxt)
      (b* ((pre-result (check-expression fundef.precondition ctxt)))
       (type-result-case
        pre-result
        :err (mv pre-result.info nil ctxt)
        :ok
        (b*
         ((type (ensure-single-type pre-result.types))
          ((when (not type))
           (mv (list :multi-valued-precondition fundef.precondition)
               nil ctxt))
          ((unless (type-equiv type (type-boolean)))
           (mv (list :non-boolean-precondition fundef.precondition)
               nil ctxt))
          (ctxt (context-add-condition fundef.precondition ctxt)))
         (mv nil pre-result.obligations ctxt))))))
    ((when err?) (mv err? nil))
    (output-types (typed-variable-list->type-list outputs))
    ((mv err? def-obligs)
     (check-function-definer fundef.definer
                             output-types fn-name ctxt))
    ((when err?) (mv err? nil))
    (ctxt
       (change-context
            ctxt
            :obligation-vars (append (context->obligation-vars ctxt)
                                     outputs)))
    ((mv err? post-obligs)
     (if (not fundef.postcondition)
         (mv nil nil)
      (b*
       ((var-ctxt (typed-variables-to-variable-context outputs))
        (ctxt (context-add-variables var-ctxt ctxt))
        (post-result (check-expression fundef.postcondition ctxt)))
       (type-result-case
        post-result
        :err (mv post-result.info nil)
        :ok
        (b*
         ((type (ensure-single-type post-result.types))
          ((when (not type))
           (mv
             (list :multi-valued-postcondition fundef.postcondition)
             nil))
          ((unless (type-equiv type (type-boolean)))
           (mv
              (list :non-boolean-postcondition fundef.postcondition)
              nil)))
         (mv nil post-result.obligations))))))
    ((when err?) (mv err? nil))
    (fn-body (function-definer-case fundef.definer
                                    :regular fundef.definer.body
                                    :quantified nil))
    (recursive-p (function-called-in fn-name fn-body))
    (fn-result-expr
     (if
      (and fn-body fundef.postcondition)
      (if recursive-p
       (make-expression-call
            :function (make-identifier :name fn-name)
            :types nil
            :arguments
            (typed-variable-list->-expression-variable-list inputs))
       fn-body)
      nil))
    (oblig?
     (if fn-result-expr
      (non-trivial-proof-obligation
          (context->obligation-vars ctxt)
          (append (context->obligation-hyps ctxt)
                  (list (obligation-hyp-binding
                             (make-binding :variables outputs
                                           :value fn-result-expr))))
          fundef.postcondition fn-body)
      nil)))
   (mv nil
       (append pre-obligs
               def-obligs post-obligs oblig?)))))

Theorem: proof-obligation-listp-of-check-function-definition-top/nontop.obligs

(defthm
 proof-obligation-listp-of-check-function-definition-top/nontop.obligs
 (b* (((mv ?err? ?obligs)
       (check-function-definition-top/nontop fundef ctxt)))
   (proof-obligation-listp obligs))
 :rule-classes :rewrite)

Theorem: check-function-definition-top/nontop-of-function-definition-fix-fundef

(defthm
 check-function-definition-top/nontop-of-function-definition-fix-fundef
 (equal (check-function-definition-top/nontop
             (function-definition-fix fundef)
             ctxt)
        (check-function-definition-top/nontop fundef ctxt)))

Theorem: check-function-definition-top/nontop-function-definition-equiv-congruence-on-fundef

(defthm
 check-function-definition-top/nontop-function-definition-equiv-congruence-on-fundef
 (implies
   (function-definition-equiv fundef fundef-equiv)
   (equal (check-function-definition-top/nontop fundef ctxt)
          (check-function-definition-top/nontop fundef-equiv ctxt)))
 :rule-classes :congruence)

Theorem: check-function-definition-top/nontop-of-context-fix-ctxt

(defthm check-function-definition-top/nontop-of-context-fix-ctxt
 (equal
    (check-function-definition-top/nontop fundef (context-fix ctxt))
    (check-function-definition-top/nontop fundef ctxt)))

Theorem: check-function-definition-top/nontop-context-equiv-congruence-on-ctxt

(defthm
 check-function-definition-top/nontop-context-equiv-congruence-on-ctxt
 (implies
   (context-equiv ctxt ctxt-equiv)
   (equal (check-function-definition-top/nontop fundef ctxt)
          (check-function-definition-top/nontop fundef ctxt-equiv)))
 :rule-classes :congruence)