case-splitting-rules

Included Books

bstar

other

(in-package "ACL2")

include-book

(include-book "std/util/bstar" :dir :system)

not-pr-bodyfunction

(defun not-pr-body
  (wrld-segment numes wrld state)
  (declare (xargs :stobjs state :mode :program))
  (info-for-rules (actual-props wrld-segment nil nil)
    numes
    (ens state)
    wrld))

not-pr-fnfunction

(defun not-pr-fn
  (name state)
  (declare (xargs :stobjs state :mode :program))
  (cond ((and (symbolp name) (not (keywordp name))) (let* ((wrld (w state)) (name (deref-macro-name name (macro-aliases wrld)))
          (numes (strip-cars (getprop name
                'runic-mapping-pairs
                nil
                'current-acl2-world
                wrld)))
          (wrld-segment (world-to-next-event (cdr (decode-logical-name name wrld)))))
        (not-pr-body wrld-segment numes wrld state)))
    (t (er hard?
        'not-pr
        "The argument to NOT-PR must be a non-keyword symbol."))))

not-pr-fn-listfunction

(defun not-pr-fn-list
  (names state)
  (declare (xargs :stobjs state :mode :program))
  (if (atom names)
    nil
    (append (not-pr-fn (car names) state)
      (not-pr-fn-list (cdr names) state))))

easy-translatefunction

(defun easy-translate
  (term ctx state)
  "Returns (MV ER VAL STATE)"
  (declare (xargs :mode :program :stobjs state))
  (translate term t t t ctx (w state) state))

has-callpmutual-recursion

(mutual-recursion (defun has-callp
    (fn x)
    (cond ((atom x) nil)
      ((quotep x) nil)
      ((equal (car x) fn) t)
      ((atom (car x)) (has-callp-list fn (cdr x)))
      (t (or (has-callp fn (third (first x)))
          (has-callp-list fn (cdr x))))))
  (defun has-callp-list
    (fn x)
    (if (atom x)
      nil
      (or (has-callp fn (car x)) (has-callp-list fn (cdr x))))))

collect-case-splitsfunction

(defun collect-case-splits
  (info-list state)
  (declare (xargs :mode :program :stobjs state))
  (b* (((when (atom info-list)) (mv nil state)) (rhs-values (cdr (assoc :rhs (car info-list))))
      ((unless rhs-values) (collect-case-splits (cdr info-list) state))
      ((mv er val state) (easy-translate (car rhs-values) 'collect-case-splits state))
      ((when er) (er hard?
          'collect-case-splits
          "something bad happened: ~@0"
          er)
        (mv nil state))
      ((mv rest state) (collect-case-splits (cdr info-list) state))
      ((when (has-callp 'if val)) (mv (cons (car info-list) rest) state)))
    (mv rest state)))

collect-rewritesfunction

(defun collect-rewrites
  (info-list)
  (if (atom info-list)
    nil
    (if (eq (caadr (assoc :rune (car info-list))) :rewrite)
      (cons (car info-list) (collect-rewrites (cdr info-list)))
      (collect-rewrites (cdr info-list)))))

case-splitting-rulesmacro

(defmacro case-splitting-rules
  (x)
  `(b* ((info (not-pr-fn-list (strip-cadrs ',X) state)) (rewrites (collect-rewrites info))
      ((mv splits state) (collect-case-splits rewrites state)))
    (print-info-for-rules splits (standard-co state) state)))