		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Fun-table-add-fun

Add static information about a function to a function table.

Signature
(fun-table-add-fun fun inputs output definedp funtab) → new-funtab
Arguments: fun — Guard (identp fun).; inputs — Guard (type-listp inputs).; output — Guard (typep output).; definedp — Guard (booleanp definedp).; funtab — Guard (fun-tablep funtab).
Returns: new-funtab — Type (fun-table-resultp new-funtab).

This is called when processing a function declaration or a function definition. Besides the name and the (input and output) types of the function, we pass a flag saying whether we are processing a function declaration or a function definition. If there is no entry in the table for the function, we add the information about the function. If there is already an entry, it must have the same input and output types [C17:6.7/4] (in our C subset, compatible types means equal types); otherwise it is an error. If the information in the table has the definedp flag nil, it means that we have not encountered a definition yet; if it is t, we have encountered it already. Thus, it is an error if the definedp flag in the table and the definedp parameter of this ACL2 function are both t, because it means that there are two definitions. For the other three combinations of the flags there is no error, but if the flag in the table is nil while the parameter of this ACL2 function is t, then we update the flag in the table, because now the function is defined.

Definitions and Theorems

Function: fun-table-add-fun

(defun fun-table-add-fun (fun inputs output definedp funtab)
  (declare (xargs :guard (and (identp fun)
                              (type-listp inputs)
                              (typep output)
                              (booleanp definedp)
                              (fun-tablep funtab))))
  (let ((__function__ 'fun-table-add-fun))
    (declare (ignorable __function__))
    (b* ((fun (ident-fix fun))
         (funtab (fun-table-fix funtab))
         (info (fun-table-lookup fun funtab))
         ((when (not info))
          (omap::update fun
                        (make-fun-sinfo :inputs inputs
                                        :output output
                                        :definedp definedp)
                        funtab))
         ((unless (and (type-list-equiv (fun-sinfo->inputs info)
                                        inputs)
                       (type-equiv (fun-sinfo->output info)
                                   output)))
          (reserrf (list :fun-type-mismatch
                         :old-inputs (fun-sinfo->inputs info)
                         :new-inputs (type-list-fix inputs)
                         :old-output (fun-sinfo->output info)
                         :new-output (type-fix output))))
         (already-definedp (fun-sinfo->definedp info))
         ((when (and already-definedp definedp))
          (reserrf (list :fun-redefinition fun)))
         ((when (and (not already-definedp) definedp))
          (omap::update fun (change-fun-sinfo info :definedp t)
                        funtab)))
      funtab)))

Theorem: fun-table-resultp-of-fun-table-add-fun

(defthm fun-table-resultp-of-fun-table-add-fun
  (b* ((new-funtab
            (fun-table-add-fun fun inputs output definedp funtab)))
    (fun-table-resultp new-funtab))
  :rule-classes :rewrite)

Theorem: fun-table-add-fun-of-ident-fix-fun

(defthm fun-table-add-fun-of-ident-fix-fun
  (equal (fun-table-add-fun (ident-fix fun)
                            inputs output definedp funtab)
         (fun-table-add-fun fun inputs output definedp funtab)))

Theorem: fun-table-add-fun-ident-equiv-congruence-on-fun

(defthm fun-table-add-fun-ident-equiv-congruence-on-fun
  (implies
       (ident-equiv fun fun-equiv)
       (equal (fun-table-add-fun fun inputs output definedp funtab)
              (fun-table-add-fun fun-equiv
                                 inputs output definedp funtab)))
  :rule-classes :congruence)

Theorem: fun-table-add-fun-of-type-list-fix-inputs

(defthm fun-table-add-fun-of-type-list-fix-inputs
  (equal (fun-table-add-fun fun (type-list-fix inputs)
                            output definedp funtab)
         (fun-table-add-fun fun inputs output definedp funtab)))

Theorem: fun-table-add-fun-type-list-equiv-congruence-on-inputs

(defthm fun-table-add-fun-type-list-equiv-congruence-on-inputs
 (implies
    (type-list-equiv inputs inputs-equiv)
    (equal (fun-table-add-fun fun inputs output definedp funtab)
           (fun-table-add-fun fun
                              inputs-equiv output definedp funtab)))
 :rule-classes :congruence)

Theorem: fun-table-add-fun-of-type-fix-output

(defthm fun-table-add-fun-of-type-fix-output
  (equal (fun-table-add-fun fun inputs (type-fix output)
                            definedp funtab)
         (fun-table-add-fun fun inputs output definedp funtab)))

Theorem: fun-table-add-fun-type-equiv-congruence-on-output

(defthm fun-table-add-fun-type-equiv-congruence-on-output
 (implies
    (type-equiv output output-equiv)
    (equal (fun-table-add-fun fun inputs output definedp funtab)
           (fun-table-add-fun fun
                              inputs output-equiv definedp funtab)))
 :rule-classes :congruence)

Theorem: fun-table-add-fun-of-bool-fix-definedp

(defthm fun-table-add-fun-of-bool-fix-definedp
  (equal (fun-table-add-fun fun
                            inputs output (acl2::bool-fix definedp)
                            funtab)
         (fun-table-add-fun fun inputs output definedp funtab)))

Theorem: fun-table-add-fun-iff-congruence-on-definedp

(defthm fun-table-add-fun-iff-congruence-on-definedp
 (implies
    (iff definedp definedp-equiv)
    (equal (fun-table-add-fun fun inputs output definedp funtab)
           (fun-table-add-fun fun
                              inputs output definedp-equiv funtab)))
 :rule-classes :congruence)

Theorem: fun-table-add-fun-of-fun-table-fix-funtab

(defthm fun-table-add-fun-of-fun-table-fix-funtab
  (equal (fun-table-add-fun fun inputs
                            output definedp (fun-table-fix funtab))
         (fun-table-add-fun fun inputs output definedp funtab)))

Theorem: fun-table-add-fun-fun-table-equiv-congruence-on-funtab

(defthm fun-table-add-fun-fun-table-equiv-congruence-on-funtab
 (implies
    (fun-table-equiv funtab funtab-equiv)
    (equal (fun-table-add-fun fun inputs output definedp funtab)
           (fun-table-add-fun fun
                              inputs output definedp funtab-equiv)))
 :rule-classes :congruence)