		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 (c$::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 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.

Under the assumption that the variable is in scope, which is included in the generated theorem, the execution of a variable never results in an error, so we pass nil as the falliblep flag to the theorem generation function, and we set to nil the falliblep component of simpadd0-gout.

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)
                             (c$::var-infop info)
                             (simpadd0-ginp gin))))
 (let ((__function__ 'simpadd0-expr-ident))
  (declare (ignorable __function__))
  (b*
   ((ident (ident-fix ident))
    ((c$::var-info info)
     (c$::var-info-fix info))
    ((simpadd0-gin gin) gin)
    (expr (make-expr-ident :ident ident
                           :info info))
    ((unless (c$::type-case info.type :sint))
     (mv expr
         (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)))
    (vars (insert ident nil))
    (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))
    (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-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
                    (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-var-info-fix-info

(defthm simpadd0-expr-ident-of-var-info-fix-info
  (equal (simpadd0-expr-ident ident (c$::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)