		Search-engine friendly clone of the ACL2 documentation.

Bed-mk1

Mk-op-reorder

Construct a reduced BED using bed-order.

Signature
(mk-op-reorder op left right order) → (mv bed order)
Arguments: op — Operator being applied.
Guard (bed-op-p op).; left — First argument to the operator (a bed).; right — Second argument to the operator (a bed).; order — The ordering for bed-order.
Returns: bed — A bed for op(left, right).; order — The (perhaps extended) order.

We expect that by now, we've already dealt with:

Trivial operators: true, false, arg1, and arg2
Constant propagation
Identical arguments

And we've decided that we're really going to construct op(left, right). We now want to take symmetry into account. That is, we can merge and(a,b) and and(b,a) into some canonical version.

Something subtle is, what do we want to do with symmetry w.r.t. the negation operators like andc1. Suppose that a < b in the bed-order. I think there are perhaps two good options:

Prefer fewer operators. We could, e.g., reduce andc1 and andc2 toward andc1(a,b) or andc1(b,a), so that we never use an andc2 operator.
Prefer fewer permutations. We could, e.g., reduce andc1 and andc2 toward andc1(a,b) or andc1(a,b), so that we never have the arguments out of order.

I think that to start, I want to try out the latter option. It seems like it might have some slight advantages w.r.t. structure sharing, and I guess the whole point of BEDs is to embrace having a lot of operators.

Definitions and Theorems

Function: mk-op-reorder

(defun mk-op-reorder (op left right order)
  (declare (xargs :guard (bed-op-p op)))
  (let ((__function__ 'mk-op-reorder))
    (declare (ignorable __function__))
    (b* ((op (bed-op-fix$ op))
         ((when (eql op (bed-op-true)))
          (mv t order))
         ((when (eql op (bed-op-false)))
          (mv nil order))
         ((when (eql op (bed-op-arg1)))
          (mv left order))
         ((when (eql op (bed-op-arg2)))
          (mv right order))
         ((when (eql op (bed-op-not2)))
          (mv (mk-not right) order))
         ((when (eql op (bed-op-not1)))
          (mv (mk-not left) order))
         ((mv okp order)
          (bed-order left right order))
         ((when (or (eql op (bed-op-and))
                    (eql op (bed-op-ior))
                    (eql op (bed-op-eqv))
                    (eql op (bed-op-nand))
                    (eql op (bed-op-nor))
                    (eql op (bed-op-xor))))
          (mv (if okp (mk-op-raw op left right)
                (mk-op-raw op right left))
              order))
         ((when (eql op (bed-op-orc1)))
          (mv (if okp (mk-op-raw op left right)
                (mk-op-raw (bed-op-orc2) right left))
              order))
         ((when (eql op (bed-op-andc1)))
          (mv (if okp (mk-op-raw op left right)
                (mk-op-raw (bed-op-andc2) right left))
              order))
         ((when (eql op (bed-op-orc2)))
          (mv (if okp (mk-op-raw op left right)
                (mk-op-raw (bed-op-orc1) right left))
              order))
         ((when (eql op (bed-op-andc2)))
          (mv (if okp (mk-op-raw op left right)
                (mk-op-raw (bed-op-andc1) right left))
              order)))
      (mv (mk-op-raw op left right) order))))

Theorem: bed-eval-of-mk-op-reorder

(defthm bed-eval-of-mk-op-reorder
  (b* (((mv bed &)
        (mk-op-reorder op left right order)))
    (equal (bed-eval bed env)
           (bed-eval (mk-op-raw op left right)
                     env))))