priorities - ACL2 Book

other

(in-package "ACL2")

other

(table priorities
  nil
  nil
  :guard (and (rationalp key)
    (< 0 key)
    (theoryp1 val (macro-aliases world) world)))

add-prioritymacro

(defmacro add-priority
  (n &rest items)
  `(table priorities
    ,N
    (union-equal ',ITEMS
      (cdr (assoc-equal ,N (table-alist 'priorities world))))))

del-prioritymacro

(defmacro del-priority
  (n &rest items)
  `(table priorities
    ,N
    (set-difference-equal (cdr (assoc-equal ,N (table-alist 'priorities world)))
      ',ITEMS)))

clr-prioritymacro

(defmacro clr-priority (n) `(table priorities ,N nil))

clr-prioritiesmacro

(defmacro clr-priorities
  nil
  `(table priorities nil nil :clear))

all-prioritized-itemsfunction

(defun all-prioritized-items
  (alist)
  (cond ((endp alist) nil)
    (t (union-equal (cdar alist)
        (all-prioritized-items (cdr alist))))))

disable-prioritized-runesmacro

(defmacro disable-prioritized-runes
  nil
  '(in-theory (set-difference-current-theory-fn (all-prioritized-items (table-alist 'priorities world))
      nil
      world)))

next-priority1function

(defun next-priority1
  (n candidate alist)
  (cond ((endp alist) candidate)
    ((< n (caar alist)) (if candidate
        (if (< (caar alist) candidate)
          (next-priority1 n (caar alist) (cdr alist))
          (next-priority1 n candidate (cdr alist)))
        (next-priority1 n (caar alist) (cdr alist))))
    (t (next-priority1 n candidate (cdr alist)))))

next-priorityfunction

(defun next-priority
  (n world)
  (next-priority1 n nil (table-alist 'priorities world)))

rules-up-to-priority1function

(defun rules-up-to-priority1
  (n alist)
  (cond ((endp alist) nil)
    ((<= (caar alist) n) (union-equal (cdar alist)
        (rules-up-to-priority1 n (cdr alist))))
    (t (rules-up-to-priority1 n (cdr alist)))))

rules-up-to-priorityfunction

(defun rules-up-to-priority
  (n world)
  (rules-up-to-priority1 n (table-alist 'priorities world)))

priority-phased-simplificationfunction

(defun priority-phased-simplification
  (world stable-under-simplificationp current-priority)
  (if stable-under-simplificationp
    (let ((next (next-priority current-priority world)))
      (if next
        `(:computed-hint-replacement ((priority-phased-simplification world
             stable-under-simplificationp
             ,NEXT))
          :in-theory (enable ,@(RULES-UP-TO-PRIORITY NEXT WORLD)))
        nil))
    nil))

*priority-phased-simplification*constant

(defconst *priority-phased-simplification*
  '(priority-phased-simplification world
    stable-under-simplificationp
    0))

local

(local (encapsulate nil
    (set-default-hints (list *priority-phased-simplification*))
    (defun ccc (x) (equal (car (cons x x)) x))
    (defun bbb
      (x)
      (and (ccc (+ x 1))
        (ccc (+ x 2))
        (ccc (+ x 3))
        (ccc (+ x 4))
        (ccc (+ x 5))))
    (defun aaa
      (x)
      (and (bbb (+ x 1))
        (bbb (+ x 2))
        (bbb (+ x 3))
        (bbb (+ x 4))
        (bbb (+ x 5))))
    (add-priority 1/5 aaa)
    (add-priority 2/5 bbb)
    (add-priority 3/5 ccc)
    (disable-prioritized-runes)
    (defthm simple-priority-example (aaa (+ x 5)))))