Generate a C expression and theorem from an ACL2 term that represents a binary expression.
(atc-gen-expr-binary fn arg1-term arg2-term arg1-expr arg2-expr arg1-type arg2-type arg1-events arg2-events arg1-thm arg2-thm in-type1 in-type2 out-type op gin state) → (mv erp gout)
The expressions and theorems for the arguments are generated in the caller, and passed here.
We do not yet support operations with an associated
Function:
(defun atc-gen-expr-binary (fn arg1-term arg2-term arg1-expr arg2-expr arg1-type arg2-type arg1-events arg2-events arg1-thm arg2-thm in-type1 in-type2 out-type op gin state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (symbolp fn) (pseudo-termp arg1-term) (pseudo-termp arg2-term) (exprp arg1-expr) (exprp arg2-expr) (typep arg1-type) (typep arg2-type) (pseudo-event-form-listp arg1-events) (pseudo-event-form-listp arg2-events) (symbolp arg1-thm) (symbolp arg2-thm) (typep in-type1) (typep in-type2) (typep out-type) (binopp op) (expr-ginp gin)))) (declare (xargs :guard (and (type-nonchar-integerp in-type1) (type-nonchar-integerp in-type2) (type-nonchar-integerp out-type)))) (let ((__function__ 'atc-gen-expr-binary)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr-gout)) (wrld (w state)) ((expr-gin gin) gin) ((unless (and (equal arg1-type in-type1) (equal arg2-type in-type2))) (reterr (msg "The binary operator ~x0 is applied ~ to an expression term ~x1 returning ~x2 ~ and to an expression term ~x3 returning ~x4, ~ but a ~x5 operand and a ~x6 operand are expected. ~ This is indicative of provably dead code, ~ given that the code is guard-verified." op arg1-term arg1-type arg2-term arg2-type in-type1 in-type2))) (expr (make-expr-binary :op op :arg1 arg1-expr :arg2 arg2-expr)) ((when (eq fn 'quote)) (reterr (raise "Internal error: function symbol is QUOTE."))) (term (cons fn (cons arg1-term (cons arg2-term 'nil)))) ((when (not gin.proofs)) (retok (make-expr-gout :expr expr :type out-type :term term :events (append arg1-events arg2-events) :thm-name nil :thm-index gin.thm-index :names-to-avoid gin.names-to-avoid))) (op-name (pack (binop-kind op))) (fn-okp (and (or (member-eq (binop-kind op) '(:div :rem :shl :shr)) (and (member-eq (binop-kind op) '(:add :sub :mul)) (type-signed-integerp out-type))) (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)) (arg1-uterm (untranslate$ arg1-term nil state)) (arg2-uterm (untranslate$ arg2-term nil state)) (okp-lemma-formula (cons fn-okp (cons arg1-uterm (cons arg2-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* ((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)) (exec-binary-strict-pure-when-op (pack 'exec-binary-strict-pure-when- op-name)) (type-pred (atc-type-to-recognizer out-type gin.prec-tags)) (arg1-fixtype (integer-type-to-fixtype arg1-type)) (arg2-fixtype (integer-type-to-fixtype arg2-type)) (op-values-when-arg1-type (pack op-name '-values-when- arg1-fixtype)) (op-arg1-type-and-value-when-arg2-type (pack op-name '- arg1-fixtype '-and-value-when- arg2-fixtype)) (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-strict-pure-binary (cons '(:e expr-kind) (cons '(:e expr-binary->op) (cons '(:e expr-binary->arg1) (cons '(:e expr-binary->arg2) (cons '(:e binop-kind) (cons '(:e member-equal) (cons arg1-thm (cons arg2-thm (cons valuep-when-arg1-type-pred (cons valuep-when-arg2-type-pred (cons exec-binary-strict-pure-when-op (cons (cons ':e (cons (pack 'binop- op-name) 'nil)) (cons op-values-when-arg1-type (cons op-arg1-type-and-value-when-arg2-type (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 (cons value-kind-when-arg1-type-pred (cons value-kind-when-arg2-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 arg1-events arg2-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-binary.gout (b* (((mv acl2::?erp ?gout) (atc-gen-expr-binary fn arg1-term arg2-term arg1-expr arg2-expr arg1-type arg2-type arg1-events arg2-events arg1-thm arg2-thm in-type1 in-type2 out-type op gin state))) (expr-goutp gout)) :rule-classes :rewrite)