		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-operations

Expr-priority-<=

Total order on expression priorities: less than or equal to.

Signature
(expr-priority-<= prio1 prio2) → yes/no
Arguments: prio1 — Guard (expr-priorityp prio1).; prio2 — Guard (expr-priorityp prio2).
Returns: yes/no — Type (booleanp yes/no).

We assign a unique numeric index to each priority, and we compare the numbers. The higher the priority, the higher the number. The exact numbers do not matter; only their relative magnitude does.

This total order on expression priorities is the reflexive and transitive closure of the binary relation that consists of the pairs priority1 < priority2 such that there is a grammar (sub)rule nonterm1: nonterm2 saying that the nonterminal nonterm1 corresponding to priority1 may expand to the nonterminal nonterm2 corresponding to priority2. For instance, priority2 is the priority of multiplicative expressions and priority1 is the priority of additive expressions, because there is a (sub)rule additive-expression: multiplicative-expression in the grammar. (Here by `subrule' we mean a rule not necessarily in the grammar but obtainable by selecting just some of the alternatives in the definiens that are on different lines in [C17].) The nonterminal additive-expression also has other alternatives, but those are not single nonterminals; here we are only concerned with single nonterminals as rule definientia.

Definitions and Theorems

Function: expr-priority-number

(defun expr-priority-number (prio)
  (declare (xargs :guard (expr-priorityp prio)))
  (expr-priority-case prio
                      :primary 16
                      :postfix 15
                      :unary 14
                      :cast 13
                      :mul 12
                      :add 11
                      :sh 10
                      :rel 9
                      :eq 8
                      :and 7
                      :xor 6
                      :ior 5
                      :logand 4
                      :logor 3
                      :cond 2
                      :asg 1
                      :expr 0))

Theorem: natp-of-expr-priority-number

(defthm natp-of-expr-priority-number
  (b* ((number (expr-priority-number prio)))
    (natp number))
  :rule-classes :rewrite)

Theorem: expr-priority-number-of-expr-priority-fix-prio

(defthm expr-priority-number-of-expr-priority-fix-prio
  (equal (expr-priority-number (expr-priority-fix prio))
         (expr-priority-number prio)))

Theorem: expr-priority-number-expr-priority-equiv-congruence-on-prio

(defthm expr-priority-number-expr-priority-equiv-congruence-on-prio
  (implies (expr-priority-equiv prio prio-equiv)
           (equal (expr-priority-number prio)
                  (expr-priority-number prio-equiv)))
  :rule-classes :congruence)

Function: expr-priority-<=

(defun expr-priority-<= (prio1 prio2)
  (declare (xargs :guard (and (expr-priorityp prio1)
                              (expr-priorityp prio2))))
  (<= (expr-priority-number prio1)
      (expr-priority-number prio2)))

Theorem: booleanp-of-expr-priority-<=

(defthm booleanp-of-expr-priority-<=
  (b* ((yes/no (expr-priority-<= prio1 prio2)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: expr-priority-<=-of-expr-priority-fix-prio1

(defthm expr-priority-<=-of-expr-priority-fix-prio1
  (equal (expr-priority-<= (expr-priority-fix prio1)
                           prio2)
         (expr-priority-<= prio1 prio2)))

Theorem: expr-priority-<=-expr-priority-equiv-congruence-on-prio1

(defthm expr-priority-<=-expr-priority-equiv-congruence-on-prio1
  (implies (expr-priority-equiv prio1 prio1-equiv)
           (equal (expr-priority-<= prio1 prio2)
                  (expr-priority-<= prio1-equiv prio2)))
  :rule-classes :congruence)

Theorem: expr-priority-<=-of-expr-priority-fix-prio2

(defthm expr-priority-<=-of-expr-priority-fix-prio2
  (equal (expr-priority-<= prio1 (expr-priority-fix prio2))
         (expr-priority-<= prio1 prio2)))

Theorem: expr-priority-<=-expr-priority-equiv-congruence-on-prio2

(defthm expr-priority-<=-expr-priority-equiv-congruence-on-prio2
  (implies (expr-priority-equiv prio2 prio2-equiv)
           (equal (expr-priority-<= prio1 prio2)
                  (expr-priority-<= prio1 prio2-equiv)))
  :rule-classes :congruence)