Generate a C expressino from an ACL2 term that represents a logical disjunction.
(atc-gen-expr-or arg1-term arg2-term arg1-expr arg2-expr arg1-type arg2-type arg1-thm arg2-thm arg1-events arg2-events gin state) → gout
This is similar to atc-gen-expr-and, but with a few differences due to the non-complete symmetry between ACL2's and and or. In particular, for the case in which the first argument is true, and thus suffices to determine the result without the second argument, we need some additional rules to resolve certain subgoals that arise.
Function:
(defun atc-gen-expr-or (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-or)) (declare (ignorable __function__)) (b* (((expr-gin gin) gin) (wrld (w state)) (term (cons 'if* (cons arg1-term (cons arg1-term (cons arg2-term 'nil))))) (expr (make-expr-binary :op (binop-logor) :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-logor-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 'test-value-when-sintp (cons 'boolean-from-sint-of-sint-from-boolean (cons 'sintp-of-sint-from-boolean (cons 'sintp-of-sint-from-integer (cons 'boolean-from-sint-of-1 (cons 'if*-of-t-and-t (cons 'sint-from-boolean-when-true-test* (cons 'equal-to-t-when-holds-and-boolean (cons 'booleanp-compound-recognizer (cons 'test*-of-t (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)) (hints-else (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons 'exec-expr-pure-when-binary-logor-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 '(:e expr-binary->arg2) (cons arg2-thm (cons valuep-when-arg2-type-pred (cons 'test-value-when-sintp (cons 'sintp-of-sint-from-boolean (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)) (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 arg1-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 (cons arg2-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-or (b* ((gout (atc-gen-expr-or 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)