		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 under the additional conditions described shortly, we generate a theorem saying that the exprssion, when executed, yields a value of the appropriate integer type. The additional conditions are that:

If the constant has type (signed or unsigned) int, it fits in 32 bits.
If the constant has type (signed or unsigned) long, it fits in 64 bits.
If the constant has type (signed or unsigned) long long, it fits in 64 bits.

The reason is that our current dynamic semantics assumes that those types have those sizes, while our validator is more general (c$::valid-iconst takes an implementation environment as input, which specifies, among other things, the size of those types). 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
                             :vartys nil
                             :diffp nil))
    ((unless (const-case const :int))
     (mv expr no-thm-gout))
    ((iconst iconst)
     (const-int->unwrap const))
    ((iconst-info info)
     (coerce-iconst-info iconst.info))
    ((unless (or (and (type-case info.type :sint)
                      (<= info.value (c::sint-max)))
                 (and (type-case info.type :uint)
                      (<= info.value (c::uint-max)))
                 (and (type-case info.type :slong)
                      (<= info.value (c::slong-max)))
                 (and (type-case info.type :ulong)
                      (<= info.value (c::ulong-max)))
                 (and (type-case info.type :sllong)
                      (<= info.value (c::sllong-max)))
                 (and (type-case info.type :ullong)
                      (<= info.value (c::ullong-max)))))
     (mv expr no-thm-gout))
    (expr (expr-const const))
    (hints
     '(("Goal"
            :in-theory '(c::exec-expr-pure (:e 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::type-of-value)
                                           (:e c::value-kind)))))
    (vartys nil)
    ((mv thm-event thm-name thm-index)
     (simpadd0-gen-expr-pure-thm
          expr expr vartys
          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 (cons thm-name gin.names-to-avoid)
            :vartys vartys
            :diffp nil)))))

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)