		Search-engine friendly clone of the ACL2 documentation.

Simpadd0-event-generation

Simpadd0-expr-ident

Transform an identifier expression (i.e. a variable).

Signature
(simpadd0-expr-ident ident info gin) → (mv expr gout)
Arguments: ident — Guard (identp ident).; info — Guard (var-infop info).; 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 identifier and validation information passed as inputs.

If the variable has a type supported in our C formalization, which we check in the validation information, then we generate a theorem saying that the expression, when executed, yields a value of the appropriate type. The generated theorem is proved via a general supporting lemma, which is proved below.

Definitions and Theorems

Function: simpadd0-expr-ident

(defun simpadd0-expr-ident (ident info gin)
 (declare (xargs :guard (and (identp ident)
                             (var-infop info)
                             (simpadd0-ginp gin))))
 (let ((__function__ 'simpadd0-expr-ident))
  (declare (ignorable __function__))
  (b*
   ((ident (ident-fix ident))
    ((var-info info) (var-info-fix info))
    ((simpadd0-gin gin) gin)
    (expr (make-expr-ident :ident ident
                           :info info))
    ((unless (and (type-formalp info.type)
                  (not (type-case info.type :void))
                  (not (type-case info.type :char))))
     (mv expr
         (make-simpadd0-gout :events nil
                             :thm-name nil
                             :thm-index gin.thm-index
                             :names-to-avoid gin.names-to-avoid
                             :vartys nil
                             :diffp nil)))
    (vartys (omap::update ident info.type nil))
    ((unless (type-formalp info.type))
     (raise "Internal error: variable ~x0 has type ~x1."
            ident info.type)
     (mv (irr-expr) (irr-simpadd0-gout)))
    ((mv & ctype) (ldm-type info.type))
    (hints
     (cons
      (cons
       '"Goal"
       (cons
        ':in-theory
        (cons
         ''((:e expr-ident)
            (:e expr-pure-formalp)
            (:e ident))
         (cons
          ':use
          (cons
           (cons
            ':instance
            (cons
             'simpadd0-expr-ident-support-lemma
             (cons
              (cons 'ident
                    (cons (cons 'quote (cons ident 'nil))
                          'nil))
              (cons
               (cons 'info
                     (cons (cons 'quote (cons info 'nil))
                           'nil))
               (cons
                (cons 'type
                      (cons (cons 'quote (cons ctype 'nil))
                            'nil))
                (cons
                 (cons
                    'kind
                    (cons (cons 'quote
                                (cons (type-to-value-kind info.type)
                                      'nil))
                          'nil))
                 'nil))))))
           'nil)))))
      '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-ident.expr

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

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

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

Theorem: expr-unambp-of-simpadd0-expr-ident

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

Theorem: simpadd0-expr-ident-support-lemma

(defthm simpadd0-expr-ident-support-lemma
  (b* ((expr (mv-nth 1 (ldm-expr (expr-ident ident info))))
       (result (c::exec-expr-pure expr compst))
       (value (c::expr-value->value result)))
    (implies (and (expr-pure-formalp (expr-ident ident info))
                  (b* ((var (mv-nth 1 (ldm-ident ident)))
                       (objdes (c::objdesign-of-var var compst))
                       (val (c::read-object objdes compst)))
                    (and objdes (c::valuep val)
                         (equal (c::type-of-value val) type)
                         (equal (c::value-kind val) kind))))
             (and (equal (c::value-kind value) kind)
                  (equal (c::type-of-value value)
                         type)))))

Theorem: simpadd0-expr-ident-of-ident-fix-ident

(defthm simpadd0-expr-ident-of-ident-fix-ident
  (equal (simpadd0-expr-ident (ident-fix ident)
                              info gin)
         (simpadd0-expr-ident ident info gin)))

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

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

Theorem: simpadd0-expr-ident-of-var-info-fix-info

(defthm simpadd0-expr-ident-of-var-info-fix-info
  (equal (simpadd0-expr-ident ident (var-info-fix info)
                              gin)
         (simpadd0-expr-ident ident info gin)))

Theorem: simpadd0-expr-ident-var-info-equiv-congruence-on-info

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

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

(defthm simpadd0-expr-ident-of-simpadd0-gin-fix-gin
  (equal (simpadd0-expr-ident ident info (simpadd0-gin-fix gin))
         (simpadd0-expr-ident ident info gin)))

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

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