		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Get-function-in/out/pre/post

Retrieve the inputs, outputs, precondition, and postcondition of a function.

Signature
(get-function-in/out/pre/post name types ctxt) → (mv err? inputs outputs precondition? postcondition?)
Arguments: name — Guard (identifierp name).; types — Guard (type-listp types).; ctxt — Guard (contextp ctxt).
Returns: inputs — Type (typed-variable-listp inputs).; outputs — Type (typed-variable-listp outputs).; precondition? — Type (maybe-expressionp precondition?).; postcondition? — Type (maybe-expressionp postcondition?).

We call a separate ACL2 function to see whether the Syntheto function is a built-in one. If that ACL2 function returns an error, we return it here too. If that ACL2 functions finds the function among the built-in ones, we return the retrieved information. Otherwise, we look for the function in the context.

Definitions and Theorems

Function: get-function-in/out/pre/post

(defun get-function-in/out/pre/post (name types ctxt)
 (declare (xargs :guard (and (identifierp name)
                             (type-listp types)
                             (contextp ctxt))))
 (let ((__function__ 'get-function-in/out/pre/post))
  (declare (ignorable __function__))
  (b*
   (((mv err?
         foundp inputs outputs precond postcond)
     (get-builtin-function-in/out/pre-post name types))
    ((when err?) (mv err? nil nil nil nil))
    ((when foundp)
     (mv nil inputs outputs precond postcond))
    ((when (consp types))
     (mv (list :non-null-types-for-non-builtin-function
               (type-list-fix types))
         nil nil nil nil))
    (fundef? (get-function-definition name (context->tops ctxt)))
    ((when fundef?)
     (b* ((header (function-definition->header fundef?))
          (inputs (function-header->inputs header))
          (outputs (function-header->outputs header))
          (precond (function-definition->precondition fundef?))
          (postcond (function-definition->postcondition fundef?)))
       (mv nil inputs outputs precond postcond)))
    (header?
       (get-function-header-in-list name (context->functions ctxt)))
    ((when header?)
     (b* ((inputs (function-header->inputs header?))
          (outputs (function-header->outputs header?)))
       (mv nil inputs outputs nil nil))))
   (mv (list :function-not-found (identifier-fix name))
       nil nil nil nil))))

Theorem: typed-variable-listp-of-get-function-in/out/pre/post.inputs

(defthm typed-variable-listp-of-get-function-in/out/pre/post.inputs
  (b* (((mv ?err? ?inputs
            ?outputs ?precondition? ?postcondition?)
        (get-function-in/out/pre/post name types ctxt)))
    (typed-variable-listp inputs))
  :rule-classes :rewrite)

Theorem: typed-variable-listp-of-get-function-in/out/pre/post.outputs

(defthm typed-variable-listp-of-get-function-in/out/pre/post.outputs
  (b* (((mv ?err? ?inputs
            ?outputs ?precondition? ?postcondition?)
        (get-function-in/out/pre/post name types ctxt)))
    (typed-variable-listp outputs))
  :rule-classes :rewrite)

Theorem: maybe-expressionp-of-get-function-in/out/pre/post.precondition?

(defthm
    maybe-expressionp-of-get-function-in/out/pre/post.precondition?
  (b* (((mv ?err? ?inputs
            ?outputs ?precondition? ?postcondition?)
        (get-function-in/out/pre/post name types ctxt)))
    (maybe-expressionp precondition?))
  :rule-classes :rewrite)

Theorem: maybe-expressionp-of-get-function-in/out/pre/post.postcondition?

(defthm
   maybe-expressionp-of-get-function-in/out/pre/post.postcondition?
  (b* (((mv ?err? ?inputs
            ?outputs ?precondition? ?postcondition?)
        (get-function-in/out/pre/post name types ctxt)))
    (maybe-expressionp postcondition?))
  :rule-classes :rewrite)

Theorem: true-listp-of-get-function-in/out/pre/post.inputs

(defthm true-listp-of-get-function-in/out/pre/post.inputs
  (b* (((mv ?err? ?inputs
            ?outputs ?precondition? ?postcondition?)
        (get-function-in/out/pre/post name types ctxt)))
    (true-listp inputs))
  :rule-classes :type-prescription)

Theorem: true-listp-of-get-function-in/out/pre/post.outputs

(defthm true-listp-of-get-function-in/out/pre/post.outputs
  (b* (((mv ?err? ?inputs
            ?outputs ?precondition? ?postcondition?)
        (get-function-in/out/pre/post name types ctxt)))
    (true-listp outputs))
  :rule-classes :type-prescription)

Theorem: get-function-in/out/pre/post-of-identifier-fix-name

(defthm get-function-in/out/pre/post-of-identifier-fix-name
  (equal (get-function-in/out/pre/post (identifier-fix name)
                                       types ctxt)
         (get-function-in/out/pre/post name types ctxt)))

Theorem: get-function-in/out/pre/post-identifier-equiv-congruence-on-name

(defthm
   get-function-in/out/pre/post-identifier-equiv-congruence-on-name
  (implies
       (identifier-equiv name name-equiv)
       (equal (get-function-in/out/pre/post name types ctxt)
              (get-function-in/out/pre/post name-equiv types ctxt)))
  :rule-classes :congruence)

Theorem: get-function-in/out/pre/post-of-type-list-fix-types

(defthm get-function-in/out/pre/post-of-type-list-fix-types
  (equal (get-function-in/out/pre/post name (type-list-fix types)
                                       ctxt)
         (get-function-in/out/pre/post name types ctxt)))

Theorem: get-function-in/out/pre/post-type-list-equiv-congruence-on-types

(defthm
   get-function-in/out/pre/post-type-list-equiv-congruence-on-types
  (implies
       (type-list-equiv types types-equiv)
       (equal (get-function-in/out/pre/post name types ctxt)
              (get-function-in/out/pre/post name types-equiv ctxt)))
  :rule-classes :congruence)

Theorem: get-function-in/out/pre/post-of-context-fix-ctxt

(defthm get-function-in/out/pre/post-of-context-fix-ctxt
 (equal (get-function-in/out/pre/post name types (context-fix ctxt))
        (get-function-in/out/pre/post name types ctxt)))

Theorem: get-function-in/out/pre/post-context-equiv-congruence-on-ctxt

(defthm
      get-function-in/out/pre/post-context-equiv-congruence-on-ctxt
  (implies
       (context-equiv ctxt ctxt-equiv)
       (equal (get-function-in/out/pre/post name types ctxt)
              (get-function-in/out/pre/post name types ctxt-equiv)))
  :rule-classes :congruence)