Order over expression ranks.
(jexpr-rank-<= rank1 rank2) → yes/no
See here for motivation.
The partial order over expression ranks is actually a linear order. (However, our pretty-printing approach should work with partial orders that are not linear orders.) So we define the linear order by mapping each rank to a numeric index so that the indices provide the order of the ranks. The specific numeric values are unimportant; only their relative ordering is.
Function:
(defun jexpr-rank-index (rank) (declare (xargs :guard (jexpr-rankp rank))) (let ((__function__ 'jexpr-rank-index)) (declare (ignorable __function__)) (jexpr-rank-case rank :expression 15 :assignment 14 :conditional 13 :conditional-or 12 :conditional-and 11 :inclusive-or 10 :exclusive-or 9 :and 8 :equality 7 :relational 6 :shift 5 :additive 4 :multiplicative 3 :unary 2 :postfix 1 :primary 0)))
Theorem:
(defthm natp-of-jexpr-rank-index (b* ((index (jexpr-rank-index rank))) (natp index)) :rule-classes :rewrite)
Function:
(defun jexpr-rank-<= (rank1 rank2) (declare (xargs :guard (and (jexpr-rankp rank1) (jexpr-rankp rank2)))) (let ((__function__ 'jexpr-rank-<=)) (declare (ignorable __function__)) (<= (jexpr-rank-index rank1) (jexpr-rank-index rank2))))
Theorem:
(defthm booleanp-of-jexpr-rank-<= (b* ((yes/no (jexpr-rank-<= rank1 rank2))) (booleanp yes/no)) :rule-classes :rewrite)