def-hash

(in-package "STOBJS")

(include-book "absstobjs")

(include-book "tools/templates" :dir :system)

(include-book "std/alists/alist-defuns" :dir :system)

(include-book "std/alists/alist-fix" :dir :system)

(defxdoc def-hash
  :parents (std/stobjs)
  :short "Defines a @(see abstract-stobj) that logically just appears to be an
alist but is implemented as a stobj hash table.")

(defconst *def-hash-template*
  '(defsection <name>
    (local (include-book "std/stobjs/def-hash-theory" :dir :system))
    (make-event `(defstobj <name>$c
        (<name>-ht$c :type (hash-table <hash-test>
            <init-size>
            <type-decl>)
          :initially ,STOBJS::<DEFAULT-VAL>)))
    (define <name>$ap
      (x)
      :enabled t
      (and (<alistp> x)
        (no-duplicatesp-equal (alist-keys x))))
    (define create-<name>$a nil nil)
    (define <name>-put$a
      ((key (:@ :key-p <key-p>)) (val (:@ :val-p <val-p>))
        (x <name>$ap))
      :enabled t
      (hons-put-assoc (:@ :key-fix (<key-fix> key))
        (:@ (not :key-fix) key)
        (:@ :val-fix (<val-fix> val))
        (:@ (not :val-fix) val)
        (:@ :alist-fix (<alist-fix> x))
        (:@ (not :alist-fix) x)))
    (define <name>-boundp$a
      ((key (:@ :key-p <key-p>)) (x <name>$ap))
      :enabled t
      (consp (hons-assoc-equal (:@ :key-fix (<key-fix> key))
          (:@ (not :key-fix) key)
          (:@ :alist-fix (<alist-fix> x))
          (:@ (not :alist-fix) x))))
    (define <name>-get$a
      ((key (:@ :key-p <key-p>)) (x <name>$ap))
      :enabled t
      (let ((look (hons-assoc-equal (:@ :key-fix (<key-fix> key))
             (:@ (not :key-fix) key)
             (:@ :alist-fix (<alist-fix> x))
             (:@ (not :alist-fix) x))))
        (if look
          (cdr look)
          <default-val>)))
    (define <name>-get?$a
      ((key (:@ :key-p <key-p>)) (x <name>$ap))
      :enabled t
      :guard-debug t
      (mv (<name>-get$a key x)
        (<name>-boundp$a key x)))
    (define <name>-rem$a
      ((key (:@ :key-p <key-p>)) (x <name>$ap))
      :enabled t
      (hons-remove-assoc (:@ :key-fix (<key-fix> key))
        (:@ (not :key-fix) key)
        (:@ :alist-fix (<alist-fix> x))
        (:@ (not :alist-fix) x)))
    (define <name>-clear$a
      ((x <name>$ap))
      :enabled t
      (declare (ignorable x))
      nil)
    (define <name>-init$a
      ((size maybe-natp) (rehash-size)
        (rehash-threshold)
        (x <name>$ap))
      :guard (and (or (not rehash-size)
          (and (rationalp rehash-size)
            (<= 1 rehash-size)))
        (or (not rehash-threshold)
          (and (rationalp rehash-threshold)
            (<= 0 rehash-threshold)
            (<= rehash-threshold 1))))
      :enabled t
      (declare (ignorable size
          rehash-size
          rehash-threshold
          x))
      nil)
    (local (define <name>-corr
        (<name>$c x)
        :non-executable t
        :enabled t
        (and (alist-equiv (nth 0 <name>$c) x)
          (no-duplicatesp-equal (alist-keys x)))))
    (local (defthm <alistp>-of-hons-remove-assoc-for-def-hash
        (implies (<alistp> x)
          (<alistp> (hons-remove-assoc k x)))
        :hints (("Goal" :in-theory (enable hons-remove-assoc)))))
    (:@ (or :key-p :val-p)
      (local (defthm defhash-<alistp>-of-hons-put-assoc
          (implies (and (:@ :key-p (<key-p> key))
              (:@ :val-p (<val-p> val))
              (<alistp> x))
            (<alistp> (hons-put-assoc key val x)))
          :hints (("Goal" :in-theory (enable hons-put-assoc))))))
    (defabsstobj-events <name>
      :foundation <name>$c
      :corr-fn <name>-corr
      :recognizer (<name>p :logic <name>$ap
        :exec <name>$cp)
      :creator (create-<name> :logic create-<name>$a)
      :exports ((<name>-put :exec <name>-ht$c-put) (<name>-get :exec <name>-ht$c-get)
        (<name>-boundp :exec <name>-ht$c-boundp)
        (<name>-get? :exec <name>-ht$c-get?)
        (<name>-rem :exec <name>-ht$c-rem)
        (<name>-clear :exec <name>-ht$c-clear)
        (<name>-init :exec <name>-ht$c-init)))
    (defxdoc <name>
      :parents <parents>
      :short (or <short>
        "Abstract stobj: logically a duplicate-free @('<ALISTP>') alist, implemented as a hash table.")
      :long (or <long>
        "<p>This is a simple abstract stobj hash table, introduced by @(see stobjs::def-hash).</p>"))))

(defun def-hash-fn
  (name alistp
    alist-fix
    key-p
    key-fix
    val-p
    val-fix
    default-val
    type-decl
    hash-test
    init-size
    rename
    pkg-sym
    parents
    short
    long)
  (declare (xargs :mode :program))
  (b* (((unless (and (symbolp name) (not (keywordp name)))) (er hard?
         'def-hash
         "Invalid stobj name: ~x0"
         name)) ((unless (implies key-fix key-p)) (er hard?
          'def-hash
          "If :key-fix is supplied, :key-p must also be"))
      ((unless (implies val-fix val-p)) (er hard?
          'def-hash
          "If :val-fix is supplied, :val-p must also be"))
      (type-decl (or type-decl
          (if val-p
            `(satisfies ,STOBJS::VAL-P)
            t)))
      (pkg-sym (or pkg-sym name))
      (features (append (and key-p '(:key-p))
          (and key-fix '(:key-fix))
          (and val-p '(:val-p))
          (and val-fix '(:val-fix))
          (and alist-fix '(:alist-fix))))
      (symsubst `((<name> . ,STOBJS::NAME) (<alistp> . ,STOBJS::ALISTP)
          (<alist-fix> . ,STOBJS::ALIST-FIX)
          (<key-p> . ,STOBJS::KEY-P)
          (<key-fix> . ,STOBJS::KEY-FIX)
          (<val-p> . ,STOBJS::VAL-P)
          (<val-fix> . ,STOBJS::VAL-FIX)
          (<default-val> . ,STOBJS::DEFAULT-VAL)
          (<type-decl> . ,STOBJS::TYPE-DECL)
          (<hash-test> . ,STOBJS::HASH-TEST)
          (<init-size> . ,STOBJS::INIT-SIZE)
          (<parents> . ,STOBJS::PARENTS)
          (<short> . ,STOBJS::SHORT)
          (<long> . ,STOBJS::LONG)))
      (strsubst (tmpl-symbol-alist-to-str-alist symsubst))
      (tmpl (template-subst *def-hash-template*
          :features features
          :atom-alist symsubst
          :str-alist strsubst
          :string-str-alist strsubst
          :pkg-sym pkg-sym)))
    (if rename
      (sublis rename tmpl)
      tmpl)))

(defmacro def-hash
  (name &key
    (alistp 'alistp)
    alist-fix
    key-p
    key-fix
    val-p
    val-fix
    default-val
    type-decl
    (hash-test 'equal)
    init-size
    rename
    pkg-sym
    parents
    short
    long)
  (def-hash-fn name
    alistp
    alist-fix
    key-p
    key-fix
    val-p
    val-fix
    default-val
    type-decl
    hash-test
    init-size
    rename
    pkg-sym
    parents
    short
    long))