		Search-engine friendly clone of the ACL2 documentation.

Atc-expression-generation

Atc-gen-expr-binary

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

Signature
(atc-gen-expr-binary fn arg1-term arg2-term arg1-expr arg2-expr arg1-type arg2-type arg1-events arg2-events arg1-thm arg2-thm in-type1 in-type2 out-type op gin state) → (mv erp gout)
Arguments: fn — Guard (symbolp fn).; arg1-term — Guard (pseudo-termp arg1-term).; arg2-term — Guard (pseudo-termp arg2-term).; arg1-expr — Guard (exprp arg1-expr).; arg2-expr — Guard (exprp arg2-expr).; arg1-type — Guard (typep arg1-type).; arg2-type — Guard (typep arg2-type).; arg1-events — Guard (pseudo-event-form-listp arg1-events).; arg2-events — Guard (pseudo-event-form-listp arg2-events).; arg1-thm — Guard (symbolp arg1-thm).; arg2-thm — Guard (symbolp arg2-thm).; in-type1 — Guard (typep in-type1).; in-type2 — Guard (typep in-type2).; out-type — Guard (typep out-type).; op — Guard (binopp op).; gin — Guard (expr-ginp gin).
Returns: gout — Type (expr-goutp gout).

The expressions and theorems for the arguments are generated in the caller, and passed here.

We do not yet support operations with an associated okp predicate. We will add support for them soon.

Definitions and Theorems

Function: atc-gen-expr-binary

(defun atc-gen-expr-binary
       (fn arg1-term arg2-term arg1-expr arg2-expr
           arg1-type arg2-type arg1-events
           arg2-events arg1-thm arg2-thm
           in-type1 in-type2 out-type op gin state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbolp fn)
                             (pseudo-termp arg1-term)
                             (pseudo-termp arg2-term)
                             (exprp arg1-expr)
                             (exprp arg2-expr)
                             (typep arg1-type)
                             (typep arg2-type)
                             (pseudo-event-form-listp arg1-events)
                             (pseudo-event-form-listp arg2-events)
                             (symbolp arg1-thm)
                             (symbolp arg2-thm)
                             (typep in-type1)
                             (typep in-type2)
                             (typep out-type)
                             (binopp op)
                             (expr-ginp gin))))
 (declare (xargs :guard (and (type-nonchar-integerp in-type1)
                             (type-nonchar-integerp in-type2)
                             (type-nonchar-integerp out-type))))
 (let ((__function__ 'atc-gen-expr-binary))
  (declare (ignorable __function__))
  (b*
   (((reterr) (irr-expr-gout))
    (wrld (w state))
    ((expr-gin gin) gin)
    ((unless (and (equal arg1-type in-type1)
                  (equal arg2-type in-type2)))
     (reterr
      (msg
       "The binary operator ~x0 is applied ~
               to an expression term ~x1 returning ~x2 ~
               and to an expression term ~x3 returning ~x4, ~
               but a ~x5 operand and a ~x6 operand are expected. ~
               This is indicative of provably dead code, ~
               given that the code is guard-verified."
       op arg1-term arg1-type
       arg2-term arg2-type in-type1 in-type2)))
    (expr (make-expr-binary :op op
                            :arg1 arg1-expr
                            :arg2 arg2-expr))
    ((when (eq fn 'quote))
     (reterr (raise "Internal error: function symbol is QUOTE.")))
    (term (cons fn
                (cons arg1-term (cons arg2-term 'nil))))
    ((when (not gin.proofs))
     (retok (make-expr-gout :expr expr
                            :type out-type
                            :term term
                            :events (append arg1-events arg2-events)
                            :thm-name nil
                            :thm-index gin.thm-index
                            :names-to-avoid gin.names-to-avoid)))
    (op-name (pack (binop-kind op)))
    (fn-okp (and (or (member-eq (binop-kind op)
                                '(:div :rem :shl :shr))
                     (and (member-eq (binop-kind op)
                                     '(:add :sub :mul))
                          (type-signed-integerp out-type)))
                 (pack fn '-okp)))
    ((mv okp-lemma-event?
         okp-lemma-name thm-index names-to-avoid)
     (if fn-okp
      (b*
       ((okp-lemma-name (pack gin.fn '-expr-
                              gin.thm-index '-okp-lemma))
        ((mv okp-lemma-name names-to-avoid)
         (fresh-logical-name-with-$s-suffix
              okp-lemma-name
              nil gin.names-to-avoid wrld))
        (arg1-uterm (untranslate$ arg1-term nil state))
        (arg2-uterm (untranslate$ arg2-term nil state))
        (okp-lemma-formula
             (cons fn-okp
                   (cons arg1-uterm (cons arg2-uterm 'nil))))
        (okp-lemma-formula
             (atc-contextualize okp-lemma-formula gin.context gin.fn
                                gin.fn-guard nil nil nil nil wrld))
        (okp-lemma-hints
         (cons
          (cons
           '"Goal"
           (cons
            ':in-theory
            (cons
             (cons
                'quote
                (cons (cons gin.fn-guard '(if* test* declar assign))
                      'nil))
             (cons ':use
                   (cons (cons ':guard-theorem
                               (cons gin.fn 'nil))
                         'nil)))))
          'nil))
        ((mv okp-lemma-event &)
         (evmac-generate-defthm okp-lemma-name
                                :formula okp-lemma-formula
                                :hints okp-lemma-hints
                                :enable nil)))
       (mv (list okp-lemma-event)
           okp-lemma-name (1+ gin.thm-index)
           names-to-avoid))
      (mv nil
          nil gin.thm-index gin.names-to-avoid)))
    (hints
     (b*
       ((arg1-type-pred
             (atc-type-to-recognizer arg1-type gin.prec-tags))
        (arg2-type-pred
             (atc-type-to-recognizer arg2-type gin.prec-tags))
        (valuep-when-arg1-type-pred
             (pack 'valuep-when- arg1-type-pred))
        (valuep-when-arg2-type-pred
             (pack 'valuep-when- arg2-type-pred))
        (value-kind-when-arg1-type-pred
             (pack 'value-kind-when- arg1-type-pred))
        (value-kind-when-arg2-type-pred
             (pack 'value-kind-when- arg2-type-pred))
        (exec-binary-strict-pure-when-op
             (pack 'exec-binary-strict-pure-when-
                   op-name))
        (type-pred (atc-type-to-recognizer out-type gin.prec-tags))
        (arg1-fixtype (integer-type-to-fixtype arg1-type))
        (arg2-fixtype (integer-type-to-fixtype arg2-type))
        (op-values-when-arg1-type (pack op-name '-values-when-
                                        arg1-fixtype))
        (op-arg1-type-and-value-when-arg2-type
             (pack op-name '-
                   arg1-fixtype '-and-value-when-
                   arg2-fixtype))
        (type-pred-of-fn (pack type-pred '-of- fn))
        (valuep-when-type-pred (pack 'valuep-when- type-pred)))
      (cons
       (cons
        '"Goal"
        (cons
         ':in-theory
         (cons
          (cons
           'quote
           (cons
            (cons
             'exec-expr-pure-when-strict-pure-binary
             (cons
              '(:e expr-kind)
              (cons
               '(:e expr-binary->op)
               (cons
                '(:e expr-binary->arg1)
                (cons
                 '(:e expr-binary->arg2)
                 (cons
                  '(:e binop-kind)
                  (cons
                   '(:e member-equal)
                   (cons
                    arg1-thm
                    (cons
                     arg2-thm
                     (cons
                      valuep-when-arg1-type-pred
                      (cons
                       valuep-when-arg2-type-pred
                       (cons
                        exec-binary-strict-pure-when-op
                        (cons
                         (cons ':e
                               (cons (pack 'binop- op-name) 'nil))
                         (cons
                          op-values-when-arg1-type
                          (cons
                           op-arg1-type-and-value-when-arg2-type
                           (cons
                            type-pred-of-fn
                            (append
                             (and fn-okp (list okp-lemma-name))
                             (cons
                              'expr-valuep-of-expr-value
                              (cons
                               'expr-value->value-of-expr-value
                               (cons
                                'value-fix-when-valuep
                                (cons
                                 valuep-when-type-pred
                                 (cons
                                  value-kind-when-arg1-type-pred
                                  (cons
                                      value-kind-when-arg2-type-pred
                                      '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 out-type term term acl2::*nil*
          gin.compst-var hints nil gin.prec-tags
          thm-index names-to-avoid state)))
   (retok (make-expr-gout
               :expr expr
               :type out-type
               :term term
               :events (append arg1-events arg2-events
                               okp-lemma-event? (list thm-event))
               :thm-name thm-name
               :thm-index thm-index
               :names-to-avoid names-to-avoid)))))

Theorem: expr-goutp-of-atc-gen-expr-binary.gout

(defthm expr-goutp-of-atc-gen-expr-binary.gout
  (b* (((mv acl2::?erp ?gout)
        (atc-gen-expr-binary fn
                             arg1-term arg2-term arg1-expr arg2-expr
                             arg1-type arg2-type arg1-events
                             arg2-events arg1-thm arg2-thm in-type1
                             in-type2 out-type op gin state)))
    (expr-goutp gout))
  :rule-classes :rewrite)