		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Check-function-specifier

Check if a function specifier is statically well-formed.

Signature
(check-function-specifier spec inputs/outputs ctxt) → (mv err? obligs)
Arguments: spec — Guard (function-specifierp spec).; inputs/outputs — Guard (typed-variable-listp inputs/outputs).; ctxt — Guard (contextp ctxt).
Returns: obligs — Type (proof-obligation-listp obligs).

When checking a function specifier, the context has no types being defined, no variables in scope, and no obligation variable and hypotheses, but there may be function headers: Ttese all come from the function specification that this specifier is contained in.

The inputs/outputs parameter of this ACL2 function is non-nil only when the specifier is an input/output one: it consists of the inputs and output of the function header (there must be exactly one) of the enclosing function specification.

A specification is a predicate, so the body must be always boolean-valued.

For a regular function specifier, we simply check the body and ensure it is a boolean. The use of this kind of function specifier seems quite limited, because there are no ordinary (not function) variables in scope: it points to the fact that we'll need to extend Syntheto with more general second-order functions (still representable in ACL2's first-order logic, e.g. via SOFT).

For a quantifier function specifier, we augment the context with the bound variables and we check the matrix ensuring it is a boolean.

For an input/output function specifier, we augment the context with the input/output variables and we check the relation ensuring it is a boolean.

Definitions and Theorems

Function: check-function-specifier

(defun check-function-specifier (spec inputs/outputs ctxt)
 (declare (xargs :guard (and (function-specifierp spec)
                             (typed-variable-listp inputs/outputs)
                             (contextp ctxt))))
 (declare
      (xargs :guard (and (null (context->types ctxt))
                         (omap::emptyp (context->variables ctxt))
                         (null (context->obligation-vars ctxt))
                         (null (context->obligation-hyps ctxt)))))
 (let ((__function__ 'check-function-specifier))
  (declare (ignorable __function__))
  (function-specifier-case
   spec :regular
   (b* ((result (check-expression spec.body ctxt)))
    (type-result-case
         result :err (mv result.info nil)
         :ok
         (if (type-list-equiv result.types (list (type-boolean)))
             (mv nil result.obligations)
           (mv (list :non-boolean-function-specifier-body spec.body)
               nil))))
   :quantified
   (b* ((bound-var-ctxt
             (typed-variables-to-variable-context spec.variables))
        (ctxt (context-add-variables bound-var-ctxt ctxt))
        (result (check-expression spec.matrix ctxt)))
    (type-result-case
     result :err (mv result.info nil)
     :ok
     (if (type-list-equiv result.types (list (type-boolean)))
         (mv nil result.obligations)
       (mv (list :non-boolean-function-specifier-matrix spec.matrix)
           nil))))
   :input-output
   (b* ((io-var-ctxt
             (typed-variables-to-variable-context inputs/outputs))
        (ctxt (context-add-variables io-var-ctxt ctxt))
        (ctxt (change-context ctxt
                              :obligation-vars inputs/outputs))
        (result (check-expression spec.relation ctxt)))
    (type-result-case
     result :err (mv result.info nil)
     :ok
     (if (type-list-equiv result.types (list (type-boolean)))
         (mv nil result.obligations)
      (mv
       (list :non-boolean-function-specifier-relation spec.relation)
       nil)))))))

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

(defthm proof-obligation-listp-of-check-function-specifier.obligs
  (b* (((mv ?err? ?obligs)
        (check-function-specifier spec inputs/outputs ctxt)))
    (proof-obligation-listp obligs))
  :rule-classes :rewrite)

Theorem: check-function-specifier-of-function-specifier-fix-spec

(defthm check-function-specifier-of-function-specifier-fix-spec
  (equal (check-function-specifier (function-specifier-fix spec)
                                   inputs/outputs ctxt)
         (check-function-specifier spec inputs/outputs ctxt)))

Theorem: check-function-specifier-function-specifier-equiv-congruence-on-spec

(defthm
 check-function-specifier-function-specifier-equiv-congruence-on-spec
 (implies
  (function-specifier-equiv spec spec-equiv)
  (equal (check-function-specifier spec inputs/outputs ctxt)
         (check-function-specifier spec-equiv inputs/outputs ctxt)))
 :rule-classes :congruence)

Theorem: check-function-specifier-of-typed-variable-list-fix-inputs/outputs

(defthm
 check-function-specifier-of-typed-variable-list-fix-inputs/outputs
 (equal
  (check-function-specifier spec
                            (typed-variable-list-fix inputs/outputs)
                            ctxt)
  (check-function-specifier spec inputs/outputs ctxt)))

Theorem: check-function-specifier-typed-variable-list-equiv-congruence-on-inputs/outputs

(defthm
 check-function-specifier-typed-variable-list-equiv-congruence-on-inputs/outputs
 (implies
  (typed-variable-list-equiv inputs/outputs inputs/outputs-equiv)
  (equal (check-function-specifier spec inputs/outputs ctxt)
         (check-function-specifier spec inputs/outputs-equiv ctxt)))
 :rule-classes :congruence)

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

(defthm check-function-specifier-of-context-fix-ctxt
 (equal
   (check-function-specifier spec inputs/outputs (context-fix ctxt))
   (check-function-specifier spec inputs/outputs ctxt)))

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

(defthm check-function-specifier-context-equiv-congruence-on-ctxt
 (implies
  (context-equiv ctxt ctxt-equiv)
  (equal (check-function-specifier spec inputs/outputs ctxt)
         (check-function-specifier spec inputs/outputs ctxt-equiv)))
 :rule-classes :congruence)