		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 new-ident new-info gout)
Arguments: ident — Guard (identp ident).; info — Guard (acl2::any-p info).; gin — Guard (simpadd0-ginp gin).
Returns: new-ident — Type (identp new-ident).; new-info — Type (acl2::any-p new-info).; 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 identifier and validation information are always the same as the inputs one. However, if the variable has type int, which we check in the validation information, then we generate a theorem saying that the expression, when executed, yields a value of type int.

Definitions and Theorems

Function: simpadd0-expr-ident

(defun simpadd0-expr-ident (ident info gin)
 (declare (xargs :guard (and (identp ident)
                             (acl2::any-p info)
                             (simpadd0-ginp gin))))
 (let ((__function__ 'simpadd0-expr-ident))
  (declare (ignorable __function__))
  (b*
   ((ident (ident-fix ident))
    ((simpadd0-gin gin) gin)
    ((c$::var-info info)
     (c$::coerce-var-info info))
    ((unless (c$::type-case info.type :sint))
     (mv ident info
         (make-simpadd0-gout :events nil
                             :thm-name nil
                             :thm-index gin.thm-index
                             :names-to-avoid gin.names-to-avoid
                             :vars nil
                             :diffp nil)))
    (vars (insert ident nil))
    (hyps (simpadd0-gen-var-hyps vars))
    (thm-name (packn-pos (list gin.const-new '-thm-
                               gin.thm-index)
                         gin.const-new))
    (thm-index (1+ gin.thm-index))
    (thm-formula
     (cons
      'b*
      (cons
       (cons
        (cons
         'expr
         (cons
          (cons
           'mv-nth
           (cons
            '1
            (cons
             (cons
                'c$::ldm-expr
                (cons (cons 'quote
                            (cons (c$::expr-ident ident info) 'nil))
                      'nil))
             'nil)))
          'nil))
        '((expr-result (c::exec-expr-pure expr compst))
          (expr-value (c::expr-value->value expr-result))))
       (cons (cons 'implies
                   (append hyps
                           '((equal (c::value-kind expr-value)
                                    :sint))))
             'nil))))
    (thm-hints
     (cons
      (cons
       '"Goal"
       (cons
        ':in-theory
        (cons
         ''((:e c$::expr-ident)
            (:e c$::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))
                          'nil))))
           'nil)))))
      'nil))
    (thm-event (cons 'defthmd
                     (cons thm-name
                           (cons thm-formula
                                 (cons ':hints
                                       (cons thm-hints 'nil)))))))
   (mv ident info
       (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)))))

Theorem: identp-of-simpadd0-expr-ident.new-ident

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

Theorem: any-p-of-simpadd0-expr-ident.new-info

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

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

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

Theorem: simpadd0-expr-ident-support-lemma

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

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-identity-info

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

Theorem: simpadd0-expr-ident-equal-congruence-on-info

(defthm simpadd0-expr-ident-equal-congruence-on-info
  (implies (equal 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)