		Search-engine friendly clone of the ACL2 documentation.

Atc-expression-generation

Atc-gen-expr-const

Generate a C expression and theorem from an ACL2 term that represents an integer constant expression.

Signature
(atc-gen-expr-const term const type type-base-const gin state) → gout
Arguments: term — Guard (pseudo-termp term).; const — Guard (iconstp const).; type — Guard (typep type).; type-base-const — Guard (symbolp type-base-const).; gin — Guard (expr-ginp gin).
Returns: gout — Type (expr-goutp gout).

The C integer constant is actually calculated by the caller, and passed as input here.

The hints cover all possible integer constants, but we could make them more nuanced to the specifics of the constant.

Definitions and Theorems

Function: atc-gen-expr-const

(defun atc-gen-expr-const
       (term const type type-base-const gin state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (pseudo-termp term)
                             (iconstp const)
                             (typep type)
                             (symbolp type-base-const)
                             (expr-ginp gin))))
 (declare (xargs :guard (type-nonchar-integerp type)))
 (let ((__function__ 'atc-gen-expr-const))
  (declare (ignorable __function__))
  (b*
   (((expr-gin gin) gin)
    (expr (expr-const (const-int const)))
    ((when (not gin.proofs))
     (make-expr-gout :expr expr
                     :type type
                     :term term
                     :events nil
                     :thm-name nil
                     :thm-index gin.thm-index
                     :names-to-avoid gin.names-to-avoid))
    (hints
     (b* ((fixtype (integer-type-to-fixtype type))
          (exec-const-to-fixtype (pack 'exec-const-to- fixtype))
          (fixtype-integerp (pack fixtype '-integerp))
          (recognizer (atc-type-to-recognizer type gin.prec-tags))
          (valuep-when-recognizer (pack 'valuep-when- recognizer))
          (recognizer-of-fixtype-from-integer
               (pack recognizer '-of-
                     fixtype '-from-integer)))
      (cons
       (cons
        '"Goal"
        (cons
         ':in-theory
         (cons
          (cons
           'quote
           (cons
            (cons
             'exec-expr-pure-when-const
             (cons
              '(:e expr-kind)
              (cons
               '(:e expr-const->get)
               (cons
                exec-const-to-fixtype
                (cons
                 '(:e const-kind)
                 (cons
                  '(:e const-int->get)
                  (cons
                   '(:e iconst->unsignedp)
                   (cons
                    '(:e iconst->length)
                    (cons
                     '(:e iconst->value)
                     (cons
                      '(:e iconst->base)
                      (cons
                       '(:e iconst-length-kind)
                       (cons
                        '(:e iconst-base-kind)
                        (cons
                         (cons ':e (cons fixtype-integerp 'nil))
                         (cons
                          type-base-const
                          (cons
                           recognizer-of-fixtype-from-integer
                           (cons
                            'expr-valuep-of-expr-value
                            (cons
                                 'expr-value->value-of-expr-value
                                 (cons 'value-fix-when-valuep
                                       (cons valuep-when-recognizer
                                             'nil)))))))))))))))))))
            'nil))
          'nil)))
       '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
          term term acl2::*nil* gin.compst-var
          hints nil gin.prec-tags gin.thm-index
          gin.names-to-avoid state)))
   (make-expr-gout :expr expr
                   :type type
                   :term term
                   :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-const

(defthm expr-goutp-of-atc-gen-expr-const
 (b*
  ((gout (atc-gen-expr-const term
                             const type type-base-const gin state)))
  (expr-goutp gout))
 :rule-classes :rewrite)