		Search-engine friendly clone of the ACL2 documentation.

Simpadd0-event-generation

Simpadd0-expr-binary

Transform a binary expression.

Signature
(simpadd0-expr-binary op arg1 arg1-new arg1-events arg1-thm-name arg1-vartys arg1-diffp arg2 arg2-new arg2-events arg2-thm-name arg2-vartys arg2-diffp info gin) → (mv expr gout)
Arguments: op — Guard (binopp op).; arg1 — Guard (exprp arg1).; arg1-new — Guard (exprp arg1-new).; arg1-events — Guard (pseudo-event-form-listp arg1-events).; arg1-thm-name — Guard (symbolp arg1-thm-name).; arg1-vartys — Guard (ident-type-mapp arg1-vartys).; arg1-diffp — Guard (booleanp arg1-diffp).; arg2 — Guard (exprp arg2).; arg2-new — Guard (exprp arg2-new).; arg2-events — Guard (pseudo-event-form-listp arg2-events).; arg2-thm-name — Guard (symbolp arg2-thm-name).; arg2-vartys — Guard (ident-type-mapp arg2-vartys).; arg2-diffp — Guard (booleanp arg2-diffp).; info — Guard (binary-infop info).; gin — Guard (simpadd0-ginp gin).
Returns: expr — Type (exprp expr).; gout — Type (simpadd0-goutp gout).

The resulting expression is obtained by combining the binary operator with the possibly transformed argument expressions, unless the binary operator is + and the possibly transformed left argument is an int expression and the possibly transformed right argument is an int octal 0 without leading zeros, in which case the resulting expression is just that expression. This is the core of this simple transformation.

We generate a theorem only if theorems were generated for both argument expressions. We generate a theorem for pure strict operators. We plan to add theorem generation for pure strict operators too. We generate a theorem for simple assignment expressions whose left side is a variable of integer type and whose right side is a pure expression of the same integer type.

Definitions and Theorems

Function: simpadd0-expr-binary

(defun simpadd0-expr-binary
       (op arg1 arg1-new arg1-events
           arg1-thm-name arg1-vartys arg1-diffp
           arg2 arg2-new arg2-events arg2-thm-name
           arg2-vartys arg2-diffp info gin)
 (declare (xargs :guard (and (binopp op)
                             (exprp arg1)
                             (exprp arg1-new)
                             (pseudo-event-form-listp arg1-events)
                             (symbolp arg1-thm-name)
                             (ident-type-mapp arg1-vartys)
                             (booleanp arg1-diffp)
                             (exprp arg2)
                             (exprp arg2-new)
                             (pseudo-event-form-listp arg2-events)
                             (symbolp arg2-thm-name)
                             (ident-type-mapp arg2-vartys)
                             (booleanp arg2-diffp)
                             (binary-infop info)
                             (simpadd0-ginp gin))))
 (declare (xargs :guard (and (expr-unambp arg1)
                             (expr-unambp arg1-new)
                             (expr-unambp arg2)
                             (expr-unambp arg2-new))))
 (let ((__function__ 'simpadd0-expr-binary))
  (declare (ignorable __function__))
  (b*
   (((simpadd0-gin gin) gin)
    (expr (make-expr-binary :op op
                            :arg1 arg1
                            :arg2 arg2
                            :info info))
    (simpp (and (binop-case op :add)
                (type-case (expr-type arg1-new) :sint)
                (expr-zerop arg2-new)))
    (expr-new (if simpp (expr-fix arg1-new)
                (make-expr-binary :op op
                                  :arg1 arg1-new
                                  :arg2 arg2-new
                                  :info info)))
    (arg1-vartys (ident-type-map-fix arg1-vartys))
    (arg2-vartys (ident-type-map-fix arg2-vartys))
    ((unless (omap::compatiblep arg1-vartys arg2-vartys))
     (raise
      "Internal error: ~
                incompatible variable-type maps ~x0 and ~x1."
      arg1-vartys arg2-vartys)
     (mv (irr-expr) (irr-simpadd0-gout)))
    (vartys (omap::update* arg1-vartys arg2-vartys))
    (diffp (or arg1-diffp arg2-diffp simpp))
    (gout-no-thm
        (make-simpadd0-gout :events (append arg1-events arg2-events)
                            :thm-name nil
                            :thm-index gin.thm-index
                            :names-to-avoid gin.names-to-avoid
                            :vartys vartys
                            :diffp diffp))
    ((unless (and arg1-thm-name arg2-thm-name))
     (mv expr-new gout-no-thm)))
   (cond
    ((member-eq (binop-kind op)
                '(:mul :div
                       :rem :add
                       :sub :shl
                       :shr :lt
                       :gt :le
                       :ge :eq
                       :ne :bitand
                       :bitxor :bitior))
     (b*
      ((hints
        (cons
         (cons
          '"Goal"
          (cons
           ':in-theory
           (cons
            ''((:e ldm-expr)
               (:e c::iconst-length-none)
               (:e c::iconst-base-oct)
               (:e c::iconst)
               (:e c::const-int)
               (:e c::expr-const)
               (:e c::binop-kind)
               (:e c::binop-add)
               (:e c::binop-purep)
               (:e c::binop-strictp)
               (:e c::expr-binary)
               (:e c::type-nonchar-integerp)
               (:e c::promote-type)
               (:e c::uaconvert-types)
               (:e c::type-sint)
               (:e member-equal))
            (cons
             ':use
             (cons
              (cons
               arg1-thm-name
               (cons
                arg2-thm-name
                (cons
                 (cons
                  ':instance
                  (cons
                   'simpadd0-expr-binary-pure-strict-support-lemma
                   (cons
                    (cons
                      'op
                      (cons (cons 'quote (cons (ldm-binop op) 'nil))
                            'nil))
                    (cons
                     (cons
                      'old-arg1
                      (cons
                       (cons
                        'mv-nth
                        (cons
                         '1
                         (cons
                          (cons 'ldm-expr
                                (cons (cons 'quote (cons arg1 'nil))
                                      'nil))
                          'nil)))
                       'nil))
                     (cons
                      (cons
                       'old-arg2
                       (cons
                        (cons
                         'mv-nth
                         (cons
                          '1
                          (cons
                           (cons
                                'ldm-expr
                                (cons (cons 'quote (cons arg2 'nil))
                                      'nil))
                           'nil)))
                        'nil))
                      (cons
                       (cons
                        'new-arg1
                        (cons
                         (cons
                          'mv-nth
                          (cons
                           '1
                           (cons
                            (cons
                             'ldm-expr
                             (cons
                                  (cons 'quote (cons arg1-new 'nil))
                                  'nil))
                            'nil)))
                         'nil))
                       (cons
                        (cons
                         'new-arg2
                         (cons
                          (cons
                           'mv-nth
                           (cons
                            '1
                            (cons
                             (cons
                              'ldm-expr
                              (cons
                                  (cons 'quote (cons arg2-new 'nil))
                                  'nil))
                             'nil)))
                          'nil))
                        'nil)))))))
                 (cons
                  (cons
                   ':instance
                   (cons
                    'simpadd0-expr-binary-pure-strict-support-lemma-error
                    (cons
                     (cons
                      'op
                      (cons (cons 'quote (cons (ldm-binop op) 'nil))
                            'nil))
                     (cons
                      (cons
                       'arg1
                       (cons
                        (cons
                         'mv-nth
                         (cons
                          '1
                          (cons
                           (cons
                                'ldm-expr
                                (cons (cons 'quote (cons arg1 'nil))
                                      'nil))
                           'nil)))
                        'nil))
                      (cons
                       (cons
                        'arg2
                        (cons
                         (cons
                          'mv-nth
                          (cons
                           '1
                           (cons
                            (cons
                                'ldm-expr
                                (cons (cons 'quote (cons arg2 'nil))
                                      'nil))
                            'nil)))
                         'nil))
                       'nil)))))
                  (and
                   simpp
                   (cons
                    (cons
                     ':instance
                     (cons
                      'simpadd0-expr-binary-support-lemma-simp
                      (cons
                       (cons
                        'expr
                        (cons
                         (cons
                          'mv-nth
                          (cons
                           '1
                           (cons
                            (cons
                             'ldm-expr
                             (cons
                                  (cons 'quote (cons arg1-new 'nil))
                                  'nil))
                            'nil)))
                         'nil))
                       'nil)))
                    'nil))))))
              'nil)))))
         'nil))
       ((mv thm-event thm-name thm-index)
        (simpadd0-gen-expr-pure-thm
             expr expr-new vartys
             gin.const-new gin.thm-index hints)))
      (mv expr-new
          (make-simpadd0-gout
               :events (append arg1-events
                               arg2-events (list thm-event))
               :thm-name thm-name
               :thm-index thm-index
               :names-to-avoid (cons thm-name gin.names-to-avoid)
               :vartys vartys
               :diffp diffp))))
    ((member-eq (binop-kind op)
                '(:logand :logor))
     (mv expr-new gout-no-thm))
    ((eq (binop-kind op) :asg)
     (b*
      (((unless (and (expr-case arg1 :ident)
                     (expr-purep arg2)
                     (equal (expr-type arg1)
                            (expr-type arg2))
                     (type-integerp (expr-type arg1))))
        (mv expr-new gout-no-thm))
       (hints
        (cons
         (cons
          '"Goal"
          (cons
           ':in-theory
           (cons
            ''((:e ldm-expr)
               (:e ldm-ident)
               (:e ident)
               (:e c::expr-kind)
               (:e c::expr-ident)
               (:e c::expr-binary)
               (:e c::binop-asg)
               (:e c::ident)
               (:e c::type-nonchar-integerp)
               c::valuep-of-read-object-of-objdesign-of-var
               c::not-errorp-when-valuep)
            (cons
             ':use
             (cons
              (cons
               arg1-thm-name
               (cons
                arg2-thm-name
                (cons
                 (cons
                  ':instance
                  (cons
                   'simpadd0-expr-binary-asg-support-lemma
                   (cons
                    (cons
                     'old-arg
                     (cons
                      (cons
                       'mv-nth
                       (cons
                        '1
                        (cons
                          (cons 'ldm-expr
                                (cons (cons 'quote (cons arg2 'nil))
                                      'nil))
                          'nil)))
                      'nil))
                    (cons
                     (cons
                      'new-arg
                      (cons
                       (cons
                        'mv-nth
                        (cons
                         '1
                         (cons
                          (cons
                            'ldm-expr
                            (cons (cons 'quote (cons arg2-new 'nil))
                                  'nil))
                          'nil)))
                       'nil))
                     (cons
                      (cons
                       'var
                       (cons
                        (cons
                         'mv-nth
                         (cons
                          '1
                          (cons
                           (cons
                            'ldm-ident
                            (cons
                             (cons
                               'quote
                               (cons (expr-ident->ident arg1) 'nil))
                             'nil))
                           'nil)))
                        'nil))
                      'nil)))))
                 (cons
                  (cons
                   ':instance
                   (cons
                    'simpadd0-expr-binary-asg-support-lemma-error
                    (cons
                     (cons
                      'var
                      (cons
                       (cons
                        'mv-nth
                        (cons
                         '1
                         (cons
                          (cons
                           'ldm-ident
                           (cons
                            (cons
                               'quote
                               (cons (expr-ident->ident arg1) 'nil))
                            'nil))
                          'nil)))
                       'nil))
                     (cons
                      (cons
                       'expr
                       (cons
                        (cons
                         'mv-nth
                         (cons
                          '1
                          (cons
                           (cons
                                'ldm-expr
                                (cons (cons 'quote (cons arg2 'nil))
                                      'nil))
                           'nil)))
                        'nil))
                      '((fenv old-fenv))))))
                  'nil))))
              'nil)))))
         'nil))
       ((mv thm-event thm-name thm-index)
        (simpadd0-gen-expr-asg-thm
             expr expr-new vartys
             gin.const-new gin.thm-index hints)))
      (mv expr-new
          (make-simpadd0-gout
               :events (append arg1-events
                               arg2-events (list thm-event))
               :thm-name thm-name
               :thm-index thm-index
               :names-to-avoid (cons thm-name gin.names-to-avoid)
               :vartys vartys
               :diffp diffp))))
    (t (mv expr-new gout-no-thm))))))

Theorem: exprp-of-simpadd0-expr-binary.expr

(defthm exprp-of-simpadd0-expr-binary.expr
 (b* (((mv ?expr ?gout)
       (simpadd0-expr-binary op arg1 arg1-new arg1-events
                             arg1-thm-name arg1-vartys arg1-diffp
                             arg2 arg2-new arg2-events arg2-thm-name
                             arg2-vartys arg2-diffp info gin)))
   (exprp expr))
 :rule-classes :rewrite)

Theorem: simpadd0-goutp-of-simpadd0-expr-binary.gout

(defthm simpadd0-goutp-of-simpadd0-expr-binary.gout
 (b* (((mv ?expr ?gout)
       (simpadd0-expr-binary op arg1 arg1-new arg1-events
                             arg1-thm-name arg1-vartys arg1-diffp
                             arg2 arg2-new arg2-events arg2-thm-name
                             arg2-vartys arg2-diffp info gin)))
   (simpadd0-goutp gout))
 :rule-classes :rewrite)

Theorem: expr-unamp-of-simpadd0-expr-binary

(defthm expr-unamp-of-simpadd0-expr-binary
 (implies
   (and (expr-unambp arg1-new)
        (expr-unambp arg2-new))
   (b*
     (((mv ?expr ?gout)
       (simpadd0-expr-binary op arg1 arg1-new arg1-events
                             arg1-thm-name arg1-vartys arg1-diffp
                             arg2 arg2-new arg2-events arg2-thm-name
                             arg2-vartys arg2-diffp info gin)))
     (expr-unambp expr))))

Theorem: simpadd0-expr-binary-pure-strict-support-lemma

(defthm simpadd0-expr-binary-pure-strict-support-lemma
 (b* ((old (c::expr-binary op old-arg1 old-arg2))
      (new (c::expr-binary op new-arg1 new-arg2))
      (old-arg1-result (c::exec-expr-pure old-arg1 compst))
      (old-arg2-result (c::exec-expr-pure old-arg2 compst))
      (new-arg1-result (c::exec-expr-pure new-arg1 compst))
      (new-arg2-result (c::exec-expr-pure new-arg2 compst))
      (old-arg1-value (c::expr-value->value old-arg1-result))
      (old-arg2-value (c::expr-value->value old-arg2-result))
      (new-arg1-value (c::expr-value->value new-arg1-result))
      (new-arg2-value (c::expr-value->value new-arg2-result))
      (old-result (c::exec-expr-pure old compst))
      (new-result (c::exec-expr-pure new compst))
      (old-value (c::expr-value->value old-result))
      (new-value (c::expr-value->value new-result))
      (type1 (c::type-of-value old-arg1-value))
      (type2 (c::type-of-value old-arg2-value)))
  (implies (and (c::binop-purep op)
                (c::binop-strictp op)
                (not (c::errorp old-result))
                (not (c::errorp new-arg1-result))
                (not (c::errorp new-arg2-result))
                (equal old-arg1-value new-arg1-value)
                (equal old-arg2-value new-arg2-value)
                (c::type-nonchar-integerp type1)
                (c::type-nonchar-integerp type2))
           (and (not (c::errorp new-result))
                (equal old-value new-value)
                (equal (c::type-of-value old-value)
                       (cond ((member-equal (c::binop-kind op)
                                            '(:mul :div
                                                   :rem :add
                                                   :sub :bitand
                                                   :bitxor :bitior))
                              (c::uaconvert-types type1 type2))
                             ((member-equal (c::binop-kind op)
                                            '(:shl :shr))
                              (c::promote-type type1))
                             (t (c::type-sint))))))))

Theorem: simpadd0-expr-binary-pure-strict-support-lemma-error

(defthm simpadd0-expr-binary-pure-strict-support-lemma-error
  (implies
       (and (c::binop-strictp op)
            (or (c::errorp (c::exec-expr-pure arg1 compst))
                (c::errorp (c::exec-expr-pure arg2 compst))))
       (c::errorp (c::exec-expr-pure (c::expr-binary op arg1 arg2)
                                     compst))))

Theorem: simpadd0-expr-binary-support-lemma-simp

(defthm simpadd0-expr-binary-support-lemma-simp
 (b*
  ((zero
       (c::expr-const
            (c::const-int
                 (c::make-iconst :value 0
                                 :base (c::iconst-base-oct)
                                 :unsignedp nil
                                 :length (c::iconst-length-none)))))
   (expr+zero (c::expr-binary (c::binop-add)
                              expr zero))
   (expr-result (c::exec-expr-pure expr compst))
   (expr-value (c::expr-value->value expr-result))
   (expr+zero-result (c::exec-expr-pure expr+zero compst))
   (expr+zero-value (c::expr-value->value expr+zero-result)))
  (implies (and (not (c::errorp expr-result))
                (equal (c::type-of-value expr-value)
                       (c::type-sint)))
           (equal expr+zero-value expr-value))))

Theorem: simpadd0-expr-binary-asg-support-lemma

(defthm simpadd0-expr-binary-asg-support-lemma
  (b* ((old (c::expr-binary (c::binop-asg)
                            (c::expr-ident var)
                            old-arg))
       (new (c::expr-binary (c::binop-asg)
                            (c::expr-ident var)
                            new-arg))
       (old-arg-result (c::exec-expr-pure old-arg compst))
       (new-arg-result (c::exec-expr-pure new-arg compst))
       (old-arg-value (c::expr-value->value old-arg-result))
       (new-arg-value (c::expr-value->value new-arg-result))
       (old-compst (c::exec-expr-asg old compst old-fenv limit))
       (new-compst (c::exec-expr-asg new compst new-fenv limit))
       (val (c::read-object (c::objdesign-of-var var compst)
                            compst))
       (type (c::type-of-value val)))
    (implies (and (not (equal (c::expr-kind old-arg) :call))
                  (not (equal (c::expr-kind new-arg) :call))
                  (not (c::errorp val))
                  (c::type-nonchar-integerp type)
                  (not (c::errorp old-compst))
                  (not (c::errorp new-arg-result))
                  (equal old-arg-value new-arg-value)
                  (equal (c::type-of-value old-arg-value)
                         type))
             (and (not (c::errorp new-compst))
                  (equal old-compst new-compst)))))

Theorem: simpadd0-expr-binary-asg-support-lemma-error

(defthm simpadd0-expr-binary-asg-support-lemma-error
 (implies
    (and (not (equal (c::expr-kind expr) :call))
         (or (c::errorp (c::exec-expr-pure (c::expr-ident var)
                                           compst))
             (c::errorp (c::exec-expr-pure expr compst))))
    (c::errorp (c::exec-expr-asg (c::expr-binary (c::binop-asg)
                                                 (c::expr-ident var)
                                                 expr)
                                 compst fenv limit))))