Check if an expression has formal dynamic semantics, as an assignment expression.
These are the expressions supported by c::exec-expr-asg. The expression must be a simple assignment expression. The sub-expressions must have formal dynamic semantics. The left expression must be pure. The right expression must be pure unless the left expression is an identifier, in which case the right expression may be a function call.
Function:
(defun expr-asg-formalp (expr) (declare (xargs :guard (exprp expr))) (declare (xargs :guard (expr-unambp expr))) (let ((__function__ 'expr-asg-formalp)) (declare (ignorable __function__)) (and (expr-case expr :binary) (binop-case (expr-binary->op expr) :asg) (if (expr-case (expr-binary->arg1 expr) :ident) (or (expr-pure-formalp (expr-binary->arg2 expr)) (expr-call-formalp (expr-binary->arg2 expr))) (and (expr-pure-formalp (expr-binary->arg1 expr)) (expr-pure-formalp (expr-binary->arg2 expr)))))))
Theorem:
(defthm booleanp-of-expr-asg-formalp (b* ((yes/no (expr-asg-formalp expr))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm expr-asg-formalp-of-expr-fix-expr (equal (expr-asg-formalp (expr-fix expr)) (expr-asg-formalp expr)))
Theorem:
(defthm expr-asg-formalp-expr-equiv-congruence-on-expr (implies (expr-equiv expr expr-equiv) (equal (expr-asg-formalp expr) (expr-asg-formalp expr-equiv))) :rule-classes :congruence)