		Search-engine friendly clone of the ACL2 documentation.

Proof-generation

Xeq-stmt-return

Equality lifting transformation of a return statement.

Signature
(xeq-stmt-return expr? expr?-new expr?-thm-name info gin) → (mv stmt gout)
Arguments: expr? — Guard (expr-optionp expr?).; expr?-new — Guard (expr-optionp expr?-new).; expr?-thm-name — Guard (symbolp expr?-thm-name).; gin — Guard (ginp gin).
Returns: stmt — Type (stmtp stmt).; gout — Type (goutp gout).

We put the new optional expression into a return statement.

We generate a theorem iff the expression is absent or a theorem was generated for the expression. Note that the expression is present in the old statement iff it is present in the new statement; also note that, if there is no expression, old and new statements are syntactically equal.

Definitions and Theorems

Function: xeq-stmt-return

(defun xeq-stmt-return (expr? expr?-new expr?-thm-name info gin)
 (declare (xargs :guard (and (expr-optionp expr?)
                             (expr-optionp expr?-new)
                             (symbolp expr?-thm-name)
                             (ginp gin))))
 (declare (xargs :guard (and (expr-option-unambp expr?)
                             (expr-option-annop expr?)
                             (expr-option-unambp expr?-new)
                             (expr-option-annop expr?-new)
                             (iff expr? expr?-new))))
 (let ((__function__ 'xeq-stmt-return))
  (declare (ignorable __function__))
  (b*
   (((gin gin) gin)
    (stmt (make-stmt-return :expr? expr?
                            :info info))
    (stmt-new (make-stmt-return :expr? expr?-new
                                :info info))
    ((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 stmt-new (irr-gout)))
    ((unless (or (not expr?) expr?-thm-name))
     (mv stmt-new (gout-no-thm gin)))
    ((mv & old-expr?)
     (ldm-expr-option expr?))
    ((mv & new-expr?)
     (ldm-expr-option expr?-new))
    (hints
     (if expr?
      (cons
       (cons
        '"Goal"
        (cons
         ':in-theory
         (cons
          ''((:e insert)
             (:e c::stmt-kind)
             (:e c::stmt-return)
             (:e c::stmt-return->value)
             (:e c::type-nonchar-integerp)
             stmt-compustate-vars)
          (cons
           ':use
           (cons
            (cons
             (cons ':instance
                   (cons expr?-thm-name '((limit (1- limit)))))
             (cons
              (cons
               ':instance
               (cons
                'stmt-return-value-congruence
                (cons
                 (cons 'old-expr
                       (cons (cons 'quote (cons old-expr? 'nil))
                             'nil))
                 (cons
                     (cons 'new-expr
                           (cons (cons 'quote (cons new-expr? 'nil))
                                 'nil))
                     'nil))))
              (cons
               (cons
                ':instance
                (cons
                 'stmt-return-errors
                 (cons
                     (cons 'expr
                           (cons (cons 'quote (cons old-expr? 'nil))
                                 'nil))
                     '((fenv old-fenv)))))
               'nil)))
            'nil)))))
       'nil)
      '(("Goal" :in-theory '((:e c::stmt-return)
                             (:e c::type-void)
                             (:e insert)
                             stmt-compustate-vars)
                :use (stmt-return-novalue-congruence)))))
    ((mv thm-event thm-name thm-index)
     (gen-stmt-thm stmt stmt-new gin.vartys
                   gin.const-new gin.thm-index hints)))
   (mv stmt-new
       (make-gout :events (cons thm-event gin.events)
                  :thm-index thm-index
                  :thm-name thm-name
                  :vartys gin.vartys)))))

Theorem: stmtp-of-xeq-stmt-return.stmt

(defthm stmtp-of-xeq-stmt-return.stmt
  (b* (((mv ?stmt ?gout)
        (xeq-stmt-return expr?
                         expr?-new expr?-thm-name info gin)))
    (stmtp stmt))
  :rule-classes :rewrite)

Theorem: goutp-of-xeq-stmt-return.gout

(defthm goutp-of-xeq-stmt-return.gout
  (b* (((mv ?stmt ?gout)
        (xeq-stmt-return expr?
                         expr?-new expr?-thm-name info gin)))
    (goutp gout))
  :rule-classes :rewrite)

Theorem: stmt-unambp-of-xeq-stmt-return

(defthm stmt-unambp-of-xeq-stmt-return
  (implies
       (expr-option-unambp expr?-new)
       (b* (((mv ?stmt ?gout)
             (xeq-stmt-return expr?
                              expr?-new expr?-thm-name info gin)))
         (stmt-unambp stmt))))

Theorem: stmt-annop-of-xeq-stmt-return

(defthm stmt-annop-of-xeq-stmt-return
  (implies
       (expr-option-annop expr?-new)
       (b* (((mv ?stmt ?gout)
             (xeq-stmt-return expr?
                              expr?-new expr?-thm-name info gin)))
         (stmt-annop stmt))))

Theorem: stmt-aidentp-of-xeq-stmt-return

(defthm stmt-aidentp-of-xeq-stmt-return
  (implies
       (expr-option-aidentp expr?-new gcc)
       (b* (((mv ?stmt ?gout)
             (xeq-stmt-return expr?
                              expr?-new expr?-thm-name info gin)))
         (stmt-aidentp stmt gcc))))