		Search-engine friendly clone of the ACL2 documentation.

Defobject-implementation

Defobject-term-to-expr

Turn a constant expression term into the represented expression.

Signature
(defobject-term-to-expr term) → (mv erp expr type)
Arguments: term — Guard (pseudo-termp term).
Returns: expr — Type (exprp expr).; type — Type (typep type).

If the term is not a constant expression term, stop with an error. If it is, also return the type of the expression.

In essence, this generates C code for a term used in the initializer of the external object.

Definitions and Theorems

Function: defobject-term-to-expr

(defun defobject-term-to-expr (term)
 (declare (xargs :guard (pseudo-termp term)))
 (let ((__function__ 'defobject-term-to-expr))
  (declare (ignorable __function__))
  (b*
   (((reterr) (irr-expr) (irr-type))
    ((erp okp & out-type const)
     (atc-check-iconst term))
    ((when okp)
     (retok (expr-const (const-int const))
            out-type))
    ((erp okp & arg in-type out-type op)
     (atc-check-unop term))
    ((when okp)
     (b*
      (((erp arg-expr type)
        (defobject-term-to-expr arg))
       ((unless (equal type in-type))
        (reterr
         (msg
          "The unary operator ~x0 ~
                            is applied to a term ~x1 returning ~x2, ~
                            but a ~x3 operand is expected."
          op arg type in-type))))
      (retok (make-expr-unary :op op :arg arg-expr)
             out-type)))
    ((erp okp &
          arg1 arg2 in-type1 in-type2 out-type op)
     (atc-check-binop term))
    ((when okp)
     (b*
      (((erp arg1-expr type1)
        (defobject-term-to-expr arg1))
       ((erp arg2-expr type2)
        (defobject-term-to-expr arg2))
       ((unless (and (equal type1 in-type1)
                     (equal type2 in-type2)))
        (reterr
         (msg
          "The binary operator ~x0 ~
                            is applied to a term ~x1 returning ~x2
                            and to a term ~x3 returning ~x4,
                            but a ~x5 and a ~x6 operand is expected."
          op arg1
          type1 arg2 type2 in-type1 in-type2))))
      (retok (make-expr-binary :op op
                               :arg1 arg1-expr
                               :arg2 arg2-expr)
             out-type)))
    ((erp okp & arg in-type out-type tyname)
     (atc-check-conv term))
    ((when okp)
     (b*
      (((erp arg-expr type)
        (defobject-term-to-expr arg))
       ((unless (equal type in-type))
        (reterr
         (msg
          "The conversion from ~x0 to ~x1 ~
                            is applied to a term ~x2 returning ~x3, ~
                            but a ~x0 operand is expected."
          in-type out-type arg type))))
      (retok (make-expr-cast :type tyname
                             :arg arg-expr)
             out-type))))
   (reterr
    (msg
     "The term ~x0 used as an array element initializer ~
                  does not have the required form."
     term)))))

Theorem: exprp-of-defobject-term-to-expr.expr

(defthm exprp-of-defobject-term-to-expr.expr
  (b* (((mv acl2::?erp ?expr ?type)
        (defobject-term-to-expr term)))
    (exprp expr))
  :rule-classes :rewrite)

Theorem: typep-of-defobject-term-to-expr.type

(defthm typep-of-defobject-term-to-expr.type
  (b* (((mv acl2::?erp ?expr ?type)
        (defobject-term-to-expr term)))
    (typep type))
  :rule-classes :rewrite)