Generate a C expression from an ACL2 term that represents an integer conversion.
(atc-gen-expr-conv fn arg-term arg-expr arg-type arg-events arg-thm in-type out-type tyname gin state) → (mv erp gout)
The expression and theorem for the argument are generated in the caller, and passed here.
For now we do not generate the theorem; we will add suppor for that later.
Function:
(defun atc-gen-expr-conv (fn arg-term arg-expr arg-type arg-events arg-thm in-type out-type tyname gin state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (symbolp fn) (pseudo-termp arg-term) (exprp arg-expr) (typep arg-type) (pseudo-event-form-listp arg-events) (symbolp arg-thm) (typep in-type) (typep out-type) (tynamep tyname) (expr-ginp gin)))) (let ((__function__ 'atc-gen-expr-conv)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr-gout)) (wrld (w state)) ((expr-gin gin) gin) ((unless (equal arg-type in-type)) (reterr (msg "The conversion from ~x0 to ~x1 is applied ~ to an expression term ~x2 returning ~x3, ~ which is not the expected type ~x0. ~ This is indicative of provably dead code, ~ given that the code is guard-verified." in-type out-type arg-term arg-type))) (expr (make-expr-cast :type tyname :arg arg-expr)) (term (cons fn (cons arg-term 'nil))) ((when (not gin.proofs)) (retok (make-expr-gout :expr expr :type out-type :term term :events arg-events :thm-name nil :thm-index gin.thm-index :names-to-avoid gin.names-to-avoid))) (fn-okp (and (or (type-case out-type :schar) (and (type-case out-type :sshort) (not (member-eq (type-kind in-type) '(:schar)))) (and (type-case out-type :sint) (not (member-eq (type-kind in-type) '(:schar :sshort)))) (and (type-case out-type :slong) (not (member-eq (type-kind in-type) '(:schar :sshort :sint)))) (and (type-case out-type :sllong) (not (member-eq (type-kind in-type) '(:schar :sshort :sint :slong))))) (pack fn '-okp))) ((mv okp-lemma-event? okp-lemma-name thm-index names-to-avoid) (if fn-okp (b* ((okp-lemma-name (pack gin.fn '-expr- gin.thm-index '-okp-lemma)) ((mv okp-lemma-name names-to-avoid) (fresh-logical-name-with-$s-suffix okp-lemma-name nil gin.names-to-avoid wrld)) (arg-uterm (untranslate$ arg-term nil state)) (okp-lemma-formula (cons fn-okp (cons arg-uterm 'nil))) (okp-lemma-formula (atc-contextualize okp-lemma-formula gin.context gin.fn gin.fn-guard nil nil nil nil wrld)) (okp-lemma-hints (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons gin.fn-guard '(if* test* declar assign)) 'nil)) (cons ':use (cons (cons ':guard-theorem (cons gin.fn 'nil)) 'nil))))) 'nil)) ((mv okp-lemma-event &) (evmac-generate-defthm okp-lemma-name :formula okp-lemma-formula :hints okp-lemma-hints :enable nil))) (mv (list okp-lemma-event) okp-lemma-name (1+ gin.thm-index) names-to-avoid)) (mv nil nil gin.thm-index gin.names-to-avoid))) (hints (b* ((arg-type-pred (atc-type-to-recognizer arg-type gin.prec-tags)) (valuep-when-arg-type-pred (pack 'valuep-when- arg-type-pred)) (exec-cast-of-out-type-when-arg-type-pred (pack 'exec-cast-of- (type-kind out-type) '-when- arg-type-pred)) (type-pred (atc-type-to-recognizer out-type gin.prec-tags)) (type-pred-of-fn (pack type-pred '-of- fn)) (valuep-when-type-pred (pack 'valuep-when- type-pred))) (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons 'exec-expr-pure-when-cast (cons '(:e expr-kind) (cons '(:e expr-cast->type) (cons '(:e expr-cast->arg) (cons arg-thm (cons valuep-when-arg-type-pred (cons exec-cast-of-out-type-when-arg-type-pred (cons type-pred-of-fn (append (and fn-okp (list okp-lemma-name)) (cons 'expr-valuep-of-expr-value (cons 'expr-value->value-of-expr-value (cons 'value-fix-when-valuep (cons valuep-when-type-pred '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 out-type term term acl2::*nil* gin.compst-var hints nil gin.prec-tags thm-index names-to-avoid state))) (retok (make-expr-gout :expr expr :type out-type :term term :events (append arg-events okp-lemma-event? (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-conv.gout (b* (((mv acl2::?erp ?gout) (atc-gen-expr-conv fn arg-term arg-expr arg-type arg-events arg-thm in-type out-type tyname gin state))) (expr-goutp gout)) :rule-classes :rewrite)