Retrieve the inputs, outputs, precondition, and postcondition of a built-in function.
(get-builtin-function-in/out/pre-post name types) → (mv err? foundp inputs outputs precondition? postcondition?)
This ACL2 function implicitly defines the inputs, outputs, preconditions, and postoconditions of the built-in functions. At this time, there is no other explicit representation of them in the Syntheto abstract syntax of top-level constructs.
The current built-in functions are polymorphic.
The
The names of the currently supported built-in functions are in *builtin-function-names*.
Function:
(defun get-builtin-function-in/out/pre-post (name types) (declare (xargs :guard (and (identifierp name) (type-listp types)))) (let ((__function__ 'get-builtin-function-in/out/pre-post)) (declare (ignorable __function__)) (cond ((identifier-equiv name (identifier "empty")) (b* (((unless (= (len types) 1)) (mv (list :builtin-wrong-types (identifier-fix name) (type-list-fix types)) nil nil nil nil nil)) (type (car types))) (cond ((type-case type :sequence) (mv nil t nil (list (make-typed-variable :name (identifier "x") :type type)) nil nil)) ((type-case type :set) (mv nil t nil (list (make-typed-variable :name (identifier "x") :type type)) nil nil)) (t (mv (list :builtin-wrong-type (identifier-fix name) (type-fix type)) nil nil nil nil nil))))) ((identifier-equiv name (identifier "add")) (b* (((unless (= (len types) 1)) (mv (list :builtin-wrong-types (identifier-fix name) (type-list-fix types)) nil nil nil nil nil)) (type (car types))) (cond ((type-case type :sequence) (mv nil t (list (make-typed-variable :name (identifier "x") :type (type-sequence->element type)) (make-typed-variable :name (identifier "y") :type type)) (list (make-typed-variable :name (identifier "xy") :type type)) nil nil)) ((type-case type :set) (mv nil t (list (make-typed-variable :name (identifier "x") :type (type-set->element type)) (make-typed-variable :name (identifier "y") :type type)) (list (make-typed-variable :name (identifier "xy") :type type)) nil nil)) (t (mv (list :builtin-wrong-type (identifier-fix name) (type-fix type)) nil nil nil nil nil))))) ((identifier-equiv name (identifier "append")) (b* (((unless (= (len types) 1)) (mv (list :builtin-wrong-types (identifier-fix name) (type-list-fix types)) nil nil nil nil nil)) (type (car types))) (cond ((type-case type :sequence) (mv nil t (list (make-typed-variable :name (identifier "x") :type type) (make-typed-variable :name (identifier "y") :type type)) (list (make-typed-variable :name (identifier "xy") :type type)) nil nil)) (t (mv (list :builtin-wrong-type (identifier-fix name) (type-fix type)) nil nil nil nil nil))))) ((identifier-equiv name (identifier "length")) (b* (((unless (= (len types) 1)) (mv (list :builtin-wrong-types (identifier-fix name) (type-list-fix types)) nil nil nil nil nil)) (type (car types))) (cond ((type-case type :sequence) (mv nil t (list (make-typed-variable :name (identifier "x") :type type)) (list (make-typed-variable :name (identifier "b") :type (type-integer))) nil nil)) ((type-case type :set) (mv nil t (list (make-typed-variable :name (identifier "x") :type type)) (list (make-typed-variable :name (identifier "b") :type (type-integer))) nil nil)) (t (mv (list :builtin-wrong-type (identifier-fix name) (type-fix type)) nil nil nil nil nil))))) ((identifier-equiv name (identifier "is_empty")) (b* (((unless (= (len types) 1)) (mv (list :builtin-wrong-types (identifier-fix name) (type-list-fix types)) nil nil nil nil nil)) (type (car types))) (cond ((type-case type :sequence) (mv nil t (list (make-typed-variable :name (identifier "x") :type type)) (list (make-typed-variable :name (identifier "b") :type (type-boolean))) nil nil)) ((type-case type :set) (mv nil t (list (make-typed-variable :name (identifier "x") :type type)) (list (make-typed-variable :name (identifier "b") :type (type-boolean))) nil nil)) (t (mv (list :builtin-wrong-type (identifier-fix name) (type-fix type)) nil nil nil nil nil))))) ((identifier-equiv name (identifier "first")) (b* (((unless (= (len types) 1)) (mv (list :builtin-wrong-types (identifier-fix name) (type-list-fix types)) nil nil nil nil nil)) (type (car types))) (cond ((type-case type :sequence) (mv nil t (list (make-typed-variable :name (identifier "x") :type type)) (list (make-typed-variable :name (identifier "y") :type (type-sequence->element type))) (make-expression-unary :operator (unary-op-not) :operand (make-expression-call :function (identifier "is_empty") :types (list type) :arguments (list (make-expression-variable :name (identifier "x"))))) nil)) ((type-case type :set) (mv nil t (list (make-typed-variable :name (identifier "x") :type type)) (list (make-typed-variable :name (identifier "y") :type (type-set->element type))) (make-expression-unary :operator (unary-op-not) :operand (make-expression-call :function (identifier "is_empty") :types (list type) :arguments (list (make-expression-variable :name (identifier "x"))))) nil)) (t (mv (list :builtin-wrong-type (identifier-fix name) (type-fix type)) nil nil nil nil nil))))) ((identifier-equiv name (identifier "last")) (b* (((unless (= (len types) 1)) (mv (list :builtin-wrong-types (identifier-fix name) (type-list-fix types)) nil nil nil nil nil)) (type (car types))) (cond ((type-case type :sequence) (mv nil t (list (make-typed-variable :name (identifier "x") :type type)) (list (make-typed-variable :name (identifier "y") :type (type-sequence->element type))) (make-expression-unary :operator (unary-op-not) :operand (make-expression-call :function (identifier "is_empty") :types (list type) :arguments (list (make-expression-variable :name (identifier "x"))))) nil)) (t (mv (list :builtin-wrong-type (identifier-fix name) (type-fix type)) nil nil nil nil nil))))) ((identifier-equiv name (identifier "rest")) (b* (((unless (= (len types) 1)) (mv (list :builtin-wrong-types (identifier-fix name) (type-list-fix types)) nil nil nil nil nil)) (type (car types))) (cond ((type-case type :sequence) (mv nil t (list (make-typed-variable :name (identifier "x") :type type)) (list (make-typed-variable :name (identifier "y") :type type)) (make-expression-unary :operator (unary-op-not) :operand (make-expression-call :function (identifier "is_empty") :types (list type) :arguments (list (make-expression-variable :name (identifier "x"))))) nil)) ((type-case type :set) (mv nil t (list (make-typed-variable :name (identifier "x") :type type)) (list (make-typed-variable :name (identifier "y") :type type)) (make-expression-unary :operator (unary-op-not) :operand (make-expression-call :function (identifier "is_empty") :types (list type) :arguments (list (make-expression-variable :name (identifier "x"))))) nil)) (t (mv (list :builtin-wrong-type (identifier-fix name) (type-fix type)) nil nil nil nil nil))))) ((identifier-equiv name (identifier "member")) (b* (((unless (= (len types) 1)) (mv (list :builtin-wrong-types (identifier-fix name) (type-list-fix types)) nil nil nil nil nil)) (type (car types))) (cond ((type-case type :sequence) (mv nil t (list (make-typed-variable :name (identifier "x") :type (type-sequence->element type)) (make-typed-variable :name (identifier "y") :type type)) (list (make-typed-variable :name (identifier "b") :type (type-boolean))) nil nil)) ((type-case type :set) (mv nil t (list (make-typed-variable :name (identifier "x") :type (type-set->element type)) (make-typed-variable :name (identifier "y") :type type)) (list (make-typed-variable :name (identifier "b") :type (type-boolean))) nil nil)) (t (mv (list :builtin-wrong-type (identifier-fix name) (type-fix type)) nil nil nil nil nil))))) ((identifier-equiv name (identifier "remove_first")) (b* (((unless (= (len types) 1)) (mv (list :builtin-wrong-types (identifier-fix name) (type-list-fix types)) nil nil nil nil nil)) (type (car types))) (cond ((type-case type :sequence) (mv nil t (list (make-typed-variable :name (identifier "x") :type (type-sequence->element type)) (make-typed-variable :name (identifier "y") :type type)) (list (make-typed-variable :name (identifier "z") :type type)) nil nil)) ((type-case type :set) (mv nil t (list (make-typed-variable :name (identifier "x") :type (type-set->element type)) (make-typed-variable :name (identifier "y") :type type)) (list (make-typed-variable :name (identifier "z") :type type)) nil nil)) (t (mv (list :builtin-wrong-type (identifier-fix name) (type-fix type)) nil nil nil nil nil))))) (t (mv nil nil nil nil nil nil)))))
Theorem:
(defthm booleanp-of-get-builtin-function-in/out/pre-post.foundp (b* (((mv ?err? ?foundp ?inputs ?outputs ?precondition? ?postcondition?) (get-builtin-function-in/out/pre-post name types))) (booleanp foundp)) :rule-classes :rewrite)
Theorem:
(defthm typed-variable-listp-of-get-builtin-function-in/out/pre-post.inputs (b* (((mv ?err? ?foundp ?inputs ?outputs ?precondition? ?postcondition?) (get-builtin-function-in/out/pre-post name types))) (typed-variable-listp inputs)) :rule-classes :rewrite)
Theorem:
(defthm typed-variable-listp-of-get-builtin-function-in/out/pre-post.outputs (b* (((mv ?err? ?foundp ?inputs ?outputs ?precondition? ?postcondition?) (get-builtin-function-in/out/pre-post name types))) (typed-variable-listp outputs)) :rule-classes :rewrite)
Theorem:
(defthm maybe-expressionp-of-get-builtin-function-in/out/pre-post.precondition? (b* (((mv ?err? ?foundp ?inputs ?outputs ?precondition? ?postcondition?) (get-builtin-function-in/out/pre-post name types))) (maybe-expressionp precondition?)) :rule-classes :rewrite)
Theorem:
(defthm maybe-expressionp-of-get-builtin-function-in/out/pre-post.postcondition? (b* (((mv ?err? ?foundp ?inputs ?outputs ?precondition? ?postcondition?) (get-builtin-function-in/out/pre-post name types))) (maybe-expressionp postcondition?)) :rule-classes :rewrite)
Theorem:
(defthm get-builtin-function-in/out/pre-post-of-identifier-fix-name (equal (get-builtin-function-in/out/pre-post (identifier-fix name) types) (get-builtin-function-in/out/pre-post name types)))
Theorem:
(defthm get-builtin-function-in/out/pre-post-identifier-equiv-congruence-on-name (implies (identifier-equiv name name-equiv) (equal (get-builtin-function-in/out/pre-post name types) (get-builtin-function-in/out/pre-post name-equiv types))) :rule-classes :congruence)
Theorem:
(defthm get-builtin-function-in/out/pre-post-of-type-list-fix-types (equal (get-builtin-function-in/out/pre-post name (type-list-fix types)) (get-builtin-function-in/out/pre-post name types)))
Theorem:
(defthm get-builtin-function-in/out/pre-post-type-list-equiv-congruence-on-types (implies (type-list-equiv types types-equiv) (equal (get-builtin-function-in/out/pre-post name types) (get-builtin-function-in/out/pre-post name types-equiv))) :rule-classes :congruence)