with-arith1-help - ACL2 Book

Included Books

rulesets

other

(in-package "ACL2")

include-book

(include-book "rulesets")

check-for-arith1-rulesetsfunction

(defun check-for-arith1-rulesets
  (world)
  (let ((ruleset-alist (table-alist 'ruleset-table world)))
    (and (consp (assoc 'arith1-enable-ruleset ruleset-alist))
      (consp (assoc 'arith1-disable-ruleset ruleset-alist)))))

*allow-arith1-help-form*constant

(defconst *allow-arith1-help-form*
  '(local (progn (defun before-including-arithmetic-1 nil nil)
      (make-event '(table pre-arith1-theory-invariants
          nil
          (table-alist 'theory-invariant-table world)
          :clear))
      (local (include-book "arithmetic/top-with-meta" :dir :system))
      (make-event '(def-ruleset! arith1-enable-ruleset
          (set-difference-theories (current-theory :here)
            (current-theory 'before-including-arithmetic-1))))
      (make-event '(def-ruleset! arith1-disable-ruleset
          (set-difference-theories (current-theory 'before-including-arithmetic-1)
            (current-theory :here))))
      (make-event '(table post-arith1-theory-invariants
          nil
          (table-alist 'theory-invariant-table world)
          :clear))
      (make-event '(table theory-invariant-table
          nil
          (table-alist 'pre-arith1-theory-invariants world)
          :clear)))))

allow-arith1-help-fnfunction

(defun allow-arith1-help-fn
  (world)
  (if (check-for-arith1-rulesets world)
    '(value-triple :redundant-allow-arith1-help)
    `(progn ,*ALLOW-ARITH1-HELP-FORM*
      (include-book "arithmetic/top-with-meta" :dir :system)
      (in-theory (current-theory 'before-including-arithmetic-1)))))

allow-arith1-helpmacro

(defmacro allow-arith1-help
  nil
  '(make-event (allow-arith1-help-fn (w state))))

my-enable-arith1macro

(defmacro my-enable-arith1
  (ctx)
  `(if (check-for-arith1-rulesets world)
    (e/d* ((:ruleset arith1-enable-ruleset))
      ((:ruleset arith1-disable-ruleset)))
    (er hard
      ,CTX
      "~
Run (ALLOW-ARITH1-HELP) in the current local scope before using ~x0.~%"
      ,CTX)))

with-arith1-helpmacro

(defmacro with-arith1-help
  (&rest stuff)
  `(encapsulate nil
    (local (in-theory (my-enable-arith1 'with-arith1-help)))
    (local (table theory-invariant-table
        nil
        (table-alist 'post-arith1-theory-invariants world)
        :clear)) . ,STUFF))

enable-arith1macro

(defmacro enable-arith1
  nil
  '(my-enable-arith1 'enable-arith1))