		Search-engine friendly clone of the ACL2 documentation.

Printer

Print-binop

Print a binary operator.

Signature
(print-binop op pstate) → new-pstate
Arguments: op — Guard (binopp op).; pstate — Guard (pristatep pstate).
Returns: new-pstate — Type (pristatep new-pstate).

Definitions and Theorems

Function: print-binop

(defun print-binop (op pstate)
  (declare (xargs :guard (and (binopp op) (pristatep pstate))))
  (let ((__function__ 'print-binop))
    (declare (ignorable __function__))
    (binop-case op
                :mul (print-astring "*" pstate)
                :div (print-astring "/" pstate)
                :rem (print-astring "%" pstate)
                :add (print-astring "+" pstate)
                :sub (print-astring "-" pstate)
                :shl (print-astring "<<" pstate)
                :shr (print-astring ">>" pstate)
                :lt (print-astring "<" pstate)
                :gt (print-astring ">" pstate)
                :le (print-astring "<=" pstate)
                :ge (print-astring ">=" pstate)
                :eq (print-astring "==" pstate)
                :ne (print-astring "!=" pstate)
                :bitand (print-astring "&" pstate)
                :bitxor (print-astring "^" pstate)
                :bitior (print-astring "|" pstate)
                :logand (print-astring "&&" pstate)
                :logor (print-astring "||" pstate)
                :asg (print-astring "=" pstate)
                :asg-mul (print-astring "*=" pstate)
                :asg-div (print-astring "/=" pstate)
                :asg-rem (print-astring "%=" pstate)
                :asg-add (print-astring "+=" pstate)
                :asg-sub (print-astring "-=" pstate)
                :asg-shl (print-astring "<<=" pstate)
                :asg-shr (print-astring ">>=" pstate)
                :asg-and (print-astring "&=" pstate)
                :asg-xor (print-astring "^=" pstate)
                :asg-ior (print-astring "|=" pstate))))

Theorem: pristatep-of-print-binop

(defthm pristatep-of-print-binop
  (b* ((new-pstate (print-binop op pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: print-binop-of-binop-fix-op

(defthm print-binop-of-binop-fix-op
  (equal (print-binop (binop-fix op) pstate)
         (print-binop op pstate)))

Theorem: print-binop-binop-equiv-congruence-on-op

(defthm print-binop-binop-equiv-congruence-on-op
  (implies (binop-equiv op op-equiv)
           (equal (print-binop op pstate)
                  (print-binop op-equiv pstate)))
  :rule-classes :congruence)

Theorem: print-binop-of-pristate-fix-pstate

(defthm print-binop-of-pristate-fix-pstate
  (equal (print-binop op (pristate-fix pstate))
         (print-binop op pstate)))

Theorem: print-binop-pristate-equiv-congruence-on-pstate

(defthm print-binop-pristate-equiv-congruence-on-pstate
  (implies (pristate-equiv pstate pstate-equiv)
           (equal (print-binop op pstate)
                  (print-binop op pstate-equiv)))
  :rule-classes :congruence)