Filtering...

tables

books/kestrel/utilities/tables
other
(in-package "ACL2")
table-programmaticfunction
(defun table-programmatic
  (table-name key-name value wrld)
  (declare (xargs :guard (and (symbolp table-name) (plist-worldp wrld))))
  (let ((old-alist (table-alist table-name wrld)))
    (if (not (alistp old-alist))
      (er hard?
        'table-programmatic
        "Table-alist for ~x0 is not an alist: ~x1."
        table-name
        old-alist)
      (putprop table-name
        'table-alist
        (put-assoc-equal key-name value old-alist)
        wrld))))
overwrite-table-programmaticfunction
(defun overwrite-table-programmatic
  (table-name alist state)
  (declare (xargs :mode :program :stobjs state))
  (with-output! :off :all (table-fn table-name
      (list nil (kwote alist) :clear)
      state
      `(table ,TABLE-NAME nil ',ALIST :clear))))
set-table-entry-programmaticfunction
(defun set-table-entry-programmatic
  (table-name key value state)
  (declare (xargs :guard (symbolp table-name)
      :mode :program :stobjs state))
  (with-output! :off :all (table-fn table-name
      (list (kwote key) (kwote value))
      state
      `(table ,TABLE-NAME nil ',KEY ',VALUE))))