		Search-engine friendly clone of the ACL2 documentation.

Simpadd0-event-generation

Simpadd0-expr-const

Transform a constant.

Signature
(simpadd0-expr-const const gin) → (mv expr gout)
Arguments: const — Guard (constp const).; gin — Guard (simpadd0-ginp gin).
Returns: expr — Type (exprp expr).; gout — Type (simpadd0-goutp gout).

This undergoes no actual transformation, but we introduce it for uniformity, also because we may eventually evolve the simpadd0 implementation into a much more general transformation. Thus, the output expression consists of the constant passed as input.

If the constant is an integer one and has type int, and under the additional condition described shortly, we generate a theorem saying that the exprssion, when executed, yields a value of type int. The additional condition is that the value of the constant fits in 32 bits. The reason is that our current dynamic semantics assumes that int has 32 bits, while our validator is more general (c$::valid-iconst takes an implementation environment as input, which specifies, among other things, the size of int). Until we extend our dynamic semantics to be more general, we need this additional condition for proof generation.

Definitions and Theorems

Function: simpadd0-expr-const

(defun simpadd0-expr-const (const gin)
 (declare (xargs :guard (and (constp const)
                             (simpadd0-ginp gin))))
 (let ((__function__ 'simpadd0-expr-const))
  (declare (ignorable __function__))
  (b*
   (((simpadd0-gin gin) gin)
    (expr (expr-const const))
    (no-thm-gout
         (make-simpadd0-gout :events nil
                             :thm-name nil
                             :thm-index gin.thm-index
                             :names-to-avoid gin.names-to-avoid
                             :vars nil
                             :diffp nil
                             :falliblep nil))
    ((unless (const-case const :int))
     (mv expr no-thm-gout))
    ((iconst iconst)
     (const-int->unwrap const))
    ((c$::iconst-info info)
     (c$::coerce-iconst-info iconst.info))
    ((unless (and (c$::type-case info.type :sint)
                  (<= info.value (c::sint-max))))
     (mv expr no-thm-gout))
    (expr (expr-const const))
    (hints
     '(("Goal"
            :in-theory '(c::exec-expr-pure (:e c$::ldm-expr)
                                           (:e c::expr-const)
                                           (:e c::expr-fix)
                                           (:e c::expr-kind)
                                           (:e c::expr-const->get)
                                           (:e c::exec-const)
                                           (:e c::expr-value->value)
                                           (:e c::value-kind)))))
    (vars nil)
    (falliblep nil)
    ((mv thm-event thm-name thm-index)
     (simpadd0-gen-expr-pure-thm
          expr expr falliblep vars
          gin.const-new gin.thm-index hints)))
   (mv expr
       (make-simpadd0-gout :events (list thm-event)
                           :thm-name thm-name
                           :thm-index thm-index
                           :names-to-avoid (list thm-name)
                           :vars vars
                           :diffp nil
                           :falliblep falliblep)))))

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

(defthm exprp-of-simpadd0-expr-const.expr
  (b* (((mv ?expr ?gout)
        (simpadd0-expr-const const gin)))
    (exprp expr))
  :rule-classes :rewrite)

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

(defthm simpadd0-goutp-of-simpadd0-expr-const.gout
  (b* (((mv ?expr ?gout)
        (simpadd0-expr-const const gin)))
    (simpadd0-goutp gout))
  :rule-classes :rewrite)

Theorem: expr-unambp-of-simpadd0-expr-const

(defthm expr-unambp-of-simpadd0-expr-const
  (b* (((mv ?expr ?gout)
        (simpadd0-expr-const const gin)))
    (expr-unambp expr)))

Theorem: simpadd0-expr-const-of-const-fix-const

(defthm simpadd0-expr-const-of-const-fix-const
  (equal (simpadd0-expr-const (const-fix const)
                              gin)
         (simpadd0-expr-const const gin)))

Theorem: simpadd0-expr-const-const-equiv-congruence-on-const

(defthm simpadd0-expr-const-const-equiv-congruence-on-const
  (implies (c$::const-equiv const const-equiv)
           (equal (simpadd0-expr-const const gin)
                  (simpadd0-expr-const const-equiv gin)))
  :rule-classes :congruence)

Theorem: simpadd0-expr-const-of-simpadd0-gin-fix-gin

(defthm simpadd0-expr-const-of-simpadd0-gin-fix-gin
  (equal (simpadd0-expr-const const (simpadd0-gin-fix gin))
         (simpadd0-expr-const const gin)))

Theorem: simpadd0-expr-const-simpadd0-gin-equiv-congruence-on-gin

(defthm simpadd0-expr-const-simpadd0-gin-equiv-congruence-on-gin
  (implies (simpadd0-gin-equiv gin gin-equiv)
           (equal (simpadd0-expr-const const gin)
                  (simpadd0-expr-const const gin-equiv)))
  :rule-classes :congruence)