Retrieve the inputs, outputs, precondition, and postcondition of a function.
(get-function-in/out/pre/post name types ctxt) → (mv err? inputs outputs precondition? 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.
Function:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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)