		Search-engine friendly clone of the ACL2 documentation.

Atc-expression-generation

Atc-gen-expr-unary

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

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

The expression and theorem for the argument are generated in the caller, and passed here.

If the operation has an associated okp predicate, we also generate a theorem saying that the okp predicate holds under the guard.

Definitions and Theorems

Function: atc-gen-expr-unary

(defun atc-gen-expr-unary (fn arg-term arg-expr arg-type arg-events
                              arg-thm in-type out-type op gin state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbolp fn)
                             (pseudo-termp arg-term)
                             (exprp arg-expr)
                             (typep arg-type)
                             (pseudo-event-form-listp arg-events)
                             (symbolp arg-thm)
                             (typep in-type)
                             (typep out-type)
                             (unopp op)
                             (expr-ginp gin))))
 (declare (xargs :guard (and (type-nonchar-integerp in-type)
                             (type-nonchar-integerp out-type))))
 (let ((__function__ 'atc-gen-expr-unary))
  (declare (ignorable __function__))
  (b*
   (((reterr) (irr-expr-gout))
    (wrld (w state))
    ((expr-gin gin) gin)
    ((unless (equal arg-type in-type))
     (reterr
      (msg
       "The unary operator ~x0 is applied ~
               to an expression term ~x1 returning ~x2, ~
               but a ~x3 operand is expected. ~
               This is indicative of provably dead code, ~
               given that the code is guard-verified."
       op arg-term arg-type in-type)))
    (expr (make-expr-unary :op op :arg arg-expr))
    (term (cons fn (cons arg-term 'nil)))
    ((when (not gin.proofs))
     (retok (make-expr-gout :expr expr
                            :type out-type
                            :term term
                            :events arg-events
                            :thm-name nil
                            :thm-index gin.thm-index
                            :names-to-avoid gin.names-to-avoid)))
    (fn-okp (and (unop-case op :minus)
                 (not (member-eq (type-kind in-type)
                                 '(:uint :ulong :ullong)))
                 (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))
        (arg-uterm (untranslate$ arg-term nil state))
        (okp-lemma-formula (cons fn-okp (cons arg-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*
      ((in-type-pred (atc-type-to-recognizer in-type gin.prec-tags))
       (valuep-when-in-type-pred (pack 'valuep-when- in-type-pred))
       (value-kind-when-in-type-pred
            (pack 'value-kind-when- in-type-pred))
       (op-name (pack (unop-kind op)))
       (exec-unary-when-op-and-in-type-pred
            (pack op-name '-value-when-
                  in-type-pred))
       (type-pred (atc-type-to-recognizer out-type gin.prec-tags))
       (valuep-when-type-pred (pack 'valuep-when- type-pred))
       (type-pred-of-fn (pack type-pred '-of- fn)))
      (cons
       (cons
        '"Goal"
        (cons
         ':in-theory
         (cons
          (cons
           'quote
           (cons
            (cons
             'exec-expr-pure-when-unary
             (cons
              'expr-valuep-of-expr-value
              (cons
               'expr-value->value-of-expr-value
               (cons
                '(:e expr-kind)
                (cons
                 '(:e expr-unary->op)
                 (cons
                  '(:e expr-unary->arg)
                  (cons
                   arg-thm
                   (cons
                    valuep-when-in-type-pred
                    (cons
                     value-kind-when-in-type-pred
                     (cons
                      valuep-when-type-pred
                      (cons
                       'value-fix-when-valuep
                       (cons
                        exec-unary-when-op-and-in-type-pred
                        (cons
                         (cons ':e
                               (cons (pack 'unop- op-name) 'nil))
                         (cons
                           type-pred-of-fn
                           (and fn-okp
                                (list okp-lemma-name))))))))))))))))
            '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 arg-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-unary.gout

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