Filtering...

table-guard

books/hacking/table-guard

Included Books

defcode rewrite-code redefun
other
(in-package "ACL2")
include-book
(include-book "defcode" :ttags ((defcode)))
include-book
(include-book "rewrite-code")
include-book
(include-book "redefun")
other
(program)
other
(set-state-ok t)
other
(defttag table-guard)
other
(progn+touchable :all (redefun+rewrite table-fn1
    (:carpat (cond ((and (iff mv-p (cdr stobjs-out)) (equal old-tterm tterm)) %redundant%)
        (old-guard %er1%)
        ((getpropc name 'table-alist nil %wrld%) %er2%)
        (t %rest%))
      :repl (cond ((and (iff mv-p (cdr stobjs-out)) (equal old-tterm tterm)) %redundant%)
        ((and old-guard (not (ttag %wrld%))) %er1%)
        ((and (getpropc name 'table-alist nil %wrld%)
           (not (ttag %wrld%))) %er2%)
        (t %rest%))
      :vars (%redundant% %er1% %er2% %wrld% %rest%)
      :mult 1)))
other
(defttag nil)
rewrite-table-guardmacro
(defmacro rewrite-table-guard
  (name rewrite-spec &key hints skip-proof)
  (declare (xargs :guard (symbolp name)))
  `(make-event (er-let* ((old-guard (table ,NAME nil nil :guard)) (old-guard (value (if (eq (car old-guard) :mv)
              `(car ,(CDR OLD-GUARD))
              old-guard)))
        (new-guard-cons (er-rewrite-form (list old-guard) . ,REWRITE-SPEC)))
      (er-progn (if ',SKIP-PROOF
          (value nil)
          (thm-fn `(implies ,OLD-GUARD ,(CAR NEW-GUARD-CONS))
            state
            nil
            ',HINTS
            nil
            nil))
        (value `(table ,',NAME nil nil :guard ,(CAR NEW-GUARD-CONS)))))))
add-acl2-defaults-table-keymacro
(defmacro add-acl2-defaults-table-key
  (name val-guard)
  (declare (xargs :guard (keywordp name)))
  (let* ((name-str (symbol-name name)) (set-sym (intern (string-append "SET-" name-str) "ACL2")))
    `(progn (rewrite-table-guard acl2-defaults-table
        (:carpat %body%
          :vars %body%
          :repl (if (eq key ',NAME)
            ,VAL-GUARD
            %body%)))
      (defmacro ,SET-SYM
        (v)
        `(with-output :off summary
          (progn (table acl2-defaults-table ,',NAME ',V)
            (table acl2-defaults-table ,',NAME)))))))