with-arith5-help - ACL2 Book

Included Books

rulesets

other

(in-package "ACL2")

include-book

(include-book "rulesets")

check-for-arith5-rulesetsfunction

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

*allow-arith5-help-form*constant

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

allow-arith5-help-fnfunction

(defun allow-arith5-help-fn
  (world)
  (if (check-for-arith5-rulesets world)
    '(value-triple :redundant-allow-arith5-help)
    *allow-arith5-help-form*))

allow-arith5-helpmacro

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

my-enable-arith5macro

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

with-arith5-helpmacro

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

with-arith5-nonlinear-helpmacro

(defmacro with-arith5-nonlinear-help
  (&rest stuff)
  `(encapsulate nil
    (local (in-theory (my-enable-arith5 'with-arith5-nonlinear-help)))
    (local (set-default-hints '((nonlinearp-default-hint stable-under-simplificationp
           hist
           pspv))))
    (local (table theory-invariant-table
        nil
        (table-alist 'post-arith5-theory-invariants world)
        :clear)) . ,STUFF))

with-arith5-nonlinear++-helpmacro

(defmacro with-arith5-nonlinear++-help
  (&rest stuff)
  `(encapsulate nil
    (local (in-theory (my-enable-arith5 'with-arith5-nonlinear++-help)))
    (local (set-default-hints '((nonlinearp-default-hint++ id
           stable-under-simplificationp
           hist
           nil))))
    (local (table theory-invariant-table
        nil
        (table-alist 'post-arith5-theory-invariants world)
        :clear)) . ,STUFF))

enable-arith5macro

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