A list of alternating expressions, operators, and attributes.
(vl-mixed-binop-list-p x) → *
All of the binary operators in Verilog are left-associative, but it is difficult to directly build a left-associative structure in straightforward recursive descent parsing.
So instead, our expression parsers build mixed binop lists which we then left-associate later.
Ignoring attributes for a moment, the idea is that these lists look like the following:
(EXPR OP EXPR OP EXPR OP EXPR ... EXPR)
So for instance, to parse the Verilog source code
(1 + 2 + 3 + 4)
and then to fully left-associate this list into the expected form,
(+ (+ (+ 1 2) 3) 4)
Attributes only make this slightly more complex. The actual format of our mixed list is
(EXPR OP ATTS EXPR OP ATTS ... EXPR)
Where each ATTS belongs to the OP immediately preceeding it.
Function:
(defun vl-mixed-binop-list-p (x) (declare (xargs :guard t)) (let ((__function__ 'vl-mixed-binop-list-p)) (declare (ignorable __function__)) (and (consp x) (vl-expr-p (car x)) (or (not (consp (cdr x))) (and (consp (cddr x)) (consp (cdddr x)) (let ((op (second x)) (atts (third x)) (rest (cdddr x))) (and (vl-binaryop-p op) (vl-atts-p atts) (vl-mixed-binop-list-p rest))))))))
Theorem:
(defthm vl-mixed-binop-list-p-when-not-consp (implies (not (consp x)) (equal (vl-mixed-binop-list-p x) nil)))
Theorem:
(defthm vl-mixed-binop-list-p-of-singleton (equal (vl-mixed-binop-list-p (list x)) (vl-expr-p x)))
Theorem:
(defthm vl-mixed-binop-list-p-of-list* (equal (vl-mixed-binop-list-p (list* x y z w)) (and (vl-expr-p x) (vl-binaryop-p y) (vl-atts-p z) (vl-mixed-binop-list-p w))))