Map expressions to expressions in the language definition.
Function:
(defun ldm-expr (expr) (declare (xargs :guard (exprp expr))) (declare (xargs :guard (expr-unambp expr))) (let ((__function__ 'ldm-expr)) (declare (ignorable __function__)) (b* (((reterr) (c::expr-ident (c::ident "irrelevant")))) (expr-case expr :ident (b* (((erp ident1) (ldm-ident expr.unwrap))) (retok (c::expr-ident ident1))) :const (b* (((erp const1) (ldm-const expr.unwrap))) (retok (c::expr-const const1))) :string (reterr (msg "Unsupported expression ~x0." (expr-fix expr))) :paren (ldm-expr expr.unwrap) :gensel (reterr (msg "Unsupported expression ~x0." (expr-fix expr))) :arrsub (b* (((erp arr1) (ldm-expr expr.arg1)) ((erp sub1) (ldm-expr expr.arg2))) (retok (c::make-expr-arrsub :arr arr1 :sub sub1))) :funcall (b* ((ident (check-expr-ident expr.fun)) ((when (not ident)) (reterr (msg "Unsupported non-identifier function ~x0." expr.fun))) ((erp ident1) (ldm-ident ident)) ((erp args1) (ldm-expr-list expr.args))) (retok (c::make-expr-call :fun ident1 :args args1))) :member (b* (((erp target1) (ldm-expr expr.arg)) ((erp ident1) (ldm-ident expr.name))) (retok (c::make-expr-member :target target1 :name ident1))) :memberp (b* (((erp target1) (ldm-expr expr.arg)) ((erp ident1) (ldm-ident expr.name))) (retok (c::make-expr-memberp :target target1 :name ident1))) :complit (reterr (msg "Unsupported expression ~x0." (expr-fix expr))) :unary (b* (((erp arg) (ldm-expr expr.arg))) (unop-case expr.op :address (retok (c::make-expr-unary :op (c::unop-address) :arg arg)) :indir (retok (c::make-expr-unary :op (c::unop-indir) :arg arg)) :plus (retok (c::make-expr-unary :op (c::unop-plus) :arg arg)) :minus (retok (c::make-expr-unary :op (c::unop-minus) :arg arg)) :bitnot (retok (c::make-expr-unary :op (c::unop-bitnot) :arg arg)) :lognot (retok (c::make-expr-unary :op (c::unop-lognot) :arg arg)) :preinc (retok (c::expr-preinc arg)) :predec (retok (c::expr-predec arg)) :postinc (retok (c::expr-postinc arg)) :postdec (retok (c::expr-postdec arg)) :sizeof (reterr (msg "Unsupported sizeof operator.")))) :sizeof (reterr (msg "Unsupported expression ~x0." (expr-fix expr))) :sizeof-ambig (prog2$ (impossible) (reterr t)) :alignof (reterr (msg "Unsupported expression ~x0." (expr-fix expr))) :cast (b* (((erp tyname) (ldm-tyname expr.type)) ((erp arg) (ldm-expr expr.arg))) (retok (c::make-expr-cast :type tyname :arg arg))) :binary (b* (((erp arg1) (ldm-expr expr.arg1)) ((erp arg2) (ldm-expr expr.arg2)) (op (ldm-binop expr.op))) (retok (c::make-expr-binary :op op :arg1 arg1 :arg2 arg2))) :cond (b* (((erp test) (ldm-expr expr.test)) ((erp then) (ldm-expr expr.then)) ((erp else) (ldm-expr expr.else))) (retok (c::make-expr-cond :test test :then then :else else))) :comma (reterr (msg "Unsupported expression ~x0." (expr-fix expr))) :cast/call-ambig (prog2$ (impossible) (reterr t)) :cast/mul-ambig (prog2$ (impossible) (reterr t)) :cast/add-ambig (prog2$ (impossible) (reterr t)) :cast/sub-ambig (prog2$ (impossible) (reterr t)) :cast/and-ambig (prog2$ (impossible) (reterr t))))))
Function:
(defun ldm-expr-list (exprs) (declare (xargs :guard (expr-listp exprs))) (declare (xargs :guard (expr-list-unambp exprs))) (let ((__function__ 'ldm-expr-list)) (declare (ignorable __function__)) (b* (((reterr) nil) ((when (endp exprs)) (retok nil)) ((erp expr1) (ldm-expr (car exprs))) ((erp exprs1) (ldm-expr-list (cdr exprs)))) (retok (cons expr1 exprs1)))))
Theorem:
(defthm return-type-of-ldm-expr.expr1 (b* (((mv acl2::?erp ?expr1) (ldm-expr expr))) (c::exprp expr1)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-ldm-expr-list.exprs1 (b* (((mv acl2::?erp ?exprs1) (ldm-expr-list exprs))) (c::expr-listp exprs1)) :rule-classes :rewrite)
Theorem:
(defthm ldm-expr-of-expr-fix-expr (equal (ldm-expr (expr-fix expr)) (ldm-expr expr)))
Theorem:
(defthm ldm-expr-list-of-expr-list-fix-exprs (equal (ldm-expr-list (expr-list-fix exprs)) (ldm-expr-list exprs)))
Theorem:
(defthm ldm-expr-expr-equiv-congruence-on-expr (implies (expr-equiv expr expr-equiv) (equal (ldm-expr expr) (ldm-expr expr-equiv))) :rule-classes :congruence)
Theorem:
(defthm ldm-expr-list-expr-list-equiv-congruence-on-exprs (implies (expr-list-equiv exprs exprs-equiv) (equal (ldm-expr-list exprs) (ldm-expr-list exprs-equiv))) :rule-classes :congruence)