		Search-engine friendly clone of the ACL2 documentation.

Simpadd0-event-generation

Simpadd0-stmt-expr

Transform an expression statement.

Signature
(simpadd0-stmt-expr expr? expr?-new expr?-events expr?-thm-name expr?-vartys expr?-diffp gin) → (mv stmt gout)
Arguments: expr? — Guard (expr-optionp expr?).; expr?-new — Guard (expr-optionp expr?-new).; expr?-events — Guard (pseudo-event-form-listp expr?-events).; expr?-thm-name — Guard (symbolp expr?-thm-name).; expr?-vartys — Guard (ident-type-mapp expr?-vartys).; expr?-diffp — Guard (booleanp expr?-diffp).; gin — Guard (simpadd0-ginp gin).
Returns: stmt — Type (stmtp stmt).; gout — Type (simpadd0-goutp gout).

We put the optional expression into an expression statement.

We generate a theorem if there is no expression or if there is an assignment expression for which a theorem was generated. When instantiating the theorem for the assignment expression, we use :extra-bindings-ok because that theorem may be a dummy t (see simpadd0-gen-expr-asg-thm).

Definitions and Theorems

Function: simpadd0-stmt-expr

(defun simpadd0-stmt-expr
       (expr? expr?-new expr?-events expr?-thm-name
              expr?-vartys expr?-diffp gin)
 (declare (xargs :guard (and (expr-optionp expr?)
                             (expr-optionp expr?-new)
                             (pseudo-event-form-listp expr?-events)
                             (symbolp expr?-thm-name)
                             (ident-type-mapp expr?-vartys)
                             (booleanp expr?-diffp)
                             (simpadd0-ginp gin))))
 (declare (xargs :guard (and (expr-option-unambp expr?)
                             (expr-option-unambp expr?-new)
                             (iff expr? expr?-new))))
 (let ((__function__ 'simpadd0-stmt-expr))
  (declare (ignorable __function__))
  (b*
   (((simpadd0-gin gin) gin)
    (stmt (stmt-expr expr?))
    (stmt-new (stmt-expr expr?-new))
    ((unless (iff expr? expr?-new))
     (raise
      "Internal error: ~
                return statement with optional expression ~x0 ~
                is transformed into ~
                return statement with optional expression ~x1."
      expr? expr?-new)
     (mv (irr-stmt) (irr-simpadd0-gout)))
    ((when (and (not expr?) expr?-diffp))
     (raise
      "Internal error: ~
                unchanged return statement marked as changed.")
     (mv (irr-stmt) (irr-simpadd0-gout)))
    ((unless (or (not expr?)
                 (and expr?-thm-name
                      (not (expr-purep expr?)))))
     (mv stmt-new
         (make-simpadd0-gout :events expr?-events
                             :thm-name nil
                             :thm-index gin.thm-index
                             :names-to-avoid gin.names-to-avoid
                             :vartys expr?-vartys
                             :diffp expr?-diffp)))
    (hints
     (if expr?
      (cons
       (cons
        '"Goal"
        (cons
         ':in-theory
         (cons
          ''((:e ldm-stmt)
             (:e ldm-expr)
             (:e ident)
             (:e c::expr-kind)
             (:e c::stmt-expr))
          (cons
           ':use
           (cons
            (cons
             (cons ':instance
                   (cons expr?-thm-name
                         '(:extra-bindings-ok (limit (- limit 2)))))
             (cons
              (cons
               ':instance
               (cons
                'simpadd0-stmt-expr-asg-support-lemma
                (cons
                 (cons
                  'old-expr
                  (cons
                   (cons
                    'mv-nth
                    (cons
                     '1
                     (cons
                         (cons 'ldm-expr
                               (cons (cons 'quote (cons expr? 'nil))
                                     'nil))
                         'nil)))
                   'nil))
                 (cons
                  (cons
                   'new-expr
                   (cons
                    (cons
                     'mv-nth
                     (cons
                      '1
                      (cons
                       (cons
                           'ldm-expr
                           (cons (cons 'quote (cons expr?-new 'nil))
                                 'nil))
                       'nil)))
                    'nil))
                  (and (not expr?-diffp)
                       '((old-fenv fenv) (new-fenv fenv)))))))
              (cons
               (cons
                ':instance
                (cons
                 'simpadd0-stmt-expr-asg-support-lemma-error
                 (cons
                  (cons
                   'expr
                   (cons
                    (cons
                     'mv-nth
                     (cons
                      '1
                      (cons
                         (cons 'ldm-expr
                               (cons (cons 'quote (cons expr? 'nil))
                                     'nil))
                         'nil)))
                    'nil))
                  (and expr?-diffp '((fenv old-fenv))))))
               'nil)))
            'nil)))))
       'nil)
      '(("Goal" :in-theory '((:e ldm-stmt) (:e c::stmt-null))
                :use simpadd0-stmt-null-support-lemma))))
    ((mv thm-event thm-name thm-index)
     (simpadd0-gen-stmt-thm stmt stmt-new expr?-vartys
                            gin.const-new gin.thm-index hints)))
   (mv stmt-new
       (make-simpadd0-gout
            :events (append expr?-events (list thm-event))
            :thm-name thm-name
            :thm-index thm-index
            :names-to-avoid (cons thm-name gin.names-to-avoid)
            :vartys expr?-vartys
            :diffp expr?-diffp)))))

Theorem: stmtp-of-simpadd0-stmt-expr.stmt

(defthm stmtp-of-simpadd0-stmt-expr.stmt
  (b* (((mv ?stmt ?gout)
        (simpadd0-stmt-expr expr?
                            expr?-new expr?-events expr?-thm-name
                            expr?-vartys expr?-diffp gin)))
    (stmtp stmt))
  :rule-classes :rewrite)

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

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

Theorem: stmt-unambp-of-simpadd0-stmt-expr

(defthm stmt-unambp-of-simpadd0-stmt-expr
 (implies
     (expr-option-unambp expr?-new)
     (b* (((mv ?stmt ?gout)
           (simpadd0-stmt-expr expr?
                               expr?-new expr?-events expr?-thm-name
                               expr?-vartys expr?-diffp gin)))
       (stmt-unambp stmt))))

Theorem: simpadd0-stmt-null-support-lemma

(defthm simpadd0-stmt-null-support-lemma
  (b* ((stmt (c::stmt-null))
       ((mv result &)
        (c::exec-stmt stmt compst fenv limit)))
    (implies (not (c::errorp result))
             (not result))))

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

(defthm simpadd0-stmt-expr-asg-support-lemma
  (b* ((old (c::stmt-expr old-expr))
       (new (c::stmt-expr new-expr))
       (old-expr-compst
            (c::exec-expr-asg old-expr compst old-fenv (- limit 2)))
       (new-expr-compst
            (c::exec-expr-asg new-expr compst new-fenv (- limit 2)))
       ((mv old-result old-compst)
        (c::exec-stmt old compst old-fenv limit))
       ((mv new-result new-compst)
        (c::exec-stmt new compst new-fenv limit)))
    (implies (and (not (equal (c::expr-kind old-expr) :call))
                  (not (equal (c::expr-kind new-expr) :call))
                  (not (c::errorp old-result))
                  (not (c::errorp new-expr-compst))
                  (equal old-expr-compst new-expr-compst))
             (and (not (c::errorp new-result))
                  (equal old-result new-result)
                  (equal old-compst new-compst)
                  (not old-result)))))

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

(defthm simpadd0-stmt-expr-asg-support-lemma-error
 (implies
   (and (not (equal (c::expr-kind expr) :call))
        (c::errorp (c::exec-expr-asg expr compst fenv (- limit 2))))
   (c::errorp (mv-nth 0
                      (c::exec-stmt (c::stmt-expr expr)
                                    compst fenv limit)))))