Turn a constant expression term into the represented expression.
(defobject-term-to-expr term) → (mv erp expr 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.
Function:
(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:
(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:
(defthm typep-of-defobject-term-to-expr.type (b* (((mv acl2::?erp ?expr ?type) (defobject-term-to-expr term))) (typep type)) :rule-classes :rewrite)