		Search-engine friendly clone of the ACL2 documentation.

Atc-expression-generation

Atc-gen-expr-or

Generate a C expressino from an ACL2 term that represents a logical disjunction.

Signature
(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
Arguments: arg1-term — Guard (pseudo-termp arg1-term).; arg2-term — Guard (pseudo-termp arg2-term).; arg1-expr — Guard (exprp arg1-expr).; arg2-expr — Guard (exprp arg2-expr).; arg1-type — Guard (typep arg1-type).; arg2-type — Guard (typep arg2-type).; arg1-thm — Guard (symbolp arg1-thm).; arg2-thm — Guard (symbolp arg2-thm).; arg1-events — Guard (pseudo-event-form-listp arg1-events).; arg2-events — Guard (pseudo-event-form-listp arg2-events).; gin — Guard (expr-ginp gin).
Returns: gout — Type (expr-goutp 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.

Definitions and Theorems

Function: atc-gen-expr-or

(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: expr-goutp-of-atc-gen-expr-or

(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)