Generate a C expression from an ACL2 term that represents a logical conjunction.
(atc-gen-expr-and arg1-term arg2-term arg1-expr arg2-expr arg1-type arg2-type arg1-thm arg2-thm arg1-events arg2-events gin state) → gout
The term returns an ACL2 boolean,
which is equated, in the generated theorem, to test-value.
However, we also need a term to equate to
the execution of the C expression:
we wrap the term with sint-from-boolean for this purpsoe,
obtaining a term that returns a C
Function:
(defun atc-gen-expr-and (arg1-term arg2-term arg1-expr arg2-expr arg1-type arg2-type arg1-thm arg2-thm arg1-events arg2-events gin state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (pseudo-termp arg1-term) (pseudo-termp arg2-term) (exprp arg1-expr) (exprp arg2-expr) (typep arg1-type) (typep arg2-type) (symbolp arg1-thm) (symbolp arg2-thm) (pseudo-event-form-listp arg1-events) (pseudo-event-form-listp arg2-events) (expr-ginp gin)))) (let ((__function__ 'atc-gen-expr-and)) (declare (ignorable __function__)) (b* (((expr-gin gin) gin) (wrld (w state)) (term (cons 'if* (cons arg1-term (cons arg2-term '('nil))))) (expr (make-expr-binary :op (binop-logand) :arg1 arg1-expr :arg2 arg2-expr)) (type (type-sint)) ((when (not gin.proofs)) (make-expr-gout :expr expr :type type :term term :events (append arg1-events arg2-events) :thm-name nil :thm-index gin.thm-index :names-to-avoid gin.names-to-avoid)) (cterm (cons 'sint-from-boolean (cons term 'nil))) (arg1-type-pred (atc-type-to-recognizer arg1-type gin.prec-tags)) (arg2-type-pred (atc-type-to-recognizer arg2-type gin.prec-tags)) (valuep-when-arg1-type-pred (pack 'valuep-when- arg1-type-pred)) (valuep-when-arg2-type-pred (pack 'valuep-when- arg2-type-pred)) (value-kind-when-arg1-type-pred (pack 'value-kind-when- arg1-type-pred)) (value-kind-when-arg2-type-pred (pack 'value-kind-when- arg2-type-pred)) (hints-then (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons 'exec-expr-pure-when-binary-logand-and-true (cons '(:e expr-kind) (cons '(:e expr-binary->op) (cons '(:e binop-kind) (cons '(:e expr-binary->arg1) (cons arg1-thm (cons valuep-when-arg1-type-pred (cons '(:e expr-binary->arg2) (cons arg2-thm (cons valuep-when-arg2-type-pred (cons 'sintp-of-sint-from-boolean (cons 'test-value-when-sintp (cons 'boolean-from-sint-of-sint-from-boolean (cons 'expr-valuep-of-expr-value (cons 'expr-value->value-of-expr-value (cons 'value-fix-when-valuep (cons 'apconvert-expr-value-when-not-value-array (cons value-kind-when-arg1-type-pred (cons value-kind-when-arg2-type-pred 'nil))))))))))))))))))) 'nil)) 'nil))) 'nil)) (hints-else (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons 'exec-expr-pure-when-binary-logand-and-false (cons '(:e expr-kind) (cons '(:e expr-binary->op) (cons '(:e binop-kind) (cons '(:e expr-binary->arg1) (cons arg1-thm (cons valuep-when-arg1-type-pred (cons 'test-value-when-sintp (cons 'sint-from-boolean-when-false (cons 'booleanp-compound-recognizer (cons 'sintp-of-sint-from-integer (cons 'boolean-from-sint-of-0 (cons 'expr-valuep-of-expr-value (cons 'expr-value->value-of-expr-value (cons 'value-fix-when-valuep (cons 'apconvert-expr-value-when-not-value-array (cons value-kind-when-arg1-type-pred 'nil))))))))))))))))) 'nil)) 'nil))) 'nil)) (instructions (cons (cons 'casesplit (cons (atc-contextualize arg1-term gin.context nil nil nil nil nil nil wrld) 'nil)) (cons (cons 'claim (cons (atc-contextualize (cons 'test* (cons arg1-term 'nil)) gin.context nil nil nil nil nil nil wrld) '(:hints (("Goal" :in-theory '(test*)))))) (cons '(drop 1) (cons (cons 'claim (cons (atc-contextualize (cons 'equal (cons term (cons arg2-term 'nil))) gin.context nil nil nil nil nil nil wrld) '(:hints (("Goal" :in-theory '(acl2::if*-when-true test*)))))) (cons (cons 'prove (cons ':hints (cons hints-then 'nil))) (cons (cons 'claim (cons (atc-contextualize (cons 'test* (cons (cons 'not (cons arg1-term 'nil)) 'nil)) gin.context nil nil nil nil nil nil wrld) '(:hints (("Goal" :in-theory '(test*)))))) (cons '(drop 1) (cons (cons 'claim (cons (atc-contextualize (cons 'equal (cons term '(nil))) gin.context nil nil nil nil nil nil wrld) '(:hints (("Goal" :in-theory '(acl2::if*-when-false test*)))))) (cons (cons 'prove (cons ':hints (cons hints-else 'nil))) 'nil)))))))))) ((mv thm-event thm-name thm-index names-to-avoid) (atc-gen-expr-bool-correct-thm gin.fn gin.fn-guard gin.context expr type term cterm acl2::*nil* gin.compst-var nil instructions gin.prec-tags gin.thm-index gin.names-to-avoid state))) (make-expr-gout :expr expr :type type :term term :events (append arg1-events arg2-events (list thm-event)) :thm-name thm-name :thm-index thm-index :names-to-avoid names-to-avoid))))
Theorem:
(defthm expr-goutp-of-atc-gen-expr-and (b* ((gout (atc-gen-expr-and arg1-term arg2-term arg1-expr arg2-expr arg1-type arg2-type arg1-thm arg2-thm arg1-events arg2-events gin state))) (expr-goutp gout)) :rule-classes :rewrite)