Generate a C expression and theorem from an ACL2 term that represents a unary expression.
(atc-gen-expr-unary fn arg-term arg-expr arg-type arg-events arg-thm in-type out-type op gin state) → (mv erp gout)
The expression and theorem for the argument are generated in the caller, and passed here.
If the operation has an associated
Function:
(defun atc-gen-expr-unary (fn arg-term arg-expr arg-type arg-events arg-thm in-type out-type op 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) (unopp op) (expr-ginp gin)))) (declare (xargs :guard (and (type-nonchar-integerp in-type) (type-nonchar-integerp out-type)))) (let ((__function__ 'atc-gen-expr-unary)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr-gout)) (wrld (w state)) ((expr-gin gin) gin) ((unless (equal arg-type in-type)) (reterr (msg "The unary operator ~x0 is applied ~ to an expression term ~x1 returning ~x2, ~ but a ~x3 operand is expected. ~ This is indicative of provably dead code, ~ given that the code is guard-verified." op arg-term arg-type in-type))) (expr (make-expr-unary :op op :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 (unop-case op :minus) (not (member-eq (type-kind in-type) '(:uint :ulong :ullong))) (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* ((in-type-pred (atc-type-to-recognizer in-type gin.prec-tags)) (valuep-when-in-type-pred (pack 'valuep-when- in-type-pred)) (value-kind-when-in-type-pred (pack 'value-kind-when- in-type-pred)) (op-name (pack (unop-kind op))) (exec-unary-when-op-and-in-type-pred (pack op-name '-value-when- in-type-pred)) (type-pred (atc-type-to-recognizer out-type gin.prec-tags)) (valuep-when-type-pred (pack 'valuep-when- type-pred)) (type-pred-of-fn (pack type-pred '-of- fn))) (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons 'exec-expr-pure-when-unary (cons 'expr-valuep-of-expr-value (cons 'expr-value->value-of-expr-value (cons '(:e expr-kind) (cons '(:e expr-unary->op) (cons '(:e expr-unary->arg) (cons arg-thm (cons valuep-when-in-type-pred (cons value-kind-when-in-type-pred (cons valuep-when-type-pred (cons 'value-fix-when-valuep (cons exec-unary-when-op-and-in-type-pred (cons (cons ':e (cons (pack 'unop- op-name) 'nil)) (cons type-pred-of-fn (and fn-okp (list okp-lemma-name)))))))))))))))) '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-unary.gout (b* (((mv acl2::?erp ?gout) (atc-gen-expr-unary fn arg-term arg-expr arg-type arg-events arg-thm in-type out-type op gin state))) (expr-goutp gout)) :rule-classes :rewrite)