		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Check-function-specification

Check if a function specification is statically well-formed.

Signature
(check-function-specification spec ctxt) → (mv err? obligs)
Arguments: spec — Guard (function-specificationp spec).; ctxt — Guard (contextp ctxt).
Returns: obligs — Type (proof-obligation-listp obligs).

This is at the top level, so the context has no type names, function headers, variables, and hypotheses.

We ensure that the name is not already used by an existing function specification.

We check all the headers, and augment the context with them. We ensure there is at least one header.

If the specifier is an input/output one, we ensure that there is exactly one header, and we pass its inputs and outputs to the ACL2 function that checks the specifier.

Definitions and Theorems

Function: check-function-specification

(defun check-function-specification (spec ctxt)
 (declare (xargs :guard (and (function-specificationp spec)
                             (contextp ctxt))))
 (declare
      (xargs :guard (and (null (context->types ctxt))
                         (null (context->functions ctxt))
                         (omap::emptyp (context->variables ctxt))
                         (null (context->obligation-vars ctxt))
                         (null (context->obligation-hyps ctxt)))))
 (let ((__function__ 'check-function-specification))
  (declare (ignorable __function__))
  (b*
   (((function-specification spec) spec)
    ((when (get-function-definition spec.name (context->tops ctxt)))
     (mv (list :function-specification-already-defined spec.name)
         nil))
    (names (function-header-list->name-list spec.functions))
    ((unless (consp names))
     (mv (list :no-function-headers-in-specification spec.name)
         nil))
    ((unless (no-duplicatesp-equal names))
     (mv (list :duplicate-functions-in-specification names)
         nil))
    (ctxt (change-context ctxt
                          :functions spec.functions)))
   (if
    (function-specifier-case spec.specifier :input-output)
    (if
     (= (len spec.functions) 1)
     (b*
      ((header (car spec.functions))
       (inputs/outputs (append (function-header->inputs header)
                               (function-header->outputs header))))
      (check-function-specifier spec.specifier inputs/outputs ctxt))
     (mv (list :input-output-specifier-multi-functions names)
         nil))
    (check-function-specifier spec.specifier nil ctxt)))))

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

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

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

(defthm
    check-function-specification-of-function-specification-fix-spec
 (equal
     (check-function-specification (function-specification-fix spec)
                                   ctxt)
     (check-function-specification spec ctxt)))

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

(defthm
 check-function-specification-function-specification-equiv-congruence-on-spec
 (implies (function-specification-equiv spec spec-equiv)
          (equal (check-function-specification spec ctxt)
                 (check-function-specification spec-equiv ctxt)))
 :rule-classes :congruence)

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

(defthm check-function-specification-of-context-fix-ctxt
  (equal (check-function-specification spec (context-fix ctxt))
         (check-function-specification spec ctxt)))

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

(defthm
      check-function-specification-context-equiv-congruence-on-ctxt
  (implies (context-equiv ctxt ctxt-equiv)
           (equal (check-function-specification spec ctxt)
                  (check-function-specification spec ctxt-equiv)))
  :rule-classes :congruence)