		Search-engine friendly clone of the ACL2 documentation.

Formalized-subset

Expr-asg-formalp

Check if an expression has formal dynamic semantics, as an assignment expression.

Signature
(expr-asg-formalp expr) → yes/no
Arguments: expr — Guard (exprp expr).
Returns: yes/no — Type (booleanp yes/no).

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.

Definitions and Theorems

Function: expr-asg-formalp

(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)
    (and
        (ident-formalp (expr-ident->ident (expr-binary->arg1 expr)))
        (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: booleanp-of-expr-asg-formalp

(defthm booleanp-of-expr-asg-formalp
  (b* ((yes/no (expr-asg-formalp expr)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: expr-asg-formalp-of-expr-fix-expr

(defthm expr-asg-formalp-of-expr-fix-expr
  (equal (expr-asg-formalp (expr-fix expr))
         (expr-asg-formalp expr)))

Theorem: expr-asg-formalp-expr-equiv-congruence-on-expr

(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)