		Search-engine friendly clone of the ACL2 documentation.

Atc-expression-generation

Atc-gen-expr-var

Generate a C expression from an ACL2 variable.

Signature
(atc-gen-expr-var var gin state) → gout
Arguments: var — Guard (symbolp var).; gin — Guard (expr-ginp gin).
Returns: gout — Type (expr-goutp gout).

An ACL2 variable is translated to a C variable. Its information is looked up in the symbol table.

If the variable has pointer or array type and is not an external object, its correctness theorem equates it to the -ptr variable, because the variable itself contains the pointed object or array.

Definitions and Theorems

Function: atc-gen-expr-var

(defun atc-gen-expr-var (var gin state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbolp var) (expr-ginp gin))))
 (let ((__function__ 'atc-gen-expr-var))
  (declare (ignorable __function__))
  (b*
   (((expr-gin gin) gin)
    (info (atc-get-var var gin.inscope))
    ((when (not info))
     (raise
      "Internal error: the variable ~x0 in function ~x1 ~
                has no associated information."
      var gin.fn)
     (irr-expr-gout))
    (type (atc-var-info->type info))
    (var-thm (atc-var-info->thm info))
    (expr (expr-ident (make-ident :name (symbol-name var))))
    ((when (not gin.proofs))
     (make-expr-gout :expr expr
                     :type type
                     :term var
                     :events nil
                     :thm-name nil
                     :thm-index gin.thm-index
                     :names-to-avoid gin.names-to-avoid))
    (hints
     (cons
      (cons
       '"Goal"
       (cons
        ':in-theory
        (cons
         (cons
            'quote
            (cons (cons var-thm
                        '(exec-expr-pure-when-ident
                              (:e expr-kind)
                              (:e expr-ident->get)
                              exec-ident-open-via-object (:e identp)
                              (:e ident->name)
                              objdesign-of-var-of-const-identifier))
                  'nil))
         'nil)))
      'nil))
    (objdes
        (cons 'objdesign-of-var
              (cons (cons 'ident
                          (cons (cons 'quote
                                      (cons (symbol-name var) 'nil))
                                'nil))
                    (cons gin.compst-var 'nil))))
    ((mv thm-event
         thm-name thm-index names-to-avoid)
     (atc-gen-expr-pure-correct-thm
          gin.fn
          gin.fn-guard gin.context expr type
          (if (and (or (type-case type :pointer)
                       (type-case type :array))
                   (not (atc-var-info->externalp info)))
              (add-suffix-to-fn var "-PTR")
            var)
          var objdes gin.compst-var
          hints nil gin.prec-tags gin.thm-index
          gin.names-to-avoid state)))
   (make-expr-gout :expr expr
                   :type type
                   :term var
                   :events (list thm-event)
                   :thm-name thm-name
                   :thm-index thm-index
                   :names-to-avoid names-to-avoid))))

Theorem: expr-goutp-of-atc-gen-expr-var

(defthm expr-goutp-of-atc-gen-expr-var
  (b* ((gout (atc-gen-expr-var var gin state)))
    (expr-goutp gout))
  :rule-classes :rewrite)