Generate a C expression and theorem from an ACL2 term that represents an integer constant expression.
(atc-gen-expr-const term const type type-base-const gin state) → gout
The C integer constant is actually calculated by the caller, and passed as input here.
The theorem says that the execution yields the term. It also says that the term satisfies the applicable shallowly embedded type predicate.
This theorem holds unconditionally; it does not actually depend on the computation state. We do not need to contextualize the theorem, i.e. we ignore the atc-context.
The hints cover all possible integer constants, but we could make them more nuanced to the specifics of the constant.
Function:
(defun atc-gen-expr-const (term const type type-base-const gin state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (pseudo-termp term) (iconstp const) (typep type) (symbolp type-base-const) (expr-ginp gin)))) (declare (xargs :guard (type-nonchar-integerp type))) (let ((__function__ 'atc-gen-expr-const)) (declare (ignorable __function__)) (b* (((expr-gin gin) gin) (expr (expr-const (const-int const))) ((when (not gin.proofs)) (make-expr-gout :expr expr :type type :term term :events nil :thm-name nil :thm-index gin.thm-index :names-to-avoid gin.names-to-avoid)) (hints (b* ((fixtype (integer-type-to-fixtype type)) (exec-const-to-fixtype (pack 'exec-const-to- fixtype)) (fixtype-integerp (pack fixtype '-integerp)) (recognizer (atc-type-to-recognizer type gin.prec-tags)) (valuep-when-recognizer (pack 'valuep-when- recognizer)) (recognizer-of-fixtype-from-integer (pack recognizer '-of- fixtype '-from-integer))) (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons 'exec-expr-pure-when-const (cons '(:e expr-kind) (cons '(:e expr-const->get) (cons exec-const-to-fixtype (cons '(:e const-kind) (cons '(:e const-int->get) (cons '(:e iconst->unsignedp) (cons '(:e iconst->length) (cons '(:e iconst->value) (cons '(:e iconst->base) (cons '(:e iconst-length-kind) (cons '(:e iconst-base-kind) (cons (cons ':e (cons fixtype-integerp 'nil)) (cons type-base-const (cons recognizer-of-fixtype-from-integer (cons 'expr-valuep-of-expr-value (cons 'expr-value->value-of-expr-value (cons 'value-fix-when-valuep (cons valuep-when-recognizer 'nil))))))))))))))))))) 'nil)) 'nil))) 'nil))) ((mv thm-event thm-name thm-index names-to-avoid) (atc-gen-expr-pure-correct-thm gin.fn gin.fn-guard gin.context expr type term term acl2::*nil* gin.compst-var hints nil gin.prec-tags gin.thm-index gin.names-to-avoid state))) (make-expr-gout :expr expr :type type :term term :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-const (b* ((gout (atc-gen-expr-const term const type type-base-const gin state))) (expr-goutp gout)) :rule-classes :rewrite)