		Search-engine friendly clone of the ACL2 documentation.

Proof-generation

Xeq-stmt-expr

Equality lifting transformation of an expression statement.

Signature
(xeq-stmt-expr 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 optional expression into an expression statement.

We generate a theorem if there is no expression (i.e. the null statement), or if we have a theorem for a supported expression. If the expression is pure, its theorem refers to c::exec-expr-pure, and so we lift that to a theorem that refers to c::exec-expr. An expression statement does not change the variables in scope, so we use the variable-type map from the validation table in the AST for both before and after the statement, in the generated theorem.

Definitions and Theorems

Function: xeq-stmt-expr

(defun xeq-stmt-expr (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-expr))
  (declare (ignorable __function__))
  (b*
   (((gin gin) gin)
    (stmt (make-stmt-expr :expr? expr?
                          :info info))
    (stmt-new (make-stmt-expr :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 lifted-thm-name thm-index events)
     (if
      (and expr? (expr-purep expr?)
           (not (expr-case expr? :ident))
           (not (expr-case expr? :const))
           (not (expr-case expr? :unary))
           (not (expr-case expr? :cast))
           (not (and (expr-case expr? :binary)
                     (b* ((op (expr-binary->op expr?)))
                       (and (c$::binop-purep op)
                            (c$::binop-strictp op))))))
      (b* (((mv thm-event thm-name thm-index)
            (lift-expr-pure-thm expr?
                                expr?-new expr?-thm-name gin.vartys
                                gin.const-new gin.thm-index)))
        (mv thm-name
            thm-index (cons thm-event gin.events)))
      (mv nil gin.thm-index gin.events)))
    ((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 c::stmt-kind)
             (:e c::stmt-expr->get)
             (:e c::stmt-expr)
             (:e insert)
             expr-compustate-vars
             stmt-compustate-vars)
          (cons
           ':use
           (cons
            (cons
             (cons ':instance
                   (cons (or lifted-thm-name expr?-thm-name)
                         '((limit (1- limit)))))
             (cons
              (cons
               ':instance
               (cons
                'stmt-expr-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-expr-errors
                 (cons
                     (cons 'expr
                           (cons (cons 'quote (cons old-expr? 'nil))
                                 'nil))
                     '((fenv old-fenv)))))
               'nil)))
            'nil)))))
       'nil)
      '(("Goal" :in-theory '((:e c::stmt-kind)
                             (:e c::stmt-null)
                             c::type-option-of-stmt-value (:e in)
                             (:e insert)
                             stmt-compustate-vars)
                :use (stmt-null-congruence)))))
    ((mv thm-event thm-name thm-index)
     (gen-stmt-thm stmt stmt-new gin.vartys
                   gin.const-new thm-index hints)))
   (mv stmt-new
       (make-gout :events (cons thm-event events)
                  :thm-index thm-index
                  :thm-name thm-name
                  :vartys gin.vartys)))))

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

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

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

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

Theorem: stmt-unambp-of-xeq-stmt-expr

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

Theorem: stmt-annop-of-xeq-stmt-expr

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

Theorem: stmt-aidentp-of-xeq-stmt-expr

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