		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Check-function-definer

Check if a function definer is statically well-formed.

Signature
(check-function-definer definer output-types fn-name ctxt) → (mv err? obligs)
Arguments: definer — Guard (function-definerp definer).; output-types — Guard (type-listp output-types).; fn-name — Guard (stringp fn-name).; ctxt — Guard (contextp ctxt).
Returns: obligs — Type (proof-obligation-listp obligs).

The context has no types being defined, but it may have functions (if this definer is part of function recursion), as well as variables in scope (namely, the function's inputs); it may also have obligation hypotheses, coming from preconditions. This motivates the guard of this ACL2 function.

For a regular function definition, we check the body and ensure that its type(s) is the same as the function's output type(s). This is too strong in general; we will relax this check.

For a quantifier function definition, we ensure that the bound variables do not conflict with the inputs; we augment the context with those variables and check the matrix, ensuring that it returns a single boolean value. We ensure also that the output of the function is a boolean.

Definitions and Theorems

Function: check-function-definer

(defun check-function-definer (definer output-types fn-name ctxt)
 (declare (xargs :guard (and (function-definerp definer)
                             (type-listp output-types)
                             (stringp fn-name)
                             (contextp ctxt))))
 (declare (ignorable fn-name))
 (declare (xargs :guard (null (context->types ctxt))))
 (let ((__function__ 'check-function-definer))
  (declare (ignorable __function__))
  (function-definer-case
   definer :regular
   (b* ((result (check-expression definer.body ctxt)))
    (type-result-case
      result :err (mv result.info nil)
      :ok
      (b*
        ((result1 (match-to-target definer.body
                                   result.types output-types ctxt)))
        (type-result-case result1
                          :err (mv result1.info nil)
                          :ok (mv nil
                                  (append result.obligations
                                          result1.obligations))))))
   :quantified
   (b*
     ((bound-names
           (typed-variable-list->name-list definer.variables))
      (free-names (typed-variable-list->name-list
                       (context->obligation-vars ctxt)))
      ((when (intersectp-equal bound-names free-names))
       (mv (list :bound-variables-conflict-with-inputs
                 bound-names free-names)
           nil))
      (bound-var-ctxt
           (typed-variables-to-variable-context definer.variables))
      (ctxt (context-add-variables bound-var-ctxt ctxt))
      (result (check-expression definer.matrix ctxt)))
    (type-result-case
      result :err (mv result.info nil)
      :ok
      (b*
        ((type (ensure-single-type result.types))
         ((when (not type))
          (mv (list :multi-valued-matrix definer.matrix)
              nil))
         ((unless (type-equiv type (type-boolean)))
          (mv (list :non-boolean-matrix definer.matrix)
              nil))
         ((unless
               (type-list-equiv output-types (list (type-boolean))))
          (mv (list :non-boolean-quantified-output-types
                    (type-list-fix output-types))
              nil)))
        (mv nil result.obligations)))))))

Theorem: proof-obligation-listp-of-check-function-definer.obligs

(defthm proof-obligation-listp-of-check-function-definer.obligs
  (b* (((mv ?err? ?obligs)
        (check-function-definer definer output-types fn-name ctxt)))
    (proof-obligation-listp obligs))
  :rule-classes :rewrite)

Theorem: check-function-definer-of-function-definer-fix-definer

(defthm check-function-definer-of-function-definer-fix-definer
 (equal (check-function-definer (function-definer-fix definer)
                                output-types fn-name ctxt)
        (check-function-definer definer output-types fn-name ctxt)))

Theorem: check-function-definer-function-definer-equiv-congruence-on-definer

(defthm
 check-function-definer-function-definer-equiv-congruence-on-definer
 (implies
   (function-definer-equiv definer definer-equiv)
   (equal (check-function-definer definer output-types fn-name ctxt)
          (check-function-definer definer-equiv
                                  output-types fn-name ctxt)))
 :rule-classes :congruence)

Theorem: check-function-definer-of-type-list-fix-output-types

(defthm check-function-definer-of-type-list-fix-output-types
 (equal (check-function-definer definer (type-list-fix output-types)
                                fn-name ctxt)
        (check-function-definer definer output-types fn-name ctxt)))

Theorem: check-function-definer-type-list-equiv-congruence-on-output-types

(defthm
  check-function-definer-type-list-equiv-congruence-on-output-types
 (implies
   (type-list-equiv output-types output-types-equiv)
   (equal (check-function-definer definer output-types fn-name ctxt)
          (check-function-definer definer
                                  output-types-equiv fn-name ctxt)))
 :rule-classes :congruence)

Theorem: check-function-definer-of-str-fix-fn-name

(defthm check-function-definer-of-str-fix-fn-name
 (equal
      (check-function-definer definer output-types (str-fix fn-name)
                              ctxt)
      (check-function-definer definer output-types fn-name ctxt)))

Theorem: check-function-definer-streqv-congruence-on-fn-name

(defthm check-function-definer-streqv-congruence-on-fn-name
 (implies
   (streqv fn-name fn-name-equiv)
   (equal (check-function-definer definer output-types fn-name ctxt)
          (check-function-definer definer
                                  output-types fn-name-equiv ctxt)))
 :rule-classes :congruence)

Theorem: check-function-definer-of-context-fix-ctxt

(defthm check-function-definer-of-context-fix-ctxt
 (equal
    (check-function-definer definer
                            output-types fn-name (context-fix ctxt))
    (check-function-definer definer output-types fn-name ctxt)))

Theorem: check-function-definer-context-equiv-congruence-on-ctxt

(defthm check-function-definer-context-equiv-congruence-on-ctxt
 (implies
   (context-equiv ctxt ctxt-equiv)
   (equal (check-function-definer definer output-types fn-name ctxt)
          (check-function-definer definer
                                  output-types fn-name ctxt-equiv)))
 :rule-classes :congruence)